-ndefinition any_status_ind :
- Πmcu.Πt.ΠP:any_status mcu t → Prop.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Prop.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition any_status_rec :
- Πmcu.Πt.ΠP:any_status mcu t → Set.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Set.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition any_status_rect :
- Πmcu.Πt.ΠP:any_status mcu t → Type.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Type.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition alu ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status (x:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]) _ _ _ ⇒ x ].
-ndefinition mem_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ x _ _ ⇒ x ].
-ndefinition chk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ x _ ⇒ x ].
-ndefinition clk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ _ x ⇒ x ].
-