new ng freescale, no external dependencies

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool.ma
new file mode 100755 (executable)
index 0000000..fe9fc4c
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool.ma
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/pts.ma".
+
+(* ******** *)
+(* BOOLEANI *)
+(* ******** *)
+
+ninductive bool : Type ≝ 
+  true : bool
+| false : bool.
+
+ndefinition bool_ind : ΠP:bool → Prop.P true → P false → Πb:bool.P b ≝
+λP:bool → Prop.λp:P true.λp1:P false.λb:bool.
+ match b with [ true ⇒ p | false ⇒ p1 ].
+
+ndefinition bool_rec : ΠP:bool → Set.P true → P false → Πb:bool.P b ≝
+λP:bool → Set.λp:P true.λp1:P false.λb:bool.
+ match b with [ true ⇒ p | false ⇒ p1 ].
+
+ndefinition bool_rect : ΠP:bool → Type.P true → P false → Πb:bool.P b ≝
+λP:bool → Type.λp:P true.λp1:P false.λb:bool.
+ match b with [ true ⇒ p | false ⇒ p1 ].
+
+(* operatori booleani *)
+
+ndefinition eq_bool ≝
+λb1,b2:bool.match b1 with
+ [ true ⇒ match b2 with [ true ⇒ true | false ⇒ false ]
+ | false ⇒ match b2 with [ true ⇒ false | false ⇒ true ]
+ ].
+
+ndefinition not_bool ≝
+λb:bool.match b with [ true ⇒ false | false ⇒ true ].
+
+ndefinition and_bool ≝
+λb1,b2:bool.match b1 with
+ [ true ⇒ b2 | false ⇒ false ].
+
+ndefinition or_bool ≝
+λb1,b2:bool.match b1 with
+ [ true ⇒ true | false ⇒ b2 ].
+
+ndefinition xor_bool ≝
+λb1,b2:bool.match b1 with
+ [ true ⇒ not_bool b2
+ | false ⇒ b2 ].
+
+(* \ominus *)
+notation "hvbox(⊖ a)" non associative with precedence 36
+ for @{ 'not_bool $a }.
+interpretation "not_bool" 'not_bool x = (not_bool x).
+
+(* \otimes *)
+notation "hvbox(a break ⊗ b)" left associative with precedence 35
+ for @{ 'and_bool $a $b }.
+interpretation "and_bool" 'and_bool x y = (and_bool x y).
+
+(* \oplus *)
+notation "hvbox(a break ⊕ b)" left associative with precedence 34
+ for @{ 'or_bool $a $b }.
+interpretation "or_bool" 'or_bool x y = (or_bool x y).
+
+(* \odot *)
+notation "hvbox(a break ⊙ b)" left associative with precedence 33
+ for @{ 'xor_bool $a $b }.
+interpretation "xor_bool" 'xor_bool x y = (xor_bool x y).
+
+ndefinition boolRelation : Type → Type ≝
+λA:Type.A → A → bool.

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
new file mode 100755 (executable)
index 0000000..5c08f23
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
@@ -0,0 +1,153 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/theory.ma".
+include "freescale/bool.ma".
+
+(* ******** *)
+(* BOOLEANI *)
+(* ******** *)
+
+ndefinition boolRelation : Type → Type ≝
+λA:Type.A → A → bool. 
+
+ndefinition boolSymmetric: ∀A:Type.∀R:boolRelation A.Prop ≝
+λA.λR.∀x,y:A.R x y = R y x.
+
+ntheorem bool_destruct_true_false : true ≠ false.
+ nnormalize;
+ #H;
+ nchange with (match true with [ true ⇒ False | false ⇒ True]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+ntheorem bool_destruct_false_true : false ≠ true.
+ nnormalize;
+ #H;
+ nchange with (match true with [ true ⇒ False | false ⇒ True]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma bsymmetric_eqbool : boolSymmetric bool eq_bool.
+ nnormalize;
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_andbool : boolSymmetric bool and_bool.
+ nnormalize;
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_orbool : boolSymmetric bool or_bool.
+ nnormalize;
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_xorbool : boolSymmetric bool xor_bool.
+ nnormalize;
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ #H;
+ ##[ ##2,3: nelim (bool_destruct_false_true H) ##]
+ napply (refl_eq ??).
+nqed.
+
+nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ #H;
+ ##[ ##2: nelim (bool_destruct_true_false H)
+ ##| ##3: nelim (bool_destruct_false_true H) ##]
+ napply (refl_eq ??).
+nqed.
+
+nlemma andb_true_true: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ #H;
+ ##[ ##3,4: nelim (bool_destruct_false_true H) ##]
+ napply (refl_eq ??).
+nqed.
+
+nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ #H;
+ ##[ ##2,3,4: nelim (bool_destruct_false_true H) ##]
+ napply (refl_eq ??).
+nqed.
+
+nlemma orb_false_false : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ #H;
+ ##[ ##1,2: nelim (bool_destruct_true_false H) ##]
+ napply (refl_eq ??).
+nqed.
+
+nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ #H;
+ ##[ ##1,3: nelim (bool_destruct_true_false H) ##]
+ napply (refl_eq ??).
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
new file mode 100755 (executable)
index 0000000..16fb11a
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
@@ -0,0 +1,1510 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/bool.ma".
+include "freescale/prod.ma".
+include "freescale/nat.ma".
+
+(* *********** *)
+(* ESADECIMALI *)
+(* *********** *)
+
+ninductive exadecim : Type ≝
+  x0: exadecim
+| x1: exadecim
+| x2: exadecim
+| x3: exadecim
+| x4: exadecim
+| x5: exadecim
+| x6: exadecim
+| x7: exadecim
+| x8: exadecim
+| x9: exadecim
+| xA: exadecim
+| xB: exadecim
+| xC: exadecim
+| xD: exadecim
+| xE: exadecim
+| xF: exadecim.
+
+ndefinition exadecim_ind :
+ ΠP:exadecim → Prop.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
+                    P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
+λP:exadecim → Prop.
+λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
+λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
+ match e with
+  [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
+  | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].                                     
+
+ndefinition exadecim_rec :
+ ΠP:exadecim → Set.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
+                    P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
+λP:exadecim → Set.
+λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
+λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
+ match e with
+  [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
+  | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].                                        
+
+ndefinition exadecim_rect :
+ ΠP:exadecim → Type.P x0 → P x1 → P x2 → P x3 → P x4 → P x5 → P x6 → P x7 →
+                    P x8 → P x9 → P xA → P xB → P xC → P xD → P xE → P xF → Πe:exadecim.P e ≝
+λP:exadecim → Type.
+λp:P x0.λp1:P x1.λp2:P x2.λp3:P x3.λp4:P x4.λp5:P x5.λp6:P x6.λp7:P x7.
+λp8:P x8.λp9:P x9.λp10:P xA.λp11:P xB.λp12:P xC.λp13:P xD.λp14:P xE.λp15:P xF.λe:exadecim.
+ match e with
+  [ x0 ⇒ p | x1 ⇒ p1 | x2 ⇒ p2 | x3 ⇒ p3 | x4 ⇒ p4 | x5 ⇒ p5 | x6 ⇒ p6 | x7 ⇒ p7
+  | x8 ⇒ p8 | x9 ⇒ p9 | xA ⇒ p10 |xB ⇒ p11 | xC ⇒ p12 | xD ⇒ p13 | xE ⇒ p14 | xF ⇒ p15 ].   
+
+(* operatore = *)
+ndefinition eq_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+  [ x0 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x1 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x2 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x3 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x4 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x5 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x6 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x7 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true 
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x8 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x9 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | xA ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | xB ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | xC ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | xD ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ] 
+  | xE ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ] 
+  | xF ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+  ].
+
+(* operatore < *)
+ndefinition lt_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+  [ x0 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+   | x4 ⇒ true  | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+   | xC ⇒ true  | xD ⇒ true | xE ⇒ true | xF ⇒ true ] 
+  | x1 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true | xB ⇒ true
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true | xF ⇒ true ] 
+  | x2 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x3 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x4 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x5 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x6 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x7 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false 
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x8 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x9 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xA ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xB ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xC ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xD ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true ] 
+  | xE ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ] 
+  | xF ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  ].
+
+(* operatore ≤ *)
+ndefinition le_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+  [ x0 ⇒ match e2 with
+   [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true 
+   | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+   | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true 
+   | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ] 
+  | x1 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true | xA ⇒ true | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true | xE ⇒ true | xF ⇒ true ] 
+  | x2 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true | xF ⇒ true ] 
+  | x3 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x4 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x5 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x6 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x7 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true 
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x8 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | x9 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xA ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xB ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xC ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xD ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
+  | xE ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true ] 
+  | xF ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+  ].
+
+(* operatore > *)
+ndefinition gt_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+  [ x0 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x1 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x2 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x3 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x4 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x5 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x6 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x7 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | x8 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | x9 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xA ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xB ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xC ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xD ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xE ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
+  | xF ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ false ]
+  ].
+
+(* operatore ≥ *)
+ndefinition ge_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+  [ x0 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x1 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x2 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ false 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x3 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x4 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x5 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x6 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x7 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | x8 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | x9 ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xA ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ false 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xB ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xC ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+  | xD ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ false | xF ⇒ false ]
+  | xE ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ false ]
+  | xF ⇒ match e2 with
+   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
+   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true 
+   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ]
+  ].
+
+(* operatore and *)
+ndefinition and_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
+  | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
+  | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0 
+  | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
+ | x1 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
+  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
+  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1 
+  | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
+ | x2 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
+  | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
+  | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2 
+  | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
+ | x3 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
+  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 
+  | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x4 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
+  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
+  | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0 
+  | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
+ | x5 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
+  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
+  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1 
+  | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x6 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
+  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
+  | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2 
+  | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
+ | x7 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
+  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 
+  | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+ | x8 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
+  | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
+  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8 
+  | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
+ | x9 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
+  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
+  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9 
+  | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xA ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
+  | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
+  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA 
+  | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
+ | xB ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
+  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
+  | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xC ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
+  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
+  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8 
+  | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ] 
+ | xD ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
+  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
+  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9 
+  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ] 
+ | xE ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
+  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
+  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA 
+  | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ] 
+ | xF ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
+  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
+  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ ]. 
+
+(* operatore or *)
+ndefinition or_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
+  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
+  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x1 ⇒ match e2 with
+  [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3 
+  | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
+  | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB 
+  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | x2 ⇒ match e2 with
+  [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3 
+  | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
+  | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB 
+  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | x3 ⇒ match e2 with
+  [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3 
+  | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
+  | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB 
+  | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | x4 ⇒ match e2 with
+  [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 
+  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+  | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
+  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x5 ⇒ match e2 with
+  [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7 
+  | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
+  | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF 
+  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | x6 ⇒ match e2 with
+  [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7 
+  | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
+  | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF 
+  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | x7 ⇒ match e2 with
+  [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7 
+  | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
+  | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF 
+  | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | x8 ⇒ match e2 with
+  [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB 
+  | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
+  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x9 ⇒ match e2 with
+  [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB 
+  | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
+  | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB 
+  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | xA ⇒ match e2 with
+  [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB 
+  | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
+  | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB 
+  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | xB ⇒ match e2 with
+  [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB 
+  | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
+  | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB 
+  | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | xC ⇒ match e2 with
+  [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF 
+  | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+  | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
+  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | xD ⇒ match e2 with
+  [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF 
+  | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
+  | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF 
+  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | xE ⇒ match e2 with
+  [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF 
+  | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
+  | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF 
+  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | xF ⇒ match e2 with
+  [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF 
+  | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
+  | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF 
+  | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ ].
+
+(* operatore xor *)
+ndefinition xor_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
+  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
+  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] 
+ | x1 ⇒ match e2 with
+  [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2 
+  | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
+  | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA 
+  | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ] 
+ | x2 ⇒ match e2 with
+  [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1 
+  | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
+  | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9 
+  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ] 
+ | x3 ⇒ match e2 with
+  [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0 
+  | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
+  | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8 
+  | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ] 
+ | x4 ⇒ match e2 with
+  [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 
+  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+  | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
+  | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ] 
+ | x5 ⇒ match e2 with
+  [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6 
+  | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
+  | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE 
+  | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ] 
+ | x6 ⇒ match e2 with
+  [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5 
+  | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
+  | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD 
+  | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ] 
+ | x7 ⇒ match e2 with
+  [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4 
+  | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
+  | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC 
+  | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ] 
+ | x8 ⇒ match e2 with
+  [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB 
+  | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 
+  | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ] 
+ | x9 ⇒ match e2 with
+  [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA 
+  | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
+  | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2 
+  | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ] 
+ | xA ⇒ match e2 with
+  [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9 
+  | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
+  | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1 
+  | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ] 
+ | xB ⇒ match e2 with
+  [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8 
+  | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
+  | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0 
+  | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
+ | xC ⇒ match e2 with
+  [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF 
+  | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+  | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 
+  | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ] 
+ | xD ⇒ match e2 with
+  [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE 
+  | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
+  | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6 
+  | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
+ | xE ⇒ match e2 with
+  [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD 
+  | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
+  | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5 
+  | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ] 
+ | xF ⇒ match e2 with
+  [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC 
+  | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
+  | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4 
+  | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ] 
+ ].
+
+(* operatore rotazione destra con carry *)
+ndefinition rcr_ex ≝
+λe:exadecim.λc:bool.match c with
+ [ true ⇒ match e with
+  [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
+  | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
+  | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
+  | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
+  | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
+  | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
+  | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
+  | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
+ | false ⇒ match e with 
+  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+  | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+  | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+  | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+  | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+  | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+  | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+  | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
+ ].
+
+(* operatore shift destro *)
+ndefinition shr_ex ≝
+λe:exadecim.match e with 
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
+
+(* operatore rotazione destra *)
+ndefinition ror_ex ≝
+λe:exadecim.match e with 
+ [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
+ | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB 
+ | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD 
+ | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
+
+(* operatore rotazione destra n-volte *)
+nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
+ match n with
+  [ O ⇒ e
+  | S n' ⇒ ror_ex_n (ror_ex e) n' ].
+
+(* operatore rotazione sinistra con carry *)
+ndefinition rcl_ex ≝
+λe:exadecim.λc:bool.match c with
+ [ true ⇒ match e with
+  [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
+  | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
+  | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
+  | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
+  | x8 ⇒ pair exadecim bool x1 true  | x9 ⇒ pair exadecim bool x3 true
+  | xA ⇒ pair exadecim bool x5 true  | xB ⇒ pair exadecim bool x7 true
+  | xC ⇒ pair exadecim bool x9 true  | xD ⇒ pair exadecim bool xB true
+  | xE ⇒ pair exadecim bool xD true  | xF ⇒ pair exadecim bool xF true ]
+ | false ⇒ match e with
+  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+  | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+  | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+  | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+  | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
+  | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
+  | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
+  | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ]
+ ].
+
+(* operatore shift sinistro *)
+ndefinition shl_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ].
+
+(* operatore rotazione sinistra *)
+ndefinition rol_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
+ | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
+ | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
+ | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
+
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
+ match n with
+  [ O ⇒ e
+  | S n' ⇒ rol_ex_n (rol_ex e) n' ].
+
+(* operatore not/complemento a 1 *)
+ndefinition not_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
+ | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
+ | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
+ | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
+
+(* operatore somma con carry *)
+ndefinition plus_ex ≝
+λe1,e2:exadecim.λc:bool.
+  match c with
+   [ true ⇒
+      match e1 with
+       [ x0 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x1 false
+            | x1 ⇒ pair exadecim bool x2 false
+            | x2 ⇒ pair exadecim bool x3 false
+            | x3 ⇒ pair exadecim bool x4 false
+            | x4 ⇒ pair exadecim bool x5 false
+            | x5 ⇒ pair exadecim bool x6 false
+            | x6 ⇒ pair exadecim bool x7 false
+            | x7 ⇒ pair exadecim bool x8 false
+            | x8 ⇒ pair exadecim bool x9 false
+            | x9 ⇒ pair exadecim bool xA false
+            | xA ⇒ pair exadecim bool xB false
+            | xB ⇒ pair exadecim bool xC false
+            | xC ⇒ pair exadecim bool xD false
+            | xD ⇒ pair exadecim bool xE false
+            | xE ⇒ pair exadecim bool xF false
+            | xF ⇒ pair exadecim bool x0 true ] 
+       | x1 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x2 false
+            | x1 ⇒ pair exadecim bool x3 false
+            | x2 ⇒ pair exadecim bool x4 false
+            | x3 ⇒ pair exadecim bool x5 false
+            | x4 ⇒ pair exadecim bool x6 false
+            | x5 ⇒ pair exadecim bool x7 false
+            | x6 ⇒ pair exadecim bool x8 false
+            | x7 ⇒ pair exadecim bool x9 false
+            | x8 ⇒ pair exadecim bool xA false
+            | x9 ⇒ pair exadecim bool xB false
+            | xA ⇒ pair exadecim bool xC false
+            | xB ⇒ pair exadecim bool xD false
+            | xC ⇒ pair exadecim bool xE false
+            | xD ⇒ pair exadecim bool xF false
+            | xE ⇒ pair exadecim bool x0 true
+            | xF ⇒ pair exadecim bool x1 true ] 
+       | x2 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x3 false
+            | x1 ⇒ pair exadecim bool x4 false
+            | x2 ⇒ pair exadecim bool x5 false
+            | x3 ⇒ pair exadecim bool x6 false
+            | x4 ⇒ pair exadecim bool x7 false
+            | x5 ⇒ pair exadecim bool x8 false
+            | x6 ⇒ pair exadecim bool x9 false
+            | x7 ⇒ pair exadecim bool xA false
+            | x8 ⇒ pair exadecim bool xB false
+            | x9 ⇒ pair exadecim bool xC false
+            | xA ⇒ pair exadecim bool xD false
+            | xB ⇒ pair exadecim bool xE false
+            | xC ⇒ pair exadecim bool xF false
+            | xD ⇒ pair exadecim bool x0 true
+            | xE ⇒ pair exadecim bool x1 true
+            | xF ⇒ pair exadecim bool x2 true ] 
+       | x3 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x4 false
+            | x1 ⇒ pair exadecim bool x5 false
+            | x2 ⇒ pair exadecim bool x6 false
+            | x3 ⇒ pair exadecim bool x7 false
+            | x4 ⇒ pair exadecim bool x8 false
+            | x5 ⇒ pair exadecim bool x9 false
+            | x6 ⇒ pair exadecim bool xA false
+            | x7 ⇒ pair exadecim bool xB false
+            | x8 ⇒ pair exadecim bool xC false
+            | x9 ⇒ pair exadecim bool xD false
+            | xA ⇒ pair exadecim bool xE false
+            | xB ⇒ pair exadecim bool xF false
+            | xC ⇒ pair exadecim bool x0 true
+            | xD ⇒ pair exadecim bool x1 true
+            | xE ⇒ pair exadecim bool x2 true
+            | xF ⇒ pair exadecim bool x3 true ] 
+       | x4 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x5 false
+            | x1 ⇒ pair exadecim bool x6 false
+            | x2 ⇒ pair exadecim bool x7 false
+            | x3 ⇒ pair exadecim bool x8 false
+            | x4 ⇒ pair exadecim bool x9 false
+            | x5 ⇒ pair exadecim bool xA false
+            | x6 ⇒ pair exadecim bool xB false
+            | x7 ⇒ pair exadecim bool xC false
+            | x8 ⇒ pair exadecim bool xD false
+            | x9 ⇒ pair exadecim bool xE false
+            | xA ⇒ pair exadecim bool xF false
+            | xB ⇒ pair exadecim bool x0 true
+            | xC ⇒ pair exadecim bool x1 true
+            | xD ⇒ pair exadecim bool x2 true
+            | xE ⇒ pair exadecim bool x3 true
+            | xF ⇒ pair exadecim bool x4 true ] 
+       | x5 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x6 false
+            | x1 ⇒ pair exadecim bool x7 false
+            | x2 ⇒ pair exadecim bool x8 false
+            | x3 ⇒ pair exadecim bool x9 false
+            | x4 ⇒ pair exadecim bool xA false
+            | x5 ⇒ pair exadecim bool xB false
+            | x6 ⇒ pair exadecim bool xC false
+            | x7 ⇒ pair exadecim bool xD false
+            | x8 ⇒ pair exadecim bool xE false
+            | x9 ⇒ pair exadecim bool xF false
+            | xA ⇒ pair exadecim bool x0 true
+            | xB ⇒ pair exadecim bool x1 true
+            | xC ⇒ pair exadecim bool x2 true
+            | xD ⇒ pair exadecim bool x3 true
+            | xE ⇒ pair exadecim bool x4 true
+            | xF ⇒ pair exadecim bool x5 true ] 
+       | x6 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x7 false
+            | x1 ⇒ pair exadecim bool x8 false
+            | x2 ⇒ pair exadecim bool x9 false
+            | x3 ⇒ pair exadecim bool xA false
+            | x4 ⇒ pair exadecim bool xB false
+            | x5 ⇒ pair exadecim bool xC false
+            | x6 ⇒ pair exadecim bool xD false
+            | x7 ⇒ pair exadecim bool xE false
+            | x8 ⇒ pair exadecim bool xF false
+            | x9 ⇒ pair exadecim bool x0 true
+            | xA ⇒ pair exadecim bool x1 true
+            | xB ⇒ pair exadecim bool x2 true
+            | xC ⇒ pair exadecim bool x3 true
+            | xD ⇒ pair exadecim bool x4 true
+            | xE ⇒ pair exadecim bool x5 true
+            | xF ⇒ pair exadecim bool x6 true ] 
+       | x7 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x8 false
+            | x1 ⇒ pair exadecim bool x9 false
+            | x2 ⇒ pair exadecim bool xA false
+            | x3 ⇒ pair exadecim bool xB false
+            | x4 ⇒ pair exadecim bool xC false
+            | x5 ⇒ pair exadecim bool xD false
+            | x6 ⇒ pair exadecim bool xE false
+            | x7 ⇒ pair exadecim bool xF false
+            | x8 ⇒ pair exadecim bool x0 true
+            | x9 ⇒ pair exadecim bool x1 true
+            | xA ⇒ pair exadecim bool x2 true
+            | xB ⇒ pair exadecim bool x3 true
+            | xC ⇒ pair exadecim bool x4 true
+            | xD ⇒ pair exadecim bool x5 true
+            | xE ⇒ pair exadecim bool x6 true
+            | xF ⇒ pair exadecim bool x7 true ] 
+       | x8 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x9 false
+            | x1 ⇒ pair exadecim bool xA false
+            | x2 ⇒ pair exadecim bool xB false
+            | x3 ⇒ pair exadecim bool xC false
+            | x4 ⇒ pair exadecim bool xD false
+            | x5 ⇒ pair exadecim bool xE false
+            | x6 ⇒ pair exadecim bool xF false
+            | x7 ⇒ pair exadecim bool x0 true
+            | x8 ⇒ pair exadecim bool x1 true
+            | x9 ⇒ pair exadecim bool x2 true
+            | xA ⇒ pair exadecim bool x3 true
+            | xB ⇒ pair exadecim bool x4 true
+            | xC ⇒ pair exadecim bool x5 true
+            | xD ⇒ pair exadecim bool x6 true
+            | xE ⇒ pair exadecim bool x7 true
+            | xF ⇒ pair exadecim bool x8 true ] 
+       | x9 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xA false
+            | x1 ⇒ pair exadecim bool xB false
+            | x2 ⇒ pair exadecim bool xC false
+            | x3 ⇒ pair exadecim bool xD false
+            | x4 ⇒ pair exadecim bool xE false
+            | x5 ⇒ pair exadecim bool xF false
+            | x6 ⇒ pair exadecim bool x0 true
+            | x7 ⇒ pair exadecim bool x1 true
+            | x8 ⇒ pair exadecim bool x2 true
+            | x9 ⇒ pair exadecim bool x3 true
+            | xA ⇒ pair exadecim bool x4 true
+            | xB ⇒ pair exadecim bool x5 true
+            | xC ⇒ pair exadecim bool x6 true
+            | xD ⇒ pair exadecim bool x7 true
+            | xE ⇒ pair exadecim bool x8 true
+            | xF ⇒ pair exadecim bool x9 true ] 
+       | xA ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xB false
+            | x1 ⇒ pair exadecim bool xC false
+            | x2 ⇒ pair exadecim bool xD false
+            | x3 ⇒ pair exadecim bool xE false
+            | x4 ⇒ pair exadecim bool xF false
+            | x5 ⇒ pair exadecim bool x0 true
+            | x6 ⇒ pair exadecim bool x1 true
+            | x7 ⇒ pair exadecim bool x2 true
+            | x8 ⇒ pair exadecim bool x3 true
+            | x9 ⇒ pair exadecim bool x4 true
+            | xA ⇒ pair exadecim bool x5 true
+            | xB ⇒ pair exadecim bool x6 true
+            | xC ⇒ pair exadecim bool x7 true
+            | xD ⇒ pair exadecim bool x8 true
+            | xE ⇒ pair exadecim bool x9 true
+            | xF ⇒ pair exadecim bool xA true ] 
+       | xB ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xC false
+            | x1 ⇒ pair exadecim bool xD false
+            | x2 ⇒ pair exadecim bool xE false
+            | x3 ⇒ pair exadecim bool xF false
+            | x4 ⇒ pair exadecim bool x0 true
+            | x5 ⇒ pair exadecim bool x1 true
+            | x6 ⇒ pair exadecim bool x2 true
+            | x7 ⇒ pair exadecim bool x3 true
+            | x8 ⇒ pair exadecim bool x4 true
+            | x9 ⇒ pair exadecim bool x5 true
+            | xA ⇒ pair exadecim bool x6 true
+            | xB ⇒ pair exadecim bool x7 true
+            | xC ⇒ pair exadecim bool x8 true
+            | xD ⇒ pair exadecim bool x9 true
+            | xE ⇒ pair exadecim bool xA true
+            | xF ⇒ pair exadecim bool xB true ] 
+       | xC ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xD false
+            | x1 ⇒ pair exadecim bool xE false
+            | x2 ⇒ pair exadecim bool xF false
+            | x3 ⇒ pair exadecim bool x0 true
+            | x4 ⇒ pair exadecim bool x1 true
+            | x5 ⇒ pair exadecim bool x2 true
+            | x6 ⇒ pair exadecim bool x3 true
+            | x7 ⇒ pair exadecim bool x4 true
+            | x8 ⇒ pair exadecim bool x5 true
+            | x9 ⇒ pair exadecim bool x6 true
+            | xA ⇒ pair exadecim bool x7 true
+            | xB ⇒ pair exadecim bool x8 true
+            | xC ⇒ pair exadecim bool x9 true
+            | xD ⇒ pair exadecim bool xA true
+            | xE ⇒ pair exadecim bool xB true
+            | xF ⇒ pair exadecim bool xC true ] 
+       | xD ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xE false
+            | x1 ⇒ pair exadecim bool xF false
+            | x2 ⇒ pair exadecim bool x0 true
+            | x3 ⇒ pair exadecim bool x1 true
+            | x4 ⇒ pair exadecim bool x2 true
+            | x5 ⇒ pair exadecim bool x3 true
+            | x6 ⇒ pair exadecim bool x4 true
+            | x7 ⇒ pair exadecim bool x5 true
+            | x8 ⇒ pair exadecim bool x6 true
+            | x9 ⇒ pair exadecim bool x7 true
+            | xA ⇒ pair exadecim bool x8 true
+            | xB ⇒ pair exadecim bool x9 true
+            | xC ⇒ pair exadecim bool xA true
+            | xD ⇒ pair exadecim bool xB true
+            | xE ⇒ pair exadecim bool xC true
+            | xF ⇒ pair exadecim bool xD true ] 
+       | xE ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xF false
+            | x1 ⇒ pair exadecim bool x0 true
+            | x2 ⇒ pair exadecim bool x1 true
+            | x3 ⇒ pair exadecim bool x2 true
+            | x4 ⇒ pair exadecim bool x3 true
+            | x5 ⇒ pair exadecim bool x4 true
+            | x6 ⇒ pair exadecim bool x5 true
+            | x7 ⇒ pair exadecim bool x6 true
+            | x8 ⇒ pair exadecim bool x7 true
+            | x9 ⇒ pair exadecim bool x8 true
+            | xA ⇒ pair exadecim bool x9 true
+            | xB ⇒ pair exadecim bool xA true
+            | xC ⇒ pair exadecim bool xB true
+            | xD ⇒ pair exadecim bool xC true
+            | xE ⇒ pair exadecim bool xD true
+            | xF ⇒ pair exadecim bool xE true ]
+       | xF ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x0 true
+            | x1 ⇒ pair exadecim bool x1 true
+            | x2 ⇒ pair exadecim bool x2 true
+            | x3 ⇒ pair exadecim bool x3 true
+            | x4 ⇒ pair exadecim bool x4 true
+            | x5 ⇒ pair exadecim bool x5 true
+            | x6 ⇒ pair exadecim bool x6 true
+            | x7 ⇒ pair exadecim bool x7 true
+            | x8 ⇒ pair exadecim bool x8 true
+            | x9 ⇒ pair exadecim bool x9 true
+            | xA ⇒ pair exadecim bool xA true
+            | xB ⇒ pair exadecim bool xB true
+            | xC ⇒ pair exadecim bool xC true
+            | xD ⇒ pair exadecim bool xD true
+            | xE ⇒ pair exadecim bool xE true
+            | xF ⇒ pair exadecim bool xF true ] 
+       ]
+   | false ⇒
+      match e1 with
+       [ x0 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x0 false
+            | x1 ⇒ pair exadecim bool x1 false
+            | x2 ⇒ pair exadecim bool x2 false
+            | x3 ⇒ pair exadecim bool x3 false
+            | x4 ⇒ pair exadecim bool x4 false
+            | x5 ⇒ pair exadecim bool x5 false
+            | x6 ⇒ pair exadecim bool x6 false
+            | x7 ⇒ pair exadecim bool x7 false
+            | x8 ⇒ pair exadecim bool x8 false
+            | x9 ⇒ pair exadecim bool x9 false
+            | xA ⇒ pair exadecim bool xA false
+            | xB ⇒ pair exadecim bool xB false
+            | xC ⇒ pair exadecim bool xC false
+            | xD ⇒ pair exadecim bool xD false
+            | xE ⇒ pair exadecim bool xE false
+            | xF ⇒ pair exadecim bool xF false ] 
+       | x1 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x1 false
+            | x1 ⇒ pair exadecim bool x2 false
+            | x2 ⇒ pair exadecim bool x3 false
+            | x3 ⇒ pair exadecim bool x4 false
+            | x4 ⇒ pair exadecim bool x5 false
+            | x5 ⇒ pair exadecim bool x6 false
+            | x6 ⇒ pair exadecim bool x7 false
+            | x7 ⇒ pair exadecim bool x8 false
+            | x8 ⇒ pair exadecim bool x9 false
+            | x9 ⇒ pair exadecim bool xA false
+            | xA ⇒ pair exadecim bool xB false
+            | xB ⇒ pair exadecim bool xC false
+            | xC ⇒ pair exadecim bool xD false
+            | xD ⇒ pair exadecim bool xE false
+            | xE ⇒ pair exadecim bool xF false
+            | xF ⇒ pair exadecim bool x0 true ] 
+       | x2 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x2 false
+            | x1 ⇒ pair exadecim bool x3 false
+            | x2 ⇒ pair exadecim bool x4 false
+            | x3 ⇒ pair exadecim bool x5 false
+            | x4 ⇒ pair exadecim bool x6 false
+            | x5 ⇒ pair exadecim bool x7 false
+            | x6 ⇒ pair exadecim bool x8 false
+            | x7 ⇒ pair exadecim bool x9 false
+            | x8 ⇒ pair exadecim bool xA false
+            | x9 ⇒ pair exadecim bool xB false
+            | xA ⇒ pair exadecim bool xC false
+            | xB ⇒ pair exadecim bool xD false
+            | xC ⇒ pair exadecim bool xE false
+            | xD ⇒ pair exadecim bool xF false
+            | xE ⇒ pair exadecim bool x0 true
+            | xF ⇒ pair exadecim bool x1 true ] 
+       | x3 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x3 false
+            | x1 ⇒ pair exadecim bool x4 false
+            | x2 ⇒ pair exadecim bool x5 false
+            | x3 ⇒ pair exadecim bool x6 false
+            | x4 ⇒ pair exadecim bool x7 false
+            | x5 ⇒ pair exadecim bool x8 false
+            | x6 ⇒ pair exadecim bool x9 false
+            | x7 ⇒ pair exadecim bool xA false
+            | x8 ⇒ pair exadecim bool xB false
+            | x9 ⇒ pair exadecim bool xC false
+            | xA ⇒ pair exadecim bool xD false
+            | xB ⇒ pair exadecim bool xE false
+            | xC ⇒ pair exadecim bool xF false
+            | xD ⇒ pair exadecim bool x0 true
+            | xE ⇒ pair exadecim bool x1 true
+            | xF ⇒ pair exadecim bool x2 true ] 
+       | x4 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x4 false
+            | x1 ⇒ pair exadecim bool x5 false
+            | x2 ⇒ pair exadecim bool x6 false
+            | x3 ⇒ pair exadecim bool x7 false
+            | x4 ⇒ pair exadecim bool x8 false
+            | x5 ⇒ pair exadecim bool x9 false
+            | x6 ⇒ pair exadecim bool xA false
+            | x7 ⇒ pair exadecim bool xB false
+            | x8 ⇒ pair exadecim bool xC false
+            | x9 ⇒ pair exadecim bool xD false
+            | xA ⇒ pair exadecim bool xE false
+            | xB ⇒ pair exadecim bool xF false
+            | xC ⇒ pair exadecim bool x0 true
+            | xD ⇒ pair exadecim bool x1 true
+            | xE ⇒ pair exadecim bool x2 true
+            | xF ⇒ pair exadecim bool x3 true ] 
+       | x5 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x5 false
+            | x1 ⇒ pair exadecim bool x6 false
+            | x2 ⇒ pair exadecim bool x7 false
+            | x3 ⇒ pair exadecim bool x8 false
+            | x4 ⇒ pair exadecim bool x9 false
+            | x5 ⇒ pair exadecim bool xA false
+            | x6 ⇒ pair exadecim bool xB false
+            | x7 ⇒ pair exadecim bool xC false
+            | x8 ⇒ pair exadecim bool xD false
+            | x9 ⇒ pair exadecim bool xE false
+            | xA ⇒ pair exadecim bool xF false
+            | xB ⇒ pair exadecim bool x0 true
+            | xC ⇒ pair exadecim bool x1 true
+            | xD ⇒ pair exadecim bool x2 true
+            | xE ⇒ pair exadecim bool x3 true
+            | xF ⇒ pair exadecim bool x4 true ] 
+       | x6 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x6 false
+            | x1 ⇒ pair exadecim bool x7 false
+            | x2 ⇒ pair exadecim bool x8 false
+            | x3 ⇒ pair exadecim bool x9 false
+            | x4 ⇒ pair exadecim bool xA false
+            | x5 ⇒ pair exadecim bool xB false
+            | x6 ⇒ pair exadecim bool xC false
+            | x7 ⇒ pair exadecim bool xD false
+            | x8 ⇒ pair exadecim bool xE false
+            | x9 ⇒ pair exadecim bool xF false
+            | xA ⇒ pair exadecim bool x0 true
+            | xB ⇒ pair exadecim bool x1 true
+            | xC ⇒ pair exadecim bool x2 true
+            | xD ⇒ pair exadecim bool x3 true
+            | xE ⇒ pair exadecim bool x4 true
+            | xF ⇒ pair exadecim bool x5 true ] 
+       | x7 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x7 false
+            | x1 ⇒ pair exadecim bool x8 false
+            | x2 ⇒ pair exadecim bool x9 false
+            | x3 ⇒ pair exadecim bool xA false
+            | x4 ⇒ pair exadecim bool xB false
+            | x5 ⇒ pair exadecim bool xC false
+            | x6 ⇒ pair exadecim bool xD false
+            | x7 ⇒ pair exadecim bool xE false
+            | x8 ⇒ pair exadecim bool xF false
+            | x9 ⇒ pair exadecim bool x0 true
+            | xA ⇒ pair exadecim bool x1 true
+            | xB ⇒ pair exadecim bool x2 true
+            | xC ⇒ pair exadecim bool x3 true
+            | xD ⇒ pair exadecim bool x4 true
+            | xE ⇒ pair exadecim bool x5 true
+            | xF ⇒ pair exadecim bool x6 true ] 
+       | x8 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x8 false
+            | x1 ⇒ pair exadecim bool x9 false
+            | x2 ⇒ pair exadecim bool xA false
+            | x3 ⇒ pair exadecim bool xB false
+            | x4 ⇒ pair exadecim bool xC false
+            | x5 ⇒ pair exadecim bool xD false
+            | x6 ⇒ pair exadecim bool xE false
+            | x7 ⇒ pair exadecim bool xF false
+            | x8 ⇒ pair exadecim bool x0 true
+            | x9 ⇒ pair exadecim bool x1 true
+            | xA ⇒ pair exadecim bool x2 true
+            | xB ⇒ pair exadecim bool x3 true
+            | xC ⇒ pair exadecim bool x4 true
+            | xD ⇒ pair exadecim bool x5 true
+            | xE ⇒ pair exadecim bool x6 true
+            | xF ⇒ pair exadecim bool x7 true ] 
+       | x9 ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool x9 false
+            | x1 ⇒ pair exadecim bool xA false
+            | x2 ⇒ pair exadecim bool xB false
+            | x3 ⇒ pair exadecim bool xC false
+            | x4 ⇒ pair exadecim bool xD false
+            | x5 ⇒ pair exadecim bool xE false
+            | x6 ⇒ pair exadecim bool xF false
+            | x7 ⇒ pair exadecim bool x0 true
+            | x8 ⇒ pair exadecim bool x1 true
+            | x9 ⇒ pair exadecim bool x2 true
+            | xA ⇒ pair exadecim bool x3 true
+            | xB ⇒ pair exadecim bool x4 true
+            | xC ⇒ pair exadecim bool x5 true
+            | xD ⇒ pair exadecim bool x6 true
+            | xE ⇒ pair exadecim bool x7 true
+            | xF ⇒ pair exadecim bool x8 true ] 
+       | xA ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xA false
+            | x1 ⇒ pair exadecim bool xB false
+            | x2 ⇒ pair exadecim bool xC false
+            | x3 ⇒ pair exadecim bool xD false
+            | x4 ⇒ pair exadecim bool xE false
+            | x5 ⇒ pair exadecim bool xF false
+            | x6 ⇒ pair exadecim bool x0 true
+            | x7 ⇒ pair exadecim bool x1 true
+            | x8 ⇒ pair exadecim bool x2 true
+            | x9 ⇒ pair exadecim bool x3 true
+            | xA ⇒ pair exadecim bool x4 true
+            | xB ⇒ pair exadecim bool x5 true
+            | xC ⇒ pair exadecim bool x6 true
+            | xD ⇒ pair exadecim bool x7 true
+            | xE ⇒ pair exadecim bool x8 true
+            | xF ⇒ pair exadecim bool x9 true ] 
+       | xB ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xB false
+            | x1 ⇒ pair exadecim bool xC false
+            | x2 ⇒ pair exadecim bool xD false
+            | x3 ⇒ pair exadecim bool xE false
+            | x4 ⇒ pair exadecim bool xF false
+            | x5 ⇒ pair exadecim bool x0 true
+            | x6 ⇒ pair exadecim bool x1 true
+            | x7 ⇒ pair exadecim bool x2 true
+            | x8 ⇒ pair exadecim bool x3 true
+            | x9 ⇒ pair exadecim bool x4 true
+            | xA ⇒ pair exadecim bool x5 true
+            | xB ⇒ pair exadecim bool x6 true
+            | xC ⇒ pair exadecim bool x7 true
+            | xD ⇒ pair exadecim bool x8 true
+            | xE ⇒ pair exadecim bool x9 true
+            | xF ⇒ pair exadecim bool xA true ] 
+       | xC ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xC false
+            | x1 ⇒ pair exadecim bool xD false
+            | x2 ⇒ pair exadecim bool xE false
+            | x3 ⇒ pair exadecim bool xF false
+            | x4 ⇒ pair exadecim bool x0 true
+            | x5 ⇒ pair exadecim bool x1 true
+            | x6 ⇒ pair exadecim bool x2 true
+            | x7 ⇒ pair exadecim bool x3 true
+            | x8 ⇒ pair exadecim bool x4 true
+            | x9 ⇒ pair exadecim bool x5 true
+            | xA ⇒ pair exadecim bool x6 true
+            | xB ⇒ pair exadecim bool x7 true
+            | xC ⇒ pair exadecim bool x8 true
+            | xD ⇒ pair exadecim bool x9 true
+            | xE ⇒ pair exadecim bool xA true
+            | xF ⇒ pair exadecim bool xB true ] 
+       | xD ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xD false
+            | x1 ⇒ pair exadecim bool xE false
+            | x2 ⇒ pair exadecim bool xF false
+            | x3 ⇒ pair exadecim bool x0 true
+            | x4 ⇒ pair exadecim bool x1 true
+            | x5 ⇒ pair exadecim bool x2 true
+            | x6 ⇒ pair exadecim bool x3 true
+            | x7 ⇒ pair exadecim bool x4 true
+            | x8 ⇒ pair exadecim bool x5 true
+            | x9 ⇒ pair exadecim bool x6 true
+            | xA ⇒ pair exadecim bool x7 true
+            | xB ⇒ pair exadecim bool x8 true
+            | xC ⇒ pair exadecim bool x9 true
+            | xD ⇒ pair exadecim bool xA true
+            | xE ⇒ pair exadecim bool xB true
+            | xF ⇒ pair exadecim bool xC true ] 
+       | xE ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xE false
+            | x1 ⇒ pair exadecim bool xF false
+            | x2 ⇒ pair exadecim bool x0 true
+            | x3 ⇒ pair exadecim bool x1 true
+            | x4 ⇒ pair exadecim bool x2 true
+            | x5 ⇒ pair exadecim bool x3 true
+            | x6 ⇒ pair exadecim bool x4 true
+            | x7 ⇒ pair exadecim bool x5 true
+            | x8 ⇒ pair exadecim bool x6 true
+            | x9 ⇒ pair exadecim bool x7 true
+            | xA ⇒ pair exadecim bool x8 true
+            | xB ⇒ pair exadecim bool x9 true
+            | xC ⇒ pair exadecim bool xA true
+            | xD ⇒ pair exadecim bool xB true
+            | xE ⇒ pair exadecim bool xC true
+            | xF ⇒ pair exadecim bool xD true ] 
+       | xF ⇒
+           match e2 with
+            [ x0 ⇒ pair exadecim bool xF false
+            | x1 ⇒ pair exadecim bool x0 true
+            | x2 ⇒ pair exadecim bool x1 true
+            | x3 ⇒ pair exadecim bool x2 true
+            | x4 ⇒ pair exadecim bool x3 true
+            | x5 ⇒ pair exadecim bool x4 true
+            | x6 ⇒ pair exadecim bool x5 true
+            | x7 ⇒ pair exadecim bool x6 true
+            | x8 ⇒ pair exadecim bool x7 true
+            | x9 ⇒ pair exadecim bool x8 true
+            | xA ⇒ pair exadecim bool x9 true
+            | xB ⇒ pair exadecim bool xA true
+            | xC ⇒ pair exadecim bool xB true
+            | xD ⇒ pair exadecim bool xC true
+            | xE ⇒ pair exadecim bool xD true
+            | xF ⇒ pair exadecim bool xE true ]
+       ]
+   ].
+
+(* operatore somma senza carry *)
+ndefinition plus_exnc ≝
+λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
+
+(* operatore carry della somma *)
+ndefinition plus_exc ≝
+λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true
+ | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ].
+
+(* esadecimali → naturali *)
+ndefinition nat_of_exadecim : exadecim → nat ≝
+λe:exadecim.
+ match e with
+  [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2  | x3 ⇒ 3  | x4 ⇒ 4  | x5 ⇒ 5  | x6 ⇒ 6  | x7 ⇒ 7
+  | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
+
+(* operatore predecessore *)
+ndefinition pred_ex ≝
+λe:exadecim.
+ match e with
+  [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+  | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
+
+(* operatore successore *)
+ndefinition succ_ex ≝
+λe:exadecim.
+ match e with
+  [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+  | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
+
+(* operatore neg/complemento a 2 *)
+ndefinition compl_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
+ | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
+ | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
+ | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
+
+(* iteratore sugli esadecimali *)
+ndefinition forall_exadecim ≝ λP.
+ P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
+ P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/nat.ma b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
new file mode 100755 (executable)
index 0000000..cff29e3
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/nat.ma
@@ -0,0 +1,71 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/pts.ma".
+include "freescale/bool.ma".
+
+(* ******** *)
+(* NATURALI *)
+(* ******** *)
+
+inductive nat : Type ≝
+  O : nat
+| S : nat → nat.
+
+interpretation "Natural numbers" 'N = nat.
+
+default "natural numbers" cic:/matita/freescale/nat/nat.ind.
+
+alias num (instance 0) = "natural number".
+
+nlet rec nat_ind (P:nat → Prop) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
+ match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_ind P p f n1) ].
+
+nlet rec nat_rec (P:nat → Set) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
+ match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rec P p f n1) ].
+
+nlet rec nat_rect (P:nat → Type) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
+ match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rect P p f n1) ].
+
+nlet rec eq_nat (n1,n2:nat) on n1 ≝
+ match n1 with
+  [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
+  | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
+  ].
+
+nlet rec plus (n1,n2:nat) on n1 ≝ 
+ match n1 with
+  [ O ⇒ n2
+  | (S n1') ⇒ S (plus n1' n2) ].
+
+interpretation "natural plus" 'plus x y = (plus x y).
+
+nlet rec times (n1,n2:nat) on n1 ≝ 
+ match n1 with 
+  [ O ⇒ O
+  | (S n1') ⇒ n2 + (times n1' n2) ].
+
+interpretation "natural times" 'times x y = (times x y).

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma
new file mode 100644 (file)
index 0000000..fde0972
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/nat_lemmas.ma
@@ -0,0 +1,115 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/bool_lemmas.ma".
+include "freescale/nat.ma".
+
+(* ******** *)
+(* NATURALI *)
+(* ******** *)
+
+nlemma nat_destruct : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
+ #n1; #n2; #H;
+ nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
+ #n; #H;
+ nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
+ #n; #H;
+ nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma bsymmetric_eqnat : boolSymmetric nat eq_nat.
+ nnormalize;
+ #n1;
+ nelim n1;
+ ##[ ##1: #n2;
+          nelim n2;
+          nnormalize;
+          ##[ ##1: napply (refl_eq ??)
+          ##| ##2: #n3; #H; napply (refl_eq ??)
+          ##]
+ ##| ##2: #n2; #H; #n3;
+          nnormalize;
+          ncases n3;
+          nnormalize;
+          ##[ ##1: napply (refl_eq ??)
+          ##| ##2: #n4; napply (H n4)
+          ##]
+ ##]
+nqed.  
+
+nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
+ #n1;
+ nelim n1;
+ ##[ ##1: #n2;
+          nelim n2;
+          nnormalize;
+          ##[ ##1: #H; napply (refl_eq ??)
+          ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1)
+          ##]
+ ##| ##2: #n2; #H; #n3; #H1;
+          ncases n3 in H1:(%) ⊢ %;
+          nnormalize;
+          ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
+          ##| ##2: #n4; #H1;
+                   napply (H n4 (nat_destruct ?? H1))
+          ##]
+ ##]
+nqed. 
+
+nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
+ #n1;
+ nelim n1;
+ ##[ ##1: #n2;
+          nelim n2;
+          nnormalize;
+          ##[ ##1: #H; napply (refl_eq ??)
+          ##| ##2: #n3; #H; #H1; nelim (bool_destruct_false_true H1)
+          ##]
+ ##| ##2: #n2; #H; #n3; #H1;
+          ncases n3 in H1:(%) ⊢ %;
+          nnormalize;
+          ##[ ##1: #H1; nelim (bool_destruct_false_true H1)
+          ##| ##2: #n4; #H1;
+                   nrewrite > (H n4 H1);
+                   napply (refl_eq ??)
+          ##]
+ ##]
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option.ma b/helm/software/matita/contribs/ng_assembly/freescale/option.ma
new file mode 100644 (file)
index 0000000..2041a2a
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/option.ma
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/bool.ma".
+
+(* ****** *)
+(* OPTION *)
+(* ****** *)
+
+ninductive option (A:Type) : Type ≝
+  None : option A
+| Some : A → option A.
+
+ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πo:option A.P o ≝
+λA:Type.λP:option A → Prop.λp:P (None A).λf:Πa:A.P (Some A a).λo:option A.
+ match o with [ None ⇒ p | Some (a:A) ⇒ f a ].
+
+ndefinition option_rec : ΠA:Type.ΠP:option A → Set.P (None A) → (Πa:A.P (Some A a)) → Πo:option A.P o ≝
+λA:Type.λP:option A → Set.λp:P (None A).λf:Πa:A.P (Some A a).λo:option A.
+ match o with [ None ⇒ p | Some (a:A) ⇒ f a ].
+
+ndefinition option_rect : ΠA:Type.ΠP:option A → Type.P (None A) → (Πa:A.P (Some A a)) → Πo:option A.P o ≝
+λA:Type.λP:option A → Type.λp:P (None A).λf:Πa:A.P (Some A a).λo:option A.
+ match o with [ None ⇒ p | Some (a:A) ⇒ f a ].
+
+ndefinition eq_option ≝
+λT.λo1,o2:option T.λf:T → T → bool.
+ match o1 with
+  [ None ⇒ match o2 with [ None ⇒ true | Some _ ⇒ false ]
+  | Some x1 ⇒ match o2 with [ None ⇒ false | Some x2 ⇒ f x1 x2 ]
+  ].
+
+(* option map = match ... with [ None ⇒ None ? | Some .. ⇒ .. ] *)
+ndefinition opt_map ≝
+λT1,T2:Type.λt:option T1.λf:T1 → option T2.
+ match t with [ None ⇒ None ? | Some x ⇒ (f x) ].

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
new file mode 100644 (file)
index 0000000..071d884
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
@@ -0,0 +1,104 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/bool_lemmas.ma".
+include "freescale/option.ma".
+
+(* ****** *)
+(* OPTION *)
+(* ****** *)
+
+nlemma option_destruct : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
+ #T; #x1; #x2; #H;
+ nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
+ #T; #x; #H;
+ nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
+ #T; #x; #H;
+ nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma bsymmetric_eqoption :
+∀T:Type.∀o1,o2:option T.∀f:T → T → bool.
+ (boolSymmetric T f) →
+ (eq_option T o1 o2 f = eq_option T o2 o1 f).
+ #T; #o1; #o2; #f; #H;
+ ncases o1;
+ ncases o2;
+ nnormalize;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##2,3: #x; napply (refl_eq ??)
+ ##| ##4: #x1; #x2; nrewrite > (H x1 x2); napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqoption :
+∀T.∀o1,o2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
+ (o1 = o2 → eq_option T o1 o2 f = true).
+ #T; #o1; #o2; #f; #H;
+ ncases o1;
+ ncases o2;
+ ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
+ ##| ##2: #H1; #H2; nelim (option_destruct_none_some ?? H2)
+ ##| ##3: #H1; #H2; nelim (option_destruct_some_none ?? H2)
+ ##| ##4: #x1; #x2; #H1;
+          nrewrite > (option_destruct ??? H1);
+          nnormalize;
+          nrewrite > (H x1 x1 (refl_eq ??));
+          napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eqoption_to_eq :
+∀T.∀o1,o2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
+ (eq_option T o1 o2 f = true → o1 = o2).
+ #T; #o1; #o2; #f; #H;
+ ncases o1;
+ ncases o2;
+ ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
+ ##| ##2,3: #H1; #H2; nnormalize in H2:(%); nelim (bool_destruct_false_true H2)
+ ##| ##4: #x1; #x2; #H1;
+          nnormalize in H1:(%);
+          nrewrite > (H ?? H1);
+          napply (refl_eq ??)
+ ##]
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
new file mode 100644 (file)
index 0000000..081d434
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma
@@ -0,0 +1,221 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/bool.ma".
+
+(* ***** *)
+(* TUPLE *)
+(* ***** *)
+
+ninductive ProdT (T1:Type) (T2:Type) : Type ≝
+ pair : T1 → T2 → ProdT T1 T2.
+
+ndefinition ProdT_ind
+ : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Prop.
+   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
+   Πp:ProdT T1 T2.P p ≝
+λT1,T2:Type.λP:ProdT T1 T2 → Prop.
+λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
+λp:ProdT T1 T2.
+ match p with [ pair t t1 ⇒ f t t1 ].
+
+ndefinition ProdT_rec
+ : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Set.
+   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
+   Πp:ProdT T1 T2.P p ≝
+λT1,T2:Type.λP:ProdT T1 T2 → Set.
+λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
+λp:ProdT T1 T2.
+ match p with [ pair t t1 ⇒ f t t1 ].
+
+ndefinition ProdT_rect
+ : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Type.
+   (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
+   Πp:ProdT T1 T2.P p ≝
+λT1,T2:Type.λP:ProdT T1 T2 → Type.
+λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
+λp:ProdT T1 T2.
+ match p with [ pair t t1 ⇒ f t t1 ].
+
+ndefinition fst ≝
+λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  x _ ⇒ x ].
+
+ndefinition snd ≝
+λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  _ x ⇒ x ].
+
+ndefinition eq_pair ≝
+λT1,T2:Type.λp1,p2:ProdT T1 T2.
+λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
+ match p1 with [ pair x1 y1 ⇒
+  match p2 with [ pair x2 y2 ⇒
+   (f1 x1 x2) ⊗ (f2 y1 y2) ]].
+
+ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
+triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
+
+ndefinition Prod3T_ind
+ : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Prop.
+   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
+   Πp:Prod3T T1 T2 T3.P p ≝
+λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Prop.
+λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
+λp:Prod3T T1 T2 T3.
+ match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
+
+ndefinition Prod3T_rec
+ : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Set.
+   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
+   Πp:Prod3T T1 T2 T3.P p ≝
+λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Set.
+λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
+λp:Prod3T T1 T2 T3.
+ match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
+
+ndefinition Prod3T_rect
+ : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Type.
+   (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
+   Πp:Prod3T T1 T2 T3.P p ≝
+λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Type.
+λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
+λp:Prod3T T1 T2 T3.
+ match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
+
+ndefinition fst3T ≝
+λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
+
+ndefinition snd3T ≝
+λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ x _ ⇒ x ].
+
+ndefinition thd3T ≝
+λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
+
+ndefinition eq_triple ≝
+λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
+λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
+ match p1 with [ triple x1 y1 z1 ⇒
+  match p2 with [ triple x2 y2 z2 ⇒
+   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ]].
+
+ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
+quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
+
+ndefinition Prod4T_ind
+ : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Prop.
+   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
+   Πp:Prod4T T1 T2 T3 T4.P p ≝
+λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Prop.
+λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
+λp:Prod4T T1 T2 T3 T4.
+ match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
+
+ndefinition Prod4T_rec
+ : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Set.
+   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
+   Πp:Prod4T T1 T2 T3 T4.P p ≝
+λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Set.
+λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
+λp:Prod4T T1 T2 T3 T4.
+ match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
+
+ndefinition Prod4T_rect
+ : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Type.
+   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
+   Πp:Prod4T T1 T2 T3 T4.P p ≝
+λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Type.
+λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
+λp:Prod4T T1 T2 T3 T4.
+ match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
+
+ndefinition fst4T ≝
+λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
+
+ndefinition snd4T ≝
+λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ x _ _ ⇒ x ].
+
+ndefinition thd4T ≝
+λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ x _ ⇒ x ].
+
+ndefinition fth4T ≝
+λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
+
+ndefinition eq_quadruple ≝
+λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
+λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
+ match p1 with [ quadruple x1 y1 z1 w1 ⇒
+  match p2 with [ quadruple x2 y2 z2 w2 ⇒
+   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ]].
+
+ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
+quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
+
+ndefinition Pro54T_ind
+ : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Prop.
+   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
+   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
+λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Prop.
+λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
+λp:Prod5T T1 T2 T3 T4 T5.
+ match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
+
+ndefinition Pro54T_rec
+ : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Set.
+   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
+   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
+λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Set.
+λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
+λp:Prod5T T1 T2 T3 T4 T5.
+ match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
+
+ndefinition Pro54T_rect
+ : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Type.
+   (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
+   Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
+λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Type.
+λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
+λp:Prod5T T1 T2 T3 T4 T5.
+ match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
+
+ndefinition fst5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].
+
+ndefinition snd5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ x _ _ _ ⇒ x ].
+
+ndefinition thd5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
+
+ndefinition frth5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
+
+ndefinition ffth5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
+
+ndefinition eq_quintuple ≝
+λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
+λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
+ match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒
+  match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒
+   (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]].

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
new file mode 100644 (file)
index 0000000..d95af89
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma
@@ -0,0 +1,491 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/bool_lemmas.ma".
+include "freescale/prod.ma".
+
+(* ***** *)
+(* TUPLE *)
+(* ***** *)
+
+nlemma pair_destruct_1 :
+∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
+ pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2.
+ #T1; #T2; #x1; #x2; #y1; #y2; #H;
+ nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma pair_destruct_2 :
+∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
+ pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2.
+ #T1; #T2; #x1; #x2; #y1; #y2; #H;
+ nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_eqpair :
+∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (boolSymmetric T1 f1) →
+ (boolSymmetric T2 f2) →
+ (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #x1; #y1;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2); napply (refl_eq ??)
+ ##| ##2: napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqpair :
+∀T1,T2.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #x1; #y1; #H;
+ nnormalize;
+ nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
+ nnormalize;
+ nrewrite > (H2 ?? (pair_destruct_2 ?????? H));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqpair_to_eq :
+∀T1,T2.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #x1; #y1; #H;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ #H3;
+ ##[ ##2: nelim (bool_destruct_false_true H3) ##]
+ #H4;
+ nrewrite > (H4 (refl_eq ??));
+ nrewrite > (H2 y1 y2 H3);
+ napply (refl_eq ??).
+nqed.
+
+nlemma triple_destruct_1 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma triple_destruct_2 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma triple_destruct_3 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_eqtriple :
+∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (boolSymmetric T1 f1) →
+ (boolSymmetric T2 f2) →
+ (boolSymmetric T3 f3) →
+ (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #x1; #y1; #z1;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+          ncases (f2 y2 y1);
+          nnormalize;
+          ##[ ##1: nrewrite > (H2 z1 z2); napply (refl_eq ??)
+          ##| ##2: napply (refl_eq ??)
+          ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqtriple :
+∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
+ (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #x1; #y1; #z1; #H;
+ nnormalize;
+ nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
+ nnormalize;
+ nrewrite > (H2 ?? (triple_destruct_2 ????????? H));
+ nnormalize;
+ nrewrite > (H3 ?? (triple_destruct_3 ????????? H));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqtriple_to_eq :
+∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
+ (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #x1; #y1; #z1; #H;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H4; nelim (bool_destruct_false_true H4) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H4; #H5; nelim (bool_destruct_false_true H5) ##]
+ #H4; #H5; #H6;
+ nrewrite > (H4 (refl_eq ??));
+ nrewrite > (H6 (refl_eq ??));
+ nrewrite > (H3 z1 z2 H5);
+ napply (refl_eq ??).
+nqed.
+
+nlemma quadruple_destruct_1 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quadruple_destruct_2 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quadruple_destruct_3 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quadruple_destruct_4 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_eqquadruple :
+∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (boolSymmetric T1 f1) →
+ (boolSymmetric T2 f2) →
+ (boolSymmetric T3 f3) →
+ (boolSymmetric T4 f4) →
+ (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+          ncases (f2 y2 y1);
+          nnormalize;
+          ##[ ##1: nrewrite > (H2 z1 z2);
+                   ncases (f3 z2 z1);
+                   nnormalize;
+                   ##[ ##1: nrewrite > (H3 v1 v2); napply (refl_eq ??)
+                   ##| ##2: napply (refl_eq ??)
+                   ##]
+          ##| ##2: napply (refl_eq ??)
+          ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqquadruple :
+∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
+ (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
+ (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1; #H;
+ nnormalize;
+ nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
+ nnormalize;
+ nrewrite > (H2 ?? (quadruple_destruct_2 ???????????? H));
+ nnormalize;
+ nrewrite > (H3 ?? (quadruple_destruct_3 ???????????? H));
+ nnormalize;
+ nrewrite > (H4 ?? (quadruple_destruct_4 ???????????? H));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqquadruple_to_eq :
+∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
+ (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
+ (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1; #H;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H5; nelim (bool_destruct_false_true H5) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H5; #H6; nelim (bool_destruct_false_true H6) ##]
+ nletin K2 ≝ (H3 z1 z2);
+ ncases (f3 z1 z2) in K2:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H5; #H6; #H7; nelim (bool_destruct_false_true H7) ##]
+ #H5; #H6; #H7; #H8;
+ nrewrite > (H5 (refl_eq ??));
+ nrewrite > (H6 (refl_eq ??));
+ nrewrite > (H8 (refl_eq ??));
+ nrewrite > (H4 v1 v2 H7);
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_1 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_2 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_3 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_4 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma quintuple_destruct_5 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma bsymmetric_eqquintuple :
+∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ (boolSymmetric T1 f1) →
+ (boolSymmetric T2 f2) →
+ (boolSymmetric T3 f3) →
+ (boolSymmetric T4 f4) →
+ (boolSymmetric T5 f5) →
+ (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+          ncases (f2 y2 y1);
+          nnormalize;
+          ##[ ##1: nrewrite > (H2 z1 z2);
+                   ncases (f3 z2 z1);
+                   nnormalize;
+                   ##[ ##1: nrewrite > (H3 v1 v2);
+                            ncases (f4 v2 v1);
+                            nnormalize;
+                            ##[ ##1: nrewrite > (H4 w1 w2); napply (refl_eq ??)
+                            ##| ##2: napply (refl_eq ??)
+                            ##]
+                   ##| ##2: napply (refl_eq ??)
+                   ##]
+          ##| ##2: napply (refl_eq ??)
+          ##]
+ ##| ##2: napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eq_to_eqquintuple :
+∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
+ (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
+ (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
+ (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1; #H;
+ nnormalize;
+ nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
+ nnormalize;
+ nrewrite > (H2 ?? (quintuple_destruct_2 ??????????????? H));
+ nnormalize;
+ nrewrite > (H3 ?? (quintuple_destruct_3 ??????????????? H));
+ nnormalize;
+ nrewrite > (H4 ?? (quintuple_destruct_4 ??????????????? H));
+ nnormalize;
+ nrewrite > (H5 ?? (quintuple_destruct_5 ??????????????? H));
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqquintuple_to_eq :
+∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
+ (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
+ (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
+ (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ ncases p1;
+ ncases p2;
+ #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1; #H;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H6; nelim (bool_destruct_false_true H6) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; nelim (bool_destruct_false_true H7) ##]
+ nletin K2 ≝ (H3 z1 z2);
+ ncases (f3 z1 z2) in K2:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; #H8; nelim (bool_destruct_false_true H8) ##]
+ nletin K3 ≝ (H4 v1 v2);
+ ncases (f4 v1 v2) in K3:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; #H8; #H9; nelim (bool_destruct_false_true H9) ##]
+ #H6; #H7; #H8; #H9; #H10;
+ nrewrite > (H6 (refl_eq ??));
+ nrewrite > (H7 (refl_eq ??));
+ nrewrite > (H8 (refl_eq ??));
+ nrewrite > (H10 (refl_eq ??));
+ nrewrite > (H5 w1 w2 H9);
+ napply (refl_eq ??).
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/pts.ma b/helm/software/matita/contribs/ng_assembly/freescale/pts.ma
new file mode 100644 (file)
index 0000000..fd31f24
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/pts.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                           Progetto FreeScale                           *)
+(*                                                                        *)
+(* Sviluppato da:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+universe constraint CProp[0] < CProp[1].
+universe constraint Type[0] ≤ CProp[0].
+universe constraint CProp[0] ≤ Type[0].
+universe constraint Type[1] ≤ CProp[1].
+universe constraint CProp[1] ≤ Type[1].
+

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
new file mode 100644 (file)
index 0000000..ceda6dc
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
@@ -0,0 +1,199 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                           Progetto FreeScale                           *)
+(*                                                                        *)
+(* Sviluppato da:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/pts.ma".
+
+(* ********************************** *)
+(* SOTTOINSIEME MINIMALE DELLA TEORIA *)
+(* ********************************** *)
+
+ninductive True: Prop ≝
+ I : True.
+
+ndefinition True_ind : ΠP:Prop.P → True → P ≝
+λP:Prop.λp:P.λH:True.
+ match H with [ I ⇒ p ].
+
+ndefinition True_rec : ΠP:Set.P → True → P ≝
+λP:Set.λp:P.λH:True.
+ match H with [ I ⇒ p ].
+
+ndefinition True_rect : ΠP:Type.P → True → P ≝
+λP:Type.λp:P.λH:True.
+ match H with [ I ⇒ p ].
+
+ninductive False: Prop ≝.
+
+ndefinition False_ind : ΠP:Prop.False → P ≝
+λP:Prop.λH:False.
+ match H in False return λH1:False.P with [].
+
+ndefinition False_rec : ΠP:Set.False → P ≝
+λP:Set.λH:False.
+ match H in False return λH1:False.P with [].
+
+ndefinition False_rect : ΠP:Type.False → P ≝
+λP:Type.λH:False.
+ match H in False return λH1:False.P with [].
+
+ndefinition Not: Prop → Prop ≝
+λA.(A → False).
+
+interpretation "logical not" 'not x = (Not x).
+
+ntheorem absurd : ∀A,C:Prop.A → ¬A → C.
+ #A; #C; #H;
+ nnormalize;
+ #H1;
+ nelim (H1 H).
+nqed.
+
+ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+ #A; #B; #H;
+ nnormalize;
+ #H1; #H2;
+ nelim (H1 (H H2)).
+nqed.
+
+ninductive And (A,B:Prop) : Prop ≝
+ conj : A → B → (And A B).
+
+ndefinition And_ind : ΠA,B:Prop.ΠP:Prop.(A → B → P) → And A B → P ≝
+λA,B:Prop.λP:Prop.λf:A → B → P.λH:And A B.
+ match H with [conj H1 H2 ⇒ f H1 H2 ].
+
+ndefinition And_rec : ΠA,B:Prop.ΠP:Set.(A → B → P) → And A B → P ≝
+λA,B:Prop.λP:Set.λf:A → B → P.λH:And A B.
+ match H with [conj H1 H2 ⇒ f H1 H2 ].
+
+ndefinition And_rect : ΠA,B:Prop.ΠP:Type.(A → B → P) → And A B → P ≝
+λA,B:Prop.λP:Type.λf:A → B → P.λH:And A B.
+ match H with [conj H1 H2 ⇒ f H1 H2 ].
+
+interpretation "logical and" 'and x y = (And x y).
+
+ntheorem proj1: ∀A,B:Prop.A ∧ B → A.
+ #A; #B; #H;
+ napply (And_ind A B ?? H);
+ #H1; #H2;
+ napply H1.
+nqed.
+
+ntheorem proj2: ∀A,B:Prop.A ∧ B → B.
+ #A; #B; #H;
+ napply (And_ind A B ?? H);
+ #H1; #H2;
+ napply H2.
+nqed.
+
+ninductive Or (A,B:Prop) : Prop ≝
+  or_introl : A → (Or A B)
+| or_intror : B → (Or A B).
+
+ndefinition Or_ind : ΠA,B:Prop.ΠP:Prop.(A → P) → (B → P) → Or A B → P ≝
+λA,B:Prop.λP:Prop.λf1:A → P.λf2:B → P.λH:Or A B.
+ match H with [ or_introl H1 ⇒ f1 H1 | or_intror H1 ⇒ f2 H1 ].
+
+interpretation "logical or" 'or x y = (Or x y).
+
+ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
+
+ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
+ ex_intro: ∀x:A.Q x → ex A Q.
+
+ndefinition ex_ind : ΠA:Type.ΠQ:A → Prop.ΠP:Prop.(Πa:A.Q a → P) → ex A Q → P ≝
+λA:Type.λQ:A → Prop.λP:Prop.λf:(Πa:A.Q a → P).λH:ex A Q.
+ match H with [ ex_intro H1 H2 ⇒ f H1 H2 ].
+
+interpretation "exists" 'exists x = (ex ? x).
+
+ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
+ ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
+
+ndefinition ex2_ind : ΠA:Type.ΠQ,R:A → Prop.ΠP:Prop.(Πa:A.Q a → R a → P) → ex2 A Q R → P ≝
+λA:Type.λQ,R:A → Prop.λP:Prop.λf:(Πa:A.Q a → R a → P).λH:ex2 A Q R.
+ match H with [ ex_intro2 H1 H2 H3 ⇒ f H1 H2 H3 ].
+
+ndefinition iff ≝
+λA,B.(A -> B) ∧ (B -> A).
+
+ndefinition relation : Type → Type ≝
+λA:Type.A → A → Prop. 
+
+ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x:A.R x x.
+
+ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x,y:A.R x y → R y x.
+
+ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x,y,z:A.R x y → R y z → R x z.
+
+ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x:A.¬ (R x x).
+
+ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
+
+ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
+λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
+
+ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x,y:A.R x y → ¬ (R y x).
+
+ninductive eq (A:Type) (x:A) : A → Prop ≝
+ refl_eq : eq A x x.
+
+ndefinition eq_ind : ΠA:Type.Πx:A.ΠP:A → Prop.P x → Πa:A.eq A x a → P a ≝
+λA:Type.λx:A.λP:A → Prop.λp:P x.λa:A.λH:eq A x a.
+ match H with [refl_eq ⇒ p ].
+
+ndefinition eq_rec : ΠA:Type.Πx:A.ΠP:A → Set.P x → Πa:A.eq A x a → P a ≝
+λA:Type.λx:A.λP:A → Set.λp:P x.λa:A.λH:eq A x a.
+ match H with [refl_eq ⇒ p ].
+
+ndefinition eq_rect : ΠA:Type.Πx:A.ΠP:A → Type.P x → Πa:A.eq A x a → P a ≝
+λA:Type.λx:A.λP:A → Type.λp:P x.λa:A.λH:eq A x a.
+ match H with [refl_eq ⇒ p ].
+
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+
+interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
+
+ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A).
+ #A;
+ nnormalize;
+ #x; #y; #H;
+ nrewrite < H;
+ napply (refl_eq ??).
+nqed.
+
+ntheorem eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+ #A; #x; #P; #H; #y; #H1;
+ napply (eq_ind ? x ? H y ?);
+ nrewrite < H1;
+ napply (refl_eq ??).
+nqed.