napply refl_eq
##]
nqed.
-
-nlemma neq_to_neqoption :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
- (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
- (op1 ≠ op2 → eq_option T op1 op2 f = false).
- #T; #op1; #op2; #f; #H;
- nelim op1;
- nelim op2;
- nnormalize;
- ##[ ##1: #H1; napply False_ind; napply (H1 (refl_eq …))
- ##| ##2,3: #a; #H1; napply refl_eq
- ##| ##4: #a; #a0; #H1;
- napply H;
- napply (neqf_to_neq … a0 a (λx.Some ? x) H1)
- ##]
-nqed.
-
-nlemma neqoption_to_neq :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
- (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
- (eq_option T op1 op2 f = false → op1 ≠ op2).
- #T; #op1; #op2; #f; #H;
- nelim op1;
- nelim op2;
- nnormalize;
- ##[ ##1: #H1; napply (bool_destruct … H1)
- ##| ##2: #a; #H1; #H2; napply (option_destruct_none_some ? a H2)
- ##| ##3: #a; #H1; #H2; napply (option_destruct_some_none ? a H2)
- ##| ##4: #a; #a0; #H1; #H2;
- napply (H a0 a H1);
- napply (option_destruct_some_some ? a0 a H2)
- ##]
-nqed.
napply (H1 H).
nqed.
-(*
-naxiom RAA : ∀P:Prop.∀f:(¬P) → False.P.
-
-nlemma nnprop_to_prop : ∀P.(¬¬P) → P.
- #P; nchange with (((¬P) → False) → P);
- #H; napply (RAA P H).
-nqed.
-*)
-
ninductive And (A,B:Prop) : Prop ≝
conj : A → B → (And A B).
ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
-(*
-nlemma decidable_prop : ∀P:Prop.decidable P.
- #P; nnormalize;
- napply RAA;
- #H;
- napply (absurd (P ∨ (¬P)) …);
- ##[ ##2: napply H
- ##| ##1: napply (or_intror P (¬P));
- napply RAA;
- #H1;
- napply (absurd (P ∨ (¬P)) …);
- ##[ ##2: napply H
- ##| ##1: napply (or_introl P (¬P));
- napply (nnprop_to_prop P H1)
- ##]
- ##]
-nqed.
-
-nlemma terzo_escluso : ∀P,G:Prop.∀ft:P → G.∀ff:(¬P) → G.G.
- #P; #G; nnormalize;
- #H; #H1;
- napply (Or_ind P (P → False) ? H H1 ?);
- napply (decidable_prop P).
-nqed.
-*)
-
nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
#P; #Q; #G; #H; #H1; #H2;
napply (Or_ind P Q ? H1 H2 ?);
napply (H (eq_f … H1)).
nqed.
-(*
-nlemma neqf2_to_neq : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.f x1 x2 ≠ f y1 y2 → (x1 ≠ y1) ∨ (x2 ≠ y2).
- #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; nnormalize; #H;
- napply (terzo_escluso (x1 = y1) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (terzo_escluso (x2 = y2) …)
- ##[ ##2: #H2; napply (or_intror … H2)
- ##| ##1: #H2; nrewrite < H1 in H:(%);
- nrewrite < H2; #H;
- nelim (H (refl_eq …))
- ##]
- ##]
-nqed.
-*)
-
nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
#A;
nnormalize;
+num/word32.ma num/word16.ma
num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
common/option.ma num/bool.ma
+num/word16.ma num/byte8.ma
+num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma
+num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
test_errori.ma
common/theory.ma
+num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma
num/quatern.ma num/bool.ma
common/prod.ma num/bool.ma
+num/byte8.ma num/bitrigesim.ma num/exadecim.ma
num/bool.ma common/theory.ma
num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
+num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma
common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma
+num/bitrigesim.ma num/bool.ma
num/bool_lemmas.ma num/bool.ma
num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
num/oct.ma num/bool.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ************* *)
+(* BITRIGESIMALI *)
+(* ************* *)
+
+ninductive bitrigesim : Type ≝
+ t00: bitrigesim
+| t01: bitrigesim
+| t02: bitrigesim
+| t03: bitrigesim
+| t04: bitrigesim
+| t05: bitrigesim
+| t06: bitrigesim
+| t07: bitrigesim
+| t08: bitrigesim
+| t09: bitrigesim
+| t0A: bitrigesim
+| t0B: bitrigesim
+| t0C: bitrigesim
+| t0D: bitrigesim
+| t0E: bitrigesim
+| t0F: bitrigesim
+| t10: bitrigesim
+| t11: bitrigesim
+| t12: bitrigesim
+| t13: bitrigesim
+| t14: bitrigesim
+| t15: bitrigesim
+| t16: bitrigesim
+| t17: bitrigesim
+| t18: bitrigesim
+| t19: bitrigesim
+| t1A: bitrigesim
+| t1B: bitrigesim
+| t1C: bitrigesim
+| t1D: bitrigesim
+| t1E: bitrigesim
+| t1F: bitrigesim.
+
+(* operatore = *)
+ndefinition eq_bit ≝
+λt1,t2:bitrigesim.
+ match t1 with
+ [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ]
+ | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
+ | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ]
+ | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
+ | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ]
+ | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
+ | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ]
+ | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
+ | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ]
+ | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
+ | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ]
+ | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
+ | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ]
+ | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
+ | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ]
+ | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
+ | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ]
+ | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
+ | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ]
+ | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
+ | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ]
+ | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
+ | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ]
+ | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
+ | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ]
+ | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
+ | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ]
+ | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
+ | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ]
+ | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
+ | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ]
+ | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
+ ].
+
+(* iteratore sui bitrigesimali *)
+ndefinition forall_bit ≝ λP.
+ P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
+ P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
+ P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
+ P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.
+
+(* operatore successore *)
+ndefinition succ_bit ≝
+λn.match n with
+ [ t00 ⇒ t01 | t01 ⇒ t02 | t02 ⇒ t03 | t03 ⇒ t04 | t04 ⇒ t05 | t05 ⇒ t06 | t06 ⇒ t07 | t07 ⇒ t08
+ | t08 ⇒ t09 | t09 ⇒ t0A | t0A ⇒ t0B | t0B ⇒ t0C | t0C ⇒ t0D | t0D ⇒ t0E | t0E ⇒ t0F | t0F ⇒ t10
+ | t10 ⇒ t11 | t11 ⇒ t12 | t12 ⇒ t13 | t13 ⇒ t14 | t14 ⇒ t15 | t15 ⇒ t16 | t16 ⇒ t17 | t17 ⇒ t18
+ | t18 ⇒ t19 | t19 ⇒ t1A | t1A ⇒ t1B | t1B ⇒ t1C | t1C ⇒ t1D | t1D ⇒ t1E | t1E ⇒ t1F | t1F ⇒ t00
+ ].
+
+(* bitrigesimali ricorsivi *)
+ninductive rec_bitrigesim : bitrigesim → Type ≝
+ bi_O : rec_bitrigesim t00
+| bi_S : ∀n.rec_bitrigesim n → rec_bitrigesim (succ_bit n).
+
+(* bitrigesimali → bitrigesimali ricorsivi *)
+ndefinition bit_to_recbit ≝
+λn.match n return λx.rec_bitrigesim x with
+ [ t00 ⇒ bi_O
+ | t01 ⇒ bi_S ? bi_O
+ | t02 ⇒ bi_S ? (bi_S ? bi_O)
+ | t03 ⇒ bi_S ? (bi_S ? (bi_S ? bi_O))
+ | t04 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))
+ | t05 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))
+ | t06 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))
+ | t07 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))
+ | t08 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ bi_O)))))))
+ | t09 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? bi_O))))))))
+ | t0A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? bi_O)))))))))
+ | t0B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))
+ | t0C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))
+ | t0D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))
+ | t0E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))
+ | t0F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))
+ | t10 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ bi_O)))))))))))))))
+ | t11 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? bi_O))))))))))))))))
+ | t12 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? bi_O)))))))))))))))))
+ | t13 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))
+ | t14 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))
+ | t15 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))
+ | t16 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))
+ | t17 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))
+ | t18 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ bi_O)))))))))))))))))))))))
+ | t19 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? bi_O))))))))))))))))))))))))
+ | t1A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))
+ | t1B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))
+ | t1C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))
+ | t1D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))
+ | t1E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))))
+ | t1F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
+ (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))))
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bitrigesim.ma".
+include "num/bool_lemmas.ma".
+
+(* ************* *)
+(* BITRIGESIMALI *)
+(* ************* *)
+
+ndefinition bitrigesim_destruct1 :
+Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct2 :
+Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct3 :
+Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct4 :
+Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct5 :
+Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct6 :
+Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct7 :
+Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct8 :
+Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct9 :
+Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##9: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct10 :
+Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##10: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct11 :
+Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##11: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct12 :
+Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##12: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct13 :
+Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##13: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct14 :
+Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##14: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct15 :
+Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##15: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct16 :
+Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##16: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct17 :
+Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##17: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct18 :
+Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##18: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct19 :
+Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##19: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct20 :
+Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##20: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct21 :
+Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##21: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct22 :
+Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##22: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct23 :
+Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##23: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct24 :
+Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##24: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct25 :
+Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##25: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct26 :
+Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##26: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct27 :
+Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##27: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct28 :
+Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##28: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct29 :
+Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##29: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct30 :
+Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##30: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct31 :
+Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##31: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct32 :
+Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ].
+ #t2; #P;
+ ncases t2;
+ nnormalize; #H;
+ ##[ ##32: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition bitrigesim_destruct_aux ≝
+Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
+ match t1 with
+ [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
+ | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
+ | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
+ | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
+ | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
+ | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
+ | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
+ | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
+ | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
+ | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
+ | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
+ | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
+ | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
+ | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
+ | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
+ | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
+ | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
+ | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
+ | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
+ | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
+ | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
+ | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
+ | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
+ | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
+ | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
+ | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
+ | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
+ | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
+ | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
+ | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
+ | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
+ | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
+ ].
+
+ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
+ #t1;
+ ncases t1;
+ ##[ ##1: napply bitrigesim_destruct1
+ ##| ##2: napply bitrigesim_destruct2
+ ##| ##3: napply bitrigesim_destruct3
+ ##| ##4: napply bitrigesim_destruct4
+ ##| ##5: napply bitrigesim_destruct5
+ ##| ##6: napply bitrigesim_destruct6
+ ##| ##7: napply bitrigesim_destruct7
+ ##| ##8: napply bitrigesim_destruct8
+ ##| ##9: napply bitrigesim_destruct9
+ ##| ##10: napply bitrigesim_destruct10
+ ##| ##11: napply bitrigesim_destruct11
+ ##| ##12: napply bitrigesim_destruct12
+ ##| ##13: napply bitrigesim_destruct13
+ ##| ##14: napply bitrigesim_destruct14
+ ##| ##15: napply bitrigesim_destruct15
+ ##| ##16: napply bitrigesim_destruct16
+ ##| ##17: napply bitrigesim_destruct17
+ ##| ##18: napply bitrigesim_destruct18
+ ##| ##19: napply bitrigesim_destruct19
+ ##| ##20: napply bitrigesim_destruct20
+ ##| ##21: napply bitrigesim_destruct21
+ ##| ##22: napply bitrigesim_destruct22
+ ##| ##23: napply bitrigesim_destruct23
+ ##| ##24: napply bitrigesim_destruct24
+ ##| ##25: napply bitrigesim_destruct25
+ ##| ##26: napply bitrigesim_destruct26
+ ##| ##27: napply bitrigesim_destruct27
+ ##| ##28: napply bitrigesim_destruct28
+ ##| ##29: napply bitrigesim_destruct29
+ ##| ##30: napply bitrigesim_destruct30
+ ##| ##31: napply bitrigesim_destruct31
+ ##| ##32: napply bitrigesim_destruct32
+ ##]
+nqed.
+
+nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
+ #t1;
+ nelim t1;
+ ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq
+ ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq
+ ##]
+nqed.
+
+nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
+ #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
+nqed.
+
+nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
+ #t1;
+ ncases t1;
+ ##[ ##1: napply eqbit_to_eq1
+ ##| ##2: napply eqbit_to_eq2
+ ##| ##3: napply eqbit_to_eq3
+ ##| ##4: napply eqbit_to_eq4
+ ##| ##5: napply eqbit_to_eq5
+ ##| ##6: napply eqbit_to_eq6
+ ##| ##7: napply eqbit_to_eq7
+ ##| ##8: napply eqbit_to_eq8
+ ##| ##9: napply eqbit_to_eq9
+ ##| ##10: napply eqbit_to_eq10
+ ##| ##11: napply eqbit_to_eq11
+ ##| ##12: napply eqbit_to_eq12
+ ##| ##13: napply eqbit_to_eq13
+ ##| ##14: napply eqbit_to_eq14
+ ##| ##15: napply eqbit_to_eq15
+ ##| ##16: napply eqbit_to_eq16
+ ##| ##17: napply eqbit_to_eq17
+ ##| ##18: napply eqbit_to_eq18
+ ##| ##19: napply eqbit_to_eq19
+ ##| ##20: napply eqbit_to_eq20
+ ##| ##21: napply eqbit_to_eq21
+ ##| ##22: napply eqbit_to_eq22
+ ##| ##23: napply eqbit_to_eq23
+ ##| ##24: napply eqbit_to_eq24
+ ##| ##25: napply eqbit_to_eq25
+ ##| ##26: napply eqbit_to_eq26
+ ##| ##27: napply eqbit_to_eq27
+ ##| ##28: napply eqbit_to_eq28
+ ##| ##29: napply eqbit_to_eq29
+ ##| ##30: napply eqbit_to_eq30
+ ##| ##31: napply eqbit_to_eq31
+ ##| ##32: napply eqbit_to_eq32
+ ##]
+nqed.
+
+nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
+ #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
+nqed.
+
+nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
+ #t1;
+ ncases t1;
+ ##[ ##1: napply eq_to_eqbit1
+ ##| ##2: napply eq_to_eqbit2
+ ##| ##3: napply eq_to_eqbit3
+ ##| ##4: napply eq_to_eqbit4
+ ##| ##5: napply eq_to_eqbit5
+ ##| ##6: napply eq_to_eqbit6
+ ##| ##7: napply eq_to_eqbit7
+ ##| ##8: napply eq_to_eqbit8
+ ##| ##9: napply eq_to_eqbit9
+ ##| ##10: napply eq_to_eqbit10
+ ##| ##11: napply eq_to_eqbit11
+ ##| ##12: napply eq_to_eqbit12
+ ##| ##13: napply eq_to_eqbit13
+ ##| ##14: napply eq_to_eqbit14
+ ##| ##15: napply eq_to_eqbit15
+ ##| ##16: napply eq_to_eqbit16
+ ##| ##17: napply eq_to_eqbit17
+ ##| ##18: napply eq_to_eqbit18
+ ##| ##19: napply eq_to_eqbit19
+ ##| ##20: napply eq_to_eqbit20
+ ##| ##21: napply eq_to_eqbit21
+ ##| ##22: napply eq_to_eqbit22
+ ##| ##23: napply eq_to_eqbit23
+ ##| ##24: napply eq_to_eqbit24
+ ##| ##25: napply eq_to_eqbit25
+ ##| ##26: napply eq_to_eqbit26
+ ##| ##27: napply eq_to_eqbit27
+ ##| ##28: napply eq_to_eqbit28
+ ##| ##29: napply eq_to_eqbit29
+ ##| ##30: napply eq_to_eqbit30
+ ##| ##31: napply eq_to_eqbit31
+ ##| ##32: napply eq_to_eqbit32
+ ##]
+nqed.
##]
nqed.
-nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2).
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,4: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (bool_destruct … H1)
- ##]
-nqed.
-
-nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false.
+nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
#b1; #b2;
ncases b1;
ncases b2;
nnormalize;
- ##[ ##1,4: #H; napply False_ind; napply (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
+ ##[ ##1,2: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
##]
nqed.
-nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
+nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
#b1; #b2;
ncases b1;
ncases b2;
nnormalize;
- ##[ ##1,2: #H; napply refl_eq
+ ##[ ##1,3: #H; napply refl_eq
##| ##*: #H; napply (bool_destruct … H)
##]
nqed.
-nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
+nlemma andb_false : ∀b1,b2.(b1 ⊗ b2) = false → (b1 = false) ∨ (b2 = false).
#b1; #b2;
ncases b1;
ncases b2;
nnormalize;
- ##[ ##1,3: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##2,4: #H; napply (or_intror … H)
+ ##| ##3: #H; napply (or_introl … H)
##]
nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/exadecim.ma".
+include "num/bitrigesim.ma".
+
+(* **** *)
+(* BYTE *)
+(* **** *)
+
+nrecord byte8 : Type ≝
+ {
+ b8h: exadecim;
+ b8l: exadecim
+ }.
+
+(* \langle \rangle *)
+notation "〈x,y〉" non associative with precedence 80
+ for @{ 'mk_byte8 $x $y }.
+interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
+
+(* operatore = *)
+ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
+
+(* operatore < *)
+ndefinition lt_b8 ≝
+λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with
+ [ true ⇒ true
+ | false ⇒ match gt_ex (b8h b1) (b8h b2) with
+ [ true ⇒ false
+ | false ⇒ lt_ex (b8l b1) (b8l b2) ]].
+
+(* operatore ≤ *)
+ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2).
+
+(* operatore > *)
+ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2).
+
+(* operatore ≥ *)
+ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2).
+
+(* operatore and *)
+ndefinition and_b8 ≝
+λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)).
+
+(* operatore or *)
+ndefinition or_b8 ≝
+λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)).
+
+(* operatore xor *)
+ndefinition xor_b8 ≝
+λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)).
+
+(* operatore rotazione destra con carry *)
+ndefinition rcr_b8 ≝
+λb:byte8.λc:bool.match rcr_ex (b8h b) c with
+ [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
+ [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
+
+(* operatore shift destro *)
+ndefinition shr_b8 ≝
+λb:byte8.match rcr_ex (b8h b) false with
+ [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
+ [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
+
+(* operatore rotazione destra *)
+ndefinition ror_b8 ≝
+λb:byte8.match rcr_ex (b8h b) false with
+ [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
+ [ pair bl' c'' ⇒ match c'' with
+ [ true ⇒ mk_byte8 (or_ex x8 bh') bl'
+ | false ⇒ mk_byte8 bh' bl' ]]].
+
+(* operatore rotazione destra n-volte *)
+nlet rec ror_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
+ match r with
+ [ oc_O ⇒ b
+ | oc_S t n' ⇒ ror_b8_n (ror_b8 b) t n' ].
+
+(* operatore rotazione sinistra con carry *)
+ndefinition rcl_b8 ≝
+λb:byte8.λc:bool.match rcl_ex (b8l b) c with
+ [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
+ [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
+
+(* operatore shift sinistro *)
+ndefinition shl_b8 ≝
+λb:byte8.match rcl_ex (b8l b) false with
+ [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
+ [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
+
+(* operatore rotazione sinistra *)
+ndefinition rol_b8 ≝
+λb:byte8.match rcl_ex (b8l b) false with
+ [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
+ [ pair bh' c'' ⇒ match c'' with
+ [ true ⇒ mk_byte8 bh' (or_ex x1 bl')
+ | false ⇒ mk_byte8 bh' bl' ]]].
+
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝
+ match r with
+ [ oc_O ⇒ b
+ | oc_S t n' ⇒ rol_b8_n (rol_b8 b) t n' ].
+
+(* operatore not/complemento a 1 *)
+ndefinition not_b8 ≝
+λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)).
+
+(* operatore somma con data+carry → data+carry *)
+ndefinition plus_b8_dc_dc ≝
+λb1,b2:byte8.λc:bool.
+ match plus_ex_dc_dc (b8l b1) (b8l b2) c with
+ [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
+ [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
+
+(* operatore somma con data+carry → data *)
+ndefinition plus_b8_dc_d ≝
+λb1,b2:byte8.λc:bool.
+ match plus_ex_dc_dc (b8l b1) (b8l b2) c with
+ [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
+
+(* operatore somma con data+carry → c *)
+ndefinition plus_b8_dc_c ≝
+λb1,b2:byte8.λc:bool.
+ plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c).
+
+(* operatore somma con data → data+carry *)
+ndefinition plus_b8_d_dc ≝
+λb1,b2:byte8.
+ match plus_ex_d_dc (b8l b1) (b8l b2) with
+ [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
+ [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
+
+(* operatore somma con data → data *)
+ndefinition plus_b8_d_d ≝
+λb1,b2:byte8.
+ match plus_ex_d_dc (b8l b1) (b8l b2) with
+ [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
+
+(* operatore somma con data → c *)
+ndefinition plus_b8_d_c ≝
+λb1,b2:byte8.
+ plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)).
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)).
+
+(* operatore predecessore *)
+ndefinition pred_b8 ≝
+λb:byte8.match eq_ex (b8l b) x0 with
+ [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b))
+ | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ].
+
+(* operatore successore *)
+ndefinition succ_b8 ≝
+λb:byte8.match eq_ex (b8l b) xF with
+ [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b))
+ | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ].
+
+(* operatore neg/complemento a 2 *)
+ndefinition compl_b8 ≝
+λb:byte8.match MSB_b8 b with
+ [ true ⇒ succ_b8 (not_b8 b)
+ | false ⇒ not_b8 (pred_b8 b) ].
+
+(* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *)
+ndefinition mul_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉
+ | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉
+ | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉
+ | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉
+ | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉
+ | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x9〉 | xA ⇒ 〈x0,xA〉 | xB ⇒ 〈x0,xB〉
+ | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,xD〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,xF〉 ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉
+ | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉
+ | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x1,x2〉 | xA ⇒ 〈x1,x4〉 | xB ⇒ 〈x1,x6〉
+ | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,xA〉 | xE ⇒ 〈x1,xC〉 | xF ⇒ 〈x1,xE〉 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉
+ | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉
+ | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,xB〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x2,x1〉
+ | xC ⇒ 〈x2,x4〉 | xD ⇒ 〈x2,x7〉 | xE ⇒ 〈x2,xA〉 | xF ⇒ 〈x2,xD〉 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉
+ | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉
+ | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x2,x4〉 | xA ⇒ 〈x2,x8〉 | xB ⇒ 〈x2,xC〉
+ | xC ⇒ 〈x3,x0〉 | xD ⇒ 〈x3,x4〉 | xE ⇒ 〈x3,x8〉 | xF ⇒ 〈x3,xC〉 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉
+ | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉
+ | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,xD〉 | xA ⇒ 〈x3,x2〉 | xB ⇒ 〈x3,x7〉
+ | xC ⇒ 〈x3,xC〉 | xD ⇒ 〈x4,x1〉 | xE ⇒ 〈x4,x6〉 | xF ⇒ 〈x4,xB〉 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉
+ | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉
+ | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x3,x6〉 | xA ⇒ 〈x3,xC〉 | xB ⇒ 〈x4,x2〉
+ | xC ⇒ 〈x4,x8〉 | xD ⇒ 〈x4,xE〉 | xE ⇒ 〈x5,x4〉 | xF ⇒ 〈x5,xA〉 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉
+ | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉
+ | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,xF〉 | xA ⇒ 〈x4,x6〉 | xB ⇒ 〈x4,xD〉
+ | xC ⇒ 〈x5,x4〉 | xD ⇒ 〈x5,xB〉 | xE ⇒ 〈x6,x2〉 | xF ⇒ 〈x6,x9〉 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x8〉 | x2 ⇒ 〈x1,x0〉 | x3 ⇒ 〈x1,x8〉
+ | x4 ⇒ 〈x2,x0〉 | x5 ⇒ 〈x2,x8〉 | x6 ⇒ 〈x3,x0〉 | x7 ⇒ 〈x3,x8〉
+ | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x4,x8〉 | xA ⇒ 〈x5,x0〉 | xB ⇒ 〈x5,x8〉
+ | xC ⇒ 〈x6,x0〉 | xD ⇒ 〈x6,x8〉 | xE ⇒ 〈x7,x0〉 | xF ⇒ 〈x7,x8〉 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x9〉 | x2 ⇒ 〈x1,x2〉 | x3 ⇒ 〈x1,xB〉
+ | x4 ⇒ 〈x2,x4〉 | x5 ⇒ 〈x2,xD〉 | x6 ⇒ 〈x3,x6〉 | x7 ⇒ 〈x3,xF〉
+ | x8 ⇒ 〈x4,x8〉 | x9 ⇒ 〈x5,x1〉 | xA ⇒ 〈x5,xA〉 | xB ⇒ 〈x6,x3〉
+ | xC ⇒ 〈x6,xC〉 | xD ⇒ 〈x7,x5〉 | xE ⇒ 〈x7,xE〉 | xF ⇒ 〈x8,x7〉 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xA〉 | x2 ⇒ 〈x1,x4〉 | x3 ⇒ 〈x1,xE〉
+ | x4 ⇒ 〈x2,x8〉 | x5 ⇒ 〈x3,x2〉 | x6 ⇒ 〈x3,xC〉 | x7 ⇒ 〈x4,x6〉
+ | x8 ⇒ 〈x5,x0〉 | x9 ⇒ 〈x5,xA〉 | xA ⇒ 〈x6,x4〉 | xB ⇒ 〈x6,xE〉
+ | xC ⇒ 〈x7,x8〉 | xD ⇒ 〈x8,x2〉 | xE ⇒ 〈x8,xC〉 | xF ⇒ 〈x9,x6〉 ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xB〉 | x2 ⇒ 〈x1,x6〉 | x3 ⇒ 〈x2,x1〉
+ | x4 ⇒ 〈x2,xC〉 | x5 ⇒ 〈x3,x7〉 | x6 ⇒ 〈x4,x2〉 | x7 ⇒ 〈x4,xD〉
+ | x8 ⇒ 〈x5,x8〉 | x9 ⇒ 〈x6,x3〉 | xA ⇒ 〈x6,xE〉 | xB ⇒ 〈x7,x9〉
+ | xC ⇒ 〈x8,x4〉 | xD ⇒ 〈x8,xF〉 | xE ⇒ 〈x9,xA〉 | xF ⇒ 〈xA,x5〉 ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xC〉 | x2 ⇒ 〈x1,x8〉 | x3 ⇒ 〈x2,x4〉
+ | x4 ⇒ 〈x3,x0〉 | x5 ⇒ 〈x3,xC〉 | x6 ⇒ 〈x4,x8〉 | x7 ⇒ 〈x5,x4〉
+ | x8 ⇒ 〈x6,x0〉 | x9 ⇒ 〈x6,xC〉 | xA ⇒ 〈x7,x8〉 | xB ⇒ 〈x8,x4〉
+ | xC ⇒ 〈x9,x0〉 | xD ⇒ 〈x9,xC〉 | xE ⇒ 〈xA,x8〉 | xF ⇒ 〈xB,x4〉 ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xD〉 | x2 ⇒ 〈x1,xA〉 | x3 ⇒ 〈x2,x7〉
+ | x4 ⇒ 〈x3,x4〉 | x5 ⇒ 〈x4,x1〉 | x6 ⇒ 〈x4,xE〉 | x7 ⇒ 〈x5,xB〉
+ | x8 ⇒ 〈x6,x8〉 | x9 ⇒ 〈x7,x5〉 | xA ⇒ 〈x8,x2〉 | xB ⇒ 〈x8,xF〉
+ | xC ⇒ 〈x9,xC〉 | xD ⇒ 〈xA,x9〉 | xE ⇒ 〈xB,x6〉 | xF ⇒ 〈xC,x3〉 ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xE〉 | x2 ⇒ 〈x1,xC〉 | x3 ⇒ 〈x2,xA〉
+ | x4 ⇒ 〈x3,x8〉 | x5 ⇒ 〈x4,x6〉 | x6 ⇒ 〈x5,x4〉 | x7 ⇒ 〈x6,x2〉
+ | x8 ⇒ 〈x7,x0〉 | x9 ⇒ 〈x7,xE〉 | xA ⇒ 〈x8,xC〉 | xB ⇒ 〈x9,xA〉
+ | xC ⇒ 〈xA,x8〉 | xD ⇒ 〈xB,x6〉 | xE ⇒ 〈xC,x4〉 | xF ⇒ 〈xD,x2〉 ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xF〉 | x2 ⇒ 〈x1,xE〉 | x3 ⇒ 〈x2,xD〉
+ | x4 ⇒ 〈x3,xC〉 | x5 ⇒ 〈x4,xB〉 | x6 ⇒ 〈x5,xA〉 | x7 ⇒ 〈x6,x9〉
+ | x8 ⇒ 〈x7,x8〉 | x9 ⇒ 〈x8,x7〉 | xA ⇒ 〈x9,x6〉 | xB ⇒ 〈xA,x5〉
+ | xC ⇒ 〈xB,x4〉 | xD ⇒ 〈xC,x3〉 | xE ⇒ 〈xD,x2〉 | xF ⇒ 〈xE,x1〉 ]
+ ].
+
+(* correzione per somma su BCD *)
+(* input: halfcarry,carry,X(BCD+BCD) *)
+(* output: X',carry' *)
+ndefinition daa_b8 ≝
+λh,c:bool.λX:byte8.
+ match lt_b8 X 〈x9,xA〉 with
+ (* [X:0x00-0x99] *)
+ (* c' = c *)
+ (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00]
+ [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *)
+ [ true ⇒
+ let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
+ [ true ⇒ X
+ | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
+ let X'' ≝ match c with
+ [ true ⇒ plus_b8_d_d X' 〈x6,x0〉
+ | false ⇒ X' ] in
+ pair … X'' c
+ (* [X:0x9A-0xFF] *)
+ (* c' = 1 *)
+ (* X' = [X:0x9A-0xFF]
+ [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60
+ [(b16l X):0xA-0xF] X + 0x6 + 0x60 *)
+ | false ⇒
+ let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with
+ [ true ⇒ X
+ | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in
+ let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in
+ pair … X'' true
+ ].
+
+(* iteratore sui byte *)
+ndefinition forall_b8 ≝
+ λP.
+ forall_ex (λbh.
+ forall_ex (λbl.
+ P (mk_byte8 bh bl))).
+
+(* byte ricorsivi *)
+ninductive rec_byte8 : byte8 → Type ≝
+ b8_O : rec_byte8 〈x0,x0〉
+| b8_S : ∀n.rec_byte8 n → rec_byte8 (succ_b8 n).
+
+(* 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))))))))))))))).
+
+(* ... cifra esadecimale superiore *)
+nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝
+ match r return λx.λy:rec_exadecim x.rec_byte8 〈x,x0〉 with
+ [ ex_O ⇒ b8_O
+ | ex_S t n' ⇒ b8_to_recb8_aux1 ? (b8_to_recb8_aux2 t n')
+ ].
+
+(* ... cifra esadecimale inferiore *)
+ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1,n2〉 ≝
+λ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))))))))))))))
+ ].
+
+ndefinition b8_to_recb8 ≝
+λn.b8_to_recb8_aux3 (b8h n) (b8l n) (b8_to_recb8_aux2 (b8h n) (ex_to_recex (b8h n))).
+
+(* ottali → esadecimali *)
+ndefinition b8_of_bit ≝
+λn.match n with
+ [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉
+ | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉
+ | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉
+ | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉
+ | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉
+ | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉
+ | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
+ | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/byte8.ma".
+include "num/exadecim_lemmas.ma".
+
+(* **** *)
+(* BYTE *)
+(* **** *)
+
+nlemma byte8_destruct_1 :
+∀x1,x2,y1,y2.
+ mk_byte8 x1 y1 = mk_byte8 x2 y2 → x1 = x2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_byte8 x2 y2 with [ mk_byte8 a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma byte8_destruct_2 :
+∀x1,x2,y1,y2.
+ mk_byte8 x1 y1 = mk_byte8 x2 y2 → y1 = y2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_byte8 x2 y2 with [ mk_byte8 _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqb8 : symmetricT byte8 bool eq_b8.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = ((eq_ex e1 e3)⊗(eq_ex e2 e4)));
+ nrewrite > (symmetric_eqex e1 e3);
+ nrewrite > (symmetric_eqex e2 e4);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_andb8 : symmetricT byte8 byte8 and_b8.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with ((mk_byte8 (and_ex e3 e1) (and_ex e4 e2)) = (mk_byte8 (and_ex e1 e3) (and_ex e2 e4)));
+ nrewrite > (symmetric_andex e1 e3);
+ nrewrite > (symmetric_andex e2 e4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_andb8 : ∀b1,b2,b3.(and_b8 (and_b8 b1 b2) b3) = (and_b8 b1 (and_b8 b2 b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nelim b3;
+ #e5; #e6;
+ nchange with (mk_byte8 (and_ex (and_ex e1 e3) e5) (and_ex (and_ex e2 e4) e6) =
+ mk_byte8 (and_ex e1 (and_ex e3 e5)) (and_ex e2 (and_ex e4 e6)));
+ nrewrite < (associative_andex e1 e3 e5);
+ nrewrite < (associative_andex e2 e4 e6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_orb8 : symmetricT byte8 byte8 or_b8.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with ((mk_byte8 (or_ex e3 e1) (or_ex e4 e2)) = (mk_byte8 (or_ex e1 e3) (or_ex e2 e4)));
+ nrewrite > (symmetric_orex e1 e3);
+ nrewrite > (symmetric_orex e2 e4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_orb8 : ∀b1,b2,b3.(or_b8 (or_b8 b1 b2) b3) = (or_b8 b1 (or_b8 b2 b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nelim b3;
+ #e5; #e6;
+ nchange with (mk_byte8 (or_ex (or_ex e1 e3) e5) (or_ex (or_ex e2 e4) e6) =
+ mk_byte8 (or_ex e1 (or_ex e3 e5)) (or_ex e2 (or_ex e4 e6)));
+ nrewrite < (associative_orex e1 e3 e5);
+ nrewrite < (associative_orex e2 e4 e6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_xorb8 : symmetricT byte8 byte8 xor_b8.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange with ((mk_byte8 (xor_ex e3 e1) (xor_ex e4 e2)) = (mk_byte8 (xor_ex e1 e3) (xor_ex e2 e4)));
+ nrewrite > (symmetric_xorex e1 e3);
+ nrewrite > (symmetric_xorex e2 e4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_xorb8 : ∀b1,b2,b3.(xor_b8 (xor_b8 b1 b2) b3) = (xor_b8 b1 (xor_b8 b2 b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nelim b3;
+ #e5; #e6;
+ nchange with (mk_byte8 (xor_ex (xor_ex e1 e3) e5) (xor_ex (xor_ex e2 e4) e6) =
+ mk_byte8 (xor_ex e1 (xor_ex e3 e5)) (xor_ex e2 (xor_ex e4 e6)));
+ nrewrite < (associative_xorex e1 e3 e5);
+ nrewrite < (associative_xorex e2 e4 e6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_dc_dc : ∀b1,b2,c.plus_b8_dc_dc b1 b2 c = plus_b8_dc_dc b2 b1 c.
+ #b1; #b2; #c;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+ match plus_ex_dc_dc e2 e4 c with
+ [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
+ [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
+ match plus_ex_dc_dc e4 e2 c with
+ [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
+ [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
+ nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
+ ncases (plus_ex_dc_dc e2 e4 c);
+ #e5; #c1;
+ nchange with (
+ match plus_ex_dc_dc e1 e3 c1 with
+ [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
+ match plus_ex_dc_dc e3 e1 c1 with
+ [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
+ nrewrite > (symmetric_plusex_dc_dc e1 e3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2 b1 c.
+ #b1; #b2; #c;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+ match plus_ex_dc_dc e2 e4 c with
+ [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
+ match plus_ex_dc_dc e4 e2 c with
+ [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
+ nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
+ ncases (plus_ex_dc_dc e2 e4 c);
+ #e5; #c1;
+ nchange with (〈plus_ex_dc_d e1 e3 c1,e5〉 = 〈plus_ex_dc_d e3 e1 c1,e5〉);
+ nrewrite > (symmetric_plusex_dc_d e1 e3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_dc_c : ∀b1,b2,c.plus_b8_dc_c b1 b2 c = plus_b8_dc_c b2 b1 c.
+ #b1; #b2; #c;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+ plus_ex_dc_c e1 e3 (plus_ex_dc_c e2 e4 c) =
+ plus_ex_dc_c e3 e1 (plus_ex_dc_c e4 e2 c));
+ nrewrite > (symmetric_plusex_dc_c e4 e2 c);
+ nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_dc_c e2 e4 c));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1.
+ #b1; #b2;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+ match plus_ex_d_dc e2 e4 with
+ [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
+ [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
+ match plus_ex_d_dc e4 e2 with
+ [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
+ [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
+ nrewrite > (symmetric_plusex_d_dc e4 e2);
+ ncases (plus_ex_d_dc e2 e4);
+ #e5; #c;
+ nchange with (
+ match plus_ex_dc_dc e1 e3 c with
+ [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
+ match plus_ex_dc_dc e3 e1 c with
+ [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
+ nrewrite > (symmetric_plusex_dc_dc e1 e3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1.
+ #b1; #b2;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+ match plus_ex_d_dc e2 e4 with
+ [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
+ match plus_ex_d_dc e4 e2 with
+ [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
+ nrewrite > (symmetric_plusex_d_dc e4 e2);
+ ncases (plus_ex_d_dc e2 e4);
+ #e5; #c;
+ nchange with (〈plus_ex_dc_d e1 e3 c,e5〉 = 〈plus_ex_dc_d e3 e1 c,e5〉);
+ nrewrite > (symmetric_plusex_dc_d e1 e3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusb8_d_c : ∀b1,b2.plus_b8_d_c b1 b2 = plus_b8_d_c b2 b1.
+ #b1; #b2;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (
+ plus_ex_dc_c e1 e3 (plus_ex_d_c e2 e4) =
+ plus_ex_dc_c e3 e1 (plus_ex_d_c e4 e2));
+ nrewrite > (symmetric_plusex_d_c e4 e2);
+ nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_d_c e2 e4));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_mulex : symmetricT exadecim byte8 mul_ex.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma eqb8_to_eq : ∀b1,b2:byte8.(eq_b8 b1 b2 = true) → (b1 = b2).
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ nchange in ⊢ (% → ?) with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = true);
+ #H;
+ nrewrite < (eqex_to_eq … (andb_true_true_l … H));
+ nrewrite < (eqex_to_eq … (andb_true_true_r … H));
+ napply refl_eq.
+nqed.
+
+nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ #e1; #e2; #e3; #e4;
+ #H;
+ nrewrite < (byte8_destruct_1 … H);
+ nrewrite < (byte8_destruct_2 … H);
+ nchange with (((eq_ex e3 e3)⊗(eq_ex e4 e4)) = true);
+ nrewrite > (eq_to_eqex e3 e3 (refl_eq …));
+ nrewrite > (eq_to_eqex e4 e4 (refl_eq …));
+ nnormalize;
+ napply refl_eq.
+nqed.
##| ##*: #H; napply (exadecim_destruct … H)
##]
nqed.
-
-nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
- #e1; #e2;
- ncases e1;
- ncases e2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
- ##]
-nqed.
-
-nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
- #e1; #e2;
- ncases e1;
- ncases e2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply False_ind; napply (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
- ##]
-nqed.
##| ##*: #H; napply (oct_destruct … H)
##]
nqed.
-
-nlemma neqoct_to_neq : ∀n1,n2.eq_oct n1 n2 = false → n1 ≠ n2.
- #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,10,19,28,37,46,55,64: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (oct_destruct … H1)
- ##]
-nqed.
-
-nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false.
- #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,10,19,28,37,46,55,64: #H; napply False_ind; napply (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
- ##]
-nqed.
##| ##*: #H; napply (quatern_destruct … H)
##]
nqed.
-
-nlemma neqqu_to_neq : ∀n1,n2.eq_qu n1 n2 = false → n1 ≠ n2.
- #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,6,11,16: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (quatern_destruct … H1)
- ##]
-nqed.
-
-nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false.
- #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,6,11,16: #H; napply False_ind; napply (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
- ##]
-nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/byte8.ma".
+
+(* **** *)
+(* WORD *)
+(* **** *)
+
+nrecord word16 : Type ≝
+ {
+ w16h: byte8;
+ w16l: byte8
+ }.
+
+(* \langle \rangle *)
+notation "〈x:y〉" non associative with precedence 80
+ for @{ 'mk_word16 $x $y }.
+interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
+
+(* operatore = *)
+ndefinition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).
+
+(* operatore < *)
+ndefinition lt_w16 ≝
+λw1,w2:word16.match lt_b8 (w16h w1) (w16h w2) with
+ [ true ⇒ true
+ | false ⇒ match gt_b8 (w16h w1) (w16h w2) with
+ [ true ⇒ false
+ | false ⇒ lt_b8 (w16l w1) (w16l w2) ]].
+
+(* operatore ≤ *)
+ndefinition le_w16 ≝ λw1,w2:word16.(eq_w16 w1 w2) ⊕ (lt_w16 w1 w2).
+
+(* operatore > *)
+ndefinition gt_w16 ≝ λw1,w2:word16.⊖ (le_w16 w1 w2).
+
+(* operatore ≥ *)
+ndefinition ge_w16 ≝ λw1,w2:word16.⊖ (lt_w16 w1 w2).
+
+(* operatore and *)
+ndefinition and_w16 ≝
+λw1,w2:word16.mk_word16 (and_b8 (w16h w1) (w16h w2)) (and_b8 (w16l w1) (w16l w2)).
+
+(* operatore or *)
+ndefinition or_w16 ≝
+λw1,w2:word16.mk_word16 (or_b8 (w16h w1) (w16h w2)) (or_b8 (w16l w1) (w16l w2)).
+
+(* operatore xor *)
+ndefinition xor_w16 ≝
+λw1,w2:word16.mk_word16 (xor_b8 (w16h w1) (w16h w2)) (xor_b8 (w16l w1) (w16l w2)).
+
+(* operatore rotazione destra con carry *)
+ndefinition rcr_w16 ≝
+λw:word16.λc:bool.match rcr_b8 (w16h w) c with
+ [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
+
+(* operatore shift destro *)
+ndefinition shr_w16 ≝
+λw:word16.match rcr_b8 (w16h w) false with
+ [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
+
+(* operatore rotazione destra *)
+ndefinition ror_w16 ≝
+λw:word16.match rcr_b8 (w16h w) false with
+ [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
+ [ pair wl' c'' ⇒ match c'' with
+ [ true ⇒ mk_word16 (or_b8 (mk_byte8 x8 x0) wh') wl'
+ | false ⇒ mk_word16 wh' wl' ]]].
+
+(* operatore rotazione destra n-volte *)
+nlet rec ror_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝
+ match r with
+ [ ex_O ⇒ w
+ | ex_S t n' ⇒ ror_w16_n (ror_w16 w) t n' ].
+
+(* operatore rotazione sinistra con carry *)
+ndefinition rcl_w16 ≝
+λw:word16.λc:bool.match rcl_b8 (w16l w) c with
+ [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
+
+(* operatore shift sinistro *)
+ndefinition shl_w16 ≝
+λw:word16.match rcl_b8 (w16l w) false with
+ [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
+
+(* operatore rotazione sinistra *)
+ndefinition rol_w16 ≝
+λw:word16.match rcl_b8 (w16l w) false with
+ [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
+ [ pair wh' c'' ⇒ match c'' with
+ [ true ⇒ mk_word16 wh' (or_b8 (mk_byte8 x0 x1) wl')
+ | false ⇒ mk_word16 wh' wl' ]]].
+
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝
+ match r with
+ [ ex_O ⇒ w
+ | ex_S t n' ⇒ rol_w16_n (rol_w16 w) t n' ].
+
+(* operatore not/complemento a 1 *)
+ndefinition not_w16 ≝
+λw:word16.mk_word16 (not_b8 (w16h w)) (not_b8 (w16l w)).
+
+(* operatore somma con data+carry → data+carry *)
+ndefinition plus_w16_dc_dc ≝
+λw1,w2:word16.λc:bool.
+ match plus_b8_dc_dc (w16l w1) (w16l w2) c with
+ [ pair l c ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c with
+ [ pair h c' ⇒ pair … 〈h:l〉 c' ]].
+
+(* operatore somma con data+carry → data *)
+ndefinition plus_w16_dc_d ≝
+λw1,w2:word16.λc:bool.
+ match plus_b8_dc_dc (w16l w1) (w16l w2) c with
+ [ pair l c ⇒ 〈plus_b8_dc_d (w16h w1) (w16h w2) c:l〉 ].
+
+(* operatore somma con data+carry → c *)
+ndefinition plus_w16_dc_c ≝
+λw1,w2:word16.λc:bool.
+ plus_b8_dc_c (w16h w1) (w16h w2) (plus_b8_dc_c (w16l w1) (w16l w2) c).
+
+(* operatore somma con data → data+carry *)
+ndefinition plus_w16_d_dc ≝
+λw1,w2:word16.
+ match plus_b8_d_dc (w16l w1) (w16l w2) with
+ [ pair l c ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c with
+ [ pair h c' ⇒ pair … 〈h:l〉 c' ]].
+
+(* operatore somma con data → data *)
+ndefinition plus_w16_d_d ≝
+λw1,w2:word16.
+ match plus_b8_d_dc (w16l w1) (w16l w2) with
+ [ pair l c ⇒ 〈plus_b8_dc_d (w16h w1) (w16h w2) c:l〉 ].
+
+(* operatore somma con data → c *)
+ndefinition plus_w16_d_c ≝
+λw1,w2:word16.
+ plus_b8_dc_c (w16h w1) (w16h w2) (plus_b8_d_c (w16l w1) (w16l w2)).
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
+
+(* operatore predecessore *)
+ndefinition pred_w16 ≝
+λw:word16.match eq_b8 (w16l w) (mk_byte8 x0 x0) with
+ [ true ⇒ mk_word16 (pred_b8 (w16h w)) (pred_b8 (w16l w))
+ | false ⇒ mk_word16 (w16h w) (pred_b8 (w16l w)) ].
+
+(* operatore successore *)
+ndefinition succ_w16 ≝
+λw:word16.match eq_b8 (w16l w) (mk_byte8 xF xF) with
+ [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w))
+ | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ].
+
+(* operatore neg/complemento a 2 *)
+ndefinition compl_w16 ≝
+λw:word16.match MSB_w16 w with
+ [ true ⇒ succ_w16 (not_w16 w)
+ | false ⇒ not_w16 (pred_w16 w) ].
+
+(*
+ operatore moltiplicazione senza segno: b*b=[0x0000,0xFE01]
+ ... in pratica (〈a,b〉*〈c,d〉) = (a*c)<<8+(a*d)<<4+(b*c)<<4+(b*d)
+*)
+ndefinition mul_b8 ≝
+λb1,b2:byte8.match b1 with
+[ mk_byte8 b1h b1l ⇒ match b2 with
+[ mk_byte8 b2h b2l ⇒ match mul_ex b1l b2l with
+[ mk_byte8 t1_h t1_l ⇒ match mul_ex b1h b2l with
+[ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with
+[ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with
+[ mk_byte8 t4_h t4_l ⇒
+ plus_w16_d_d
+ (plus_w16_d_d
+ (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
+]]]]]].
+
+(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
+nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:oct) (rc:rec_oct c) on rc ≝
+ let w' ≝ plus_w16_d_d divd (compl_w16 divs) in
+ match rc with
+ [ oc_O ⇒ match le_w16 divs divd with
+ [ true ⇒ triple … (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
+ | false ⇒ triple … q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
+ | oc_S t c' ⇒ match le_w16 divs divd with
+ [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) t c'
+ | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q t c' ]].
+
+ndefinition div_b8 ≝
+λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
+(*
+ la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
+*)
+ [ true ⇒ triple … 〈xF,xF〉 (w16l w) true
+ | false ⇒ match eq_w16 w 〈〈x0,x0〉:〈x0,x0〉〉 with
+(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
+ [ true ⇒ triple … 〈x0,x0〉 〈x0,x0〉 false
+(* 1) e' una divisione sensata che produrra' overflow/risultato *)
+(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
+(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
+(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
+(* puo' essere sottratto al dividendo *)
+ | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 ? (ex_to_recex x7)) 〈x8,x0〉 〈x0,x0〉 ? (oct_to_recoct o7) ]].
+
+(* operatore x in [inf,sup] *)
+ndefinition inrange_w16 ≝
+λx,inf,sup:word16.(le_w16 inf sup) ⊗ (ge_w16 x inf) ⊗ (le_w16 x sup).
+
+(* iteratore sulle word *)
+ndefinition forall_w16 ≝
+ λP.
+ forall_b8 (λbh.
+ forall_b8 (λbl.
+ P (mk_word16 bh bl ))).
+
+(* word16 ricorsive *)
+ninductive rec_word16 : word16 → Type ≝
+ w16_O : rec_word16 〈〈x0,x0〉:〈x0,x0〉〉
+| w16_S : ∀n.rec_word16 n → rec_word16 (succ_w16 n).
+
+(* word16 → word16 ricorsive *)
+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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? 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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (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 ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_15 ? recw)
+ ))))))))))))))).
+
+(* ... cifra byte superiore *)
+nlet rec w16_to_recw16_aux2 (n:byte8) (r:rec_byte8 n) on r ≝
+ match r return λx.λy:rec_byte8 x.rec_word16 〈x:〈x0,x0〉〉 with
+ [ b8_O ⇒ w16_O
+ | b8_S t n' ⇒ w16_to_recw16_aux1 ? (w16_to_recw16_aux2 t n')
+ ].
+
+(* ... cifra esadecimale n.2 *)
+ndefinition w16_to_recw16_aux3 ≝
+λb,n.λrecw:rec_word16 〈b:〈x0,x0〉〉.
+ match n return λx.rec_word16 〈b:〈x,x0〉〉 with
+ [ x0 ⇒ recw
+ | x1 ⇒ w16_to_recw16_aux1_1 ? recw
+ | x2 ⇒ w16_to_recw16_aux1_2 ? recw
+ | x3 ⇒ w16_to_recw16_aux1_3 ? recw
+ | x4 ⇒ w16_to_recw16_aux1_4 ? recw
+ | x5 ⇒ w16_to_recw16_aux1_5 ? recw
+ | x6 ⇒ w16_to_recw16_aux1_6 ? recw
+ | x7 ⇒ w16_to_recw16_aux1_7 ? recw
+ | x8 ⇒ w16_to_recw16_aux1_8 ? recw
+ | x9 ⇒ w16_to_recw16_aux1_9 ? recw
+ | xA ⇒ w16_to_recw16_aux1_10 ? recw
+ | xB ⇒ w16_to_recw16_aux1_11 ? recw
+ | xC ⇒ w16_to_recw16_aux1_12 ? recw
+ | xD ⇒ w16_to_recw16_aux1_13 ? recw
+ | xE ⇒ w16_to_recw16_aux1_14 ? recw
+ | 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;
+ (* non funziona nelim e *)
+ #H;
+ nelim e in H:(%) ⊢ %;
+ #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.
+
+(* ... cifra esadecimale n.1 *)
+ndefinition w16_to_recw16_aux4 ≝
+λb,e,n.λrecw:rec_word16 〈b:〈e,x0〉〉.
+ match n return λx.rec_word16 〈b:〈e,x〉〉 with
+ [ x0 ⇒ recw
+ | x1 ⇒ w16_to_recw16_aux4_1 … recw
+ | x2 ⇒ w16_to_recw16_aux4_2 … recw
+ | x3 ⇒ w16_to_recw16_aux4_3 … recw
+ | x4 ⇒ w16_to_recw16_aux4_4 … recw
+ | x5 ⇒ w16_to_recw16_aux4_5 … recw
+ | x6 ⇒ w16_to_recw16_aux4_6 … recw
+ | x7 ⇒ w16_to_recw16_aux4_7 … recw
+ | x8 ⇒ w16_to_recw16_aux4_8 … recw
+ | x9 ⇒ w16_to_recw16_aux4_9 … recw
+ | xA ⇒ w16_to_recw16_aux4_10 … recw
+ | xB ⇒ w16_to_recw16_aux4_11 … recw
+ | xC ⇒ w16_to_recw16_aux4_12 … recw
+ | xD ⇒ w16_to_recw16_aux4_13 … recw
+ | xE ⇒ w16_to_recw16_aux4_14 … recw
+ | xF ⇒ w16_to_recw16_aux4_15 … recw
+ ].
+
+nlemma w16_to_recw16_aux5 : ∀b.rec_byte8 (〈b8h b,b8l b〉) → rec_byte8 b.
+ #b; nelim b; #e1; #e2; nnormalize; #input; napply input. nqed.
+
+ndefinition w16_to_recw16 ≝
+λn.w16_to_recw16_aux4 (w16h n) (b8h (w16l n)) (b8l (w16l n))
+ (w16_to_recw16_aux3 (w16h n) (b8h (w16l n)) (w16_to_recw16_aux2 (w16h n) ?)).
+ nelim n; #b1; #b2;
+ nchange with (rec_byte8 b1);
+ napply (w16_to_recw16_aux5 b1);
+ napply (b8_to_recb8 b1).
+nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/word16.ma".
+include "num/byte8_lemmas.ma".
+
+(* **** *)
+(* WORD *)
+(* **** *)
+
+nlemma word16_destruct_1 :
+∀x1,x2,y1,y2.
+ mk_word16 x1 y1 = mk_word16 x2 y2 → x1 = x2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_word16 x2 y2 with [ mk_word16 a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma word16_destruct_2 :
+∀x1,x2,y1,y2.
+ mk_word16 x1 y1 = mk_word16 x2 y2 → y1 = y2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_word16 x2 y2 with [ mk_word16 _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqw16 : symmetricT word16 bool eq_w16.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = ((eq_b8 b1 b3)⊗(eq_b8 b2 b4)));
+ nrewrite > (symmetric_eqb8 b1 b3);
+ nrewrite > (symmetric_eqb8 b2 b4);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_andw16 : symmetricT word16 word16 and_w16.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((mk_word16 (and_b8 b3 b1) (and_b8 b4 b2)) = (mk_word16 (and_b8 b1 b3) (and_b8 b2 b4)));
+ nrewrite > (symmetric_andb8 b1 b3);
+ nrewrite > (symmetric_andb8 b2 b4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_andw16 : ∀w1,w2,w3.(and_w16 (and_w16 w1 w2) w3) = (and_w16 w1 (and_w16 w2 w3)).
+ #w1; #w2; #w3;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nelim w3;
+ #b5; #b6;
+ nchange with (mk_word16 (and_b8 (and_b8 b1 b3) b5) (and_b8 (and_b8 b2 b4) b6) =
+ mk_word16 (and_b8 b1 (and_b8 b3 b5)) (and_b8 b2 (and_b8 b4 b6)));
+ nrewrite < (associative_andb8 b1 b3 b5);
+ nrewrite < (associative_andb8 b2 b4 b6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_orw16 : symmetricT word16 word16 or_w16.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((mk_word16 (or_b8 b3 b1) (or_b8 b4 b2)) = (mk_word16 (or_b8 b1 b3) (or_b8 b2 b4)));
+ nrewrite > (symmetric_orb8 b1 b3);
+ nrewrite > (symmetric_orb8 b2 b4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_orw16 : ∀w1,w2,w3.(or_w16 (or_w16 w1 w2) w3) = (or_w16 w1 (or_w16 w2 w3)).
+ #w1; #w2; #w3;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nelim w3;
+ #b5; #b6;
+ nchange with (mk_word16 (or_b8 (or_b8 b1 b3) b5) (or_b8 (or_b8 b2 b4) b6) =
+ mk_word16 (or_b8 b1 (or_b8 b3 b5)) (or_b8 b2 (or_b8 b4 b6)));
+ nrewrite < (associative_orb8 b1 b3 b5);
+ nrewrite < (associative_orb8 b2 b4 b6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_xorw16 : symmetricT word16 word16 xor_w16.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((mk_word16 (xor_b8 b3 b1) (xor_b8 b4 b2)) = (mk_word16 (xor_b8 b1 b3) (xor_b8 b2 b4)));
+ nrewrite > (symmetric_xorb8 b1 b3);
+ nrewrite > (symmetric_xorb8 b2 b4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_xorw16 : ∀w1,w2,w3.(xor_w16 (xor_w16 w1 w2) w3) = (xor_w16 w1 (xor_w16 w2 w3)).
+ #w1; #w2; #w3;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nelim w3;
+ #b5; #b6;
+ nchange with (mk_word16 (xor_b8 (xor_b8 b1 b3) b5) (xor_b8 (xor_b8 b2 b4) b6) =
+ mk_word16 (xor_b8 b1 (xor_b8 b3 b5)) (xor_b8 b2 (xor_b8 b4 b6)));
+ nrewrite < (associative_xorb8 b1 b3 b5);
+ nrewrite < (associative_xorb8 b2 b4 b6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc_dc w2 w1 c.
+ #w1; #w2; #c;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+ match plus_b8_dc_dc b2 b4 c with
+ [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
+ [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+ match plus_b8_dc_dc b4 b2 c with
+ [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
+ [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+ nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
+ ncases (plus_b8_dc_dc b2 b4 c);
+ #b5; #c1;
+ nchange with (
+ match plus_b8_dc_dc b1 b3 c1 with
+ [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+ match plus_b8_dc_dc b3 b1 c1 with
+ [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+ nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d w2 w1 c.
+ #w1; #w2; #c;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+ match plus_b8_dc_dc b2 b4 c with
+ [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+ match plus_b8_dc_dc b4 b2 c with
+ [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+ nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
+ ncases (plus_b8_dc_dc b2 b4 c);
+ #b5; #c1;
+ nchange with (〈plus_b8_dc_d b1 b3 c1:b5〉 = 〈plus_b8_dc_d b3 b1 c1:b5〉);
+ nrewrite > (symmetric_plusb8_dc_d b1 b3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_dc_c : ∀w1,w2,c.plus_w16_dc_c w1 w2 c = plus_w16_dc_c w2 w1 c.
+ #w1; #w2; #c;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+ plus_b8_dc_c b1 b3 (plus_b8_dc_c b2 b4 c) =
+ plus_b8_dc_c b3 b1 (plus_b8_dc_c b4 b2 c));
+ nrewrite > (symmetric_plusb8_dc_c b4 b2 c);
+ nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_dc_c b2 b4 c));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2 w1.
+ #w1; #w2;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+ match plus_b8_d_dc b2 b4 with
+ [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
+ [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+ match plus_b8_d_dc b4 b2 with
+ [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
+ [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+ nrewrite > (symmetric_plusb8_d_dc b4 b2);
+ ncases (plus_b8_d_dc b2 b4);
+ #b5; #c;
+ nchange with (
+ match plus_b8_dc_dc b1 b3 c with
+ [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+ match plus_b8_dc_dc b3 b1 c with
+ [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+ nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1.
+ #w1; #w2;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+ match plus_b8_d_dc b2 b4 with
+ [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+ match plus_b8_d_dc b4 b2 with
+ [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+ nrewrite > (symmetric_plusb8_d_dc b4 b2);
+ ncases (plus_b8_d_dc b2 b4);
+ #b5; #c;
+ nchange with (〈plus_b8_dc_d b1 b3 c:b5〉 = 〈plus_b8_dc_d b3 b1 c:b5〉);
+ nrewrite > (symmetric_plusb8_dc_d b1 b3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw16_d_c : ∀w1,w2.plus_w16_d_c w1 w2 = plus_w16_d_c w2 w1.
+ #w1; #w2;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (
+ plus_b8_dc_c b1 b3 (plus_b8_d_c b2 b4) =
+ plus_b8_dc_c b3 b1 (plus_b8_d_c b4 b2));
+ nrewrite > (symmetric_plusb8_d_c b4 b2);
+ nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_d_c b2 b4));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_mulb8 : symmetricT byte8 word16 mul_b8.
+ #b1; #b2;
+ nelim b1;
+ #e1; #e2;
+ nelim b2;
+ #e3; #e4;
+ nchange with (match mul_ex e2 e4 with
+ [ mk_byte8 t1_h t1_l ⇒ match mul_ex e1 e4 with
+ [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
+ [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
+ ]]]] = match mul_ex e4 e2 with
+ [ mk_byte8 t1_h t1_l ⇒ match mul_ex e3 e2 with
+ [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
+ [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉
+ ]]]]);
+ nrewrite < (symmetric_mulex e2 e4);
+ ncases (mul_ex e2 e4);
+ #e5; #e6;
+ nchange with (match mul_ex e1 e4 with
+ [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with
+ [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
+ ]]] = match mul_ex e3 e2 with
+ [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with
+ [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
+ ]]]);
+ ncases (mul_ex e3 e2);
+ #e7; #e8;
+ ncases (mul_ex e1 e4);
+ #e9; #e10;
+ nchange with (match mul_ex e1 e3 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
+ ] = match mul_ex e3 e1 with
+ [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉
+ ]);
+ nrewrite < (symmetric_mulex e1 e3);
+ ncases (mul_ex e1 e3);
+ #e11; #e12;
+ nchange with ((plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉) =
+ (plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉));
+ nrewrite > (symmetric_plusw16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉);
+ napply refl_eq.
+nqed.
+
+nlemma eqw16_to_eq : ∀w1,w2:word16.(eq_w16 w1 w2 = true) → (w1 = w2).
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange in ⊢ (% → ?) with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = true);
+ #H;
+ nrewrite < (eqb8_to_eq … (andb_true_true_l … H));
+ nrewrite < (eqb8_to_eq … (andb_true_true_r … H));
+ napply refl_eq.
+nqed.
+
+nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true.
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ #H;
+ nrewrite < (word16_destruct_1 … H);
+ nrewrite < (word16_destruct_2 … H);
+ nchange with (((eq_b8 b3 b3)⊗(eq_b8 b4 b4)) = true);
+ nrewrite > (eq_to_eqb8 b3 b3 (refl_eq …));
+ nrewrite > (eq_to_eqb8 b4 b4 (refl_eq …));
+ nnormalize;
+ napply refl_eq.
+nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/word16.ma".
+
+(* ***** *)
+(* DWORD *)
+(* ***** *)
+
+nrecord word32 : Type ≝
+ {
+ w32h: word16;
+ w32l: word16
+ }.
+
+(* \langle \rangle *)
+notation "〈x.y〉" non associative with precedence 80
+ for @{ 'mk_word32 $x $y }.
+interpretation "mk_word32" 'mk_word32 x y = (mk_word32 x y).
+
+(* operatore = *)
+ndefinition eq_w32 ≝ λdw1,dw2.(eq_w16 (w32h dw1) (w32h dw2)) ⊗ (eq_w16 (w32l dw1) (w32l dw2)).
+
+(* operatore < *)
+ndefinition lt_w32 ≝
+λdw1,dw2:word32.match lt_w16 (w32h dw1) (w32h dw2) with
+ [ true ⇒ true
+ | false ⇒ match gt_w16 (w32h dw1) (w32h dw2) with
+ [ true ⇒ false
+ | false ⇒ lt_w16 (w32l dw1) (w32l dw2) ]].
+
+(* operatore ≤ *)
+ndefinition le_w32 ≝ λdw1,dw2:word32.(eq_w32 dw1 dw2) ⊕ (lt_w32 dw1 dw2).
+
+(* operatore > *)
+ndefinition gt_w32 ≝ λdw1,dw2:word32.⊖ (le_w32 dw1 dw2).
+
+(* operatore ≥ *)
+ndefinition ge_w32 ≝ λdw1,dw2:word32.⊖ (lt_w32 dw1 dw2).
+
+(* operatore and *)
+ndefinition and_w32 ≝
+λdw1,dw2:word32.mk_word32 (and_w16 (w32h dw1) (w32h dw2)) (and_w16 (w32l dw1) (w32l dw2)).
+
+(* operatore or *)
+ndefinition or_w32 ≝
+λdw1,dw2:word32.mk_word32 (or_w16 (w32h dw1) (w32h dw2)) (or_w16 (w32l dw1) (w32l dw2)).
+
+(* operatore xor *)
+ndefinition xor_w32 ≝
+λdw1,dw2:word32.mk_word32 (xor_w16 (w32h dw1) (w32h dw2)) (xor_w16 (w32l dw1) (w32l dw2)).
+
+(* operatore rotazione destra con carry *)
+ndefinition rcr_w32 ≝
+λdw:word32.λc:bool.match rcr_w16 (w32h dw) c with
+ [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
+ [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
+
+(* operatore shift destro *)
+ndefinition shr_w32 ≝
+λdw:word32.match rcr_w16 (w32h dw) false with
+ [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
+ [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
+
+(* operatore rotazione destra *)
+ndefinition ror_w32 ≝
+λdw:word32.match rcr_w16 (w32h dw) false with
+ [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with
+ [ pair wl' c'' ⇒ match c'' with
+ [ true ⇒ mk_word32 (or_w16 (mk_word16 (mk_byte8 x8 x0) (mk_byte8 x0 x0)) wh') wl'
+ | false ⇒ mk_word32 wh' wl' ]]].
+
+(* operatore rotazione destra n-volte *)
+nlet rec ror_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝
+ match r with
+ [ bi_O ⇒ dw
+ | bi_S t n' ⇒ ror_w32_n (ror_w32 dw) t n' ].
+
+(* operatore rotazione sinistra con carry *)
+ndefinition rcl_w32 ≝
+λdw:word32.λc:bool.match rcl_w16 (w32l dw) c with
+ [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
+ [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
+
+(* operatore shift sinistro *)
+ndefinition shl_w32 ≝
+λdw:word32.match rcl_w16 (w32l dw) false with
+ [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
+ [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]].
+
+(* operatore rotazione sinistra *)
+ndefinition rol_w32 ≝
+λdw:word32.match rcl_w16 (w32l dw) false with
+ [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with
+ [ pair wh' c'' ⇒ match c'' with
+ [ true ⇒ mk_word32 wh' (or_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x1)) wl')
+ | false ⇒ mk_word32 wh' wl' ]]].
+
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝
+ match r with
+ [ bi_O ⇒ dw
+ | bi_S t n' ⇒ rol_w32_n (rol_w32 dw) t n' ].
+
+(* operatore not/complemento a 1 *)
+ndefinition not_w32 ≝
+λdw:word32.mk_word32 (not_w16 (w32h dw)) (not_w16 (w32l dw)).
+
+(* operatore somma con data+carry → data+carry *)
+ndefinition plus_w32_dc_dc ≝
+λdw1,dw2:word32.λc:bool.
+ match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
+ [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
+ [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
+
+(* operatore somma con data+carry → data *)
+ndefinition plus_w32_dc_d ≝
+λdw1,dw2:word32.λc:bool.
+ match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
+ [ pair l c ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c.l〉 ].
+
+(* operatore somma con data+carry → c *)
+ndefinition plus_w32_dc_c ≝
+λdw1,dw2:word32.λc:bool.
+ plus_w16_dc_c (w32h dw1) (w32h dw2) (plus_w16_dc_c (w32l dw1) (w32l dw2) c).
+
+(* operatore somma con data → data+carry *)
+ndefinition plus_w32_d_dc ≝
+λdw1,dw2:word32.
+ match plus_w16_d_dc (w32l dw1) (w32l dw2) with
+ [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
+ [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
+
+(* operatore somma con data → data *)
+ndefinition plus_w32_d_d ≝
+λdw1,dw2:word32.
+ match plus_w16_d_dc (w32l dw1) (w32l dw2) with
+ [ pair l c ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c.l〉 ].
+
+(* operatore somma con data → c *)
+ndefinition plus_w32_d_c ≝
+λdw1,dw2:word32.
+ plus_w16_dc_c (w32h dw1) (w32h dw2) (plus_w16_d_c (w32l dw1) (w32l dw2)).
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_w32 ≝ λdw:word32.eq_ex x8 (and_ex x8 (b8h (w16h (w32h dw)))).
+
+(* operatore predecessore *)
+ndefinition pred_w32 ≝
+λdw:word32.match eq_w16 (w32l dw) (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) with
+ [ true ⇒ mk_word32 (pred_w16 (w32h dw)) (pred_w16 (w32l dw))
+ | false ⇒ mk_word32 (w32h dw) (pred_w16 (w32l dw)) ].
+
+(* operatore successore *)
+ndefinition succ_w32 ≝
+λdw:word32.match eq_w16 (w32l dw) (mk_word16 (mk_byte8 xF xF) (mk_byte8 xF xF)) with
+ [ true ⇒ mk_word32 (succ_w16 (w32h dw)) (succ_w16 (w32l dw))
+ | false ⇒ mk_word32 (w32h dw) (succ_w16 (w32l dw)) ].
+
+(* operatore neg/complemento a 2 *)
+ndefinition compl_w32 ≝
+λdw:word32.match MSB_w32 dw with
+ [ true ⇒ succ_w32 (not_w32 dw)
+ | false ⇒ not_w32 (pred_w32 dw) ].
+
+(*
+ operatore moltiplicazione senza segno: b*b=[0x00000000,0xFFFE0001]
+ ... in pratica (〈a:b〉*〈c:d〉) = (a*c)<<16+(a*d)<<8+(b*c)<<8+(b*d)
+*)
+ndefinition mul_w16 ≝
+λw1,w2:word16.match w1 with
+[ mk_word16 b1h b1l ⇒ match w2 with
+[ mk_word16 b2h b2l ⇒ match mul_b8 b1l b2l with
+[ mk_word16 t1_h t1_l ⇒ match mul_b8 b1h b2l with
+[ mk_word16 t2_h t2_l ⇒ match mul_b8 b2h b1l with
+[ mk_word16 t3_h t3_l ⇒ match mul_b8 b1h b2h with
+[ mk_word16 t4_h t4_l ⇒
+ plus_w32_d_d
+ (plus_w32_d_d
+ (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
+]]]]]].
+
+(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
+nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:exadecim) (rc:rec_exadecim c) on rc ≝
+ let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
+ match rc with
+ [ ex_O ⇒ match le_w32 divs divd with
+ [ true ⇒ triple … (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
+ | false ⇒ triple … q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
+ | ex_S t c' ⇒ match le_w32 divs divd with
+ [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) t c'
+ | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q t c' ]].
+
+ndefinition div_w16 ≝
+λw:word32.λb:word16.match eq_w16 b 〈〈x0,x0〉:〈x0,x0〉〉 with
+(*
+ la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
+*)
+ [ true ⇒ triple … 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true
+ | false ⇒ match eq_w32 w 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 with
+(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
+ [ true ⇒ triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 false
+(* 1) e' una divisione sensata che produrra' overflow/risultato *)
+(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
+(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
+(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
+(* puo' essere sottratto al dividendo *)
+ | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 ? (bit_to_recbit t0F)) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 ? (ex_to_recex xF) ]].
+
+(* operatore x in [inf,sup] *)
+ndefinition inrange_w32 ≝
+λx,inf,sup:word32.(le_w32 inf sup) ⊗ (ge_w32 x inf) ⊗ (le_w32 x sup).
+
+(* iteratore sulle word *)
+ndefinition forall_w32 ≝
+ λP.
+ forall_w16 (λbh.
+ forall_w16 (λbl.
+ P (mk_word32 bh bl ))).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/word32.ma".
+include "num/word16_lemmas.ma".
+
+(* ***** *)
+(* DWORD *)
+(* ***** *)
+
+nlemma word32_destruct_1 :
+∀x1,x2,y1,y2.
+ mk_word32 x1 y1 = mk_word32 x2 y2 → x1 = x2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_word32 x2 y2 with [ mk_word32 a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma word32_destruct_2 :
+∀x1,x2,y1,y2.
+ mk_word32 x1 y1 = mk_word32 x2 y2 → y1 = y2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match mk_word32 x2 y2 with [ mk_word32 _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqw32 : symmetricT word32 bool eq_w32.
+ #dw1; #dw2;
+ nelim dw1;
+ nelim dw2;
+ #w1; #w2; #w3; #w4;
+ nchange with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = ((eq_w16 w1 w3)⊗(eq_w16 w2 w4)));
+ nrewrite > (symmetric_eqw16 w1 w3);
+ nrewrite > (symmetric_eqw16 w2 w4);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_andw32 : symmetricT word32 word32 and_w32.
+ #dw1; #dw2;
+ nelim dw1;
+ nelim dw2;
+ #w1; #w2; #w3; #w4;
+ nchange with ((mk_word32 (and_w16 w3 w1) (and_w16 w4 w2)) = (mk_word32 (and_w16 w1 w3) (and_w16 w2 w4)));
+ nrewrite > (symmetric_andw16 w1 w3);
+ nrewrite > (symmetric_andw16 w2 w4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_andw32 : ∀dw1,dw2,dw3.(and_w32 (and_w32 dw1 dw2) dw3) = (and_w32 dw1 (and_w32 dw2 dw3)).
+ #dw1; #dw2; #dw3;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nelim dw3;
+ #w5; #w6;
+ nchange with (mk_word32 (and_w16 (and_w16 w1 w3) w5) (and_w16 (and_w16 w2 w4) w6) =
+ mk_word32 (and_w16 w1 (and_w16 w3 w5)) (and_w16 w2 (and_w16 w4 w6)));
+ nrewrite < (associative_andw16 w1 w3 w5);
+ nrewrite < (associative_andw16 w2 w4 w6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_orw32 : symmetricT word32 word32 or_w32.
+ #dw1; #dw2;
+ nelim dw1;
+ nelim dw2;
+ #w1; #w2; #w3; #w4;
+ nchange with ((mk_word32 (or_w16 w3 w1) (or_w16 w4 w2)) = (mk_word32 (or_w16 w1 w3) (or_w16 w2 w4)));
+ nrewrite > (symmetric_orw16 w1 w3);
+ nrewrite > (symmetric_orw16 w2 w4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_orw32 : ∀dw1,dw2,dw3.(or_w32 (or_w32 dw1 dw2) dw3) = (or_w32 dw1 (or_w32 dw2 dw3)).
+ #dw1; #dw2; #dw3;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nelim dw3;
+ #w5; #w6;
+ nchange with (mk_word32 (or_w16 (or_w16 w1 w3) w5) (or_w16 (or_w16 w2 w4) w6) =
+ mk_word32 (or_w16 w1 (or_w16 w3 w5)) (or_w16 w2 (or_w16 w4 w6)));
+ nrewrite < (associative_orw16 w1 w3 w5);
+ nrewrite < (associative_orw16 w2 w4 w6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_xorw32 : symmetricT word32 word32 xor_w32.
+ #dw1; #dw2;
+ nelim dw1;
+ nelim dw2;
+ #w1; #w2; #w3; #w4;
+ nchange with ((mk_word32 (xor_w16 w3 w1) (xor_w16 w4 w2)) = (mk_word32 (xor_w16 w1 w3) (xor_w16 w2 w4)));
+ nrewrite > (symmetric_xorw16 w1 w3);
+ nrewrite > (symmetric_xorw16 w2 w4);
+ napply refl_eq.
+nqed.
+
+nlemma associative_xorw32 : ∀dw1,dw2,dw3.(xor_w32 (xor_w32 dw1 dw2) dw3) = (xor_w32 dw1 (xor_w32 dw2 dw3)).
+ #dw1; #dw2; #dw3;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nelim dw3;
+ #w5; #w6;
+ nchange with (mk_word32 (xor_w16 (xor_w16 w1 w3) w5) (xor_w16 (xor_w16 w2 w4) w6) =
+ mk_word32 (xor_w16 w1 (xor_w16 w3 w5)) (xor_w16 w2 (xor_w16 w4 w6)));
+ nrewrite < (associative_xorw16 w1 w3 w5);
+ nrewrite < (associative_xorw16 w2 w4 w6);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw32_dc_dc : ∀dw1,dw2,c.plus_w32_dc_dc dw1 dw2 c = plus_w32_dc_dc dw2 dw1 c.
+ #dw1; #dw2; #c;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nchange with (
+ match plus_w16_dc_dc w2 w4 c with
+ [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
+ [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
+ match plus_w16_dc_dc w4 w2 c with
+ [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
+ [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
+ nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
+ ncases (plus_w16_dc_dc w2 w4 c);
+ #w5; #c1;
+ nchange with (
+ match plus_w16_dc_dc w1 w3 c1 with
+ [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
+ match plus_w16_dc_dc w3 w1 c1 with
+ [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
+ nrewrite > (symmetric_plusw16_dc_dc w1 w3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw32_dc_d : ∀dw1,dw2,c.plus_w32_dc_d dw1 dw2 c = plus_w32_dc_d dw2 dw1 c.
+ #dw1; #dw2; #c;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nchange with (
+ match plus_w16_dc_dc w2 w4 c with
+ [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
+ match plus_w16_dc_dc w4 w2 c with
+ [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
+ nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
+ ncases (plus_w16_dc_dc w2 w4 c);
+ #w5; #c1;
+ nchange with (〈plus_w16_dc_d w1 w3 c1.w5〉 = 〈plus_w16_dc_d w3 w1 c1.w5〉);
+ nrewrite > (symmetric_plusw16_dc_d w1 w3 c1);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw32_dc_c : ∀dw1,dw2,c.plus_w32_dc_c dw1 dw2 c = plus_w32_dc_c dw2 dw1 c.
+ #dw1; #dw2; #c;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nchange with (
+ plus_w16_dc_c w1 w3 (plus_w16_dc_c w2 w4 c) =
+ plus_w16_dc_c w3 w1 (plus_w16_dc_c w4 w2 c));
+ nrewrite > (symmetric_plusw16_dc_c w4 w2 c);
+ nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_dc_c w2 w4 c));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw32_d_dc : ∀dw1,dw2.plus_w32_d_dc dw1 dw2 = plus_w32_d_dc dw2 dw1.
+ #dw1; #dw2;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nchange with (
+ match plus_w16_d_dc w2 w4 with
+ [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
+ [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
+ match plus_w16_d_dc w4 w2 with
+ [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
+ [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
+ nrewrite > (symmetric_plusw16_d_dc w4 w2);
+ ncases (plus_w16_d_dc w2 w4);
+ #w5; #c;
+ nchange with (
+ match plus_w16_dc_dc w1 w3 c with
+ [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
+ match plus_w16_dc_dc w3 w1 c with
+ [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
+ nrewrite > (symmetric_plusw16_dc_dc w1 w3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw32_d_d : ∀dw1,dw2.plus_w32_d_d dw1 dw2 = plus_w32_d_d dw2 dw1.
+ #dw1; #dw2;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nchange with (
+ match plus_w16_d_dc w2 w4 with
+ [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
+ match plus_w16_d_dc w4 w2 with
+ [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
+ nrewrite > (symmetric_plusw16_d_dc w4 w2);
+ ncases (plus_w16_d_dc w2 w4);
+ #w5; #c;
+ nchange with (〈plus_w16_dc_d w1 w3 c.w5〉 = 〈plus_w16_dc_d w3 w1 c.w5〉);
+ nrewrite > (symmetric_plusw16_dc_d w1 w3 c);
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusw32_d_c : ∀dw1,dw2.plus_w32_d_c dw1 dw2 = plus_w32_d_c dw2 dw1.
+ #dw1; #dw2;
+ nelim dw1;
+ #w1; #w2;
+ nelim dw2;
+ #w3; #w4;
+ nchange with (
+ plus_w16_dc_c w1 w3 (plus_w16_d_c w2 w4) =
+ plus_w16_dc_c w3 w1 (plus_w16_d_c w4 w2));
+ nrewrite > (symmetric_plusw16_d_c w4 w2);
+ nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_d_c w2 w4));
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_mulw16 : symmetricT word16 word32 mul_w16.
+ #w1; #w2;
+ nelim w1;
+ #b1; #b2;
+ nelim w2;
+ #b3; #b4;
+ nchange with (match mul_b8 b2 b4 with
+ [ mk_word16 t1_h t1_l ⇒ match mul_b8 b1 b4 with
+ [ mk_word16 t2_h t2_l ⇒ match mul_b8 b3 b2 with
+ [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1 b3 with
+ [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
+ ]]]] = match mul_b8 b4 b2 with
+ [ mk_word16 t1_h t1_l ⇒ match mul_b8 b3 b2 with
+ [ mk_word16 t2_h t2_l ⇒ match mul_b8 b1 b4 with
+ [ mk_word16 t3_h t3_l ⇒ match mul_b8 b3 b1 with
+ [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
+ ]]]]);
+ nrewrite < (symmetric_mulb8 b2 b4);
+ ncases (mul_b8 b2 b4);
+ #b5; #b6;
+ nchange with (match mul_b8 b1 b4 with
+ [ mk_word16 t2_h t2_l ⇒ match mul_b8 b3 b2 with
+ [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1 b3 with
+ [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
+ ]]] = match mul_b8 b3 b2 with
+ [ mk_word16 t2_h t2_l ⇒ match mul_b8 b1 b4 with
+ [ mk_word16 t3_h t3_l ⇒ match mul_b8 b3 b1 with
+ [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
+ ]]]);
+ ncases (mul_b8 b3 b2);
+ #b7; #b8;
+ ncases (mul_b8 b1 b4);
+ #b9; #b10;
+ nchange with (match mul_b8 b1 b3 with
+ [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
+ ] = match mul_b8 b3 b1 with
+ [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
+ ]);
+ nrewrite < (symmetric_mulb8 b1 b3);
+ ncases (mul_b8 b1 b3);
+ #b11; #b12;
+ nchange with ((plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉) =
+ (plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉));
+ nrewrite > (symmetric_plusw32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉);
+ napply refl_eq.
+nqed.
+
+nlemma eqw32_to_eq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = true) → (dw1 = dw2).
+ #dw1; #dw2;
+ nelim dw1;
+ nelim dw2;
+ #w1; #w2; #w3; #w4;
+ nchange in ⊢ (% → ?) with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = true);
+ #H;
+ nrewrite < (eqw16_to_eq … (andb_true_true_l … H));
+ nrewrite < (eqw16_to_eq … (andb_true_true_r … H));
+ napply refl_eq.
+nqed.
+
+nlemma eq_to_eqw32 : ∀dw1,dw2.dw1 = dw2 → eq_w32 dw1 dw2 = true.
+ #dw1; #dw2;
+ nelim dw1;
+ nelim dw2;
+ #w1; #w2; #w3; #w4;
+ #H;
+ nrewrite < (word32_destruct_1 … H);
+ nrewrite < (word32_destruct_2 … H);
+ nchange with (((eq_w16 w3 w3)⊗(eq_w16 w4 w4)) = true);
+ nrewrite > (eq_to_eqw16 w3 w3 (refl_eq …));
+ nrewrite > (eq_to_eqw16 w4 w4 (refl_eq …));
+ nnormalize;
+ napply refl_eq.
+nqed.
projects / helm.git / commitdiff