(* NATURALI *)
(* ******** *)
-inductive nat : Type ≝
+ninductive nat : Type ≝
O : nat
| S : nat → nat.
+(*
interpretation "Natural numbers" 'N = nat.
default "natural numbers" cic:/matita/common/nat/nat.ind.
alias num (instance 0) = "natural number".
+*)
nlet rec eq_nat (n1,n2:nat) on n1 ≝
match n1 with
napply I.
nqed.
-nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
- nnormalize;
- #n1;
- nelim n1;
- ##[ ##1: #n2;
- nelim n2;
- nnormalize;
- ##[ ##1: napply refl_eq
- ##| ##2: #n3; #H; napply refl_eq
- ##]
- ##| ##2: #n2; #H; #n3;
- nnormalize;
- ncases n3;
- nnormalize;
- ##[ ##1: napply refl_eq
- ##| ##2: #n4; napply (H n4)
- ##]
- ##]
-nqed.
-
nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
#n1;
nelim n1;
##]
nqed.
+nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_nat n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqnat n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
+ ##]
+nqed.
+
nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
#n1;
nelim n1;
##]
nqed.
-nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
- #x; nelim x; nnormalize;
- ##[ ##1: #y; ncases y;
- ##[ ##1: napply (or2_intro1 (O = O) (O ≠ O) (refl_eq …))
- ##| ##2: #n2; napply (or2_intro2 (O = (S n2)) (O ≠ (S n2)) ?);
- nnormalize; #H; napply (nat_destruct_0_S n2 H)
- ##]
- ##| ##2: #n1; #H; #y; ncases y;
- ##[ ##1: napply (or2_intro2 ((S n1) = O) ((S n1) ≠ O) ?);
- nnormalize; #H1; napply (nat_destruct_S_0 n1 H1)
- ##| ##2: #n2; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (H n2) …);
- ##[ ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) …);
- nrewrite > H1; napply refl_eq
- ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …);
- nnormalize; #H2; napply (H1 (nat_destruct_S_S … H2))
- ##]
- ##]
- ##]
+nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_nat n1 n2));
+ napply (not_to_not (eq_nat n1 n2 = true) (n1 = n2) ? H);
+ napply (eqnat_to_eq n1 n2).
nqed.
-nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
- #n1; nelim n1;
- ##[ ##1: #n2; ncases n2;
- ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
- ##| ##2: #nn2; #H; nnormalize; napply refl_eq
- ##]
- ##| ##2: #nn1; #H; #n2; ncases n2;
- ##[ ##1: #H1; nnormalize; napply refl_eq
- ##| ##2: #nn2; nnormalize; #H1;
- napply (H nn2 ?); nnormalize; #H2;
- nrewrite > H2 in H1:(%); #H1;
- napply (H1 (refl_eq …))
- ##]
+nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_nat x y = true) (eq_nat x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqnat_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqnat_to_neq … H))
##]
nqed.
-nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
- #n1; nelim n1;
- ##[ ##1: #n2; ncases n2;
- ##[ ##1: nnormalize; #H; napply (bool_destruct … H)
- ##| ##2: #nn2; nnormalize; #H; #H1; nelim (nat_destruct_0_S … H1)
- ##]
- ##| ##2: #nn1; #H; #n2; ncases n2;
- ##[ ##1: nnormalize; #H1; #H2; nelim (nat_destruct_S_0 … H2)
- ##| ##2: #nn2; nnormalize; #H1; #H2; napply (H nn2 H1 ?);
- napply (nat_destruct_S_S … H2)
- ##]
+nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqnat n1 n2 H);
+ napply (symmetric_eq ? (eq_nat n2 n1) false);
+ napply (neq_to_neqnat n2 n1 (symmetric_neq ? n1 n2 H))
##]
nqed.
#y; nelim y; #yy1; #yy2;
nnormalize;
napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
- ##[ ##1: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H3; napply (H2 (pair_destruct_1 T1 T2 … H3))
- ##| ##2: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
- ##[ ##1: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+ ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H4; napply (H3 (pair_destruct_2 T1 T2 … H4))
- ##| ##2: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
nrewrite > H2; nrewrite > H3; napply refl_eq
##]
##]
nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2)) = false) → ?); #H;
nnormalize; #H3;
napply (or2_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ? (andb_false2 … H) ?);
- ##[ ##1: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
- ##| ##2: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
+ ##[ ##1: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
+ ##| ##2: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
##]
nqed.
#T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2;
nnormalize; #H;
napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
- ##[ ##1: #H3; napply (or2_intro1 … H3)
- ##| ##2: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
- ##[ ##1: #H4; napply (or2_intro2 … H4)
- ##| ##2: #H4; nrewrite > H3 in H:(%);
+ ##[ ##2: #H3; napply (or2_intro1 … H3)
+ ##| ##1: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##2: #H4; napply (or2_intro2 … H4)
+ ##| ##1: #H4; nrewrite > H3 in H:(%);
nrewrite > H4; #H; nelim (H (refl_eq …))
##]
##]
#x2; #y2; #H;
nchange with (((f1 x1 x2) ⊗ (f2 y1 y2)) = false);
napply (or2_elim (x1 ≠ x2) (y1 ≠ y2) ? (pair_destruct T1 T2 H1 H2 … H) ?);
- ##[ ##1: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
- ##| ##2: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
+ ##[ ##2: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
+ ##| ##1: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
##]
nqed.
#y; nelim y; #yy1; #yy2; #yy3;
nnormalize;
napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
- ##[ ##1: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H4; napply (H3 (triple_destruct_1 T1 T2 T3 … H4))
- ##| ##2: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
- ##[ ##1: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+ ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H5; napply (H4 (triple_destruct_2 T1 T2 T3 … H5))
- ##| ##2: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
- ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+ ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H6; napply (H5 (triple_destruct_3 T1 T2 T3 … H6))
- ##| ##2: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
nrewrite > H3;
nrewrite > H4;
nrewrite > H5;
nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false) → ?); #H;
nnormalize; #H4;
napply (or3_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ? (andb_false3 … H) ?);
- ##[ ##1: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
- ##| ##2: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
- ##| ##3: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
+ ##[ ##1: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
+ ##| ##2: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
+ ##| ##3: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
##]
nqed.
#T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2;
nnormalize; #H;
napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
- ##[ ##1: #H4; napply (or3_intro1 … H4)
- ##| ##2: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
- ##[ ##1: #H5; napply (or3_intro2 … H5)
- ##| ##2: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
- ##[ ##1: #H6; napply (or3_intro3 … H6)
- ##| ##2: #H6; nrewrite > H4 in H:(%);
+ ##[ ##2: #H4; napply (or3_intro1 … H4)
+ ##| ##1: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##2: #H5; napply (or3_intro2 … H5)
+ ##| ##1: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+ ##[ ##2: #H6; napply (or3_intro3 … H6)
+ ##| ##1: #H6; nrewrite > H4 in H:(%);
nrewrite > H5;
nrewrite > H6; #H; nelim (H (refl_eq …))
##]
#x2; #y2; #z2; #H;
nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false);
napply (or3_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) ? (triple_destruct T1 T2 T3 H1 H2 H3 … H) ?);
- ##[ ##1: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
- ##| ##2: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
- ##| ##3: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
+ ##[ ##1: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
+ ##| ##2: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
+ ##| ##3: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
##]
nqed.
#y; nelim y; #yy1; #yy2; #yy3; #yy4;
nnormalize;
napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
- ##[ ##1: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H5; napply (H4 (quadruple_destruct_1 T1 T2 T3 T4 … H5))
- ##| ##2: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
- ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+ ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H6; napply (H5 (quadruple_destruct_2 T1 T2 T3 T4 … H6))
- ##| ##2: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
- ##[ ##1: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+ ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H7; napply (H6 (quadruple_destruct_3 T1 T2 T3 T4 … H7))
- ##| ##2: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
- ##[ ##1: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
+ ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H8; napply (H7 (quadruple_destruct_4 T1 T2 T3 T4 … H8))
- ##| ##2: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
nrewrite > H4;
nrewrite > H5;
nrewrite > H6;
nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false) → ?); #H;
nnormalize; #H5;
napply (or4_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ? (andb_false4 … H) ?);
- ##[ ##1: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
- ##| ##2: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
- ##| ##3: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
- ##| ##4: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
+ ##[ ##1: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
+ ##| ##2: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
+ ##| ##3: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
+ ##| ##4: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
##]
nqed.
#x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2;
nnormalize; #H;
napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
- ##[ ##1: #H5; napply (or4_intro1 … H5)
- ##| ##2: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
- ##[ ##1: #H6; napply (or4_intro2 … H6)
- ##| ##2: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
- ##[ ##1: #H7; napply (or4_intro3 … H7)
- ##| ##2: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
- ##[ ##1: #H8; napply (or4_intro4 … H8)
- ##| ##2: #H8; nrewrite > H5 in H:(%);
+ ##[ ##2: #H5; napply (or4_intro1 … H5)
+ ##| ##1: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##2: #H6; napply (or4_intro2 … H6)
+ ##| ##1: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+ ##[ ##2: #H7; napply (or4_intro3 … H7)
+ ##| ##1: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
+ ##[ ##2: #H8; napply (or4_intro4 … H8)
+ ##| ##1: #H8; nrewrite > H5 in H:(%);
nrewrite > H6;
nrewrite > H7;
nrewrite > H8; #H; nelim (H (refl_eq …))
#x2; #y2; #z2; #v2; #H;
nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false);
napply (or4_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) ? (quadruple_destruct T1 T2 T3 T4 H1 H2 H3 H4 … H) ?);
- ##[ ##1: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
- ##| ##2: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
- ##| ##3: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
- ##| ##4: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##[ ##1: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##| ##2: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##| ##3: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
+ ##| ##4: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
##]
nqed.
#y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5;
nnormalize;
napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
- ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H6; napply (H5 (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6))
- ##| ##2: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
- ##[ ##1: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+ ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H7; napply (H6 (quintuple_destruct_2 T1 T2 T3 T4 T5 … H7))
- ##| ##2: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
- ##[ ##1: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+ ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H8; napply (H7 (quintuple_destruct_3 T1 T2 T3 T4 T5 … H8))
- ##| ##2: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
- ##[ ##1: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
+ ##[ ##2: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H9; napply (H8 (quintuple_destruct_4 T1 T2 T3 T4 T5 … H9))
- ##| ##2: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
- ##[ ##1: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
+ ##[ ##2: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
nnormalize; #H10; napply (H9 (quintuple_destruct_5 T1 T2 T3 T4 T5 … H10))
- ##| ##2: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ ##| ##1: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
nrewrite > H5;
nrewrite > H6;
nrewrite > H7;
nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false) → ?); #H;
nnormalize; #H6;
napply (or5_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ((f5 w1 w2) = false) ? (andb_false5 … H) ?);
- ##[ ##1: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
- ##| ##2: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
- ##| ##3: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
- ##| ##4: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
- ##| ##5: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
+ ##[ ##1: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
+ ##| ##2: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
+ ##| ##3: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
+ ##| ##4: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
+ ##| ##5: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
##]
nqed.
#x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2;
nnormalize; #H;
napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
- ##[ ##1: #H6; napply (or5_intro1 … H6)
- ##| ##2: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
- ##[ ##1: #H7; napply (or5_intro2 … H7)
- ##| ##2: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
- ##[ ##1: #H8; napply (or5_intro3 … H8)
- ##| ##2: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
- ##[ ##1: #H9; napply (or5_intro4 … H9)
- ##| ##2: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
- ##[ ##1: #H10; napply (or5_intro5 … H10)
- ##| ##2: #H10; nrewrite > H6 in H:(%);
+ ##[ ##2: #H6; napply (or5_intro1 … H6)
+ ##| ##1: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##2: #H7; napply (or5_intro2 … H7)
+ ##| ##1: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+ ##[ ##2: #H8; napply (or5_intro3 … H8)
+ ##| ##1: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
+ ##[ ##2: #H9; napply (or5_intro4 … H9)
+ ##| ##1: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
+ ##[ ##2: #H10; napply (or5_intro5 … H10)
+ ##| ##1: #H10; nrewrite > H6 in H:(%);
nrewrite > H7;
nrewrite > H8;
nrewrite > H9;
#x2; #y2; #z2; #v2; #w2; #H;
nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false);
napply (or5_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2) ? (quintuple_destruct T1 T2 T3 T4 T5 H1 H2 H3 H4 H5 … H) ?);
- ##[ ##1: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
- ##| ##2: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
- ##| ##3: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
- ##| ##4: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
- ##| ##5: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##[ ##1: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##| ##2: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##| ##3: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##| ##4: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
+ ##| ##5: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
##]
nqed.
freescale/opcode_base_lemmas_opcode.ma freescale/opcode_base.ma num/bool_lemmas.ma
common/list_lemmas.ma common/list.ma
common/sigma.ma
-universe/universe.ma common/list.ma num/bool_lemmas.ma
+universe/universe.ma common/list.ma common/nat_lemmas.ma
num/bitrigesim.ma num/bool.ma
common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma
freescale/opcode_base_lemmas_instrmode.ma freescale/opcode_base.ma num/bitrigesim_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma
(* byte → byte ricorsivi *)
ndefinition b8_to_recb8_aux1 : Πn.rec_byte8 〈n,x0〉 → rec_byte8 〈succ_ex n,x0〉 ≝
λn.λrecb:rec_byte8 〈n,x0〉.
- b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (
- b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))).
+ b8_S 〈n,xF〉 (b8_S 〈n,xE〉 (b8_S 〈n,xD〉 (b8_S 〈n,xC〉 (
+ b8_S 〈n,xB〉 (b8_S 〈n,xA〉 (b8_S 〈n,x9〉 (b8_S 〈n,x8〉 (
+ b8_S 〈n,x7〉 (b8_S 〈n,x6〉 (b8_S 〈n,x5〉 (b8_S 〈n,x4〉 (
+ b8_S 〈n,x3〉 (b8_S 〈n,x2〉 (b8_S 〈n,x1〉 (b8_S 〈n,x0〉 recb))))))))))))))).
(* ... cifra esadecimale superiore *)
nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
λn1,n2.λrecb:rec_byte8 〈n1,x0〉.
match n2 return λx.rec_byte8 〈n1,x〉 with
[ x0 ⇒ recb
- | x1 ⇒ b8_S ? recb
- | x2 ⇒ b8_S ? (b8_S ? recb)
- | x3 ⇒ b8_S ? (b8_S ? (b8_S ? recb))
- | x4 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))
- | x5 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))
- | x6 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))
- | x7 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))
- | x8 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))
- | x9 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))
- | xA ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))
- | xB ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))
- | xC ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))
- | xD ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))
- | xE ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))))
- | xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))
+ | x1 ⇒ b8_S 〈n1,x0〉 recb
+ | x2 ⇒ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)
+ | x3 ⇒ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))
+ | x4 ⇒ b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))
+ | x5 ⇒ b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
+ b8_S 〈n1,x0〉 recb))))
+ | x6 ⇒ b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
+ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))
+ | x7 ⇒ b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
+ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))
+ | x8 ⇒ b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
+ b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))
+ | x9 ⇒ b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
+ b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
+ b8_S 〈n1,x0〉 recb))))))))
+ | xA ⇒ b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
+ b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
+ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))
+ | xB ⇒ b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
+ b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
+ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))
+ | xC ⇒ b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (
+ b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (
+ b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))
+ | xD ⇒ b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (
+ b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (
+ b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (
+ b8_S 〈n1,x0〉 recb))))))))))))
+ | xE ⇒ b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (b8_S 〈n1,xA〉 (
+ b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (b8_S 〈n1,x6〉 (
+ b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (b8_S 〈n1,x2〉 (
+ b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb)))))))))))))
+ | xF ⇒ b8_S 〈n1,xE〉 (b8_S 〈n1,xD〉 (b8_S 〈n1,xC〉 (b8_S 〈n1,xB〉 (
+ b8_S 〈n1,xA〉 (b8_S 〈n1,x9〉 (b8_S 〈n1,x8〉 (b8_S 〈n1,x7〉 (
+ b8_S 〈n1,x6〉 (b8_S 〈n1,x5〉 (b8_S 〈n1,x4〉 (b8_S 〈n1,x3〉 (
+ b8_S 〈n1,x2〉 (b8_S 〈n1,x1〉 (b8_S 〈n1,x0〉 recb))))))))))))))
].
(*
*)
ndefinition b8_to_recb8 : Πb.rec_byte8 b ≝
- λb.match b with
- [ mk_byte8 h l ⇒
- b8_to_recb8_aux3
- h l (b8_to_recb8_aux2 h (ex_to_recex h)) ].
+λb.match b with [ mk_byte8 h l ⇒ b8_to_recb8_aux3 h l (b8_to_recb8_aux2 h (ex_to_recex h)) ].
(* ottali → esadecimali *)
ndefinition b8_of_bit ≝
| w16_S : ∀n.rec_word16 n → rec_word16 (succ_w16 n).
(* word16 → word16 ricorsive *)
+
+(* EX: ancora problema di tempi ???
ndefinition w16_to_recw16_aux1_1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x1,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x0,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? recw
+ w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? recw
+ ))))))))))))))).
+*)
+
+ndefinition w16_to_recw16_aux1_1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x1,x0〉〉 ≝
+λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
+ w16_S 〈n:〈x0,xF〉〉 (w16_S 〈n:〈x0,xE〉〉 (w16_S 〈n:〈x0,xD〉〉 (w16_S 〈n:〈x0,xC〉〉 (
+ w16_S 〈n:〈x0,xB〉〉 (w16_S 〈n:〈x0,xA〉〉 (w16_S 〈n:〈x0,x9〉〉 (w16_S 〈n:〈x0,x8〉〉 (
+ w16_S 〈n:〈x0,x7〉〉 (w16_S 〈n:〈x0,x6〉〉 (w16_S 〈n:〈x0,x5〉〉 (w16_S 〈n:〈x0,x4〉〉 (
+ w16_S 〈n:〈x0,x3〉〉 (w16_S 〈n:〈x0,x2〉〉 (w16_S 〈n:〈x0,x1〉〉 (w16_S 〈n:〈x0,x0〉〉 recw
))))))))))))))).
ndefinition w16_to_recw16_aux1_2 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x2,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x1,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_1 ? recw)
+ w16_S 〈n:〈x1,xF〉〉 (w16_S 〈n:〈x1,xE〉〉 (w16_S 〈n:〈x1,xD〉〉 (w16_S 〈n:〈x1,xC〉〉 (
+ w16_S 〈n:〈x1,xB〉〉 (w16_S 〈n:〈x1,xA〉〉 (w16_S 〈n:〈x1,x9〉〉 (w16_S 〈n:〈x1,x8〉〉 (
+ w16_S 〈n:〈x1,x7〉〉 (w16_S 〈n:〈x1,x6〉〉 (w16_S 〈n:〈x1,x5〉〉 (w16_S 〈n:〈x1,x4〉〉 (
+ w16_S 〈n:〈x1,x3〉〉 (w16_S 〈n:〈x1,x2〉〉 (w16_S 〈n:〈x1,x1〉〉 (w16_S 〈n:〈x1,x0〉〉 (w16_to_recw16_aux1_1 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_3 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x3,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x2,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_2 ? recw)
+ w16_S 〈n:〈x2,xF〉〉 (w16_S 〈n:〈x2,xE〉〉 (w16_S 〈n:〈x2,xD〉〉 (w16_S 〈n:〈x2,xC〉〉 (
+ w16_S 〈n:〈x2,xB〉〉 (w16_S 〈n:〈x2,xA〉〉 (w16_S 〈n:〈x2,x9〉〉 (w16_S 〈n:〈x2,x8〉〉 (
+ w16_S 〈n:〈x2,x7〉〉 (w16_S 〈n:〈x2,x6〉〉 (w16_S 〈n:〈x2,x5〉〉 (w16_S 〈n:〈x2,x4〉〉 (
+ w16_S 〈n:〈x2,x3〉〉 (w16_S 〈n:〈x2,x2〉〉 (w16_S 〈n:〈x2,x1〉〉 (w16_S 〈n:〈x2,x0〉〉 (w16_to_recw16_aux1_2 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_4 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x4,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x3,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_3 ? recw)
+ w16_S 〈n:〈x3,xF〉〉 (w16_S 〈n:〈x3,xE〉〉 (w16_S 〈n:〈x3,xD〉〉 (w16_S 〈n:〈x3,xC〉〉 (
+ w16_S 〈n:〈x3,xB〉〉 (w16_S 〈n:〈x3,xA〉〉 (w16_S 〈n:〈x3,x9〉〉 (w16_S 〈n:〈x3,x8〉〉 (
+ w16_S 〈n:〈x3,x7〉〉 (w16_S 〈n:〈x3,x6〉〉 (w16_S 〈n:〈x3,x5〉〉 (w16_S 〈n:〈x3,x4〉〉 (
+ w16_S 〈n:〈x3,x3〉〉 (w16_S 〈n:〈x3,x2〉〉 (w16_S 〈n:〈x3,x1〉〉 (w16_S 〈n:〈x3,x0〉〉 (w16_to_recw16_aux1_3 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_5 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x5,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x4,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_4 ? recw)
+ w16_S 〈n:〈x4,xF〉〉 (w16_S 〈n:〈x4,xE〉〉 (w16_S 〈n:〈x4,xD〉〉 (w16_S 〈n:〈x4,xC〉〉 (
+ w16_S 〈n:〈x4,xB〉〉 (w16_S 〈n:〈x4,xA〉〉 (w16_S 〈n:〈x4,x9〉〉 (w16_S 〈n:〈x4,x8〉〉 (
+ w16_S 〈n:〈x4,x7〉〉 (w16_S 〈n:〈x4,x6〉〉 (w16_S 〈n:〈x4,x5〉〉 (w16_S 〈n:〈x4,x4〉〉 (
+ w16_S 〈n:〈x4,x3〉〉 (w16_S 〈n:〈x4,x2〉〉 (w16_S 〈n:〈x4,x1〉〉 (w16_S 〈n:〈x4,x0〉〉 (w16_to_recw16_aux1_4 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_6 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x6,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x5,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_5 ? recw)
+ w16_S 〈n:〈x5,xF〉〉 (w16_S 〈n:〈x5,xE〉〉 (w16_S 〈n:〈x5,xD〉〉 (w16_S 〈n:〈x5,xC〉〉 (
+ w16_S 〈n:〈x5,xB〉〉 (w16_S 〈n:〈x5,xA〉〉 (w16_S 〈n:〈x5,x9〉〉 (w16_S 〈n:〈x5,x8〉〉 (
+ w16_S 〈n:〈x5,x7〉〉 (w16_S 〈n:〈x5,x6〉〉 (w16_S 〈n:〈x5,x5〉〉 (w16_S 〈n:〈x5,x4〉〉 (
+ w16_S 〈n:〈x5,x3〉〉 (w16_S 〈n:〈x5,x2〉〉 (w16_S 〈n:〈x5,x1〉〉 (w16_S 〈n:〈x5,x0〉〉 (w16_to_recw16_aux1_5 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_7 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x7,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x6,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_6 ? recw)
+ w16_S 〈n:〈x6,xF〉〉 (w16_S 〈n:〈x6,xE〉〉 (w16_S 〈n:〈x6,xD〉〉 (w16_S 〈n:〈x6,xC〉〉 (
+ w16_S 〈n:〈x6,xB〉〉 (w16_S 〈n:〈x6,xA〉〉 (w16_S 〈n:〈x6,x9〉〉 (w16_S 〈n:〈x6,x8〉〉 (
+ w16_S 〈n:〈x6,x7〉〉 (w16_S 〈n:〈x6,x6〉〉 (w16_S 〈n:〈x6,x5〉〉 (w16_S 〈n:〈x6,x4〉〉 (
+ w16_S 〈n:〈x6,x3〉〉 (w16_S 〈n:〈x6,x2〉〉 (w16_S 〈n:〈x6,x1〉〉 (w16_S 〈n:〈x6,x0〉〉 (w16_to_recw16_aux1_6 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_8 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x8,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x7,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_7 ? recw)
+ w16_S 〈n:〈x7,xF〉〉 (w16_S 〈n:〈x7,xE〉〉 (w16_S 〈n:〈x7,xD〉〉 (w16_S 〈n:〈x7,xC〉〉 (
+ w16_S 〈n:〈x7,xB〉〉 (w16_S 〈n:〈x7,xA〉〉 (w16_S 〈n:〈x7,x9〉〉 (w16_S 〈n:〈x7,x8〉〉 (
+ w16_S 〈n:〈x7,x7〉〉 (w16_S 〈n:〈x7,x6〉〉 (w16_S 〈n:〈x7,x5〉〉 (w16_S 〈n:〈x7,x4〉〉 (
+ w16_S 〈n:〈x7,x3〉〉 (w16_S 〈n:〈x7,x2〉〉 (w16_S 〈n:〈x7,x1〉〉 (w16_S 〈n:〈x7,x0〉〉 (w16_to_recw16_aux1_7 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_9 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x9,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x8,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_8 ? recw)
+ w16_S 〈n:〈x8,xF〉〉 (w16_S 〈n:〈x8,xE〉〉 (w16_S 〈n:〈x8,xD〉〉 (w16_S 〈n:〈x8,xC〉〉 (
+ w16_S 〈n:〈x8,xB〉〉 (w16_S 〈n:〈x8,xA〉〉 (w16_S 〈n:〈x8,x9〉〉 (w16_S 〈n:〈x8,x8〉〉 (
+ w16_S 〈n:〈x8,x7〉〉 (w16_S 〈n:〈x8,x6〉〉 (w16_S 〈n:〈x8,x5〉〉 (w16_S 〈n:〈x8,x4〉〉 (
+ w16_S 〈n:〈x8,x3〉〉 (w16_S 〈n:〈x8,x2〉〉 (w16_S 〈n:〈x8,x1〉〉 (w16_S 〈n:〈x8,x0〉〉 (w16_to_recw16_aux1_8 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_10 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xA,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈x9,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_9 ? recw)
+ w16_S 〈n:〈x9,xF〉〉 (w16_S 〈n:〈x9,xE〉〉 (w16_S 〈n:〈x9,xD〉〉 (w16_S 〈n:〈x9,xC〉〉 (
+ w16_S 〈n:〈x9,xB〉〉 (w16_S 〈n:〈x9,xA〉〉 (w16_S 〈n:〈x9,x9〉〉 (w16_S 〈n:〈x9,x8〉〉 (
+ w16_S 〈n:〈x9,x7〉〉 (w16_S 〈n:〈x9,x6〉〉 (w16_S 〈n:〈x9,x5〉〉 (w16_S 〈n:〈x9,x4〉〉 (
+ w16_S 〈n:〈x9,x3〉〉 (w16_S 〈n:〈x9,x2〉〉 (w16_S 〈n:〈x9,x1〉〉 (w16_S 〈n:〈x9,x0〉〉 (w16_to_recw16_aux1_9 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_11 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xB,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈xA,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_10 ? recw)
+ w16_S 〈n:〈xA,xF〉〉 (w16_S 〈n:〈xA,xE〉〉 (w16_S 〈n:〈xA,xD〉〉 (w16_S 〈n:〈xA,xC〉〉 (
+ w16_S 〈n:〈xA,xB〉〉 (w16_S 〈n:〈xA,xA〉〉 (w16_S 〈n:〈xA,x9〉〉 (w16_S 〈n:〈xA,x8〉〉 (
+ w16_S 〈n:〈xA,x7〉〉 (w16_S 〈n:〈xA,x6〉〉 (w16_S 〈n:〈xA,x5〉〉 (w16_S 〈n:〈xA,x4〉〉 (
+ w16_S 〈n:〈xA,x3〉〉 (w16_S 〈n:〈xA,x2〉〉 (w16_S 〈n:〈xA,x1〉〉 (w16_S 〈n:〈xA,x0〉〉 (w16_to_recw16_aux1_10 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_12 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xC,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈xB,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_11 ? recw)
+ w16_S 〈n:〈xB,xF〉〉 (w16_S 〈n:〈xB,xE〉〉 (w16_S 〈n:〈xB,xD〉〉 (w16_S 〈n:〈xB,xC〉〉 (
+ w16_S 〈n:〈xB,xB〉〉 (w16_S 〈n:〈xB,xA〉〉 (w16_S 〈n:〈xB,x9〉〉 (w16_S 〈n:〈xB,x8〉〉 (
+ w16_S 〈n:〈xB,x7〉〉 (w16_S 〈n:〈xB,x6〉〉 (w16_S 〈n:〈xB,x5〉〉 (w16_S 〈n:〈xB,x4〉〉 (
+ w16_S 〈n:〈xB,x3〉〉 (w16_S 〈n:〈xB,x2〉〉 (w16_S 〈n:〈xB,x1〉〉 (w16_S 〈n:〈xB,x0〉〉 (w16_to_recw16_aux1_11 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_13 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xD,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈xC,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_12 ? recw)
+ w16_S 〈n:〈xC,xF〉〉 (w16_S 〈n:〈xC,xE〉〉 (w16_S 〈n:〈xC,xD〉〉 (w16_S 〈n:〈xC,xC〉〉 (
+ w16_S 〈n:〈xC,xB〉〉 (w16_S 〈n:〈xC,xA〉〉 (w16_S 〈n:〈xC,x9〉〉 (w16_S 〈n:〈xC,x8〉〉 (
+ w16_S 〈n:〈xC,x7〉〉 (w16_S 〈n:〈xC,x6〉〉 (w16_S 〈n:〈xC,x5〉〉 (w16_S 〈n:〈xC,x4〉〉 (
+ w16_S 〈n:〈xC,x3〉〉 (w16_S 〈n:〈xC,x2〉〉 (w16_S 〈n:〈xC,x1〉〉 (w16_S 〈n:〈xC,x0〉〉 (w16_to_recw16_aux1_12 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_14 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xE,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈xD,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_13 ? recw)
+ w16_S 〈n:〈xD,xF〉〉 (w16_S 〈n:〈xD,xE〉〉 (w16_S 〈n:〈xD,xD〉〉 (w16_S 〈n:〈xD,xC〉〉 (
+ w16_S 〈n:〈xD,xB〉〉 (w16_S 〈n:〈xD,xA〉〉 (w16_S 〈n:〈xD,x9〉〉 (w16_S 〈n:〈xD,x8〉〉 (
+ w16_S 〈n:〈xD,x7〉〉 (w16_S 〈n:〈xD,x6〉〉 (w16_S 〈n:〈xD,x5〉〉 (w16_S 〈n:〈xD,x4〉〉 (
+ w16_S 〈n:〈xD,x3〉〉 (w16_S 〈n:〈xD,x2〉〉 (w16_S 〈n:〈xD,x1〉〉 (w16_S 〈n:〈xD,x0〉〉 (w16_to_recw16_aux1_13 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1_15 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xF,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈xE,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_14 ? recw)
+ w16_S 〈n:〈xE,xF〉〉 (w16_S 〈n:〈xE,xE〉〉 (w16_S 〈n:〈xE,xD〉〉 (w16_S 〈n:〈xE,xC〉〉 (
+ w16_S 〈n:〈xE,xB〉〉 (w16_S 〈n:〈xE,xA〉〉 (w16_S 〈n:〈xE,x9〉〉 (w16_S 〈n:〈xE,x8〉〉 (
+ w16_S 〈n:〈xE,x7〉〉 (w16_S 〈n:〈xE,x6〉〉 (w16_S 〈n:〈xE,x5〉〉 (w16_S 〈n:〈xE,x4〉〉 (
+ w16_S 〈n:〈xE,x3〉〉 (w16_S 〈n:〈xE,x2〉〉 (w16_S 〈n:〈xE,x1〉〉 (w16_S 〈n:〈xE,x0〉〉 (w16_to_recw16_aux1_14 ? recw)
))))))))))))))).
ndefinition w16_to_recw16_aux1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈(succ_b8 n):〈x0,x0〉〉 ≝
λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S 〈n:〈xF,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_15 ? recw)
+ w16_S 〈n:〈xF,xF〉〉 (w16_S 〈n:〈xF,xE〉〉 (w16_S 〈n:〈xF,xD〉〉 (w16_S 〈n:〈xF,xC〉〉 (
+ w16_S 〈n:〈xF,xB〉〉 (w16_S 〈n:〈xF,xA〉〉 (w16_S 〈n:〈xF,x9〉〉 (w16_S 〈n:〈xF,x8〉〉 (
+ w16_S 〈n:〈xF,x7〉〉 (w16_S 〈n:〈xF,x6〉〉 (w16_S 〈n:〈xF,x5〉〉 (w16_S 〈n:〈xF,x4〉〉 (
+ w16_S 〈n:〈xF,x3〉〉 (w16_S 〈n:〈xF,x2〉〉 (w16_S 〈n:〈xF,x1〉〉 (w16_S 〈n:〈xF,x0〉〉 (w16_to_recw16_aux1_15 ? recw)
))))))))))))))).
(* ... cifra byte superiore *)
| xF ⇒ w16_to_recw16_aux1_15 ? recw
].
-nlemma w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉.
- #n; #e; nelim e;
- #input; napply (w16_S ? input).
-nqed.
-
-nlemma w16_to_recw16_aux4_2 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x2〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_1 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_3 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x3〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_2 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_4 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x4〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_3 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_5 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x5〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_4 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_6 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x6〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_5 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_7 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x7〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_6 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_8 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x8〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_7 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_9 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x9〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_8 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_10 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xA〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_9 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_11 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xB〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_10 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_12 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xC〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_11 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_13 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xD〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_12 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_14 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xE〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_13 … input)).
-nqed.
-
-nlemma w16_to_recw16_aux4_15 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xF〉〉.
- #n; #e; #H;
- nelim e in H:(%) ⊢ %;
- #input; napply (w16_S ? (w16_to_recw16_aux4_14 … input)).
-nqed.
+ndefinition w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x1〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? recw
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? recw
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? recw
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? recw
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? recw
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? recw
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? recw
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? recw
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? recw
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? recw
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? recw
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? recw
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? recw
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? recw
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? recw
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? recw
+ ].
+
+ndefinition w16_to_recw16_aux4_2 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x2〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x2〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_1 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_3 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x3〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x3〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_2 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_4 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x4〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x4〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_3 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_5 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x5〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x5〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_4 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_6 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x6〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x6〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_5 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_7 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x7〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x7〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_6 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_8 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x8〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x8〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_7 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_9 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x9〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,x9〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_8 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_10 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xA〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xA〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_9 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_11 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xB〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xB〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_10 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_12 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xC〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xC〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_11 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_13 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xD〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xD〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_12 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_14 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xE〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xE〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_13 … recw)
+ ].
+
+ndefinition w16_to_recw16_aux4_15 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xF〉〉 ≝
+λn,e.
+ match e return λx.rec_word16 〈n:〈x,x0〉〉 → rec_word16 〈n:〈x,xF〉〉 with
+ [ x0 ⇒ λrecw:rec_word16 〈n:〈x0,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x1 ⇒ λrecw:rec_word16 〈n:〈x1,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x2 ⇒ λrecw:rec_word16 〈n:〈x2,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x3 ⇒ λrecw:rec_word16 〈n:〈x3,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x4 ⇒ λrecw:rec_word16 〈n:〈x4,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x5 ⇒ λrecw:rec_word16 〈n:〈x5,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x6 ⇒ λrecw:rec_word16 〈n:〈x6,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x7 ⇒ λrecw:rec_word16 〈n:〈x7,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x8 ⇒ λrecw:rec_word16 〈n:〈x8,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | x9 ⇒ λrecw:rec_word16 〈n:〈x9,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | xA ⇒ λrecw:rec_word16 〈n:〈xA,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | xB ⇒ λrecw:rec_word16 〈n:〈xB,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | xC ⇒ λrecw:rec_word16 〈n:〈xC,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | xD ⇒ λrecw:rec_word16 〈n:〈xD,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | xE ⇒ λrecw:rec_word16 〈n:〈xE,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ | xF ⇒ λrecw:rec_word16 〈n:〈xF,x0〉〉.w16_S ? (w16_to_recw16_aux4_14 … recw)
+ ].
(* ... cifra esadecimale n.1 *)
ndefinition w16_to_recw16_aux4 ≝
| xF ⇒ w16_to_recw16_aux4_15 … recw
].
-ndefinition w16_to_recw16 : Πw.rec_word16 w.
- #w;
- nletin K ≝ (w16_to_recw16_aux4 (w16h w) (b8h (w16l w)) (b8l (w16l w))
- (w16_to_recw16_aux3 (w16h w) (b8h (w16l w)) (w16_to_recw16_aux2 (w16h w) (b8_to_recb8 (w16h w)))));
- nelim w in K:(%) ⊢ %;
- #b1; #b2;
- nelim b2;
- #e1; #e2; nnormalize; #H; napply H.
-nqed.
+ndefinition w16_to_recw16 : Πw.rec_word16 w ≝
+λw.
+ match w with [ mk_word16 h l ⇒
+ match l with [ mk_byte8 lh ll ⇒
+ w16_to_recw16_aux4 h lh ll (w16_to_recw16_aux3 h lh (w16_to_recw16_aux2 h (b8_to_recb8 h))) ]].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "universe/universe.ma".
-
-ndefinition ASCII_UN ≝ [ uch_0; uch_1; uch_2; uch_3; uch_4; uch_5; uch_6; uch_7; uch_8; uch_9;
- uch__; uch_A; uch_B; uch_C; uch_D; uch_E; uch_F; uch_G; uch_H; uch_I;
- uch_J; uch_K; uch_L; uch_M; uch_N; uch_O; uch_P; uch_Q; uch_R; uch_S;
- uch_T; uch_U; uch_V; uch_W; uch_X; uch_Y; uch_Z; uch_a; uch_b; uch_c;
- uch_d; uch_e; uch_f; uch_g; uch_h; uch_i; uch_j; uch_k; uch_l; uch_m;
- uch_n; uch_o; uch_p; uch_q; uch_r; uch_s; uch_t; uch_u; uch_v; uch_w;
- uch_x; uch_y; uch_z ].
-
-(* derivati dall'universo
- 1) SUN_destruct ASCII_UN
- 2) eq_to_eqSUN ASCII_UN
- 3) neq_to_neqSUN ASCII_UN
- 4) eqSUN_to_eq ASCII_UN
- 5) neqSUN_to_neq ASCII_UN
- 6) decidable_SUN ASCII_UN
- 7) symmetric_eqSUN ASCII_UN
-*)
-
-nlemma un_ch_0 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_0 (refl_eq …) ?); #y; nelim y; ##[ ##61: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_1 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_1 (refl_eq …) ?); #y; nelim y; ##[ ##62: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_2 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_2 (refl_eq …) ?); #y; nelim y; ##[ ##63: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_3 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_3 (refl_eq …) ?); #y; nelim y; ##[ ##64: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_4 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_4 (refl_eq …) ?); #y; nelim y; ##[ ##65: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_5 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_5 (refl_eq …) ?); #y; nelim y; ##[ ##66: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_6 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_6 (refl_eq …) ?); #y; nelim y; ##[ ##67: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_7 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_7 (refl_eq …) ?); #y; nelim y; ##[ ##68: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_8 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_8 (refl_eq …) ?); #y; nelim y; ##[ ##69: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_9 : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_9 (refl_eq …) ?); #y; nelim y; ##[ ##70: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch__ : S_UN ASCII_UN. napply (S_EL ASCII_UN uch__ (refl_eq …) ?); #y; nelim y; ##[ ##71: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_A : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_A (refl_eq …) ?); #y; nelim y; ##[ ##72: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_B : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_B (refl_eq …) ?); #y; nelim y; ##[ ##73: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_C : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_C (refl_eq …) ?); #y; nelim y; ##[ ##74: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_D : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_D (refl_eq …) ?); #y; nelim y; ##[ ##75: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_E : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_E (refl_eq …) ?); #y; nelim y; ##[ ##76: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_F : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_F (refl_eq …) ?); #y; nelim y; ##[ ##77: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_G : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_G (refl_eq …) ?); #y; nelim y; ##[ ##78: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_H : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_H (refl_eq …) ?); #y; nelim y; ##[ ##79: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_I : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_I (refl_eq …) ?); #y; nelim y; ##[ ##80: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_J : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_J (refl_eq …) ?); #y; nelim y; ##[ ##81: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_K : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_K (refl_eq …) ?); #y; nelim y; ##[ ##82: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_L : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_L (refl_eq …) ?); #y; nelim y; ##[ ##83: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_M : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_M (refl_eq …) ?); #y; nelim y; ##[ ##84: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_N : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_N (refl_eq …) ?); #y; nelim y; ##[ ##85: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_O : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_O (refl_eq …) ?); #y; nelim y; ##[ ##86: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_P : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_P (refl_eq …) ?); #y; nelim y; ##[ ##87: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_Q : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_Q (refl_eq …) ?); #y; nelim y; ##[ ##88: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_R : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_R (refl_eq …) ?); #y; nelim y; ##[ ##89: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_S : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_S (refl_eq …) ?); #y; nelim y; ##[ ##90: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_T : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_T (refl_eq …) ?); #y; nelim y; ##[ ##91: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_U : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_U (refl_eq …) ?); #y; nelim y; ##[ ##92: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_V : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_V (refl_eq …) ?); #y; nelim y; ##[ ##93: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_W : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_W (refl_eq …) ?); #y; nelim y; ##[ ##94: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_X : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_X (refl_eq …) ?); #y; nelim y; ##[ ##95: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_Y : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_Y (refl_eq …) ?); #y; nelim y; ##[ ##96: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_Z : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_Z (refl_eq …) ?); #y; nelim y; ##[ ##97: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_a : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_a (refl_eq …) ?); #y; nelim y; ##[ ##98: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_b : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_b (refl_eq …) ?); #y; nelim y; ##[ ##99: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_c : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_c (refl_eq …) ?); #y; nelim y; ##[ ##100: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_d : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_d (refl_eq …) ?); #y; nelim y; ##[ ##101: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_e : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_e (refl_eq …) ?); #y; nelim y; ##[ ##102: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_f : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_f (refl_eq …) ?); #y; nelim y; ##[ ##103: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_g : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_g (refl_eq …) ?); #y; nelim y; ##[ ##104: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_h : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_h (refl_eq …) ?); #y; nelim y; ##[ ##105: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_i : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_i (refl_eq …) ?); #y; nelim y; ##[ ##106: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_j : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_j (refl_eq …) ?); #y; nelim y; ##[ ##107: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_k : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_k (refl_eq …) ?); #y; nelim y; ##[ ##108: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_l : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_l (refl_eq …) ?); #y; nelim y; ##[ ##109: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_m : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_m (refl_eq …) ?); #y; nelim y; ##[ ##110: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_n : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_n (refl_eq …) ?); #y; nelim y; ##[ ##111: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_o : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_o (refl_eq …) ?); #y; nelim y; ##[ ##112: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_p : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_p (refl_eq …) ?); #y; nelim y; ##[ ##113: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_q : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_q (refl_eq …) ?); #y; nelim y; ##[ ##114: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_r : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_r (refl_eq …) ?); #y; nelim y; ##[ ##115: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_s : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_s (refl_eq …) ?); #y; nelim y; ##[ ##116: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_t : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_t (refl_eq …) ?); #y; nelim y; ##[ ##117: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_u : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_u (refl_eq …) ?); #y; nelim y; ##[ ##118: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_v : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_v (refl_eq …) ?); #y; nelim y; ##[ ##119: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_w : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_w (refl_eq …) ?); #y; nelim y; ##[ ##120: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_x : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_x (refl_eq …) ?); #y; nelim y; ##[ ##121: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_y : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_y (refl_eq …) ?); #y; nelim y; ##[ ##122: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ch_z : S_UN ASCII_UN. napply (S_EL ASCII_UN uch_z (refl_eq …) ?); #y; nelim y; ##[ ##123: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "universe/universe.ma".
-
-ndefinition BIT_UN ≝ [ ut00; ut01; ut02; ut03; ut04; ut05; ut06; ut07; ut08; ut09; ut0A; ut0B; ut0C; ut0D; ut0E; ut0F;
- ut10; ut11; ut12; ut13; ut14; ut15; ut16; ut17; ut18; ut19; ut1A; ut1B; ut1C; ut1D; ut1E; ut1F ].
-
-(* derivati dall'universo
- 1) SUN_destruct BIT_UN
- 2) eq_to_eqSUN BIT_UN
- 3) neq_to_neqSUN BIT_UN
- 4) eqSUN_to_eq BIT_UN
- 5) neqSUN_to_neq BIT_UN
- 6) decidable_SUN BIT_UN
- 7) symmetric_eqSUN BIT_UN
-*)
-
-nlemma un_t00 : S_UN BIT_UN. napply (S_EL BIT_UN ut00 (refl_eq …) ?); #y; nelim y; ##[ ##29: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t01 : S_UN BIT_UN. napply (S_EL BIT_UN ut01 (refl_eq …) ?); #y; nelim y; ##[ ##30: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t02 : S_UN BIT_UN. napply (S_EL BIT_UN ut02 (refl_eq …) ?); #y; nelim y; ##[ ##31: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t03 : S_UN BIT_UN. napply (S_EL BIT_UN ut03 (refl_eq …) ?); #y; nelim y; ##[ ##32: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t04 : S_UN BIT_UN. napply (S_EL BIT_UN ut04 (refl_eq …) ?); #y; nelim y; ##[ ##33: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t05 : S_UN BIT_UN. napply (S_EL BIT_UN ut05 (refl_eq …) ?); #y; nelim y; ##[ ##34: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t06 : S_UN BIT_UN. napply (S_EL BIT_UN ut06 (refl_eq …) ?); #y; nelim y; ##[ ##35: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t07 : S_UN BIT_UN. napply (S_EL BIT_UN ut07 (refl_eq …) ?); #y; nelim y; ##[ ##36: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t08 : S_UN BIT_UN. napply (S_EL BIT_UN ut08 (refl_eq …) ?); #y; nelim y; ##[ ##37: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t09 : S_UN BIT_UN. napply (S_EL BIT_UN ut09 (refl_eq …) ?); #y; nelim y; ##[ ##38: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t0A : S_UN BIT_UN. napply (S_EL BIT_UN ut0A (refl_eq …) ?); #y; nelim y; ##[ ##39: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t0B : S_UN BIT_UN. napply (S_EL BIT_UN ut0B (refl_eq …) ?); #y; nelim y; ##[ ##40: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t0C : S_UN BIT_UN. napply (S_EL BIT_UN ut0C (refl_eq …) ?); #y; nelim y; ##[ ##41: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t0D : S_UN BIT_UN. napply (S_EL BIT_UN ut0D (refl_eq …) ?); #y; nelim y; ##[ ##42: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t0E : S_UN BIT_UN. napply (S_EL BIT_UN ut0E (refl_eq …) ?); #y; nelim y; ##[ ##43: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t0F : S_UN BIT_UN. napply (S_EL BIT_UN ut0F (refl_eq …) ?); #y; nelim y; ##[ ##44: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t10 : S_UN BIT_UN. napply (S_EL BIT_UN ut10 (refl_eq …) ?); #y; nelim y; ##[ ##45: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t11 : S_UN BIT_UN. napply (S_EL BIT_UN ut11 (refl_eq …) ?); #y; nelim y; ##[ ##46: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t12 : S_UN BIT_UN. napply (S_EL BIT_UN ut12 (refl_eq …) ?); #y; nelim y; ##[ ##47: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t13 : S_UN BIT_UN. napply (S_EL BIT_UN ut13 (refl_eq …) ?); #y; nelim y; ##[ ##48: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t14 : S_UN BIT_UN. napply (S_EL BIT_UN ut14 (refl_eq …) ?); #y; nelim y; ##[ ##49: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t15 : S_UN BIT_UN. napply (S_EL BIT_UN ut15 (refl_eq …) ?); #y; nelim y; ##[ ##50: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t16 : S_UN BIT_UN. napply (S_EL BIT_UN ut16 (refl_eq …) ?); #y; nelim y; ##[ ##51: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t17 : S_UN BIT_UN. napply (S_EL BIT_UN ut17 (refl_eq …) ?); #y; nelim y; ##[ ##52: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t18 : S_UN BIT_UN. napply (S_EL BIT_UN ut18 (refl_eq …) ?); #y; nelim y; ##[ ##53: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t19 : S_UN BIT_UN. napply (S_EL BIT_UN ut19 (refl_eq …) ?); #y; nelim y; ##[ ##54: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t1A : S_UN BIT_UN. napply (S_EL BIT_UN ut1A (refl_eq …) ?); #y; nelim y; ##[ ##55: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t1B : S_UN BIT_UN. napply (S_EL BIT_UN ut1B (refl_eq …) ?); #y; nelim y; ##[ ##56: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t1C : S_UN BIT_UN. napply (S_EL BIT_UN ut1C (refl_eq …) ?); #y; nelim y; ##[ ##57: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t1D : S_UN BIT_UN. napply (S_EL BIT_UN ut1D (refl_eq …) ?); #y; nelim y; ##[ ##58: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t1E : S_UN BIT_UN. napply (S_EL BIT_UN ut1E (refl_eq …) ?); #y; nelim y; ##[ ##59: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_t1F : S_UN BIT_UN. napply (S_EL BIT_UN ut1F (refl_eq …) ?); #y; nelim y; ##[ ##60: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "universe/universe.ma".
-
-ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
-
-(* derivati dall'universo
- 1) SUN_destruct EX_UN
- 2) eq_to_eqSUN EX_UN
- 3) neq_to_neqSUN EX_UN
- 4) eqSUN_to_eq EX_UN
- 5) neqSUN_to_neq EX_UN
- 6) decidable_SUN EX_UN
- 7) symmetric_eqSUN EX_UN
-*)
-
-nlemma un_x0 : S_UN EX_UN. napply (S_EL EX_UN ux0 (refl_eq …) ?); #y; nelim y; ##[ ##13: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x1 : S_UN EX_UN. napply (S_EL EX_UN ux1 (refl_eq …) ?); #y; nelim y; ##[ ##14: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x2 : S_UN EX_UN. napply (S_EL EX_UN ux2 (refl_eq …) ?); #y; nelim y; ##[ ##15: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x3 : S_UN EX_UN. napply (S_EL EX_UN ux3 (refl_eq …) ?); #y; nelim y; ##[ ##16: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x4 : S_UN EX_UN. napply (S_EL EX_UN ux4 (refl_eq …) ?); #y; nelim y; ##[ ##17: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x5 : S_UN EX_UN. napply (S_EL EX_UN ux5 (refl_eq …) ?); #y; nelim y; ##[ ##18: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x6 : S_UN EX_UN. napply (S_EL EX_UN ux6 (refl_eq …) ?); #y; nelim y; ##[ ##19: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x7 : S_UN EX_UN. napply (S_EL EX_UN ux7 (refl_eq …) ?); #y; nelim y; ##[ ##20: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x8 : S_UN EX_UN. napply (S_EL EX_UN ux8 (refl_eq …) ?); #y; nelim y; ##[ ##21: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_x9 : S_UN EX_UN. napply (S_EL EX_UN ux9 (refl_eq …) ?); #y; nelim y; ##[ ##22: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_xA : S_UN EX_UN. napply (S_EL EX_UN uxA (refl_eq …) ?); #y; nelim y; ##[ ##23: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_xB : S_UN EX_UN. napply (S_EL EX_UN uxB (refl_eq …) ?); #y; nelim y; ##[ ##24: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_xC : S_UN EX_UN. napply (S_EL EX_UN uxC (refl_eq …) ?); #y; nelim y; ##[ ##25: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_xD : S_UN EX_UN. napply (S_EL EX_UN uxD (refl_eq …) ?); #y; nelim y; ##[ ##26: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_xE : S_UN EX_UN. napply (S_EL EX_UN uxE (refl_eq …) ?); #y; nelim y; ##[ ##27: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_xF : S_UN EX_UN. napply (S_EL EX_UN uxF (refl_eq …) ?); #y; nelim y; ##[ ##28: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "universe/exadecim.ma".
-
-(* operazioni su EX_UN *)
-
-(* scheletro di funzione a 1 argomento *)
-ndefinition farg1_unex ≝
-λT:Type.λf1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:T.λe2:S_UN EX_UN.
- match getelem ? e2 return λx.member_list ? x eq_UN EX_UN = true → T with
- [ ux0 ⇒ λq:(true = true).f1 | ux1 ⇒ λq:(true = true).f2
- | ux2 ⇒ λq:(true = true).f3 | ux3 ⇒ λq:(true = true).f4
- | ux4 ⇒ λq:(true = true).f5 | ux5 ⇒ λq:(true = true).f6
- | ux6 ⇒ λq:(true = true).f7 | ux7 ⇒ λq:(true = true).f8
- | ux8 ⇒ λq:(true = true).f9 | ux9 ⇒ λq:(true = true).f10
- | uxA ⇒ λq:(true = true).f11 | uxB ⇒ λq:(true = true).f12
- | uxC ⇒ λq:(true = true).f13 | uxD ⇒ λq:(true = true).f14
- | uxE ⇒ λq:(true = true).f15 | uxF ⇒ λq:(true = true).f16
- | _ ⇒ λq:(false = true).False_rect_Type0 ? (bool_destruct … q)
- ] (getdim1 ? e2).
-
-(* scheletro di funzione a 2 argomenti *)
-ndefinition farg2_unex ≝
-λT:Type.λf1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN → T.λe1:S_UN EX_UN.
- match getelem ? e1 return λx.member_list ? x eq_UN EX_UN = true → S_UN EX_UN → T with
- [ ux0 ⇒ λp:(true = true).f1
- | ux1 ⇒ λp:(true = true).f2
- | ux2 ⇒ λp:(true = true).f3
- | ux3 ⇒ λp:(true = true).f4
- | ux4 ⇒ λp:(true = true).f5
- | ux5 ⇒ λp:(true = true).f6
- | ux6 ⇒ λp:(true = true).f7
- | ux7 ⇒ λp:(true = true).f8
- | ux8 ⇒ λp:(true = true).f9
- | ux9 ⇒ λp:(true = true).f10
- | uxA ⇒ λp:(true = true).f11
- | uxB ⇒ λp:(true = true).f12
- | uxC ⇒ λp:(true = true).f13
- | uxD ⇒ λp:(true = true).f14
- | uxE ⇒ λp:(true = true).f15
- | uxF ⇒ λp:(true = true).f16
- | _ ⇒ λp:(false = true).False_rect_Type0 ? (bool_destruct … p)
- ] (getdim1 ? e1).
-
-(* scheletro di funzione a 2 argomenti simmetrica *)
-ndefinition farg2sym_unex ≝
-λT:Type.
-λf00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
-λf11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
-λf22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
-λf33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
-λf44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
-λf55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
-λf66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
-λf77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
-λf88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
-λf99,f9A,f9B,f9C,f9D,f9E,f9F:T.
-λfAA,fAB,fAC,fAD,fAE,fAF:T.
-λfBB,fBC,fBD,fBE,fBF:T.
-λfCC,fCD,fCE,fCF:T.
-λfDD,fDE,fDF:T.
-λfEE,fEF:T.
-λfFF:T.
- farg2_unex ?
- (farg1_unex ? f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F)
- (farg1_unex ? f01 f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F)
- (farg1_unex ? f02 f12 f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F)
- (farg1_unex ? f03 f13 f23 f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F)
- (farg1_unex ? f04 f14 f24 f34 f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F)
- (farg1_unex ? f05 f15 f25 f35 f45 f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F)
- (farg1_unex ? f06 f16 f26 f36 f46 f56 f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F)
- (farg1_unex ? f07 f17 f27 f37 f47 f57 f67 f77 f78 f79 f7A f7B f7C f7D f7E f7F)
- (farg1_unex ? f08 f18 f28 f38 f48 f58 f68 f78 f88 f89 f8A f8B f8C f8D f8E f8F)
- (farg1_unex ? f09 f19 f29 f39 f49 f59 f69 f79 f89 f99 f9A f9B f9C f9D f9E f9F)
- (farg1_unex ? f0A f1A f2A f3A f4A f5A f6A f7A f8A f9A fAA fAB fAC fAD fAE fAF)
- (farg1_unex ? f0B f1B f2B f3B f4B f5B f6B f7B f8B f9B fAB fBB fBC fBD fBE fBF)
- (farg1_unex ? f0C f1C f2C f3C f4C f5C f6C f7C f8C f9C fAC fBC fCC fCD fCE fCF)
- (farg1_unex ? f0D f1D f2D f3D f4D f5D f6D f7D f8D f9D fAD fBD fCD fDD fDE fDF)
- (farg1_unex ? f0E f1E f2E f3E f4E f5E f6E f7E f8E f9E fAE fBE fCE fDE fEE fEF)
- (farg1_unex ? f0F f1F f2F f3F f4F f5F f6F f7F f8F f9F fAF fBF fCF fDF fEF fFF).
-
-(* operatore = *)
-ndefinition eq_unex ≝ λe1,e2:S_UN EX_UN.eq_SUN ? e1 e2.
-
-(* operatore < *)
-ndefinition lt_unex ≝
- farg2_unex ?
- (farg1_unex ? false true true true true true true true true true true true true true true true)
- (farg1_unex ? false false true true true true true true true true true true true true true true)
- (farg1_unex ? false false false true true true true true true true true true true true true true)
- (farg1_unex ? false false false false true true true true true true true true true true true true)
- (farg1_unex ? false false false false false true true true true true true true true true true true)
- (farg1_unex ? false false false false false false true true true true true true true true true true)
- (farg1_unex ? false false false false false false false true true true true true true true true true)
- (farg1_unex ? false false false false false false false false true true true true true true true true)
- (farg1_unex ? false false false false false false false false false true true true true true true true)
- (farg1_unex ? false false false false false false false false false false true true true true true true)
- (farg1_unex ? false false false false false false false false false false false true true true true true)
- (farg1_unex ? false false false false false false false false false false false false true true true true)
- (farg1_unex ? false false false false false false false false false false false false false true true true)
- (farg1_unex ? false false false false false false false false false false false false false false true true)
- (farg1_unex ? false false false false false false false false false false false false false false false true)
- (farg1_unex ? false false false false false false false false false false false false false false false false).
-
-(* operatore ≤ *)
-ndefinition le_unex ≝
- farg2_unex ?
- (farg1_unex ? true true true true true true true true true true true true true true true true)
- (farg1_unex ? false true true true true true true true true true true true true true true true)
- (farg1_unex ? false false true true true true true true true true true true true true true true)
- (farg1_unex ? false false false true true true true true true true true true true true true true)
- (farg1_unex ? false false false false true true true true true true true true true true true true)
- (farg1_unex ? false false false false false true true true true true true true true true true true)
- (farg1_unex ? false false false false false false true true true true true true true true true true)
- (farg1_unex ? false false false false false false false true true true true true true true true true)
- (farg1_unex ? false false false false false false false false true true true true true true true true)
- (farg1_unex ? false false false false false false false false false true true true true true true true)
- (farg1_unex ? false false false false false false false false false false true true true true true true)
- (farg1_unex ? false false false false false false false false false false false true true true true true)
- (farg1_unex ? false false false false false false false false false false false false true true true true)
- (farg1_unex ? false false false false false false false false false false false false false true true true)
- (farg1_unex ? false false false false false false false false false false false false false false true true)
- (farg1_unex ? false false false false false false false false false false false false false false false true).
-
-(* operatore > *)
-ndefinition gt_unex ≝ λe1,e2:S_UN EX_UN.⊖(le_unex e1 e2).
-
-(* operatore ≥ *)
-ndefinition ge_unex ≝ λe1,e2:S_UN EX_UN.⊖(lt_unex e1 e2).
-
-(* opeartore and : simmetrico per costruzione *)
-ndefinition and_unex ≝
- farg2sym_unex ?
- un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0 un_x0
- un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1 un_x0 un_x1
- un_x2 un_x2 un_x0 un_x0 un_x2 un_x2 un_x0 un_x0 un_x2 un_x2 un_x0 un_x0 un_x2 un_x2
- un_x3 un_x0 un_x1 un_x2 un_x3 un_x0 un_x1 un_x2 un_x3 un_x0 un_x1 un_x2 un_x3
- un_x4 un_x4 un_x4 un_x4 un_x0 un_x0 un_x0 un_x0 un_x4 un_x4 un_x4 un_x4
- un_x5 un_x4 un_x5 un_x0 un_x1 un_x0 un_x1 un_x4 un_x5 un_x4 un_x5
- un_x6 un_x6 un_x0 un_x0 un_x2 un_x2 un_x4 un_x4 un_x6 un_x6
- un_x7 un_x0 un_x1 un_x2 un_x3 un_x4 un_x5 un_x6 un_x7
- un_x8 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8 un_x8
- un_x9 un_x8 un_x9 un_x8 un_x9 un_x8 un_x9
- un_xA un_xA un_x8 un_x8 un_xA un_xA
- un_xB un_x8 un_x9 un_xA un_xB
- un_xC un_xC un_xC un_xC
- un_xD un_xC un_xD
- un_xE un_xE
- un_xF.
-
-(*
- esiste una regola semplice per ottenere associativo per costruzione?
- ragionando in matrice simmetrico e' : a(i,j) = a(j,i) → A = trasposta(A)
- ragionando in matrice associativo e' : a(a(i,j),k) = a(i,a(j,k)) → come espresso?
-
-nlemma pippo : un_x3 = (and_unex un_x3 un_xF).
- nnormalize;
- perche' non riduce?
-
-nlemma symmetric_farg2unex1 :
- ∀T:Type.
- ∀f00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
- ∀f11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
- ∀f22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
- ∀f33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
- ∀f44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
- ∀f55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
- ∀f66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
- ∀f77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
- ∀f88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
- ∀f99,f9A,f9B,f9C,f9D,f9E,f9F:T.
- ∀fAA,fAB,fAC,fAD,fAE,fAF:T.
- ∀fBB,fBC,fBD,fBE,fBF:T.
- ∀fCC,fCD,fCE,fCF:T.
- ∀fDD,fDE,fDF:T.
- ∀fEE,fEF:T.
- ∀fFF:T.
- ∀dim1.∀dim2.∀y:S_UN EX_UN.
- (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
- f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
- f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
- f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
- f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
- f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
- f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
- f77 f78 f79 f7A f7B f7C f7D f7E f7F
- f88 f89 f8A f8B f8C f8D f8E f8F
- f99 f9A f9B f9C f9D f9E f9F
- fAA fAB fAC fAD fAE fAF
- fBB fBC fBD fBE fBF
- fCC fCD fCE fCF
- fDD fDE fDF
- fEE fEF
- fFF
- (S_EL EX_UN ux0 dim1 dim2) y) =
- (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
- f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
- f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
- f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
- f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
- f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
- f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
- f77 f78 f79 f7A f7B f7C f7D f7E f7F
- f88 f89 f8A f8B f8C f8D f8E f8F
- f99 f9A f9B f9C f9D f9E f9F
- fAA fAB fAC fAD fAE fAF
- fBB fBC fBD fBE fBF
- fCC fCD fCE fCF
- fDD fDE fDF
- fEE fEF
- fFF
- y (S_EL EX_UN ux0 dim1 dim2)).
- #T;
- #f00; #f01; #f02; #f03; #f04; #f05; #f06; #f07; #f08; #f09; #f0A; #f0B; #f0C; #f0D; #f0E; #f0F;
- #f11; #f12; #f13; #f14; #f15; #f16; #f17; #f18; #f19; #f1A; #f1B; #f1C; #f1D; #f1E; #f1F;
- #f22; #f23; #f24; #f25; #f26; #f27; #f28; #f29; #f2A; #f2B; #f2C; #f2D; #f2E; #f2F;
- #f33; #f34; #f35; #f36; #f37; #f38; #f39; #f3A; #f3B; #f3C; #f3D; #f3E; #f3F;
- #f44; #f45; #f46; #f47; #f48; #f49; #f4A; #f4B; #f4C; #f4D; #f4E; #f4F;
- #f55; #f56; #f57; #f58; #f59; #f5A; #f5B; #f5C; #f5D; #f5E; #f5F;
- #f66; #f67; #f68; #f69; #f6A; #f6B; #f6C; #f6D; #f6E; #f6F;
- #f77; #f78; #f79; #f7A; #f7B; #f7C; #f7D; #f7E; #f7F;
- #f88; #f89; #f8A; #f8B; #f8C; #f8D; #f8E; #f8F;
- #f99; #f9A; #f9B; #f9C; #f9D; #f9E; #f9F;
- #fAA; #fAB; #fAC; #fAD; #fAE; #fAF;
- #fBB; #fBC; #fBD; #fBE; #fBF;
- #fCC; #fCD; #fCE; #fCF;
- #fDD; #fDE; #fDF;
- #fEE; #fEF;
- #fFF;
- #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u; ncases u;
- ##[ ##13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: #dim21; #dim22; nnormalize; napply refl_eq
- ##| ##*: #dim21; nnormalize in dim21:(%); napply (bool_destruct … dim21)
- ##]
- ##]
-nqed.
-
-... e cosi via fino a
-
-nlemma symmetric_farg2unex :
- ∀T:Type.
- ∀f00,f01,f02,f03,f04,f05,f06,f07,f08,f09,f0A,f0B,f0C,f0D,f0E,f0F:T.
- ∀f11,f12,f13,f14,f15,f16,f17,f18,f19,f1A,f1B,f1C,f1D,f1E,f1F:T.
- ∀f22,f23,f24,f25,f26,f27,f28,f29,f2A,f2B,f2C,f2D,f2E,f2F:T.
- ∀f33,f34,f35,f36,f37,f38,f39,f3A,f3B,f3C,f3D,f3E,f3F:T.
- ∀f44,f45,f46,f47,f48,f49,f4A,f4B,f4C,f4D,f4E,f4F:T.
- ∀f55,f56,f57,f58,f59,f5A,f5B,f5C,f5D,f5E,f5F:T.
- ∀f66,f67,f68,f69,f6A,f6B,f6C,f6D,f6E,f6F:T.
- ∀f77,f78,f79,f7A,f7B,f7C,f7D,f7E,f7F:T.
- ∀f88,f89,f8A,f8B,f8C,f8D,f8E,f8F:T.
- ∀f99,f9A,f9B,f9C,f9D,f9E,f9F:T.
- ∀fAA,fAB,fAC,fAD,fAE,fAF:T.
- ∀fBB,fBC,fBD,fBE,fBF:T.
- ∀fCC,fCD,fCE,fCF:T.
- ∀fDD,fDE,fDF:T.
- ∀fEE,fEF:T.
- ∀fFF:T.
- ∀x,y:S_UN EX_UN.
- (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
- f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
- f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
- f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
- f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
- f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
- f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
- f77 f78 f79 f7A f7B f7C f7D f7E f7F
- f88 f89 f8A f8B f8C f8D f8E f8F
- f99 f9A f9B f9C f9D f9E f9F
- fAA fAB fAC fAD fAE fAF
- fBB fBC fBD fBE fBF
- fCC fCD fCE fCF
- fDD fDE fDF
- fEE fEF
- fFF
- x y) =
- (fsym_unex T f00 f01 f02 f03 f04 f05 f06 f07 f08 f09 f0A f0B f0C f0D f0E f0F
- f11 f12 f13 f14 f15 f16 f17 f18 f19 f1A f1B f1C f1D f1E f1F
- f22 f23 f24 f25 f26 f27 f28 f29 f2A f2B f2C f2D f2E f2F
- f33 f34 f35 f36 f37 f38 f39 f3A f3B f3C f3D f3E f3F
- f44 f45 f46 f47 f48 f49 f4A f4B f4C f4D f4E f4F
- f55 f56 f57 f58 f59 f5A f5B f5C f5D f5E f5F
- f66 f67 f68 f69 f6A f6B f6C f6D f6E f6F
- f77 f78 f79 f7A f7B f7C f7D f7E f7F
- f88 f89 f8A f8B f8C f8D f8E f8F
- f99 f9A f9B f9C f9D f9E f9F
- fAA fAB fAC fAD fAE fAF
- fBB fBC fBD fBE fBF
- fCC fCD fCE fCF
- fDD fDE fDF
- fEE fEF
- fFF
- y x).
- #T;
- #f00; #f01; #f02; #f03; #f04; #f05; #f06; #f07; #f08; #f09; #f0A; #f0B; #f0C; #f0D; #f0E; #f0F;
- #f11; #f12; #f13; #f14; #f15; #f16; #f17; #f18; #f19; #f1A; #f1B; #f1C; #f1D; #f1E; #f1F;
- #f22; #f23; #f24; #f25; #f26; #f27; #f28; #f29; #f2A; #f2B; #f2C; #f2D; #f2E; #f2F;
- #f33; #f34; #f35; #f36; #f37; #f38; #f39; #f3A; #f3B; #f3C; #f3D; #f3E; #f3F;
- #f44; #f45; #f46; #f47; #f48; #f49; #f4A; #f4B; #f4C; #f4D; #f4E; #f4F;
- #f55; #f56; #f57; #f58; #f59; #f5A; #f5B; #f5C; #f5D; #f5E; #f5F;
- #f66; #f67; #f68; #f69; #f6A; #f6B; #f6C; #f6D; #f6E; #f6F;
- #f77; #f78; #f79; #f7A; #f7B; #f7C; #f7D; #f7E; #f7F;
- #f88; #f89; #f8A; #f8B; #f8C; #f8D; #f8E; #f8F;
- #f99; #f9A; #f9B; #f9C; #f9D; #f9E; #f9F;
- #fAA; #fAB; #fAC; #fAD; #fAE; #fAF;
- #fBB; #fBC; #fBD; #fBE; #fBF;
- #fCC; #fCD; #fCE; #fCF;
- #fDD; #fDE; #fDF;
- #fEE; #fEF;
- #fFF;
- #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u; ncases u;
- ##[ ##13: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##14: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##15: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##16: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##17: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##18: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##19: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##20: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##21: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##22: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##23: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##24: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##25: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##26: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##27: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##28: #dim1; #dim2; napply (sym_unex1 T … dim1 dim2)
- ##| ##*: #dim1; nnormalize in dim1:(%) napply (bool_destruct … dim1)
- ##]
- ##]
-nqed.
-*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "universe/universe.ma".
-
-ndefinition OCT_UN ≝ [ uo0; uo1; uo2; uo3; uo4; uo5; uo6; uo7 ].
-
-(* derivati dall'universo
- 1) SUN_destruct OCT_UN
- 2) eq_to_eqSUN OCT_UN
- 3) neq_to_neqSUN OCT_UN
- 4) eqSUN_to_eq OCT_UN
- 5) neqSUN_to_neq OCT_UN
- 6) decidable_SUN OCT_UN
- 7) symmetric_eqSUN OCT_UN
-*)
-
-nlemma un_o0 : S_UN OCT_UN. napply (S_EL OCT_UN uo0 (refl_eq …) ?); #y; nelim y; ##[ ##5: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_o1 : S_UN OCT_UN. napply (S_EL OCT_UN uo1 (refl_eq …) ?); #y; nelim y; ##[ ##6: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_o2 : S_UN OCT_UN. napply (S_EL OCT_UN uo2 (refl_eq …) ?); #y; nelim y; ##[ ##7: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_o3 : S_UN OCT_UN. napply (S_EL OCT_UN uo3 (refl_eq …) ?); #y; nelim y; ##[ ##8: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_o4 : S_UN OCT_UN. napply (S_EL OCT_UN uo4 (refl_eq …) ?); #y; nelim y; ##[ ##9: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_o5 : S_UN OCT_UN. napply (S_EL OCT_UN uo5 (refl_eq …) ?); #y; nelim y; ##[ ##10: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_o6 : S_UN OCT_UN. napply (S_EL OCT_UN uo6 (refl_eq …) ?); #y; nelim y; ##[ ##11: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_o7 : S_UN OCT_UN. napply (S_EL OCT_UN uo7 (refl_eq …) ?); #y; nelim y; ##[ ##12: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "universe/universe.ma".
-
-ndefinition OP_UN ≝ [ uADC; uADD; uAIS; uAIX; uAND; uASL; uASR; uBCC; uBCLRn; uBCS;
- uBEQ; uBGE; uBGND; uBGT; uBHCC; uBHCS; uBHI; uBIH; uBIL; uBIT;
- uBLE; uBLS; uBLT; uBMC; uBMI; uBMS; uBNE; uBPL; uBRA; uBRCLRn;
- uBRN; uBRSETn; uBSETn; uBSR; uCBEQA; uCBEQX; uCLC; uCLI; uCLR;
- uCMP; uCOM; uCPHX; uCPX; uDAA; uDBNZ; uDEC; uDIV; uEOR; uINC;
- uJMP; uJSR; uLDA; uLDHX; uLDX; uLSR; uMOV; uMUL; uNEG; uNOP;
- uNSA; uORA; uPSHA; uPSHH; uPSHX; uPULA; uPULH; uPULX; uROL;
- uROR; uRSP; uRTI; uRTS; uSBC; uSEC; uSEI; uSHA; uSLA; uSTA;
- uSTHX; uSTOP; uSTX; uSUB; uSWI; uTAP; uTAX; uTPA; uTST; uTSX;
- uTXA; uTXS; uWAIT ].
-
-(* derivati dall'universo
- 1) SUN_destruct OP_UN
- 2) eq_to_eqSUN OP_UN
- 3) neq_to_neqSUN OP_UN
- 4) eqSUN_to_eq OP_UN
- 5) neqSUN_to_neq OP_UN
- 6) decidable_SUN OP_UN
- 7) symmetric_eqSUN OP_UN
-*)
-
-nlemma un_ADC : S_UN OP_UN. napply (S_EL OP_UN uADC (refl_eq …) ?); #y; nelim y; ##[ ##124: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ADD : S_UN OP_UN. napply (S_EL OP_UN uADD (refl_eq …) ?); #y; nelim y; ##[ ##125: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_AIS : S_UN OP_UN. napply (S_EL OP_UN uAIS (refl_eq …) ?); #y; nelim y; ##[ ##126: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_AIX : S_UN OP_UN. napply (S_EL OP_UN uAIX (refl_eq …) ?); #y; nelim y; ##[ ##127: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_AND : S_UN OP_UN. napply (S_EL OP_UN uAND (refl_eq …) ?); #y; nelim y; ##[ ##128: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ASL : S_UN OP_UN. napply (S_EL OP_UN uASL (refl_eq …) ?); #y; nelim y; ##[ ##129: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ASR : S_UN OP_UN. napply (S_EL OP_UN uASR (refl_eq …) ?); #y; nelim y; ##[ ##130: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BCC : S_UN OP_UN. napply (S_EL OP_UN uBCC (refl_eq …) ?); #y; nelim y; ##[ ##131: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BCLRn : S_UN OP_UN. napply (S_EL OP_UN uBCLRn (refl_eq …) ?); #y; nelim y; ##[ ##132: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BCS : S_UN OP_UN. napply (S_EL OP_UN uBCS (refl_eq …) ?); #y; nelim y; ##[ ##133: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BEQ : S_UN OP_UN. napply (S_EL OP_UN uBEQ (refl_eq …) ?); #y; nelim y; ##[ ##134: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BGE : S_UN OP_UN. napply (S_EL OP_UN uBGE (refl_eq …) ?); #y; nelim y; ##[ ##135: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BGND : S_UN OP_UN. napply (S_EL OP_UN uBGND (refl_eq …) ?); #y; nelim y; ##[ ##136: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BGT : S_UN OP_UN. napply (S_EL OP_UN uBGT (refl_eq …) ?); #y; nelim y; ##[ ##137: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BHCC : S_UN OP_UN. napply (S_EL OP_UN uBHCC (refl_eq …) ?); #y; nelim y; ##[ ##138: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BHCS : S_UN OP_UN. napply (S_EL OP_UN uBHCS (refl_eq …) ?); #y; nelim y; ##[ ##139: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BHI : S_UN OP_UN. napply (S_EL OP_UN uBHI (refl_eq …) ?); #y; nelim y; ##[ ##140: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BIH : S_UN OP_UN. napply (S_EL OP_UN uBIH (refl_eq …) ?); #y; nelim y; ##[ ##141: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BIL : S_UN OP_UN. napply (S_EL OP_UN uBIL (refl_eq …) ?); #y; nelim y; ##[ ##142: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BIT : S_UN OP_UN. napply (S_EL OP_UN uBIT (refl_eq …) ?); #y; nelim y; ##[ ##143: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BLE : S_UN OP_UN. napply (S_EL OP_UN uBLE (refl_eq …) ?); #y; nelim y; ##[ ##144: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BLS : S_UN OP_UN. napply (S_EL OP_UN uBLS (refl_eq …) ?); #y; nelim y; ##[ ##145: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BLT : S_UN OP_UN. napply (S_EL OP_UN uBLT (refl_eq …) ?); #y; nelim y; ##[ ##146: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BMC : S_UN OP_UN. napply (S_EL OP_UN uBMC (refl_eq …) ?); #y; nelim y; ##[ ##147: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BMI : S_UN OP_UN. napply (S_EL OP_UN uBMI (refl_eq …) ?); #y; nelim y; ##[ ##148: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BMS : S_UN OP_UN. napply (S_EL OP_UN uBMS (refl_eq …) ?); #y; nelim y; ##[ ##149: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BNE : S_UN OP_UN. napply (S_EL OP_UN uBNE (refl_eq …) ?); #y; nelim y; ##[ ##150: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BPL : S_UN OP_UN. napply (S_EL OP_UN uBPL (refl_eq …) ?); #y; nelim y; ##[ ##151: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BRA : S_UN OP_UN. napply (S_EL OP_UN uBRA (refl_eq …) ?); #y; nelim y; ##[ ##152: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BRCLRn : S_UN OP_UN. napply (S_EL OP_UN uBRCLRn (refl_eq …) ?); #y; nelim y; ##[ ##153: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BRN : S_UN OP_UN. napply (S_EL OP_UN uBRN (refl_eq …) ?); #y; nelim y; ##[ ##154: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BRSETn : S_UN OP_UN. napply (S_EL OP_UN uBRSETn (refl_eq …) ?); #y; nelim y; ##[ ##155: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BSETn : S_UN OP_UN. napply (S_EL OP_UN uBSETn (refl_eq …) ?); #y; nelim y; ##[ ##156: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_BSR : S_UN OP_UN. napply (S_EL OP_UN uBSR (refl_eq …) ?); #y; nelim y; ##[ ##157: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_CBEQA : S_UN OP_UN. napply (S_EL OP_UN uCBEQA (refl_eq …) ?); #y; nelim y; ##[ ##158: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_CBEQX : S_UN OP_UN. napply (S_EL OP_UN uCBEQX (refl_eq …) ?); #y; nelim y; ##[ ##159: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_CLC : S_UN OP_UN. napply (S_EL OP_UN uCLC (refl_eq …) ?); #y; nelim y; ##[ ##160: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_CLI : S_UN OP_UN. napply (S_EL OP_UN uCLI (refl_eq …) ?); #y; nelim y; ##[ ##161: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_CLR : S_UN OP_UN. napply (S_EL OP_UN uCLR (refl_eq …) ?); #y; nelim y; ##[ ##162: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_CMP : S_UN OP_UN. napply (S_EL OP_UN uCMP (refl_eq …) ?); #y; nelim y; ##[ ##163: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_COM : S_UN OP_UN. napply (S_EL OP_UN uCOM (refl_eq …) ?); #y; nelim y; ##[ ##164: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_CPHX : S_UN OP_UN. napply (S_EL OP_UN uCPHX (refl_eq …) ?); #y; nelim y; ##[ ##165: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_CPX : S_UN OP_UN. napply (S_EL OP_UN uCPX (refl_eq …) ?); #y; nelim y; ##[ ##166: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_DAA : S_UN OP_UN. napply (S_EL OP_UN uDAA (refl_eq …) ?); #y; nelim y; ##[ ##167: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_DBNZ : S_UN OP_UN. napply (S_EL OP_UN uDBNZ (refl_eq …) ?); #y; nelim y; ##[ ##168: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_DEC : S_UN OP_UN. napply (S_EL OP_UN uDEC (refl_eq …) ?); #y; nelim y; ##[ ##169: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_DIV : S_UN OP_UN. napply (S_EL OP_UN uDIV (refl_eq …) ?); #y; nelim y; ##[ ##170: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_EOR : S_UN OP_UN. napply (S_EL OP_UN uEOR (refl_eq …) ?); #y; nelim y; ##[ ##171: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_INC : S_UN OP_UN. napply (S_EL OP_UN uINC (refl_eq …) ?); #y; nelim y; ##[ ##172: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_JMP : S_UN OP_UN. napply (S_EL OP_UN uJMP (refl_eq …) ?); #y; nelim y; ##[ ##173: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_JSR : S_UN OP_UN. napply (S_EL OP_UN uJSR (refl_eq …) ?); #y; nelim y; ##[ ##174: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_LDA : S_UN OP_UN. napply (S_EL OP_UN uLDA (refl_eq …) ?); #y; nelim y; ##[ ##175: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_LDHX : S_UN OP_UN. napply (S_EL OP_UN uLDHX (refl_eq …) ?); #y; nelim y; ##[ ##176: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_LDX : S_UN OP_UN. napply (S_EL OP_UN uLDX (refl_eq …) ?); #y; nelim y; ##[ ##177: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_LSR : S_UN OP_UN. napply (S_EL OP_UN uLSR (refl_eq …) ?); #y; nelim y; ##[ ##178: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_MOV : S_UN OP_UN. napply (S_EL OP_UN uMOV (refl_eq …) ?); #y; nelim y; ##[ ##179: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_MUL : S_UN OP_UN. napply (S_EL OP_UN uMUL (refl_eq …) ?); #y; nelim y; ##[ ##180: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_NEG : S_UN OP_UN. napply (S_EL OP_UN uNEG (refl_eq …) ?); #y; nelim y; ##[ ##181: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_NOP : S_UN OP_UN. napply (S_EL OP_UN uNOP (refl_eq …) ?); #y; nelim y; ##[ ##182: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_NSA : S_UN OP_UN. napply (S_EL OP_UN uNSA (refl_eq …) ?); #y; nelim y; ##[ ##183: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ORA : S_UN OP_UN. napply (S_EL OP_UN uORA (refl_eq …) ?); #y; nelim y; ##[ ##184: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_PSHA : S_UN OP_UN. napply (S_EL OP_UN uPSHA (refl_eq …) ?); #y; nelim y; ##[ ##185: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_PSHH : S_UN OP_UN. napply (S_EL OP_UN uPSHH (refl_eq …) ?); #y; nelim y; ##[ ##186: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_PSHX : S_UN OP_UN. napply (S_EL OP_UN uPSHX (refl_eq …) ?); #y; nelim y; ##[ ##187: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_PULA : S_UN OP_UN. napply (S_EL OP_UN uPULA (refl_eq …) ?); #y; nelim y; ##[ ##188: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_PULH : S_UN OP_UN. napply (S_EL OP_UN uPULH (refl_eq …) ?); #y; nelim y; ##[ ##189: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_PULX : S_UN OP_UN. napply (S_EL OP_UN uPULX (refl_eq …) ?); #y; nelim y; ##[ ##190: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ROL : S_UN OP_UN. napply (S_EL OP_UN uROL (refl_eq …) ?); #y; nelim y; ##[ ##191: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_ROR : S_UN OP_UN. napply (S_EL OP_UN uROR (refl_eq …) ?); #y; nelim y; ##[ ##192: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_RSP : S_UN OP_UN. napply (S_EL OP_UN uRSP (refl_eq …) ?); #y; nelim y; ##[ ##193: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_RTI : S_UN OP_UN. napply (S_EL OP_UN uRTI (refl_eq …) ?); #y; nelim y; ##[ ##194: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_RTS : S_UN OP_UN. napply (S_EL OP_UN uRTS (refl_eq …) ?); #y; nelim y; ##[ ##195: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_SBC : S_UN OP_UN. napply (S_EL OP_UN uSBC (refl_eq …) ?); #y; nelim y; ##[ ##196: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_SEC : S_UN OP_UN. napply (S_EL OP_UN uSEC (refl_eq …) ?); #y; nelim y; ##[ ##197: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_SEI : S_UN OP_UN. napply (S_EL OP_UN uSEI (refl_eq …) ?); #y; nelim y; ##[ ##198: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_SHA : S_UN OP_UN. napply (S_EL OP_UN uSHA (refl_eq …) ?); #y; nelim y; ##[ ##199: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_SLA : S_UN OP_UN. napply (S_EL OP_UN uSLA (refl_eq …) ?); #y; nelim y; ##[ ##200: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_STA : S_UN OP_UN. napply (S_EL OP_UN uSTA (refl_eq …) ?); #y; nelim y; ##[ ##201: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_STHX : S_UN OP_UN. napply (S_EL OP_UN uSTHX (refl_eq …) ?); #y; nelim y; ##[ ##202: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_STOP : S_UN OP_UN. napply (S_EL OP_UN uSTOP (refl_eq …) ?); #y; nelim y; ##[ ##203: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_STX : S_UN OP_UN. napply (S_EL OP_UN uSTX (refl_eq …) ?); #y; nelim y; ##[ ##204: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_SUB : S_UN OP_UN. napply (S_EL OP_UN uSUB (refl_eq …) ?); #y; nelim y; ##[ ##205: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_SWI : S_UN OP_UN. napply (S_EL OP_UN uSWI (refl_eq …) ?); #y; nelim y; ##[ ##206: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_TAP : S_UN OP_UN. napply (S_EL OP_UN uTAP (refl_eq …) ?); #y; nelim y; ##[ ##207: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_TAX : S_UN OP_UN. napply (S_EL OP_UN uTAX (refl_eq …) ?); #y; nelim y; ##[ ##208: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_TPA : S_UN OP_UN. napply (S_EL OP_UN uTPA (refl_eq …) ?); #y; nelim y; ##[ ##209: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_TST : S_UN OP_UN. napply (S_EL OP_UN uTST (refl_eq …) ?); #y; nelim y; ##[ ##210: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_TSX : S_UN OP_UN. napply (S_EL OP_UN uTSX (refl_eq …) ?); #y; nelim y; ##[ ##211: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_TXA : S_UN OP_UN. napply (S_EL OP_UN uTXA (refl_eq …) ?); #y; nelim y; ##[ ##212: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_TXS : S_UN OP_UN. napply (S_EL OP_UN uTXS (refl_eq …) ?); #y; nelim y; ##[ ##213: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_WAIT : S_UN OP_UN. napply (S_EL OP_UN uWAIT (refl_eq …) ?); #y; nelim y; ##[ ##214: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "universe/universe.ma".
-
-ndefinition QU_UN ≝ [ uq0; uq1; uq2; uq3 ].
-
-(* derivati dall'universo
- 1) SUN_destruct QU_UN
- 2) eq_to_eqSUN QU_UN
- 3) neq_to_neqSUN QU_UN
- 4) eqSUN_to_eq QU_UN
- 5) neqSUN_to_neq QU_UN
- 6) decidable_SUN QU_UN
- 7) symmetric_eqSUN QU_UN
-*)
-
-nlemma un_q0 : S_UN QU_UN. napply (S_EL QU_UN uq0 (refl_eq …) ?); #y; nelim y; ##[ ##1: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_q1 : S_UN QU_UN. napply (S_EL QU_UN uq1 (refl_eq …) ?); #y; nelim y; ##[ ##2: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_q2 : S_UN QU_UN. napply (S_EL QU_UN uq2 (refl_eq …) ?); #y; nelim y; ##[ ##3: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
-nlemma un_q3 : S_UN QU_UN. napply (S_EL QU_UN uq3 (refl_eq …) ?); #y; nelim y; ##[ ##4: nnormalize; #H; napply refl_eq ##| ##*: nnormalize; #H; napply (bool_destruct … H) ##] nqed.
(* ********************************************************************** *)
include "common/list.ma".
-include "num/bool_lemmas.ma".
+include "common/nat_lemmas.ma".
+include "common/prod.ma".
-nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
+nlet rec nmember_natList (elem:nat) (l:ne_list nat) on l ≝
match l with
- [ nil ⇒ true
- | cons h t ⇒ match f elem h with
- [ true ⇒ false | false ⇒ nmember_list T elem f t ]
+ [ ne_nil h ⇒ ⊖(eq_nat elem h)
+ | ne_cons h t ⇒ match eq_nat elem h with
+ [ true ⇒ false | false ⇒ nmember_natList elem t ]
].
(* elem presente una ed una sola volta in l *)
-nlet rec member_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
+nlet rec member_natList (elem:nat) (l:ne_list nat) on l ≝
match l with
- [ nil ⇒ false
- | cons h t ⇒ match f elem h with
- [ true ⇒ nmember_list T elem f t | false ⇒ member_list T elem f t ]
+ [ ne_nil h ⇒ eq_nat elem h
+ | ne_cons h t ⇒ match eq_nat elem h with
+ [ true ⇒ nmember_natList elem t | false ⇒ member_natList elem t ]
].
-(* tutti gli atomi dell'universo che poi saranno raggruppati in sottouniversi *)
-ninductive UN : Type ≝
-(* quaternari[4] 1-4 *)
- uq0 : UN
-| uq1 : UN
-| uq2 : UN
-| uq3 : UN
-
-(* ottali[8] 5-12 *)
-| uo0 : UN
-| uo1 : UN
-| uo2 : UN
-| uo3 : UN
-| uo4 : UN
-| uo5 : UN
-| uo6 : UN
-| uo7 : UN
-
-(* esadecimali[16] 13-28 *)
-| ux0 : UN
-| ux1 : UN
-| ux2 : UN
-| ux3 : UN
-| ux4 : UN
-| ux5 : UN
-| ux6 : UN
-| ux7 : UN
-| ux8 : UN
-| ux9 : UN
-| uxA : UN
-| uxB : UN
-| uxC : UN
-| uxD : UN
-| uxE : UN
-| uxF : UN
-
-(* bitrigesimali[32] 29-60 *)
-| ut00 : UN
-| ut01 : UN
-| ut02 : UN
-| ut03 : UN
-| ut04 : UN
-| ut05 : UN
-| ut06 : UN
-| ut07 : UN
-| ut08 : UN
-| ut09 : UN
-| ut0A : UN
-| ut0B : UN
-| ut0C : UN
-| ut0D : UN
-| ut0E : UN
-| ut0F : UN
-| ut10 : UN
-| ut11 : UN
-| ut12 : UN
-| ut13 : UN
-| ut14 : UN
-| ut15 : UN
-| ut16 : UN
-| ut17 : UN
-| ut18 : UN
-| ut19 : UN
-| ut1A : UN
-| ut1B : UN
-| ut1C : UN
-| ut1D : UN
-| ut1E : UN
-| ut1F : UN
-
-(* ascii[63] 61-123 *)
-| uch_0 : UN
-| uch_1 : UN
-| uch_2 : UN
-| uch_3 : UN
-| uch_4 : UN
-| uch_5 : UN
-| uch_6 : UN
-| uch_7 : UN
-| uch_8 : UN
-| uch_9 : UN
-| uch__ : UN
-| uch_A : UN
-| uch_B : UN
-| uch_C : UN
-| uch_D : UN
-| uch_E : UN
-| uch_F : UN
-| uch_G : UN
-| uch_H : UN
-| uch_I : UN
-| uch_J : UN
-| uch_K : UN
-| uch_L : UN
-| uch_M : UN
-| uch_N : UN
-| uch_O : UN
-| uch_P : UN
-| uch_Q : UN
-| uch_R : UN
-| uch_S : UN
-| uch_T : UN
-| uch_U : UN
-| uch_V : UN
-| uch_W : UN
-| uch_X : UN
-| uch_Y : UN
-| uch_Z : UN
-| uch_a : UN
-| uch_b : UN
-| uch_c : UN
-| uch_d : UN
-| uch_e : UN
-| uch_f : UN
-| uch_g : UN
-| uch_h : UN
-| uch_i : UN
-| uch_j : UN
-| uch_k : UN
-| uch_l : UN
-| uch_m : UN
-| uch_n : UN
-| uch_o : UN
-| uch_p : UN
-| uch_q : UN
-| uch_r : UN
-| uch_s : UN
-| uch_t : UN
-| uch_u : UN
-| uch_v : UN
-| uch_w : UN
-| uch_x : UN
-| uch_y : UN
-| uch_z : UN
-
-(* opcode[91] 124-214 *)
-| uADC : UN
-| uADD : UN
-| uAIS : UN
-| uAIX : UN
-| uAND : UN
-| uASL : UN
-| uASR : UN
-| uBCC : UN
-| uBCLRn : UN
-| uBCS : UN
-| uBEQ : UN
-| uBGE : UN
-| uBGND : UN
-| uBGT : UN
-| uBHCC : UN
-| uBHCS : UN
-| uBHI : UN
-| uBIH : UN
-| uBIL : UN
-| uBIT : UN
-| uBLE : UN
-| uBLS : UN
-| uBLT : UN
-| uBMC : UN
-| uBMI : UN
-| uBMS : UN
-| uBNE : UN
-| uBPL : UN
-| uBRA : UN
-| uBRCLRn : UN
-| uBRN : UN
-| uBRSETn : UN
-| uBSETn : UN
-| uBSR : UN
-| uCBEQA : UN
-| uCBEQX : UN
-| uCLC : UN
-| uCLI : UN
-| uCLR : UN
-| uCMP : UN
-| uCOM : UN
-| uCPHX : UN
-| uCPX : UN
-| uDAA : UN
-| uDBNZ : UN
-| uDEC : UN
-| uDIV : UN
-| uEOR : UN
-| uINC : UN
-| uJMP : UN
-| uJSR : UN
-| uLDA : UN
-| uLDHX : UN
-| uLDX : UN
-| uLSR : UN
-| uMOV : UN
-| uMUL : UN
-| uNEG : UN
-| uNOP : UN
-| uNSA : UN
-| uORA : UN
-| uPSHA : UN
-| uPSHH : UN
-| uPSHX : UN
-| uPULA : UN
-| uPULH : UN
-| uPULX : UN
-| uROL : UN
-| uROR : UN
-| uRSP : UN
-| uRTI : UN
-| uRTS : UN
-| uSBC : UN
-| uSEC : UN
-| uSEI : UN
-| uSHA : UN
-| uSLA : UN
-| uSTA : UN
-| uSTHX : UN
-| uSTOP : UN
-| uSTX : UN
-| uSUB : UN
-| uSWI : UN
-| uTAP : UN
-| uTAX : UN
-| uTPA : UN
-| uTST : UN
-| uTSX : UN
-| uTXA : UN
-| uTXS : UN
-| uWAIT : UN
-.
-
-(* funzione di uguaglianza sugli atomi *)
-ndefinition eq_UN ≝
-λu1,u2.match u1 with
- [ uq0 ⇒ match u2 with [ uq0 ⇒ true | _ ⇒ false ]
- | uq1 ⇒ match u2 with [ uq1 ⇒ true | _ ⇒ false ]
- | uq2 ⇒ match u2 with [ uq2 ⇒ true | _ ⇒ false ]
- | uq3 ⇒ match u2 with [ uq3 ⇒ true | _ ⇒ false ]
-
- | uo0 ⇒ match u2 with [ uo0 ⇒ true | _ ⇒ false ]
- | uo1 ⇒ match u2 with [ uo1 ⇒ true | _ ⇒ false ]
- | uo2 ⇒ match u2 with [ uo2 ⇒ true | _ ⇒ false ]
- | uo3 ⇒ match u2 with [ uo3 ⇒ true | _ ⇒ false ]
- | uo4 ⇒ match u2 with [ uo4 ⇒ true | _ ⇒ false ]
- | uo5 ⇒ match u2 with [ uo5 ⇒ true | _ ⇒ false ]
- | uo6 ⇒ match u2 with [ uo6 ⇒ true | _ ⇒ false ]
- | uo7 ⇒ match u2 with [ uo7 ⇒ true | _ ⇒ false ]
-
- | ux0 ⇒ match u2 with [ ux0 ⇒ true | _ ⇒ false ]
- | ux1 ⇒ match u2 with [ ux1 ⇒ true | _ ⇒ false ]
- | ux2 ⇒ match u2 with [ ux2 ⇒ true | _ ⇒ false ]
- | ux3 ⇒ match u2 with [ ux3 ⇒ true | _ ⇒ false ]
- | ux4 ⇒ match u2 with [ ux4 ⇒ true | _ ⇒ false ]
- | ux5 ⇒ match u2 with [ ux5 ⇒ true | _ ⇒ false ]
- | ux6 ⇒ match u2 with [ ux6 ⇒ true | _ ⇒ false ]
- | ux7 ⇒ match u2 with [ ux7 ⇒ true | _ ⇒ false ]
- | ux8 ⇒ match u2 with [ ux8 ⇒ true | _ ⇒ false ]
- | ux9 ⇒ match u2 with [ ux9 ⇒ true | _ ⇒ false ]
- | uxA ⇒ match u2 with [ uxA ⇒ true | _ ⇒ false ]
- | uxB ⇒ match u2 with [ uxB ⇒ true | _ ⇒ false ]
- | uxC ⇒ match u2 with [ uxC ⇒ true | _ ⇒ false ]
- | uxD ⇒ match u2 with [ uxD ⇒ true | _ ⇒ false ]
- | uxE ⇒ match u2 with [ uxE ⇒ true | _ ⇒ false ]
- | uxF ⇒ match u2 with [ uxF ⇒ true | _ ⇒ false ]
-
- | ut00 ⇒ match u2 with [ ut00 ⇒ true | _ ⇒ false ]
- | ut01 ⇒ match u2 with [ ut01 ⇒ true | _ ⇒ false ]
- | ut02 ⇒ match u2 with [ ut02 ⇒ true | _ ⇒ false ]
- | ut03 ⇒ match u2 with [ ut03 ⇒ true | _ ⇒ false ]
- | ut04 ⇒ match u2 with [ ut04 ⇒ true | _ ⇒ false ]
- | ut05 ⇒ match u2 with [ ut05 ⇒ true | _ ⇒ false ]
- | ut06 ⇒ match u2 with [ ut06 ⇒ true | _ ⇒ false ]
- | ut07 ⇒ match u2 with [ ut07 ⇒ true | _ ⇒ false ]
- | ut08 ⇒ match u2 with [ ut08 ⇒ true | _ ⇒ false ]
- | ut09 ⇒ match u2 with [ ut09 ⇒ true | _ ⇒ false ]
- | ut0A ⇒ match u2 with [ ut0A ⇒ true | _ ⇒ false ]
- | ut0B ⇒ match u2 with [ ut0B ⇒ true | _ ⇒ false ]
- | ut0C ⇒ match u2 with [ ut0C ⇒ true | _ ⇒ false ]
- | ut0D ⇒ match u2 with [ ut0D ⇒ true | _ ⇒ false ]
- | ut0E ⇒ match u2 with [ ut0E ⇒ true | _ ⇒ false ]
- | ut0F ⇒ match u2 with [ ut0F ⇒ true | _ ⇒ false ]
- | ut10 ⇒ match u2 with [ ut10 ⇒ true | _ ⇒ false ]
- | ut11 ⇒ match u2 with [ ut11 ⇒ true | _ ⇒ false ]
- | ut12 ⇒ match u2 with [ ut12 ⇒ true | _ ⇒ false ]
- | ut13 ⇒ match u2 with [ ut13 ⇒ true | _ ⇒ false ]
- | ut14 ⇒ match u2 with [ ut14 ⇒ true | _ ⇒ false ]
- | ut15 ⇒ match u2 with [ ut15 ⇒ true | _ ⇒ false ]
- | ut16 ⇒ match u2 with [ ut16 ⇒ true | _ ⇒ false ]
- | ut17 ⇒ match u2 with [ ut17 ⇒ true | _ ⇒ false ]
- | ut18 ⇒ match u2 with [ ut18 ⇒ true | _ ⇒ false ]
- | ut19 ⇒ match u2 with [ ut19 ⇒ true | _ ⇒ false ]
- | ut1A ⇒ match u2 with [ ut1A ⇒ true | _ ⇒ false ]
- | ut1B ⇒ match u2 with [ ut1B ⇒ true | _ ⇒ false ]
- | ut1C ⇒ match u2 with [ ut1C ⇒ true | _ ⇒ false ]
- | ut1D ⇒ match u2 with [ ut1D ⇒ true | _ ⇒ false ]
- | ut1E ⇒ match u2 with [ ut1E ⇒ true | _ ⇒ false ]
- | ut1F ⇒ match u2 with [ ut1F ⇒ true | _ ⇒ false ]
-
- | uch_0 ⇒ match u2 with [ uch_0 ⇒ true | _ ⇒ false ]
- | uch_1 ⇒ match u2 with [ uch_1 ⇒ true | _ ⇒ false ]
- | uch_2 ⇒ match u2 with [ uch_2 ⇒ true | _ ⇒ false ]
- | uch_3 ⇒ match u2 with [ uch_3 ⇒ true | _ ⇒ false ]
- | uch_4 ⇒ match u2 with [ uch_4 ⇒ true | _ ⇒ false ]
- | uch_5 ⇒ match u2 with [ uch_5 ⇒ true | _ ⇒ false ]
- | uch_6 ⇒ match u2 with [ uch_6 ⇒ true | _ ⇒ false ]
- | uch_7 ⇒ match u2 with [ uch_7 ⇒ true | _ ⇒ false ]
- | uch_8 ⇒ match u2 with [ uch_8 ⇒ true | _ ⇒ false ]
- | uch_9 ⇒ match u2 with [ uch_9 ⇒ true | _ ⇒ false ]
- | uch__ ⇒ match u2 with [ uch__ ⇒ true | _ ⇒ false ]
- | uch_A ⇒ match u2 with [ uch_A ⇒ true | _ ⇒ false ]
- | uch_B ⇒ match u2 with [ uch_B ⇒ true | _ ⇒ false ]
- | uch_C ⇒ match u2 with [ uch_C ⇒ true | _ ⇒ false ]
- | uch_D ⇒ match u2 with [ uch_D ⇒ true | _ ⇒ false ]
- | uch_E ⇒ match u2 with [ uch_E ⇒ true | _ ⇒ false ]
- | uch_F ⇒ match u2 with [ uch_F ⇒ true | _ ⇒ false ]
- | uch_G ⇒ match u2 with [ uch_G ⇒ true | _ ⇒ false ]
- | uch_H ⇒ match u2 with [ uch_H ⇒ true | _ ⇒ false ]
- | uch_I ⇒ match u2 with [ uch_I ⇒ true | _ ⇒ false ]
- | uch_J ⇒ match u2 with [ uch_J ⇒ true | _ ⇒ false ]
- | uch_K ⇒ match u2 with [ uch_K ⇒ true | _ ⇒ false ]
- | uch_L ⇒ match u2 with [ uch_L ⇒ true | _ ⇒ false ]
- | uch_M ⇒ match u2 with [ uch_M ⇒ true | _ ⇒ false ]
- | uch_N ⇒ match u2 with [ uch_N ⇒ true | _ ⇒ false ]
- | uch_O ⇒ match u2 with [ uch_O ⇒ true | _ ⇒ false ]
- | uch_P ⇒ match u2 with [ uch_P ⇒ true | _ ⇒ false ]
- | uch_Q ⇒ match u2 with [ uch_Q ⇒ true | _ ⇒ false ]
- | uch_R ⇒ match u2 with [ uch_R ⇒ true | _ ⇒ false ]
- | uch_S ⇒ match u2 with [ uch_S ⇒ true | _ ⇒ false ]
- | uch_T ⇒ match u2 with [ uch_T ⇒ true | _ ⇒ false ]
- | uch_U ⇒ match u2 with [ uch_U ⇒ true | _ ⇒ false ]
- | uch_V ⇒ match u2 with [ uch_V ⇒ true | _ ⇒ false ]
- | uch_W ⇒ match u2 with [ uch_W ⇒ true | _ ⇒ false ]
- | uch_X ⇒ match u2 with [ uch_X ⇒ true | _ ⇒ false ]
- | uch_Y ⇒ match u2 with [ uch_Y ⇒ true | _ ⇒ false ]
- | uch_Z ⇒ match u2 with [ uch_Z ⇒ true | _ ⇒ false ]
- | uch_a ⇒ match u2 with [ uch_a ⇒ true | _ ⇒ false ]
- | uch_b ⇒ match u2 with [ uch_b ⇒ true | _ ⇒ false ]
- | uch_c ⇒ match u2 with [ uch_c ⇒ true | _ ⇒ false ]
- | uch_d ⇒ match u2 with [ uch_d ⇒ true | _ ⇒ false ]
- | uch_e ⇒ match u2 with [ uch_e ⇒ true | _ ⇒ false ]
- | uch_f ⇒ match u2 with [ uch_f ⇒ true | _ ⇒ false ]
- | uch_g ⇒ match u2 with [ uch_g ⇒ true | _ ⇒ false ]
- | uch_h ⇒ match u2 with [ uch_h ⇒ true | _ ⇒ false ]
- | uch_i ⇒ match u2 with [ uch_i ⇒ true | _ ⇒ false ]
- | uch_j ⇒ match u2 with [ uch_j ⇒ true | _ ⇒ false ]
- | uch_k ⇒ match u2 with [ uch_k ⇒ true | _ ⇒ false ]
- | uch_l ⇒ match u2 with [ uch_l ⇒ true | _ ⇒ false ]
- | uch_m ⇒ match u2 with [ uch_m ⇒ true | _ ⇒ false ]
- | uch_n ⇒ match u2 with [ uch_n ⇒ true | _ ⇒ false ]
- | uch_o ⇒ match u2 with [ uch_o ⇒ true | _ ⇒ false ]
- | uch_p ⇒ match u2 with [ uch_p ⇒ true | _ ⇒ false ]
- | uch_q ⇒ match u2 with [ uch_q ⇒ true | _ ⇒ false ]
- | uch_r ⇒ match u2 with [ uch_r ⇒ true | _ ⇒ false ]
- | uch_s ⇒ match u2 with [ uch_s ⇒ true | _ ⇒ false ]
- | uch_t ⇒ match u2 with [ uch_t ⇒ true | _ ⇒ false ]
- | uch_u ⇒ match u2 with [ uch_u ⇒ true | _ ⇒ false ]
- | uch_v ⇒ match u2 with [ uch_v ⇒ true | _ ⇒ false ]
- | uch_w ⇒ match u2 with [ uch_w ⇒ true | _ ⇒ false ]
- | uch_x ⇒ match u2 with [ uch_x ⇒ true | _ ⇒ false ]
- | uch_y ⇒ match u2 with [ uch_y ⇒ true | _ ⇒ false ]
- | uch_z ⇒ match u2 with [ uch_z ⇒ true | _ ⇒ false ]
-
- | uADC ⇒ match u2 with [ uADC ⇒ true | _ ⇒ false ]
- | uADD ⇒ match u2 with [ uADD ⇒ true | _ ⇒ false ]
- | uAIS ⇒ match u2 with [ uAIS ⇒ true | _ ⇒ false ]
- | uAIX ⇒ match u2 with [ uAIX ⇒ true | _ ⇒ false ]
- | uAND ⇒ match u2 with [ uAND ⇒ true | _ ⇒ false ]
- | uASL ⇒ match u2 with [ uASL ⇒ true | _ ⇒ false ]
- | uASR ⇒ match u2 with [ uASR ⇒ true | _ ⇒ false ]
- | uBCC ⇒ match u2 with [ uBCC ⇒ true | _ ⇒ false ]
- | uBCLRn ⇒ match u2 with [ uBCLRn ⇒ true | _ ⇒ false ]
- | uBCS ⇒ match u2 with [ uBCS ⇒ true | _ ⇒ false ]
- | uBEQ ⇒ match u2 with [ uBEQ ⇒ true | _ ⇒ false ]
- | uBGE ⇒ match u2 with [ uBGE ⇒ true | _ ⇒ false ]
- | uBGND ⇒ match u2 with [ uBGND ⇒ true | _ ⇒ false ]
- | uBGT ⇒ match u2 with [ uBGT ⇒ true | _ ⇒ false ]
- | uBHCC ⇒ match u2 with [ uBHCC ⇒ true | _ ⇒ false ]
- | uBHCS ⇒ match u2 with [ uBHCS ⇒ true | _ ⇒ false ]
- | uBHI ⇒ match u2 with [ uBHI ⇒ true | _ ⇒ false ]
- | uBIH ⇒ match u2 with [ uBIH ⇒ true | _ ⇒ false ]
- | uBIL ⇒ match u2 with [ uBIL ⇒ true | _ ⇒ false ]
- | uBIT ⇒ match u2 with [ uBIT ⇒ true | _ ⇒ false ]
- | uBLE ⇒ match u2 with [ uBLE ⇒ true | _ ⇒ false ]
- | uBLS ⇒ match u2 with [ uBLS ⇒ true | _ ⇒ false ]
- | uBLT ⇒ match u2 with [ uBLT ⇒ true | _ ⇒ false ]
- | uBMC ⇒ match u2 with [ uBMC ⇒ true | _ ⇒ false ]
- | uBMI ⇒ match u2 with [ uBMI ⇒ true | _ ⇒ false ]
- | uBMS ⇒ match u2 with [ uBMS ⇒ true | _ ⇒ false ]
- | uBNE ⇒ match u2 with [ uBNE ⇒ true | _ ⇒ false ]
- | uBPL ⇒ match u2 with [ uBPL ⇒ true | _ ⇒ false ]
- | uBRA ⇒ match u2 with [ uBRA ⇒ true | _ ⇒ false ]
- | uBRCLRn ⇒ match u2 with [ uBRCLRn ⇒ true | _ ⇒ false ]
- | uBRN ⇒ match u2 with [ uBRN ⇒ true | _ ⇒ false ]
- | uBRSETn ⇒ match u2 with [ uBRSETn ⇒ true | _ ⇒ false ]
- | uBSETn ⇒ match u2 with [ uBSETn ⇒ true | _ ⇒ false ]
- | uBSR ⇒ match u2 with [ uBSR ⇒ true | _ ⇒ false ]
- | uCBEQA ⇒ match u2 with [ uCBEQA ⇒ true | _ ⇒ false ]
- | uCBEQX ⇒ match u2 with [ uCBEQX ⇒ true | _ ⇒ false ]
- | uCLC ⇒ match u2 with [ uCLC ⇒ true | _ ⇒ false ]
- | uCLI ⇒ match u2 with [ uCLI ⇒ true | _ ⇒ false ]
- | uCLR ⇒ match u2 with [ uCLR ⇒ true | _ ⇒ false ]
- | uCMP ⇒ match u2 with [ uCMP ⇒ true | _ ⇒ false ]
- | uCOM ⇒ match u2 with [ uCOM ⇒ true | _ ⇒ false ]
- | uCPHX ⇒ match u2 with [ uCPHX ⇒ true | _ ⇒ false ]
- | uCPX ⇒ match u2 with [ uCPX ⇒ true | _ ⇒ false ]
- | uDAA ⇒ match u2 with [ uDAA ⇒ true | _ ⇒ false ]
- | uDBNZ ⇒ match u2 with [ uDBNZ ⇒ true | _ ⇒ false ]
- | uDEC ⇒ match u2 with [ uDEC ⇒ true | _ ⇒ false ]
- | uDIV ⇒ match u2 with [ uDIV ⇒ true | _ ⇒ false ]
- | uEOR ⇒ match u2 with [ uEOR ⇒ true | _ ⇒ false ]
- | uINC ⇒ match u2 with [ uINC ⇒ true | _ ⇒ false ]
- | uJMP ⇒ match u2 with [ uJMP ⇒ true | _ ⇒ false ]
- | uJSR ⇒ match u2 with [ uJSR ⇒ true | _ ⇒ false ]
- | uLDA ⇒ match u2 with [ uLDA ⇒ true | _ ⇒ false ]
- | uLDHX ⇒ match u2 with [ uLDHX ⇒ true | _ ⇒ false ]
- | uLDX ⇒ match u2 with [ uLDX ⇒ true | _ ⇒ false ]
- | uLSR ⇒ match u2 with [ uLSR ⇒ true | _ ⇒ false ]
- | uMOV ⇒ match u2 with [ uMOV ⇒ true | _ ⇒ false ]
- | uMUL ⇒ match u2 with [ uMUL ⇒ true | _ ⇒ false ]
- | uNEG ⇒ match u2 with [ uNEG ⇒ true | _ ⇒ false ]
- | uNOP ⇒ match u2 with [ uNOP ⇒ true | _ ⇒ false ]
- | uNSA ⇒ match u2 with [ uNSA ⇒ true | _ ⇒ false ]
- | uORA ⇒ match u2 with [ uORA ⇒ true | _ ⇒ false ]
- | uPSHA ⇒ match u2 with [ uPSHA ⇒ true | _ ⇒ false ]
- | uPSHH ⇒ match u2 with [ uPSHH ⇒ true | _ ⇒ false ]
- | uPSHX ⇒ match u2 with [ uPSHX ⇒ true | _ ⇒ false ]
- | uPULA ⇒ match u2 with [ uPULA ⇒ true | _ ⇒ false ]
- | uPULH ⇒ match u2 with [ uPULH ⇒ true | _ ⇒ false ]
- | uPULX ⇒ match u2 with [ uPULX ⇒ true | _ ⇒ false ]
- | uROL ⇒ match u2 with [ uROL ⇒ true | _ ⇒ false ]
- | uROR ⇒ match u2 with [ uROR ⇒ true | _ ⇒ false ]
- | uRSP ⇒ match u2 with [ uRSP ⇒ true | _ ⇒ false ]
- | uRTI ⇒ match u2 with [ uRTI ⇒ true | _ ⇒ false ]
- | uRTS ⇒ match u2 with [ uRTS ⇒ true | _ ⇒ false ]
- | uSBC ⇒ match u2 with [ uSBC ⇒ true | _ ⇒ false ]
- | uSEC ⇒ match u2 with [ uSEC ⇒ true | _ ⇒ false ]
- | uSEI ⇒ match u2 with [ uSEI ⇒ true | _ ⇒ false ]
- | uSHA ⇒ match u2 with [ uSHA ⇒ true | _ ⇒ false ]
- | uSLA ⇒ match u2 with [ uSLA ⇒ true | _ ⇒ false ]
- | uSTA ⇒ match u2 with [ uSTA ⇒ true | _ ⇒ false ]
- | uSTHX ⇒ match u2 with [ uSTHX ⇒ true | _ ⇒ false ]
- | uSTOP ⇒ match u2 with [ uSTOP ⇒ true | _ ⇒ false ]
- | uSTX ⇒ match u2 with [ uSTX ⇒ true | _ ⇒ false ]
- | uSUB ⇒ match u2 with [ uSUB ⇒ true | _ ⇒ false ]
- | uSWI ⇒ match u2 with [ uSWI ⇒ true | _ ⇒ false ]
- | uTAP ⇒ match u2 with [ uTAP ⇒ true | _ ⇒ false ]
- | uTAX ⇒ match u2 with [ uTAX ⇒ true | _ ⇒ false ]
- | uTPA ⇒ match u2 with [ uTPA ⇒ true | _ ⇒ false ]
- | uTST ⇒ match u2 with [ uTST ⇒ true | _ ⇒ false ]
- | uTSX ⇒ match u2 with [ uTSX ⇒ true | _ ⇒ false ]
- | uTXA ⇒ match u2 with [ uTXA ⇒ true | _ ⇒ false ]
- | uTXS ⇒ match u2 with [ uTXS ⇒ true | _ ⇒ false ]
- | uWAIT ⇒ match u2 with [ uWAIT ⇒ true | _ ⇒ false ]
-
- ].
-
(* costruttore di un sottouniverso:
S_EL cioe' uno qualsiasi degli elementi del sottouniverso
- S_KO cioe' il caso impossibile
*)
-ninductive S_UN (l:list UN) : Type ≝
- S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l
-| S_KO : False → S_UN l.
+ninductive S_UN (l:ne_list nat) : Type ≝
+ S_EL : Πx:nat.((member_natList x l) = true) → S_UN l.
-ndefinition getelem : ∀l.∀e:S_UN l.UN.
+ndefinition getelem : ∀l.∀e:S_UN l.nat.
#l; #s; nelim s;
- ##[ ##1: #u; #dim1; #dim2; napply u
- ##| ##2: #F; nelim F
- ##]
+ #u; #dim;
+ napply u.
nqed.
-ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y).
-
-ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true.
- #l; #s; nelim s;
- ##[ ##2: #F; nelim F
- ##| ##1: #u; #dim1; #dim2; napply dim1
- ##]
-nqed.
+ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_nat (getelem ? x) (getelem ? y).
-ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y).
+ndefinition getdim : ∀l.∀e:S_UN l.member_natList (getelem ? e) l = true.
#l; #s; nelim s;
- ##[ ##2: #F; nelim F
- ##| ##1: #u; #dim1; #dim2; napply dim2
- ##]
+ #u; #dim;
+ napply dim.
nqed.
nlemma SUN_destruct_1
- : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2.
- #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H;
- nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]);
+ : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
+ #l; #e1; #e2; #dim1; #dim2; #H;
+ nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a ]);
nrewrite < H;
nnormalize;
napply refl_eq.
nqed.
-ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P | false ⇒ P ].
- #x; #y; #P; #H;
- nrewrite > H;
- nelim y;
- nnormalize;
- napply (λx.x).
-nqed.
-
+(* destruct universale *)
ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ].
#l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22; #P;
- nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
- #H; napply (UN_destruct u1 u2);
- napply (SUN_destruct_1 l … H)
- ##]
- ##]
-nqed.
-
-nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
- #e1; #e2; #H;
- nrewrite > H;
- nelim e2;
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ #P;
+ nchange with (? → (match eq_nat u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
+ #H;
+ nrewrite > (SUN_destruct_1 l … H);
+ nrewrite > (eq_to_eqnat u2 u2 (refl_eq …));
nnormalize;
- napply refl_eq.
+ napply (λx.x).
nqed.
+(* eq_to_eqxx universale *)
nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
#l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- nchange with (? → eq_UN u1 u2 = true);
- #H; napply (eq_to_eqUN u1 u2);
- napply (SUN_destruct_1 l … H)
- ##]
- ##]
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ nchange with (? → eq_nat u1 u2 = true);
+ #H; napply (eq_to_eqnat u1 u2);
+ napply (SUN_destruct_1 l … H).
nqed.
-nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
- #e1; #e2; #H;
- napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …);
- ##[ ##1: napply (eq_to_eqUN e1 e2)
+(* neqxx_to_neq universale *)
+nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
+ #l; #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_SUN l n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqSUN l n1 n2)
##| ##2: napply (eqfalse_to_neqtrue … H)
##]
nqed.
-nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- nchange with ((eq_UN u1 u2 = false) → ?);
- #H; nnormalize; #H1;
- napply (neqUN_to_neq u1 u2 H);
- napply (SUN_destruct_1 l … H1)
- ##]
- ##]
+(* perche' non si riesce a dimstrare ??? *
+nlemma SUN_construct
+ : ∀l.∀u.
+ ∀dim1,dim2:(member_natList u l = true).
+ ((S_EL l u dim1) = (S_EL l u dim2)).
+ #l; #u; #dim1; #dim2;
+ nchange with (S_EL l u dim1 = S_EL l u dim1);
+ napply refl_eq.
nqed.
-
+*)
naxiom SUN_construct
: ∀l.∀u.
- ∀dim11,dim21:(member_list UN u eq_UN l = true).
- ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)).
- ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)).
+ ∀dim1,dim2:(member_natList u l = true).
+ ((S_EL l u dim1) = (S_EL l u dim2)).
nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
#l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- nchange with (u1 = u2 → ?); #H;
- nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12;
- napply (SUN_construct l u2 dim11 dim21 dim12 dim22);
- ##]
- ##]
-nqed.
-
-nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22; #H;
- napply (not_to_not ((getelem l ?) = (getelem l ?))
- ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?);
- ##[ ##1: napply H
- ##| ##2: napply (eqgetelem_to_eq l …)
- ##]
- ##]
- ##]
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ nchange with (u1 = u2 → ?);
+ #H;
+ nrewrite > H in dim1:(%) ⊢ %;
+ #dim1;
+ napply (SUN_construct l u2 dim1 dim2).
nqed.
+(* eqxx_to_eq universale *)
nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
#l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- nchange with ((eq_UN u1 u2 = true) → ?); #H;
- nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H));
- napply refl_eq
- ##]
- ##]
+ #u1; #dim1;
+ #y; nelim y;
+ #u2; #dim2;
+ nchange with ((eq_nat u1 u2 = true) → ?);
+ #H;
+ nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim1) (S_EL l u2 dim2) (eqnat_to_eq u1 u2 H));
+ napply refl_eq.
nqed.
+(* neq_to_neqxx universale *)
nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22; #H;
- napply neqtrue_to_eqfalse;
- napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ;
- napply H
- ##]
- ##]
+ #l; #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_SUN l n1 n2));
+ napply (not_to_not (eq_SUN l n1 n2 = true) (n1 = n2) ? H);
+ napply (eqSUN_to_eq l n1 n2).
nqed.
+(* decidibilita' universale *)
nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22; nnormalize;
- napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))));
- ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H))
- ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H))
+ #l; #x; #y; nnormalize;
+ napply (or2_elim (eq_SUN l x y = true) (eq_SUN l x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqSUN_to_eq l … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqSUN_to_neq l … H))
##]
nqed.
+(* simmetria di uguaglianza universale *)
nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
- #l; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim21; #dim22;
- napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)));
+ #l; #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_SUN l n1 n2));
##[ ##1: #H; nrewrite > H; napply refl_eq
- ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H);
- napply (symmetric_eq ? (eq_SUN l ??) false);
- napply (neq_to_neqSUN l … (symmetric_neq … H))
+ ##| ##2: #H; nrewrite > (neq_to_neqSUN l n1 n2 H);
+ napply (symmetric_eq ? (eq_SUN l n2 n1) false);
+ napply (neq_to_neqSUN l n2 n1 (symmetric_neq ? n1 n2 H))
##]
nqed.
+
+(* scheletro di funzione generica ad 1 argomento *)
+nlet rec farg1_auxT (T:Type) (l:ne_list nat) on l ≝
+ match l with
+ [ ne_nil _ ⇒ T
+ | ne_cons _ t ⇒ ProdT T (farg1_auxT T t)
+ ].
+
+nlemma farg1_auxDim : ∀h,t,x.eq_nat x h = false → member_natList x (h§§t) = true → member_natList x t = true.
+ #h; #t; #x; #H; #H1;
+ nnormalize in H1:(%);
+ nrewrite > H in H1:(%);
+ nnormalize;
+ napply (λx.x).
+nqed.
+
+nlet rec farg1 (T:Type) (l:ne_list nat) on l ≝
+ match l with
+ [ ne_nil h ⇒ λarg:farg1_auxT T «£h».λx:S_UN «£h».arg
+ | ne_cons h t ⇒ λarg:farg1_auxT T (h§§t).λx:S_UN (h§§t).
+ match eq_nat (getelem ? x) h
+ return λy.eq_nat (getelem ? x) h = y → ?
+ with
+ [ true ⇒ λp:(eq_nat (getelem ? x) h = true).fst … arg
+ | false ⇒ λp:(eq_nat (getelem ? x) h = false).
+ farg1 T t
+ (snd … arg)
+ (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
+ ] (refl_eq ? (eq_nat (getelem ? x) h))
+ ].
+
+(* scheletro di funzione generica a 2 argomenti *)
+nlet rec farg2 (T:Type) (l,lfix:ne_list nat) on l ≝
+ match l with
+ [ ne_nil h ⇒ λarg:farg1_auxT (farg1_auxT T lfix) «£h».λx:S_UN «£h».farg1 T lfix arg
+ | ne_cons h t ⇒ λarg:farg1_auxT (farg1_auxT T lfix) (h§§t).λx:S_UN (h§§t).
+ match eq_nat (getelem ? x) h
+ return λy.eq_nat (getelem ? x) h = y → ?
+ with
+ [ true ⇒ λp:(eq_nat (getelem ? x) h = true).farg1 T lfix (fst … arg)
+ | false ⇒ λp:(eq_nat (getelem ? x) h = false).
+ farg2 T t lfix
+ (snd … arg)
+ (S_EL t (getelem ? x) (farg1_auxDim h t (getelem ? x) p (getdim ? x)))
+ ] (refl_eq ? (eq_nat (getelem ? x) h))
+ ].
+
+(* esempio0: universo ottale *)
+ndefinition oct0 ≝ O.
+ndefinition oct1 ≝ S O.
+ndefinition oct2 ≝ S (S O).
+ndefinition oct3 ≝ S (S (S O)).
+ndefinition oct4 ≝ S (S (S (S O))).
+ndefinition oct5 ≝ S (S (S (S (S O)))).
+ndefinition oct6 ≝ S (S (S (S (S (S O))))).
+ndefinition oct7 ≝ S (S (S (S (S (S (S O)))))).
+
+ndefinition oct_UN ≝ « oct0 ; oct1 ; oct2 ; oct3 ; oct4 ; oct5 ; oct6 £ oct7 ».
+
+ndefinition uoct0 ≝ S_EL oct_UN oct0 (refl_eq …).
+ndefinition uoct1 ≝ S_EL oct_UN oct1 (refl_eq …).
+ndefinition uoct2 ≝ S_EL oct_UN oct2 (refl_eq …).
+ndefinition uoct3 ≝ S_EL oct_UN oct3 (refl_eq …).
+ndefinition uoct4 ≝ S_EL oct_UN oct4 (refl_eq …).
+ndefinition uoct5 ≝ S_EL oct_UN oct5 (refl_eq …).
+ndefinition uoct6 ≝ S_EL oct_UN oct6 (refl_eq …).
+ndefinition uoct7 ≝ S_EL oct_UN oct7 (refl_eq …).
+
+(* esempio1: NOT ottale *)
+ndefinition octNOT ≝
+ farg1 (S_UN oct_UN) oct_UN
+ (pair … uoct7 (pair … uoct6 (pair … uoct5 (pair … uoct4 (pair … uoct3 (pair … uoct2 (pair … uoct1 uoct0))))))).
+
+(* esempio2: AND ottale *)
+ndefinition octAND0 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 uoct0)))))).
+ndefinition octAND1 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct0 uoct1)))))).
+ndefinition octAND2 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct0 (pair … uoct0 (pair … uoct2 uoct2)))))).
+ndefinition octAND3 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct0 (pair … uoct1 (pair … uoct2 uoct3)))))).
+ndefinition octAND4 ≝ pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct0 (pair … uoct4 (pair … uoct4 (pair … uoct4 uoct4)))))).
+ndefinition octAND5 ≝ pair … uoct0 (pair … uoct1 (pair … uoct0 (pair … uoct1 (pair … uoct4 (pair … uoct5 (pair … uoct4 uoct5)))))).
+ndefinition octAND6 ≝ pair … uoct0 (pair … uoct0 (pair … uoct2 (pair … uoct2 (pair … uoct4 (pair … uoct4 (pair … uoct6 uoct6)))))).
+ndefinition octAND7 ≝ pair … uoct0 (pair … uoct1 (pair … uoct2 (pair … uoct3 (pair … uoct4 (pair … uoct5 (pair … uoct6 uoct7)))))).
+
+ndefinition octAND ≝
+ farg2 (S_UN oct_UN) oct_UN oct_UN
+ (pair … octAND0 (pair … octAND1 (pair … octAND2 (pair … octAND3 (pair … octAND4 (pair … octAND5 (pair … octAND6 octAND7))))))).
+
+(* ora e' possibile fare
+ octNOT uoctX
+ octAND uoctX uoctY
+*)
projects / helm.git / commitdiff