| AST_BASE_TYPE_WORD16: ast_base_type
| AST_BASE_TYPE_WORD32: ast_base_type.
-(*ndefinition ast_base_type_ind
- : ΠP:ast_base_type → Prop.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
- Πa:ast_base_type.P a ≝
-λP:ast_base_type → Prop.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
-λa:ast_base_type.
- match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
-
-ndefinition ast_base_type_rec
- : ΠP:ast_base_type → Set.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
- Πa:ast_base_type.P a ≝
-λP:ast_base_type → Set.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
-λa:ast_base_type.
- match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
-
-ndefinition ast_base_type_rect
- : ΠP:ast_base_type → Type.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 →
- Πa:ast_base_type.P a ≝
-λP:ast_base_type → Type.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32.
-λa:ast_base_type.
- match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ].
-*)
ninductive ast_type : Type ≝
AST_TYPE_BASE: ast_base_type → ast_type
| AST_TYPE_ARRAY: ast_type → nat → ast_type
| AST_TYPE_STRUCT: ne_list ast_type → ast_type.
-nlet rec ast_type_ind_aux (P:ast_type → Prop)
- (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
- (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
- (f2:Πt.P t)
- (t:ne_list ast_type) on t ≝
+(* principio di eliminazione arricchito *)
+nlet rec ast_type_index_aux (P:ast_type → Prop)
+ (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+ (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+ (f2:Πt.P t)
+ (t:ne_list ast_type) on t ≝
match t return λt.P (AST_TYPE_STRUCT t) with
[ ne_nil h ⇒ f h (f2 h)
- | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_ind_aux P f f1 f2 t)
+ | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_index_aux P f f1 f2 t)
].
-(*nlet rec ast_type_ind (P:ast_type → Prop)
- (f:Πb.P (AST_TYPE_BASE b))
- (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
- (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
- (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
- (t:ast_type) on t : P t ≝
+nlet rec ast_type_index (P:ast_type → Prop)
+ (f:Πb.P (AST_TYPE_BASE b))
+ (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
+ (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+ (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+ (t:ast_type) on t : P t ≝
match t return λt.P t with
[ AST_TYPE_BASE b ⇒ f b
- | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_ind P f f1 f2 f3 t')
+ | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_index P f f1 f2 f3 t')
| AST_TYPE_STRUCT nl ⇒ match nl with
- [ ne_nil h ⇒ f2 h (ast_type_ind P f f1 f2 f3 h)
- | ne_cons h t ⇒ f3 h t (ast_type_ind P f f1 f2 f3 h) (ast_type_ind_aux P f2 f3 (ast_type_ind P f f1 f2 f3) t)
+ [ ne_nil h ⇒ f2 h (ast_type_index P f f1 f2 f3 h)
+ | ne_cons h t ⇒ f3 h t (ast_type_index P f f1 f2 f3 h) (ast_type_index_aux P f2 f3 (ast_type_index P f f1 f2 f3) t)
]
].
-nlet rec ast_type_rec_aux (P:ast_type → Type[0])
- (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
- (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
- (f2:Πt.P t)
- (t:ne_list ast_type) on t ≝
+nlet rec ast_type_rectex_aux (P:ast_type → Type)
+ (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+ (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+ (f2:Πt.P t)
+ (t:ne_list ast_type) on t ≝
match t return λt.P (AST_TYPE_STRUCT t) with
[ ne_nil h ⇒ f h (f2 h)
- | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rec_aux P f f1 f2 t)
+ | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rectex_aux P f f1 f2 t)
].
-nlet rec ast_type_rec (P:ast_type → Set)
- (f:Πb.P (AST_TYPE_BASE b))
- (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
- (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
- (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
- (t:ast_type) on t : P t ≝
+nlet rec ast_type_rectex (P:ast_type → Type)
+ (f:Πb.P (AST_TYPE_BASE b))
+ (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
+ (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+ (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+ (t:ast_type) on t : P t ≝
match t return λt.P t with
[ AST_TYPE_BASE b ⇒ f b
- | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rec P f f1 f2 f3 t')
+ | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rectex P f f1 f2 f3 t')
| AST_TYPE_STRUCT nl ⇒ match nl with
- [ ne_nil h ⇒ f2 h (ast_type_rec P f f1 f2 f3 h)
- | ne_cons h t ⇒ f3 h t (ast_type_rec P f f1 f2 f3 h) (ast_type_rec_aux P f2 f3 (ast_type_rec P f f1 f2 f3) t)
+ [ ne_nil h ⇒ f2 h (ast_type_rectex P f f1 f2 f3 h)
+ | ne_cons h t ⇒ f3 h t (ast_type_rectex P f f1 f2 f3 h) (ast_type_rectex_aux P f2 f3 (ast_type_rectex P f f1 f2 f3) t)
]
].
-nlet rec ast_type_rect_aux (P:ast_type → Type)
- (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
- (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
- (f2:Πt.P t)
- (t:ne_list ast_type) on t ≝
- match t return λt.P (AST_TYPE_STRUCT t) with
- [ ne_nil h ⇒ f h (f2 h)
- | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rect_aux P f f1 f2 t)
- ].
-
-nlet rec ast_type_rect (P:ast_type → Type)
- (f:Πb.P (AST_TYPE_BASE b))
- (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
- (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
- (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
- (t:ast_type) on t : P t ≝
- match t return λt.P t with
- [ AST_TYPE_BASE b ⇒ f b
- | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rect P f f1 f2 f3 t')
- | AST_TYPE_STRUCT nl ⇒ match nl with
- [ ne_nil h ⇒ f2 h (ast_type_rect P f f1 f2 f3 h)
- | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t)
- ]
- ].
-*)
ndefinition eq_ast_base_type ≝
λt1,t2:ast_base_type.match t1 with
[ AST_BASE_TYPE_BYTE8 ⇒ match t2 with
[ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eq_nat dim1 dim2)
| _ ⇒ false ]
| AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
- [ AST_TYPE_STRUCT nelSubType2 ⇒
- match eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2)
- return λx.eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = x → bool
- with
- [ true ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = true).
- fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc)
- true nelSubType1 nelSubType2
- (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p)
- | false ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = false).false
- ] (refl_eq ? (eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2)))
+ [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_ast_type x1 x2) nelSubType1 nelSubType2
| _ ⇒ false
]
].
nnormalize;
#H;
##[ ##1,5,9: napply (λx:P.x)
- ##| ##2,3: napply (False_ind ??);
+ ##| ##2,3: napply (False_ind (λ_.?) ?);
nchange with (match AST_BASE_TYPE_BYTE8 with [ AST_BASE_TYPE_BYTE8 ⇒ False | _ ⇒ True]);
nrewrite > H;
nnormalize;
napply I
- ##| ##4,6: napply (False_ind ??);
+ ##| ##4,6: napply (False_ind (λ_.?) ?);
nchange with (match AST_BASE_TYPE_WORD16 with [ AST_BASE_TYPE_WORD16 ⇒ False | _ ⇒ True]);
nrewrite > H;
nnormalize;
napply I
- ##| ##7,8: napply (False_ind ??);
+ ##| ##7,8: napply (False_ind (λ_.?) ?);
nchange with (match AST_BASE_TYPE_WORD32 with [ AST_BASE_TYPE_WORD32 ⇒ False | _ ⇒ True]);
nrewrite > H;
nnormalize;
##| ##2: #t; #n; #b; nnormalize; #H
##| ##3: #l; #b; nnormalize; #H
##]
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match AST_TYPE_BASE b with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##2: ncases b2;
##| ##1: #b; #t; #n; nnormalize; #H
##| ##3: #l; #t; #n; nnormalize; #H
##]
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match AST_TYPE_ARRAY t n with [ AST_TYPE_ARRAY _ _ ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##3: ncases b2;
##| ##1: #b; #l; nnormalize; #H
##| ##2: #t; #n; #l; nnormalize; #H
##]
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match AST_TYPE_STRUCT l with [ AST_TYPE_STRUCT _ ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nqed.
-(* eq_ast lemmas missing *)
+nlemma symmetric_eqasttype_aux1
+ : ∀nl1,nl2.
+ (eq_ast_type (AST_TYPE_STRUCT nl1) (AST_TYPE_STRUCT nl2)) = (eq_ast_type (AST_TYPE_STRUCT nl2) (AST_TYPE_STRUCT nl1)) →
+ (bfold_right_neList2 ? (λx,y.eq_ast_type x y) nl1 nl2) = (bfold_right_neList2 ? (λx,y.eq_ast_type x y) nl2 nl1).
+ #nl1; #nl2; #H;
+ napply H.
+nqed.
+
+nlemma symmetric_eqasttype : symmetricT ast_type bool eq_ast_type.
+ #t1; napply (ast_type_index ????? t1);
+ ##[ ##1: #b1; #t2; ncases t2;
+ ##[ ##1: #b2; nchange with ((eq_ast_base_type b1 b2) = (eq_ast_base_type b2 b1));
+ nrewrite > (symmetric_eqastbasetype b1 b2);
+ napply (refl_eq ??)
+ ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??)
+ ##| ##3: #nl2; nnormalize; napply (refl_eq ??)
+ ##]
+ ##| ##2: #st1; #n1; #H; #t2; ncases t2;
+ ##[ ##2: #st2; #n2; nchange with (((eq_ast_type st1 st2)⊗(eq_nat n1 n2)) = ((eq_ast_type st2 st1)⊗(eq_nat n2 n1)));
+ nrewrite > (symmetric_eqnat n1 n2);
+ nrewrite > (H st2);
+ napply (refl_eq ??)
+ ##| ##1: #b2; nnormalize; napply (refl_eq ??)
+ ##| ##3: #nl2; nnormalize; napply (refl_eq ??)
+ ##]
+ ##| ##3: #hh1; #H; #t2; ncases t2;
+ ##[ ##3: #nl2; ncases nl2;
+ ##[ ##1: #hh2; nchange with ((eq_ast_type hh1 hh2) = (eq_ast_type hh2 hh1));
+ nrewrite > (H hh2);
+ napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; nnormalize; napply (refl_eq ??)
+ ##]
+ ##| ##1: #b2; nnormalize; napply (refl_eq ??)
+ ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??)
+ ##]
+ ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
+ ##[ ##3: #nl2; ncases nl2;
+ ##[ ##1: #hh2; nnormalize; napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; nnormalize;
+ nrewrite > (H hh2);
+ nrewrite > (symmetric_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2)));
+ napply (refl_eq ??)
+ ##]
+ ##| ##1: #b2; nnormalize; napply (refl_eq ??)
+ ##| ##2: #st2; #n2; nnormalize; napply (refl_eq ??)
+ ##]
+ ##]
+nqed.
+
+...
+
nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
#ast;
| o6: oct
| o7: oct.
-(*ndefinition oct_ind :
- ΠP:oct → Prop.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
-λP:oct → Prop.
-λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
- match n with
- [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
-
-ndefinition oct_rec :
- ΠP:oct → Set.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
-λP:oct → Set.
-λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
- match n with
- [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
-
-ndefinition oct_rect :
- ΠP:oct → Type.P o0 → P o1 → P o2 → P o3 → P o4 → P o5 → P o6 → P o7 → Πn:oct.P n ≝
-λP:oct → Type.
-λp:P o0.λp1:P o1.λp2:P o2.λp3:P o3.λp4:P o4.λp5:P o5.λp6:P o6.λp7:P o7.λn:oct.
- match n with
- [ o0 ⇒ p | o1 ⇒ p1 | o2 ⇒ p2 | o3 ⇒ p3 | o4 ⇒ p4 | o5 ⇒ p5 | o6 ⇒ p6 | o7 ⇒ p7 ].
-*)
(* operatore = *)
ndefinition eq_oct ≝
λn1,n2:oct.
| t1E: bitrigesim
| t1F: bitrigesim.
-(*ndefinition bitrigesim_ind :
- ΠP:bitrigesim → Prop.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
- P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
- P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
- P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
-λP:bitrigesim → Prop.
-λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
-λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
-λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
-λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
- match t with
- [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
- | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
- | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
- | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
-
-ndefinition bitrigesim_rec :
- ΠP:bitrigesim → Set.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
- P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
- P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
- P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
-λP:bitrigesim → Set.
-λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
-λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
-λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
-λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
- match t with
- [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
- | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
- | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
- | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
-
-ndefinition bitrigesim_rect :
- ΠP:bitrigesim → Type.P t00 → P t01 → P t02 → P t03 → P t04 → P t05 → P t06 → P t07 →
- P t08 → P t09 → P t0A → P t0B → P t0C → P t0D → P t0E → P t0F →
- P t10 → P t11 → P t12 → P t13 → P t14 → P t15 → P t16 → P t17 →
- P t18 → P t19 → P t1A → P t1B → P t1C → P t1D → P t1E → P t1F → Πt:bitrigesim.P t ≝
-λP:bitrigesim → Type.
-λp:P t00.λp1:P t01.λp2:P t02.λp3:P t03.λp4:P t04.λp5:P t05.λp6:P t06.λp7:P t07.
-λp8:P t08.λp9:P t09.λp10:P t0A.λp11:P t0B.λp12:P t0C.λp13:P t0D.λp14:P t0E.λp15:P t0F.
-λp16:P t10.λp17:P t11.λp18:P t12.λp19:P t13.λp20:P t14.λp21:P t15.λp22:P t16.λp23:P t17.
-λp24:P t18.λp25:P t19.λp26:P t1A.λp27:P t1B.λp28:P t1C.λp29:P t1D.λp30:P t1E.λp31:P t1F.λt:bitrigesim.
- match t with
- [ t00 ⇒ p | t01 ⇒ p1 | t02 ⇒ p2 | t03 ⇒ p3 | t04 ⇒ p4 | t05 ⇒ p5 | t06 ⇒ p6 | t07 ⇒ p7
- | t08 ⇒ p8 | t09 ⇒ p9 | t0A ⇒ p10 | t0B ⇒ p11 | t0C ⇒ p12 | t0D ⇒ p13 | t0E ⇒ p14 | t0F ⇒ p15
- | t10 ⇒ p16 | t11 ⇒ p17 | t12 ⇒ p18 | t13 ⇒ p19 | t14 ⇒ p20 | t15 ⇒ p21 | t16 ⇒ p22 | t17 ⇒ p23
- | t18 ⇒ p24 | t19 ⇒ p25 | t1A ⇒ p26 | t1B ⇒ p27 | t1C ⇒ p28 | t1D ⇒ p29 | t1E ⇒ p30 | t1F ⇒ p31 ].
-*)
(* operatore = *)
ndefinition eq_bitrig ≝
λt1,t2:bitrigesim.
nelim n1;
##[ ##1: nelim n2; nnormalize; #H;
##[ ##1: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##2: nelim n2; nnormalize; #H;
##[ ##2: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##3: nelim n2; nnormalize; #H;
##[ ##3: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##4: nelim n2; nnormalize; #H;
##[ ##4: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##5: nelim n2; nnormalize; #H;
##[ ##5: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##6: nelim n2; nnormalize; #H;
##[ ##6: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##7: nelim n2; nnormalize; #H;
##[ ##7: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##8: nelim n2; nnormalize; #H;
##[ ##8: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##1: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##2: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##3: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##4: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##5: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##6: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##7: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##8: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##9: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##10: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##11: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##12: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##13: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##14: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##15: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##16: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##17: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##18: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##19: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##20: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##21: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##22: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##23: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##24: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##25: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##26: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##27: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##28: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##29: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##30: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##31: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases t2;
nnormalize; #H;
##[ ##32: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##31: napply bitrigesim_destruct31
##| ##32: napply bitrigesim_destruct32
##]
-nqed.
+nqed.
nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
#t1;
nnormalize;
#H;
##[ ##2: napply (False_ind (λx.?) ?);
- (* perche' non napply (False_ind ??); !!! *)
nchange with (match true with [ true ⇒ False | false ⇒ True]);
nrewrite > H;
nnormalize;
napply I
##| ##3: napply (False_ind (λx.?) ?);
- (* perche' non napply (False_ind ??); !!! *)
nchange with (match true with [ true ⇒ False | false ⇒ True]);
nrewrite < H;
nnormalize;
b8l: exadecim
}.
-(*ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
-λP:byte8 → Prop.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
- match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
-
-ndefinition byte8_rec : ΠP:byte8 → Set.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
-λP:byte8 → Set.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
- match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
-
-ndefinition byte8_rect : ΠP:byte8 → Type.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
-λP:byte8 → Type.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
- match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
-
-ndefinition b8h ≝ λb:byte8.match b with [ mk_byte8 x _ ⇒ x ].
-ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].*)
-
(* \langle \rangle *)
notation "〈x,y〉" non associative with precedence 80
for @{ 'mk_byte8 $x $y }.
ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##1: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##2: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##3: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##4: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##5: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##6: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##7: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##8: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##9: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##10: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##11: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##12: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##13: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##14: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##15: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
#e2; #P; ncases e2; nnormalize; #H;
##[ ##16: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
| HCS08 : mcu_type
| RS08 : mcu_type.
-(*ndefinition mcu_type_ind : ΠP:mcu_type → Prop.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
-λP:mcu_type → Prop.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
- match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
-
-ndefinition mcu_type_rec : ΠP:mcu_type → Set.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
-λP:mcu_type → Set.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
- match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
-
-ndefinition mcu_type_rect : ΠP:mcu_type → Type.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
-λP:mcu_type → Type.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
- match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].*)
-
ndefinition eq_mcutype ≝
λm1,m2:mcu_type.
match m1 with
| MODE_SRT : bitrigesim → instr_mode
.
-(*ndefinition instr_mode_ind
- : ΠP:instr_mode → Prop.
- P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
- P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
- P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
- P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
- P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
- P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
- (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
- (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
-λP:instr_mode → Prop.
-λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
-λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
-λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
-λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
-λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
-λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
-λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
-λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
- match i with
- [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
- | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
- | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
- | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
- | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
- | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
- | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
- | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
- | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
- | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
-
-ndefinition instr_mode_rec
- : ΠP:instr_mode → Set.
- P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
- P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
- P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
- P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
- P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
- P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
- (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
- (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
-λP:instr_mode → Set.
-λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
-λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
-λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
-λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
-λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
-λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
-λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
-λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
- match i with
- [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
- | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
- | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
- | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
- | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
- | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
- | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
- | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
- | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
- | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
-
-ndefinition instr_mode_rect
- : ΠP:instr_mode → Type.
- P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
- P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
- P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
- P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
- P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
- P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
- (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
- (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
-λP:instr_mode → Type.
-λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
-λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
-λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
-λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
-λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
-λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
-λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
-λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
- match i with
- [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
- | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
- | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
- | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
- | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
- | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
- | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
- | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
- | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
- | MODE_SRT (d:bitrigesim) ⇒ f3 d ].*)
-
ndefinition eq_instrmode ≝
λi1,i2:instr_mode.
match i1 with
| WAIT : opcode (* !!wait mode!! *)
.
-(*ndefinition opcode_ind
- : ΠP:opcode → Prop.
- P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
- P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
- P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
- P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
- P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
- P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
- P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
- P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
- Πo:opcode.P o ≝
-λP:opcode → Prop.
-λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
-λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
-λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
-λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
-λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
-λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
-λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
-λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
-λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
-λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
-λp90:P WAIT.λo:opcode.
- match o with
- [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
- | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
- | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
- | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
- | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
- | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
- | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
- | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
- | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
- | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
- | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
- | TXS ⇒ p89 | WAIT ⇒ p90 ].
-
-ndefinition opcode_rec
- : ΠP:opcode → Set.
- P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
- P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
- P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
- P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
- P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
- P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
- P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
- P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
- Πo:opcode.P o ≝
-λP:opcode → Set.
-λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
-λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
-λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
-λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
-λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
-λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
-λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
-λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
-λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
-λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
-λp90:P WAIT.λo:opcode.
- match o with
- [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
- | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
- | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
- | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
- | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
- | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
- | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
- | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
- | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
- | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
- | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
- | TXS ⇒ p89 | WAIT ⇒ p90 ].
-
-ndefinition opcode_rect
- : ΠP:opcode → Type.
- P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
- P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
- P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
- P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
- P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
- P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
- P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
- P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
- Πo:opcode.P o ≝
-λP:opcode → Type.
-λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
-λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
-λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
-λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
-λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
-λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
-λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
-λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
-λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
-λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
-λp90:P WAIT.λo:opcode.
- match o with
- [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
- | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
- | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
- | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
- | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
- | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
- | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
- | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
- | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
- | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
- | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
- | TXS ⇒ p89 | WAIT ⇒ p90 ].*)
-
ndefinition eq_op ≝
λop1,op2:opcode.
match op1 with
ninductive any_opcode (m:mcu_type) : Type ≝
anyOP : opcode → any_opcode m.
-(*ndefinition any_opcode_ind
- : Πm:mcu_type.ΠP:any_opcode m → Prop.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
-λm:mcu_type.λP:any_opcode m → Prop.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
- match a with [ anyOP (o:opcode) ⇒ f o ].
-
-ndefinition any_opcode_rec
- : Πm:mcu_type.ΠP:any_opcode m → Set.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
-λm:mcu_type.λP:any_opcode m → Set.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
- match a with [ anyOP (o:opcode) ⇒ f o ].
-
-ndefinition any_opcode_rect
- : Πm:mcu_type.ΠP:any_opcode m → Type.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
-λm:mcu_type.λP:any_opcode m → Type.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
- match a with [ anyOP (o:opcode) ⇒ f o ].*)
-
ndefinition eq_anyop ≝
λm:mcu_type.λop1,op2:any_opcode m.
match op1 with [ anyOP op1' ⇒
Byte: byte8 → byte8_or_word16
| Word: word16 → byte8_or_word16.
-(*ndefinition byte8_or_word16_ind
- : ΠP:byte8_or_word16 → Prop.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
-λP:byte8_or_word16 → Prop.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
- match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
-
-ndefinition byte8_or_word16_rec
- : ΠP:byte8_or_word16 → Set.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
-λP:byte8_or_word16 → Set.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
- match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
-
-ndefinition byte8_or_word16_rect
- : ΠP:byte8_or_word16 → Type.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
-λP:byte8_or_word16 → Type.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
- match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].*)
-
ndefinition eq_b8w16 ≝
λbw1,bw2:byte8_or_word16.
match bw1 with
nelim m1;
##[ ##1: nelim m2; nnormalize; #H;
##[ ##1: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match HC05 with [ HC05 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##2: nelim m2; nnormalize; #H;
##[ ##2: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match HC08 with [ HC08 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##3: nelim m2; nnormalize; #H;
##[ ##3: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match HCS08 with [ HCS08 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
##| ##4: nelim m2; nnormalize; #H;
##[ ##4: napply (λx:P.x)
- ##| ##*: napply (False_ind ??);
+ ##| ##*: napply (False_ind (λ_.?) ?);
nchange with (match RS08 with [ RS08 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##1: #H; napply (λx:P.x)
##| ##2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INH with [ MODE_INH ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##2: #H; napply (λx:P.x)
##| ##1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHA with [ MODE_INHA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##3: #H; napply (λx:P.x)
##| ##1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX with [ MODE_INHX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##4: #H; napply (λx:P.x)
##| ##1,2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHH with [ MODE_INHH ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##5: #H; napply (λx:P.x)
##| ##1,2,3,4,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX0ADD with [ MODE_INHX0ADD ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##6: #H; napply (λx:P.x)
##| ##1,2,3,4,5,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX1ADD with [ MODE_INHX1ADD ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##7: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX2ADD with [ MODE_INHX2ADD ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##8: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM1 with [ MODE_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##9: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM1EXT with [ MODE_IMM1EXT ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##10: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM2 with [ MODE_IMM2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##11: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR1 with [ MODE_DIR1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##12: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR2 with [ MODE_DIR2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##13: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX0 with [ MODE_IX0 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##14: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX1 with [ MODE_IX1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##15: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX2 with [ MODE_IX2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##16: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_SP1 with [ MODE_SP1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##17: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_SP2 with [ MODE_SP2 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##18: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR1_to_DIR1 with [ MODE_DIR1_to_DIR1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##19: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM1_to_DIR1 with [ MODE_IMM1_to_DIR1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##20: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX0p_to_DIR1 with [ MODE_IX0p_to_DIR1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##21: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR1_to_IX0p with [ MODE_DIR1_to_IX0p ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##22: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHA_and_IMM1 with [ MODE_INHA_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##23: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_INHX_and_IMM1 with [ MODE_INHX_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##24: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IMM1_and_IMM1 with [ MODE_IMM1_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##25: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIR1_and_IMM1 with [ MODE_DIR1_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##26: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX0_and_IMM1 with [ MODE_IX0_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##27: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX0p_and_IMM1 with [ MODE_IX0p_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##28: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX1_and_IMM1 with [ MODE_IX1_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##29: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_IX1p_and_IMM1 with [ MODE_IX1p_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
nnormalize;
##[ ##30: #H; napply (λx:P.x)
##| ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_SP1_and_IMM1 with [ MODE_SP1_and_IMM1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ncases i2;
nnormalize;
##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIRn n1 with [ MODE_DIRn a ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##32,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIRn n1 with [ MODE_DIRn n1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31: #n2;
ncases i2;
nnormalize;
##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 a ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,33,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_DIRn_and_IMM1 n1 with [ MODE_DIRn_and_IMM1 n1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##32: #n2;
ncases i2;
nnormalize;
##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_TNY n1 with [ MODE_TNY a ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,34: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_TNY n1 with [ MODE_TNY n1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##33: #n2;
ncases i2;
nnormalize;
##[ ##1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30: #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_SRT n1 with [ MODE_SRT a ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##31,32,33: #n; #H;
- napply (False_ind ??);
+ napply (False_ind (λ_.?) ?);
nchange with (match MODE_SRT n1 with [ MODE_SRT n1 ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##| ##34: #n2;
ndefinition opcode_destruct1 : Πop2.ΠP:Prop.ADC = op2 → match op2 with [ ADC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##1: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match ADC with [ ADC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct2 : Πop2.ΠP:Prop.ADD = op2 → match op2 with [ ADD ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##2: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match ADD with [ ADD ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct3 : Πop2.ΠP:Prop.AIS = op2 → match op2 with [ AIS ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##3: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match AIS with [ AIS ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct4 : Πop2.ΠP:Prop.AIX = op2 → match op2 with [ AIX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##4: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match AIX with [ AIX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct5 : Πop2.ΠP:Prop.AND = op2 → match op2 with [ AND ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##5: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match AND with [ AND ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct6 : Πop2.ΠP:Prop.ASL = op2 → match op2 with [ ASL ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##6: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match ASL with [ ASL ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct7 : Πop2.ΠP:Prop.ASR = op2 → match op2 with [ ASR ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##7: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match ASR with [ ASR ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct8 : Πop2.ΠP:Prop.BCC = op2 → match op2 with [ BCC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##8: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BCC with [ BCC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct9 : Πop2.ΠP:Prop.BCLRn = op2 → match op2 with [ BCLRn ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##9: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BCLRn with [ BCLRn ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct10 : Πop2.ΠP:Prop.BCS = op2 → match op2 with [ BCS ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##10: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BCS with [ BCS ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct11 : Πop2.ΠP:Prop.BEQ = op2 → match op2 with [ BEQ ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##11: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BEQ with [ BEQ ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct12 : Πop2.ΠP:Prop.BGE = op2 → match op2 with [ BGE ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##12: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BGE with [ BGE ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct13 : Πop2.ΠP:Prop.BGND = op2 → match op2 with [ BGND ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##13: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BGND with [ BGND ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct14 : Πop2.ΠP:Prop.BGT = op2 → match op2 with [ BGT ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##14: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BGT with [ BGT ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct15 : Πop2.ΠP:Prop.BHCC = op2 → match op2 with [ BHCC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##15: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BHCC with [ BHCC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct16 : Πop2.ΠP:Prop.BHCS = op2 → match op2 with [ BHCS ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##16: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BHCS with [ BHCS ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct17 : Πop2.ΠP:Prop.BHI = op2 → match op2 with [ BHI ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##17: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BHI with [ BHI ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct18 : Πop2.ΠP:Prop.BIH = op2 → match op2 with [ BIH ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##18: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BIH with [ BIH ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct19 : Πop2.ΠP:Prop.BIL = op2 → match op2 with [ BIL ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##19: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BIL with [ BIL ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct20 : Πop2.ΠP:Prop.BIT = op2 → match op2 with [ BIT ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##20: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BIT with [ BIT ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct21 : Πop2.ΠP:Prop.BLE = op2 → match op2 with [ BLE ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##21: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BLE with [ BLE ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct22 : Πop2.ΠP:Prop.BLS = op2 → match op2 with [ BLS ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##22: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BLS with [ BLS ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct23 : Πop2.ΠP:Prop.BLT = op2 → match op2 with [ BLT ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##23: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BLT with [ BLT ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct24 : Πop2.ΠP:Prop.BMC = op2 → match op2 with [ BMC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##24: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BMC with [ BMC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct25 : Πop2.ΠP:Prop.BMI = op2 → match op2 with [ BMI ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##25: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BMI with [ BMI ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct26 : Πop2.ΠP:Prop.BMS = op2 → match op2 with [ BMS ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##26: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BMS with [ BMS ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct27 : Πop2.ΠP:Prop.BNE = op2 → match op2 with [ BNE ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##27: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BNE with [ BNE ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct28 : Πop2.ΠP:Prop.BPL = op2 → match op2 with [ BPL ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##28: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BPL with [ BPL ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct29 : Πop2.ΠP:Prop.BRA = op2 → match op2 with [ BRA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##29: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BRA with [ BRA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct30 : Πop2.ΠP:Prop.BRCLRn = op2 → match op2 with [ BRCLRn ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##30: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BRCLRn with [ BRCLRn ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct31 : Πop2.ΠP:Prop.BRN = op2 → match op2 with [ BRN ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##31: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BRN with [ BRN ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct32 : Πop2.ΠP:Prop.BRSETn = op2 → match op2 with [ BRSETn ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##32: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BRSETn with [ BRSETn ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct33 : Πop2.ΠP:Prop.BSETn = op2 → match op2 with [ BSETn ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##33: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BSETn with [ BSETn ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct34 : Πop2.ΠP:Prop.BSR = op2 → match op2 with [ BSR ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##34: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match BSR with [ BSR ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct35 : Πop2.ΠP:Prop.CBEQA = op2 → match op2 with [ CBEQA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##35: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match CBEQA with [ CBEQA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct36 : Πop2.ΠP:Prop.CBEQX = op2 → match op2 with [ CBEQX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##36: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match CBEQX with [ CBEQX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct37 : Πop2.ΠP:Prop.CLC = op2 → match op2 with [ CLC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##37: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match CLC with [ CLC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct38 : Πop2.ΠP:Prop.CLI = op2 → match op2 with [ CLI ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##38: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match CLI with [ CLI ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct39 : Πop2.ΠP:Prop.CLR = op2 → match op2 with [ CLR ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##39: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match CLR with [ CLR ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct40 : Πop2.ΠP:Prop.CMP = op2 → match op2 with [ CMP ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##40: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match CMP with [ CMP ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct41 : Πop2.ΠP:Prop.COM = op2 → match op2 with [ COM ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##41: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match COM with [ COM ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct42 : Πop2.ΠP:Prop.CPHX = op2 → match op2 with [ CPHX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##42: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match CPHX with [ CPHX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct43 : Πop2.ΠP:Prop.CPX = op2 → match op2 with [ CPX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##43: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match CPX with [ CPX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct44 : Πop2.ΠP:Prop.DAA = op2 → match op2 with [ DAA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##44: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match DAA with [ DAA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct45 : Πop2.ΠP:Prop.DBNZ = op2 → match op2 with [ DBNZ ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##45: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match DBNZ with [ DBNZ ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct46 : Πop2.ΠP:Prop.DEC = op2 → match op2 with [ DEC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##46: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match DEC with [ DEC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct47 : Πop2.ΠP:Prop.DIV = op2 → match op2 with [ DIV ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##47: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match DIV with [ DIV ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct48 : Πop2.ΠP:Prop.EOR = op2 → match op2 with [ EOR ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##48: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match EOR with [ EOR ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct49 : Πop2.ΠP:Prop.INC = op2 → match op2 with [ INC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##49: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match INC with [ INC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct50 : Πop2.ΠP:Prop.JMP = op2 → match op2 with [ JMP ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##50: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match JMP with [ JMP ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct51 : Πop2.ΠP:Prop.JSR = op2 → match op2 with [ JSR ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##51: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match JSR with [ JSR ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct52 : Πop2.ΠP:Prop.LDA = op2 → match op2 with [ LDA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##52: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match LDA with [ LDA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct53 : Πop2.ΠP:Prop.LDHX = op2 → match op2 with [ LDHX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##53: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match LDHX with [ LDHX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct54 : Πop2.ΠP:Prop.LDX = op2 → match op2 with [ LDX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##54: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match LDX with [ LDX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct55 : Πop2.ΠP:Prop.LSR = op2 → match op2 with [ LSR ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##55: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match LSR with [ LSR ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct56 : Πop2.ΠP:Prop.MOV = op2 → match op2 with [ MOV ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##56: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match MOV with [ MOV ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct57 : Πop2.ΠP:Prop.MUL = op2 → match op2 with [ MUL ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##57: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match MUL with [ MUL ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct58 : Πop2.ΠP:Prop.NEG = op2 → match op2 with [ NEG ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##58: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match NEG with [ NEG ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct59 : Πop2.ΠP:Prop.NOP = op2 → match op2 with [ NOP ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##59: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match NOP with [ NOP ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct60 : Πop2.ΠP:Prop.NSA = op2 → match op2 with [ NSA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##60: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match NSA with [ NSA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct61 : Πop2.ΠP:Prop.ORA = op2 → match op2 with [ ORA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##61: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match ORA with [ ORA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct62 : Πop2.ΠP:Prop.PSHA = op2 → match op2 with [ PSHA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##62: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match PSHA with [ PSHA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct63 : Πop2.ΠP:Prop.PSHH = op2 → match op2 with [ PSHH ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##63: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match PSHH with [ PSHH ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct64 : Πop2.ΠP:Prop.PSHX = op2 → match op2 with [ PSHX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##64: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match PSHX with [ PSHX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct65 : Πop2.ΠP:Prop.PULA = op2 → match op2 with [ PULA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##65: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match PULA with [ PULA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct66 : Πop2.ΠP:Prop.PULH = op2 → match op2 with [ PULH ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##66: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match PULH with [ PULH ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct67 : Πop2.ΠP:Prop.PULX = op2 → match op2 with [ PULX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##67: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match PULX with [ PULX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct68 : Πop2.ΠP:Prop.ROL = op2 → match op2 with [ ROL ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##68: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match ROL with [ ROL ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct69 : Πop2.ΠP:Prop.ROR = op2 → match op2 with [ ROR ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##69: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match ROR with [ ROR ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct70 : Πop2.ΠP:Prop.RSP = op2 → match op2 with [ RSP ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##70: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match RSP with [ RSP ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct71 : Πop2.ΠP:Prop.RTI = op2 → match op2 with [ RTI ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##71: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match RTI with [ RTI ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct72 : Πop2.ΠP:Prop.RTS = op2 → match op2 with [ RTS ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##72: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match RTS with [ RTS ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct73 : Πop2.ΠP:Prop.SBC = op2 → match op2 with [ SBC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##73: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match SBC with [ SBC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct74 : Πop2.ΠP:Prop.SEC = op2 → match op2 with [ SEC ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##74: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match SEC with [ SEC ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct75 : Πop2.ΠP:Prop.SEI = op2 → match op2 with [ SEI ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##75: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match SEI with [ SEI ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct76 : Πop2.ΠP:Prop.SHA = op2 → match op2 with [ SHA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##76: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match SHA with [ SHA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct77 : Πop2.ΠP:Prop.SLA = op2 → match op2 with [ SLA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##77: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match SLA with [ SLA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct78 : Πop2.ΠP:Prop.STA = op2 → match op2 with [ STA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##78: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match STA with [ STA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct79 : Πop2.ΠP:Prop.STHX = op2 → match op2 with [ STHX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##79: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match STHX with [ STHX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct80 : Πop2.ΠP:Prop.STOP = op2 → match op2 with [ STOP ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##80: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match STOP with [ STOP ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct81 : Πop2.ΠP:Prop.STX = op2 → match op2 with [ STX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##81: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match STX with [ STX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct82 : Πop2.ΠP:Prop.SUB = op2 → match op2 with [ SUB ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##82: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match SUB with [ SUB ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct83 : Πop2.ΠP:Prop.SWI = op2 → match op2 with [ SWI ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##83: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match SWI with [ SWI ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct84 : Πop2.ΠP:Prop.TAP = op2 → match op2 with [ TAP ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##84: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match TAP with [ TAP ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct85 : Πop2.ΠP:Prop.TAX = op2 → match op2 with [ TAX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##85: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match TAX with [ TAX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct86 : Πop2.ΠP:Prop.TPA = op2 → match op2 with [ TPA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##86: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match TPA with [ TPA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct87 : Πop2.ΠP:Prop.TST = op2 → match op2 with [ TST ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##87: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match TST with [ TST ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct88 : Πop2.ΠP:Prop.TSX = op2 → match op2 with [ TSX ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##88: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match TSX with [ TSX ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct89 : Πop2.ΠP:Prop.TXA = op2 → match op2 with [ TXA ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##89: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match TXA with [ TXA ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct90 : Πop2.ΠP:Prop.TXS = op2 → match op2 with [ TXS ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##90: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match TXS with [ TXS ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
ndefinition opcode_destruct91 : Πop2.ΠP:Prop.WAIT = op2 → match op2 with [ WAIT ⇒ P → P | _ ⇒ P ].
#op2; #P; ncases op2; nnormalize;
##[ ##91: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??);
+ ##| ##*: #H; napply (False_ind (λ_.?) ?);
nchange with (match WAIT with [ WAIT ⇒ False | _ ⇒ True ]);
nrewrite > H; nnormalize; napply I
##]
None : option A
| Some : A → option A.
-(*ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
-λA:Type.λP:option A → Prop.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
- match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
-
-ndefinition option_rec : ΠA:Type.ΠP:option A → Set.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
-λA:Type.λP:option A → Set.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
- match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
-
-ndefinition option_rect : ΠA:Type.ΠP:option A → Type.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
-λA:Type.λP:option A → Type.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
- match op with [ None ⇒ p | Some (a:A) ⇒ f a ].*)
-
ndefinition eq_option ≝
λT.λop1,op2:option T.λf:T → T → bool.
match op1 with
(symmetricT T bool f) →
(eq_option T op1 op2 f = eq_option T op2 op1 f).
#T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
nnormalize;
##[ ##1: napply (refl_eq ??)
##| ##2,3: #H; napply (refl_eq ??)
(∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
(op1 = op2 → eq_option T op1 op2 f = true).
#T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
nnormalize;
##[ ##1: #H1; napply (refl_eq ??)
##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
(∀x1,x2:T.f x1 x2 = true → x1 = x2) →
(eq_option T op1 op2 f = true → op1 = op2).
#T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
nnormalize;
##[ ##1: #H1; napply (refl_eq ??)
##| ##2,3: #a; #H1; napply (bool_destruct ??? H1)
(symmetricT T2 bool f2) →
(eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
#T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
#x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
#x2; #y2;
nnormalize;
nrewrite > (H x1 x2);
(∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
(p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
#T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
#x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
#x2; #y2; #H;
nnormalize;
nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
(∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
(eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
#T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- napply (ProdT_ind T1 T2 ?? p1);
+ nelim p1;
#x1; #y1;
- napply (ProdT_ind T1 T2 ?? p2);
+ nelim p2;
#x2; #y2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
(symmetricT T3 bool f3) →
(eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
#x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
#x2; #y2; #z2;
nnormalize;
nrewrite > (H x1 x2);
(∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
(p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
#x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
#x2; #y2; #z2; #H;
nnormalize;
nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
(∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
(eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- napply (Prod3T_ind T1 T2 T3 ?? p1);
+ nelim p1;
#x1; #y1; #z1;
- napply (Prod3T_ind T1 T2 T3 ?? p2);
+ nelim p2;
#x2; #y2; #z2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
(symmetricT T4 bool f4) →
(eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
#x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
#x2; #y2; #z2; #v2;
nnormalize;
nrewrite > (H x1 x2);
(∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
(p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
#x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
#x2; #y2; #z2; #v2; #H;
nnormalize;
nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
(∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
(eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ nelim p1;
#x1; #y1; #z1; #v1;
- napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ nelim p2;
#x2; #y2; #z2; #v2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
(symmetricT T5 bool f5) →
(eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
#x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
#x2; #y2; #z2; #v2; #w2;
nnormalize;
nrewrite > (H x1 x2);
(∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
(p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
#x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
#x2; #y2; #z2; #v2; #w2; #H;
nnormalize;
nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
(∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
(eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ nelim p1;
#x1; #y1; #z1; #v1; #w1;
- napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ nelim p2;
#x2; #y2; #z2; #v2; #w2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
nqed.
nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
- #T; #l; nelim l;
+ #T; #l;
+ nelim l;
nnormalize;
##[ ##1: napply (refl_eq ??)
##| ##2: #x; #y; #H;
nrewrite > (associative_list T l [a] l1);
nnormalize;
napply (refl_eq ??).
-nqed.
\ No newline at end of file
+nqed.
w16l: byte8
}.
-(*ndefinition word16_ind : ΠP:word16 → Prop.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
-λP:word16 → Prop.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
- match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
-
-ndefinition word16_rec : ΠP:word16 → Set.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
-λP:word16 → Set.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
- match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
-
-ndefinition word16_rect : ΠP:word16 → Type.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
-λP:word16 → Type.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
- match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
-
-ndefinition w16h ≝ λw:word16.match w with [ mk_word16 x _ ⇒ x ].
-ndefinition w16l ≝ λw:word16.match w with [ mk_word16 _ x ⇒ x ].*)
-
(* \langle \rangle *)
notation "〈x:y〉" non associative with precedence 80
for @{ 'mk_word16 $x $y }.
w32l: word16
}.
-(*ndefinition word32_ind : ΠP:word32 → Prop.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Prop.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition word32_rec : ΠP:word32 → Set.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Set.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition word32_rect : ΠP:word32 → Type.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
-λP:word32 → Type.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
- match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
-
-ndefinition w32h ≝ λdw:word32.match dw with [ mk_word32 x _ ⇒ x ].
-ndefinition w32l ≝ λdw:word32.match dw with [ mk_word32 _ x ⇒ x ].*)
-
(* \langle \rangle *)
notation "〈x.y〉" non associative with precedence 80
for @{ 'mk_word32 $x $y }.
| ch_y: ascii
| ch_z: ascii.
-(*ndefinition ascii_ind
- : ΠP:ascii → Prop.
- P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
- P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
- P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V →
- P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g →
- P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r →
- P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝
-λP:ascii → Prop.
-λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9.
-λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H.
-λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q.
-λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z.
-λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i.
-λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r.
-λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii.
- match a with
- [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7
- | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15
- | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23
- | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31
- | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39
- | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
- | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
- | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
-
-ndefinition ascii_rect
- : ΠP:ascii → Type.
- P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
- P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
- P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V →
- P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g →
- P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r →
- P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝
-λP:ascii → Type.
-λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9.
-λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H.
-λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q.
-λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z.
-λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i.
-λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r.
-λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii.
- match a with
- [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7
- | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15
- | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23
- | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31
- | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39
- | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
- | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
- | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
-*)
(* confronto fra ascii *)
ndefinition eq_ascii ≝
λc,c':ascii.match c with
ndefinition ascii_destruct2 : Πc2.ΠP:Prop.ch_1 = c2 → match c2 with [ ch_1 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##2: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_1 with [ ch_1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_1 with [ ch_1 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct3 : Πc2.ΠP:Prop.ch_2 = c2 → match c2 with [ ch_2 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##3: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_2 with [ ch_2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_2 with [ ch_2 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct4 : Πc2.ΠP:Prop.ch_3 = c2 → match c2 with [ ch_3 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##4: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_3 with [ ch_3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_3 with [ ch_3 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct5 : Πc2.ΠP:Prop.ch_4 = c2 → match c2 with [ ch_4 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##5: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_4 with [ ch_4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_4 with [ ch_4 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct6 : Πc2.ΠP:Prop.ch_5 = c2 → match c2 with [ ch_5 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##6: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_5 with [ ch_5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_5 with [ ch_5 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct7 : Πc2.ΠP:Prop.ch_6 = c2 → match c2 with [ ch_6 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##7: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_6 with [ ch_6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_6 with [ ch_6 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct8 : Πc2.ΠP:Prop.ch_7 = c2 → match c2 with [ ch_7 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##8: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_7 with [ ch_7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_7 with [ ch_7 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct9 : Πc2.ΠP:Prop.ch_8 = c2 → match c2 with [ ch_8 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##9: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_8 with [ ch_8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_8 with [ ch_8 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct10 : Πc2.ΠP:Prop.ch_9 = c2 → match c2 with [ ch_9 ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##10: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_9 with [ ch_9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_9 with [ ch_9 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct11 : Πc2.ΠP:Prop.ch__ = c2 → match c2 with [ ch__ ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##11: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch__ with [ ch__ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch__ with [ ch__ ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct12 : Πc2.ΠP:Prop.ch_A = c2 → match c2 with [ ch_A ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##12: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_A with [ ch_A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_A with [ ch_A ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct13 : Πc2.ΠP:Prop.ch_B = c2 → match c2 with [ ch_B ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##13: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_B with [ ch_B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_B with [ ch_B ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct14 : Πc2.ΠP:Prop.ch_C = c2 → match c2 with [ ch_C ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##14: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_C with [ ch_C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_C with [ ch_C ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct15 : Πc2.ΠP:Prop.ch_D = c2 → match c2 with [ ch_D ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##15: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_D with [ ch_D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_D with [ ch_D ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct16 : Πc2.ΠP:Prop.ch_E = c2 → match c2 with [ ch_E ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##16: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_E with [ ch_E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_E with [ ch_E ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct17 : Πc2.ΠP:Prop.ch_F = c2 → match c2 with [ ch_F ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##17: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_F with [ ch_F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_F with [ ch_F ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct18 : Πc2.ΠP:Prop.ch_G = c2 → match c2 with [ ch_G ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##18: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_G with [ ch_G ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_G with [ ch_G ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct19 : Πc2.ΠP:Prop.ch_H = c2 → match c2 with [ ch_H ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##19: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_H with [ ch_H ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_H with [ ch_H ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct20 : Πc2.ΠP:Prop.ch_I = c2 → match c2 with [ ch_I ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##20: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_I with [ ch_I ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_I with [ ch_I ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct21 : Πc2.ΠP:Prop.ch_J = c2 → match c2 with [ ch_J ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##21: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_J with [ ch_J ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_J with [ ch_J ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct22 : Πc2.ΠP:Prop.ch_K = c2 → match c2 with [ ch_K ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##22: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_K with [ ch_K ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_K with [ ch_K ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct23 : Πc2.ΠP:Prop.ch_L = c2 → match c2 with [ ch_L ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##23: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_L with [ ch_L ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_L with [ ch_L ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct24 : Πc2.ΠP:Prop.ch_M = c2 → match c2 with [ ch_M ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##24: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_M with [ ch_M ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_M with [ ch_M ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct25 : Πc2.ΠP:Prop.ch_N = c2 → match c2 with [ ch_N ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##25: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_N with [ ch_N ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_N with [ ch_N ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct26 : Πc2.ΠP:Prop.ch_O = c2 → match c2 with [ ch_O ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##26: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_O with [ ch_O ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_O with [ ch_O ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct27 : Πc2.ΠP:Prop.ch_P = c2 → match c2 with [ ch_P ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##27: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_P with [ ch_P ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_P with [ ch_P ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct28 : Πc2.ΠP:Prop.ch_Q = c2 → match c2 with [ ch_Q ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##28: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_Q with [ ch_Q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Q with [ ch_Q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct29 : Πc2.ΠP:Prop.ch_R = c2 → match c2 with [ ch_R ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##29: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_R with [ ch_R ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_R with [ ch_R ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct30 : Πc2.ΠP:Prop.ch_S = c2 → match c2 with [ ch_S ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##30: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_S with [ ch_S ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_S with [ ch_S ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct31 : Πc2.ΠP:Prop.ch_T = c2 → match c2 with [ ch_T ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##31: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_T with [ ch_T ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_T with [ ch_T ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct32 : Πc2.ΠP:Prop.ch_U = c2 → match c2 with [ ch_U ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##32: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_U with [ ch_U ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_U with [ ch_U ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct33 : Πc2.ΠP:Prop.ch_V = c2 → match c2 with [ ch_V ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##33: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_V with [ ch_V ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_V with [ ch_V ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct34 : Πc2.ΠP:Prop.ch_W = c2 → match c2 with [ ch_W ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##34: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_W with [ ch_W ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_W with [ ch_W ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct35 : Πc2.ΠP:Prop.ch_X = c2 → match c2 with [ ch_X ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##35: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_X with [ ch_X ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_X with [ ch_X ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct36 : Πc2.ΠP:Prop.ch_Y = c2 → match c2 with [ ch_Y ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##36: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_Y with [ ch_Y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Y with [ ch_Y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct37 : Πc2.ΠP:Prop.ch_Z = c2 → match c2 with [ ch_Z ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##37: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_Z with [ ch_Z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_Z with [ ch_Z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct38 : Πc2.ΠP:Prop.ch_a = c2 → match c2 with [ ch_a ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##38: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_a with [ ch_a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_a with [ ch_a ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct39 : Πc2.ΠP:Prop.ch_b = c2 → match c2 with [ ch_b ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##39: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_b with [ ch_b ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_b with [ ch_b ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct40 : Πc2.ΠP:Prop.ch_c = c2 → match c2 with [ ch_c ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##40: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_c with [ ch_c ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_c with [ ch_c ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct41 : Πc2.ΠP:Prop.ch_d = c2 → match c2 with [ ch_d ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##41: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_d with [ ch_d ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_d with [ ch_d ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct42 : Πc2.ΠP:Prop.ch_e = c2 → match c2 with [ ch_e ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##42: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_e with [ ch_e ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_e with [ ch_e ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct43 : Πc2.ΠP:Prop.ch_f = c2 → match c2 with [ ch_f ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##43: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_f with [ ch_f ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_f with [ ch_f ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct44 : Πc2.ΠP:Prop.ch_g = c2 → match c2 with [ ch_g ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##44: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_g with [ ch_g ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_g with [ ch_g ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct45 : Πc2.ΠP:Prop.ch_h = c2 → match c2 with [ ch_h ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##45: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_h with [ ch_h ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_h with [ ch_h ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct46 : Πc2.ΠP:Prop.ch_i = c2 → match c2 with [ ch_i ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##46: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_i with [ ch_i ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_i with [ ch_i ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct47 : Πc2.ΠP:Prop.ch_j = c2 → match c2 with [ ch_j ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##47: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_j with [ ch_j ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_j with [ ch_j ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct48 : Πc2.ΠP:Prop.ch_k = c2 → match c2 with [ ch_k ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##48: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_k with [ ch_k ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_k with [ ch_k ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct49 : Πc2.ΠP:Prop.ch_l = c2 → match c2 with [ ch_l ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##49: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_l with [ ch_l ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_l with [ ch_l ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct50 : Πc2.ΠP:Prop.ch_m = c2 → match c2 with [ ch_m ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##50: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_m with [ ch_m ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_m with [ ch_m ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct51 : Πc2.ΠP:Prop.ch_n = c2 → match c2 with [ ch_n ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##51: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_n with [ ch_n ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_n with [ ch_n ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct52 : Πc2.ΠP:Prop.ch_o = c2 → match c2 with [ ch_o ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##52: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_o with [ ch_o ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_o with [ ch_o ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct53 : Πc2.ΠP:Prop.ch_p = c2 → match c2 with [ ch_p ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##53: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_p with [ ch_p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_p with [ ch_p ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct54 : Πc2.ΠP:Prop.ch_q = c2 → match c2 with [ ch_q ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##54: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_q with [ ch_q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_q with [ ch_q ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct55 : Πc2.ΠP:Prop.ch_r = c2 → match c2 with [ ch_r ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##55: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_r with [ ch_r ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_r with [ ch_r ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct56 : Πc2.ΠP:Prop.ch_s = c2 → match c2 with [ ch_s ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##56: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_s with [ ch_s ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_s with [ ch_s ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct57 : Πc2.ΠP:Prop.ch_t = c2 → match c2 with [ ch_t ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##57: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_t with [ ch_t ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_t with [ ch_t ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct58 : Πc2.ΠP:Prop.ch_u = c2 → match c2 with [ ch_u ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##58: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_u with [ ch_u ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_u with [ ch_u ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct59 : Πc2.ΠP:Prop.ch_v = c2 → match c2 with [ ch_v ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##59: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_v with [ ch_v ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_v with [ ch_v ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct60 : Πc2.ΠP:Prop.ch_w = c2 → match c2 with [ ch_w ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##60: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_w with [ ch_w ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_w with [ ch_w ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct61 : Πc2.ΠP:Prop.ch_x = c2 → match c2 with [ ch_x ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##61: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_x with [ ch_x ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_x with [ ch_x ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct62 : Πc2.ΠP:Prop.ch_y = c2 → match c2 with [ ch_y ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##62: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_y with [ ch_y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_y with [ ch_y ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
ndefinition ascii_destruct63 : Πc2.ΠP:Prop.ch_z = c2 → match c2 with [ ch_z ⇒ P → P | _ ⇒ P ].
#c2; #P; ncases c2; nnormalize;
##[ ##63: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_z with [ ch_z ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
##]
nqed.
include "utility/ascii.ma".
include "freescale/theory.ma".
include "freescale/nat.ma".
+include "utility/utility.ma".
(* ************************ *)
(* MANIPOLAZIONE DI STRINGA *)
ndefinition aux_str_type ≝ list ascii.
(* strcmp *)
-nlet rec eq_str (str,str':aux_str_type) ≝
- match str with
- [ nil ⇒ match str' with
- [ nil => true
- | cons _ _ => false ]
- | cons h t ⇒ match str' with
- [ nil ⇒ false
- | cons h' t' ⇒ (eq_ascii h h')⊗(eq_str t t')
- ]
- ].
+ndefinition eq_str ≝
+ bfold_right_list2 ascii (λx,y.eq_ascii x y).
(* ************ *)
(* STRINGA + ID *)
(* ************ *)
(* tipo pubblico *)
-ninductive aux_strId_type : Type ≝
- STR_ID: aux_str_type → nat → aux_strId_type.
-
-(*ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
-λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].
-
-ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
-λP:aux_strId_type → Set.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].
-
-ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
-λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].*)
-
-(* getter *)
-ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
-ndefinition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
+nrecord strId : Type ≝
+ {
+ str_elem: aux_str_type;
+ id_elem: nat
+ }.
(* confronto *)
ndefinition eq_strId ≝
-λsid,sid':aux_strId_type.(eq_str (get_name_strId sid) (get_name_strId sid'))⊗(eq_nat (get_id_strId sid) (get_id_strId sid')).
+λsid,sid':strId.
+ (eq_str (str_elem sid) (str_elem sid'))⊗
+ (eq_nat (id_elem sid) (id_elem sid')).
include "utility/string.ma".
include "utility/ascii_lemmas2.ma".
include "freescale/nat_lemmas.ma".
+include "utility/utility_lemmas.ma".
(* ************************ *)
(* MANIPOLAZIONE DI STRINGA *)
(* ************************ *)
-nlemma symmetric_eqstr : symmetricT aux_str_type bool eq_str.
- #l1;
- napply (list_ind ascii ??? l1);
- ##[ ##1: #l2; ncases l2;
- ##[ ##1: nnormalize; napply (refl_eq ??)
- ##| ##2: #x; #y; nnormalize; napply (refl_eq ??)
- ##]
- ##| ##2: #x1; #x2; #H; #l2; ncases l2;
- ##[ ##1: nnormalize; napply (refl_eq ??)
- ##| ##2: #y1; #y2;
- nchange with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = ((eq_ascii y1 x1)⊗(eq_str y2 x2)));
- nrewrite > (symmetric_eqascii x1 y1);
- nrewrite > (H y2);
- napply (refl_eq ??)
- ##]
- ##]
+nlemma symmetric_eqstr : symmetricT (list ascii) bool eq_str.
+ #s1; #s2;
+ napply (symmetric_bfoldrightlist2 ascii eq_ascii s1 s2 symmetric_eqascii).
nqed.
nlemma eqstr_to_eq : ∀s,s'.eq_str s s' = true → s = s'.
- #l1;
- napply (list_ind ascii ??? l1);
- ##[ ##1: #l2; ncases l2;
- ##[ ##1: nnormalize; #H; napply (refl_eq ??)
- ##| ##2: #x1; #x2; nnormalize; #H; napply (bool_destruct ??? H)
- ##]
- ##| ##2: #x1; #x2; #H; #l2; ncases l2;
- ##[ ##1: nnormalize; #H1; napply (bool_destruct ??? H1)
- ##| ##2: #y1; #y2; #H1;
- nchange in H1:(%) with (((eq_ascii x1 y1)⊗(eq_str x2 y2)) = true);
- nrewrite > (eqascii_to_eq x1 y1 (andb_true_true_l ?? H1));
- nrewrite > (H y2 (andb_true_true_r ?? H1));
- napply (refl_eq ??)
- ##]
- ##]
+ #s1; #s2;
+ napply (bfoldrightlist2_to_eq ascii eq_ascii s1 s2 eqascii_to_eq).
nqed.
nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true.
- #l1;
- napply (list_ind ascii ??? l1);
- ##[ ##1: #l2; ncases l2;
- ##[ ##1: nnormalize; #H; napply (refl_eq ??)
- ##| ##2: #x1; #x2; nnormalize; #H; nelim (list_destruct_nil_cons ascii ?? H)
- ##]
- ##| ##2: #x1; #x2; #H; #l2; ncases l2;
- ##[ ##1: #H; nelim (list_destruct_cons_nil ascii ?? H)
- ##| ##2: #y1; #y2; #H1;
- nrewrite > (list_destruct_1 ascii ???? H1);
- nchange with (((eq_ascii y1 y1)⊗(eq_str x2 y2)) = true);
- nrewrite > (H y2 (list_destruct_2 ascii ???? H1));
- nrewrite > (eq_to_eqascii y1 y1 (refl_eq ??));
- nnormalize;
- napply (refl_eq ??)
- ##]
- ##]
+ #s1; #s2;
+ napply (eq_to_bfoldrightlist2 ascii eq_ascii s1 s2 eq_to_eqascii).
nqed.
(* ************ *)
(* STRINGA + ID *)
(* ************ *)
-nlemma strid_destruct_1 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → x1 = x2.
+nlemma strid_destruct_1 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → x1 = x2.
#x1; #x2; #y1; #y2; #H;
- nchange with (match STR_ID x2 y2 with [ STR_ID a _ ⇒ x1 = a ]);
+ nchange with (match mk_strId x2 y2 with [ mk_strId a _ ⇒ x1 = a ]);
nrewrite < H;
nnormalize;
napply (refl_eq ??).
nqed.
-nlemma strid_destruct_2 : ∀x1,x2,y1,y2.STR_ID x1 y1 = STR_ID x2 y2 → y1 = y2.
+nlemma strid_destruct_2 : ∀x1,x2,y1,y2.mk_strId x1 y1 = mk_strId x2 y2 → y1 = y2.
#x1; #x2; #y1; #y2; #H;
- nchange with (match STR_ID x2 y2 with [ STR_ID _ b ⇒ y1 = b ]);
+ nchange with (match mk_strId x2 y2 with [ mk_strId _ b ⇒ y1 = b ]);
nrewrite < H;
nnormalize;
napply (refl_eq ??).
nqed.
-nlemma symmetric_eqstrid : symmetricT aux_strId_type bool eq_strId.
+nlemma symmetric_eqstrid : symmetricT strId bool eq_strId.
#si1; #si2;
- ncases si1;
- #l1; #n1;
- ncases si2;
- #l2; #n2;
- nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = ((eq_str l2 l1)⊗(eq_nat n2 n1)));
- nrewrite > (symmetric_eqstr l1 l2);
- nrewrite > (symmetric_eqnat n1 n2);
+ nchange with (
+ ((eq_str (str_elem si1) (str_elem si2))⊗(eq_nat (id_elem si1) (id_elem si2))) =
+ ((eq_str (str_elem si2) (str_elem si1))⊗(eq_nat (id_elem si2) (id_elem si1))));
+ nrewrite > (symmetric_eqstr (str_elem si1) (str_elem si2));
+ nrewrite > (symmetric_eqnat (id_elem si1) (id_elem si2));
napply (refl_eq ??).
-nqed.
+nqed.
nlemma eqstrid_to_eq : ∀s,s'.eq_strId s s' = true → s = s'.
- #si1; #si2;
- ncases si1;
+ #si1; #si2;
+ nelim si1;
#l1; #n1;
- ncases si2;
+ nelim si2;
#l2; #n2; #H;
nchange in H:(%) with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
nrewrite > (eqstr_to_eq l1 l2 (andb_true_true_l ?? H));
nqed.
nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true.
- #si1; #si2;
- ncases si1;
+ #si1; #si2;
+ nelim si1;
#l1; #n1;
- ncases si2;
+ nelim si2;
#l2; #n2; #H;
nchange with (((eq_str l1 l2)⊗(eq_nat n1 n2)) = true);
nrewrite > (strid_destruct_1 ???? H);
| ne_nil: A → ne_list A
| ne_cons: A → ne_list A → ne_list A.
-(*nlet rec ne_list_ind (A:Type) (P:ne_list A → Prop) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
- match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_ind A P f f1 t) ].
-
-nlet rec ne_list_rec (A:Type) (P:ne_list A → Set) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
- match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rec A P f f1 t) ].
-
-nlet rec ne_list_rect (A:Type) (P:ne_list A → Type) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
- match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rect A P f f1 t) ].*)
-
(* append *)
nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
match l1 with
nlemma fold_right_list2_aux3 :
∀T.∀h,h',t,t'.len_list T (h::t) = len_list T (h'::t') → len_list T t = len_list T t'.
#T; #h; #h'; #t; #t';
- napply (list_ind T ??? t);
- napply (list_ind T ??? t');
+ nelim t;
+ nelim t';
##[ ##1: nnormalize; #H; napply (refl_eq ??)
##| ##2: #a; #l'; #H; #H1;
nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
]
].
+nlet rec bfold_right_list2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:list T1) on l1 ≝
+ match l1 with
+ [ nil ⇒ match l2 with
+ [ nil ⇒ true | cons h t ⇒ false ]
+ | cons h t ⇒ match l2 with
+ [ nil ⇒ false | cons h' t' ⇒ (f h h') ⊗ (bfold_right_list2 T1 f t t')
+ ]
+ ].
+
nlemma fold_right_neList2_aux1 :
∀T.∀h,h',t'.len_neList T «£h» = len_neList T (h'§§t') → False.
#T; #h; #h'; #t';
nlemma fold_right_neList2_aux3 :
∀T.∀h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
#T; #h; #h'; #t; #t';
- napply (ne_list_ind T ??? t);
- napply (ne_list_ind T ??? t');
+ nelim t;
+ nelim t';
##[ ##1: nnormalize; #x; #y; #H; napply (refl_eq ??)
##| ##2: #a; #l'; #H; #x; #H1;
nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
]
].
+nlet rec bfold_right_neList2 (T1:Type) (f:T1 → T1 → bool) (l1,l2:ne_list T1) on l1 ≝
+ match l1 with
+ [ ne_nil h ⇒ match l2 with
+ [ ne_nil h' ⇒ f h h' | ne_cons h' t' ⇒ false ]
+ | ne_cons h t ⇒ match l2 with
+ [ ne_nil h' ⇒ false | ne_cons h' t' ⇒ (f h h') ⊗ (bfold_right_neList2 T1 f t t')
+ ]
+ ].
+
(* ******** *)
(* naturali *)
(* ******** *)
nlemma symmetric_eqlenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
#T; #l1;
- napply (list_ind ???? l1);
+ nelim l1;
##[ ##1: #l2; ncases l2; nnormalize;
##[ ##1: #H; napply (refl_eq ??)
##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H)
(∀x,y,z.f x y z = f y x z) →
fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2.
#T1; #T2; #f; #acc; #l1;
- napply (list_ind ???? l1);
+ nelim l1;
##[ ##1: #l2; ncases l2;
##[ ##1: nnormalize; #H1; #H2; #H3; napply (refl_eq ??)
##| ##2: #h; #l; #H1; #H2; #H3;
napply (refl_eq ??).
nqed.
+nlemma symmetric_bfoldrightlist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+ (∀x,y.f x y = f y x) →
+ bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+ ##[ ##1: #H; nnormalize; napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; #H; nnormalize; napply (refl_eq ??)
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #H1; nnormalize; napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; #H1; nnormalize;
+ nrewrite > (H ll2 H1);
+ nrewrite > (H1 hh1 hh2);
+ napply (refl_eq ??)
+ ##]
+ ##]
+nqed.
+
+nlemma bfoldrightlist2_to_eq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+ (∀x,y.(f x y = true → x = y)) →
+ (bfold_right_list2 T1 f l1 l2 = true → l1 = l2).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+ ##[ ##1: #H; #H1; napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct ??? H1)
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct ??? H2)
+ ##| ##2: #hh2; #ll2; #H1; #H2;
+ nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
+ nrewrite > (H1 hh1 hh2 (andb_true_true_l ?? H2));
+ nrewrite > (H ll2 H1 (andb_true_true_r ?? H2));
+ napply (refl_eq ??)
+ ##]
+ ##]
+nqed.
+
+nlemma eq_to_bfoldrightlist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+ (∀x,y.(x = y → f x y = true)) →
+ (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+ ##[ ##1: #H; #H1; nnormalize; napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
+ ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
+ nrewrite > (list_destruct_1 ????? H2);
+ nrewrite > (H1 hh2 hh2 (refl_eq ??));
+ nnormalize;
+ nrewrite > (H ll2 H1 (list_destruct_2 ????? H2));
+ napply (refl_eq ??)
+ ##]
+ ##]
+nqed.
+
nlemma symmetric_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
#T; #l1;
- napply (ne_list_ind ???? l1);
+ nelim l1;
##[ ##1: #h; #l2; ncases l2; nnormalize;
##[ ##1: #H; #H1; napply (refl_eq ??)
##| ##2: #h; #t; #H; nrewrite > H; napply (refl_eq ??)
(∀x,y,z.f x y z = f y x z) →
fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
#T1; #T2; #f; #acc; #l1;
- napply (ne_list_ind ???? l1);
+ nelim l1;
##[ ##1: #h; #l2; ncases l2;
##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply (refl_eq ??)
##| ##2: #h1; #l; ncases l;
napply (refl_eq ??).
nqed.
+nlemma symmetric_bfoldrightnelist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+ (∀x,y.f x y = f y x) →
+ bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+ ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; #H; nnormalize; napply (refl_eq ??)
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #hh2; #H1; nnormalize; napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; #H1; nnormalize;
+ nrewrite > (H ll2 H1);
+ nrewrite > (H1 hh1 hh2);
+ napply (refl_eq ??)
+ ##]
+ ##]
+nqed.
+
+nlemma bfoldrightnelist2_to_eq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+ (∀x,y.(f x y = true → x = y)) →
+ (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+ ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct ??? H1)
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct ??? H2)
+ ##| ##2: #hh2; #ll2; #H1; #H2;
+ nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
+ nrewrite > (H1 hh1 hh2 (andb_true_true_l ?? H2));
+ nrewrite > (H ll2 H1 (andb_true_true_r ?? H2));
+ napply (refl_eq ??)
+ ##]
+ ##]
+nqed.
+
+nlemma eq_to_bfoldrightnelist2
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+ (∀x,y.(x = y → f x y = true)) →
+ (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+ ##[ ##1: #hh2; #H; #H1; nnormalize;
+ nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil ??? H1));
+ napply (refl_eq ??)
+ ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
+ ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
+ nrewrite > (nelist_destruct_cons_cons_1 ????? H2);
+ nrewrite > (H1 hh2 hh2 (refl_eq ??));
+ nnormalize;
+ nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 ????? H2));
+ napply (refl_eq ??)
+ ##]
+ ##]
+nqed.
+
nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
#T; #l;
ncases l;
projects / helm.git / commitdiff