From: Cosimo Oliboni Date: Thu, 3 Sep 2009 06:59:00 +0000 (+0000) Subject: freescale porting, work in progress X-Git-Tag: make_still_working~3504 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a62de71cf6821c955bd41fa691c52ea62173f25d;p=helm.git freescale porting, work in progress --- diff --git a/helm/software/matita/contribs/ng_assembly/common/nat.ma b/helm/software/matita/contribs/ng_assembly/common/nat.ma index 4db935b1e..9188bef9e 100755 --- a/helm/software/matita/contribs/ng_assembly/common/nat.ma +++ b/helm/software/matita/contribs/ng_assembly/common/nat.ma @@ -26,15 +26,17 @@ include "num/bool.ma". (* 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 diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma index bbce188e5..64eeb50f1 100644 --- a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma @@ -51,26 +51,6 @@ nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False. 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; @@ -90,6 +70,14 @@ nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true. ##] 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; @@ -110,53 +98,28 @@ nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2). ##] 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. diff --git a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma index 15afe0a68..b73d1347f 100644 --- a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma @@ -118,12 +118,12 @@ nlemma decidable_pair #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 ##] ##] @@ -143,8 +143,8 @@ nlemma neqpair_to_neq : 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. @@ -156,10 +156,10 @@ nlemma pair_destruct #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 …)) ##] ##] @@ -180,8 +180,8 @@ nlemma neq_to_neqpair : #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. @@ -305,15 +305,15 @@ nlemma decidable_triple #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; @@ -338,9 +338,9 @@ nlemma neqtriple_to_neq : 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. @@ -354,12 +354,12 @@ nlemma triple_destruct #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 …)) ##] @@ -384,9 +384,9 @@ nlemma neq_to_neqtriple : #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. @@ -536,18 +536,18 @@ nlemma decidable_quadruple #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; @@ -575,10 +575,10 @@ nlemma neqquadruple_to_neq : 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. @@ -595,14 +595,14 @@ nlemma quadruple_destruct #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 …)) @@ -631,10 +631,10 @@ nlemma neq_to_neqquadruple : #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. @@ -810,21 +810,21 @@ nlemma decidable_quintuple #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; @@ -855,11 +855,11 @@ nlemma neqquintuple_to_neq : 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. @@ -877,16 +877,16 @@ nlemma quintuple_destruct #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; @@ -921,10 +921,10 @@ nlemma neq_to_neqquintuple : #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. diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index bb7ca3697..92d177c42 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -66,7 +66,7 @@ num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma 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 diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index eb4b32ce3..698736af6 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -314,8 +314,10 @@ ninductive rec_byte8 : byte8 → Type ≝ (* 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 ≝ @@ -329,21 +331,42 @@ ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1 λ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)))))))))))))) ]. (* @@ -355,10 +378,7 @@ nqed. *) 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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma index addc35386..1abaf0599 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -243,100 +243,141 @@ ninductive rec_word16 : word16 → Type ≝ | 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 *) @@ -368,94 +409,320 @@ ndefinition w16_to_recw16_aux3 ≝ | 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 ≝ @@ -479,12 +746,8 @@ 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))) ]]. diff --git a/helm/software/matita/contribs/ng_assembly/universe/ascii.ma b/helm/software/matita/contribs/ng_assembly/universe/ascii.ma deleted file mode 100755 index a16343588..000000000 --- a/helm/software/matita/contribs/ng_assembly/universe/ascii.ma +++ /dev/null @@ -1,105 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/helm/software/matita/contribs/ng_assembly/universe/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/universe/bitrigesim.ma deleted file mode 100755 index bbed39718..000000000 --- a/helm/software/matita/contribs/ng_assembly/universe/bitrigesim.ma +++ /dev/null @@ -1,69 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/helm/software/matita/contribs/ng_assembly/universe/exadecim.ma b/helm/software/matita/contribs/ng_assembly/universe/exadecim.ma deleted file mode 100755 index f51d2ce3b..000000000 --- a/helm/software/matita/contribs/ng_assembly/universe/exadecim.ma +++ /dev/null @@ -1,52 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/helm/software/matita/contribs/ng_assembly/universe/exadecim_lib.ma b/helm/software/matita/contribs/ng_assembly/universe/exadecim_lib.ma deleted file mode 100755 index c034d83b7..000000000 --- a/helm/software/matita/contribs/ng_assembly/universe/exadecim_lib.ma +++ /dev/null @@ -1,354 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. -*) diff --git a/helm/software/matita/contribs/ng_assembly/universe/oct.ma b/helm/software/matita/contribs/ng_assembly/universe/oct.ma deleted file mode 100755 index 4de98f2e3..000000000 --- a/helm/software/matita/contribs/ng_assembly/universe/oct.ma +++ /dev/null @@ -1,44 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/helm/software/matita/contribs/ng_assembly/universe/opcode.ma b/helm/software/matita/contribs/ng_assembly/universe/opcode.ma deleted file mode 100755 index 287d2668e..000000000 --- a/helm/software/matita/contribs/ng_assembly/universe/opcode.ma +++ /dev/null @@ -1,136 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/helm/software/matita/contribs/ng_assembly/universe/quatern.ma b/helm/software/matita/contribs/ng_assembly/universe/quatern.ma deleted file mode 100755 index d4137d6f1..000000000 --- a/helm/software/matita/contribs/ng_assembly/universe/quatern.ma +++ /dev/null @@ -1,40 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/helm/software/matita/contribs/ng_assembly/universe/universe.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma index 2d84b78e5..a673c999b 100755 --- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma +++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma @@ -21,663 +21,242 @@ (* ********************************************************************** *) 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 +*)