X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Fexadecim.ma;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Fexadecim.ma;h=246ab983eef67519ce572b32909c6f352b8b8f0b;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/assembly/freescale/exadecim.ma b/matita/contribs/assembly/freescale/exadecim.ma
new file mode 100644
index 000000000..246ab983e
--- /dev/null
+++ b/matita/contribs/assembly/freescale/exadecim.ma
@@ -0,0 +1,1823 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/extra.ma".
+
+(* ***************************** *)
+(* DEFINIZIONE DEGLI ESADECIMALI *)
+(* ***************************** *)
+
+inductive 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.
+
+(* operatore = *)
+definition 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 < *)
+definition 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 ≤ *)
+definition 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 > *)
+definition 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 ≥ *)
+definition 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 *)
+definition 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 *)
+definition 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 *)
+definition 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 *)
+definition 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 *)
+definition 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 *)
+definition 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 *)
+let 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 *)
+definition 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 *)
+definition 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 *)
+definition 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 *)
+let 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 *)
+definition 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 *)
+definition 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 *)
+definition plus_exnc ≝
+λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
+
+(* operatore carry della somma *)
+definition plus_exc ≝
+λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
+
+(* operatore Most Significant Bit *)
+definition 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 *)
+definition nat_of_exadecim ≝
+λ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 ].
+
+coercion cic:/matita/freescale/exadecim/nat_of_exadecim.con.
+
+(* naturali → esadecimali *)
+let rec exadecim_of_nat n ≝
+ match n with [ O ⇒ x0 | S n ⇒
+  match n with [ O ⇒ x1 | S n ⇒
+   match n with [ O ⇒ x2 | S n ⇒ 
+    match n with [ O ⇒ x3 | S n ⇒ 
+     match n with [ O ⇒ x4 | S n ⇒ 
+      match n with [ O ⇒ x5 | S n ⇒ 
+       match n with [ O ⇒ x6 | S n ⇒ 
+        match n with [ O ⇒ x7 | S n ⇒ 
+         match n with [ O ⇒ x8 | S n ⇒ 
+          match n with [ O ⇒ x9 | S n ⇒ 
+           match n with [ O ⇒ xA | S n ⇒ 
+            match n with [ O ⇒ xB | S n ⇒ 
+             match n with [ O ⇒ xC | S n ⇒ 
+              match n with [ O ⇒ xD | S n ⇒ 
+               match n with [ O ⇒ xE | S n ⇒ 
+                match n with [ O ⇒ xF | S n ⇒ exadecim_of_nat n ]]]]]]]]]]]]]]]]. 
+
+(* operatore predecessore *)
+definition 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 *)
+definition 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 *)
+definition 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 *)
+definition 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.
+
+(* ********************** *)
+(* TEOREMI/LEMMMI/ASSIOMI *)
+(* ********************** *)
+
+(* ESPERIMENTO UTILIZZO DELL'ITERATORE *)
+
+(*
+lemma forall_exadecim_eqProp_left_aux :
+ ∀P.(∀e:exadecim.P e = true) →
+ ((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) = true).
+ intros;
+ elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
+ elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
+ elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
+ elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
+ elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
+ elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
+ elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
+ elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
+ reflexivity.
+qed.
+
+lemma forall_exadecim_eqProp_left :
+ ∀P.(∀e:exadecim. P e = true) → (forall_exadecim (λe.P e) = true).
+ intro;
+ elim P 0;
+ [ simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
+   simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
+   autobatch; ].
+qed.
+
+lemma forall_exadecim_eqProp_right_aux :
+ ∀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) = true) →
+    (∀e:exadecim.P e = true).
+ elim daemon.
+qed.
+
+lemma forall_exadecim_eqProp_right :
+ ∀P.(forall_exadecim (λe.P e) = true) → (∀e:exadecim.P e = true).
+ intro;
+ elim P 0;
+ [ simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
+   simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
+   autobatch; ].
+qed.
+
+lemma lt_nat_of_exadecim_16_forall: ∀e.ltb (nat_of_exadecim e) 16 = true.
+ apply forall_exadecim_eqProp_right;
+ reflexivity;
+qed.
+*)
+
+(* FINE DELL'ESPERIMENTO *)
+
+lemma lt_nat_of_exadecim_16: ∀e.nat_of_exadecim e < 16.
+ intro;
+ elim e;
+ simplify;
+ autobatch depth=17.
+qed.
+
+lemma exadecim_of_nat_mod:
+ ∀n.exadecim_of_nat n = exadecim_of_nat (n \mod 16).
+ intros;
+ apply (nat_elim1 n); intro;
+ cases m; [ intro; reflexivity | ];
+ cases n1; [ intro; reflexivity | ];
+ cases n2; [ intro; reflexivity | ];
+ cases n3; [ intro; reflexivity | ];
+ cases n4; [ intro; reflexivity | ];
+ cases n5; [ intro; reflexivity | ];
+ cases n6; [ intro; reflexivity | ];
+ cases n7; [ intro; reflexivity | ];
+ cases n8; [ intro; reflexivity | ];
+ cases n9; [ intro; reflexivity | ];
+ cases n10; [ intro; reflexivity | ];
+ cases n11; [ intro; reflexivity | ];
+ cases n12; [ intro; reflexivity | ];
+ cases n13; [ intro; reflexivity | ];
+ cases n14; [ intro; reflexivity | ];
+ cases n15; [ intro; reflexivity | ];
+ intros;
+ change in ⊢ (? ? % ?) with (exadecim_of_nat n16);
+ change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
+ rewrite > mod_plus;
+ change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
+ rewrite < mod_mod;
+  [ apply H;
+    unfold lt;
+    autobatch.
+  | autobatch
+  ]
+qed.
+
+lemma nat_of_exadecim_exadecim_of_nat:
+ ∀n. nat_of_exadecim (exadecim_of_nat n) = n \mod 16.
+ intro;
+ rewrite > exadecim_of_nat_mod;
+ generalize in match (lt_mod_m_m n 16 ?); [2: autobatch | ]
+ generalize in match (n \mod 16); intro;
+ cases n1; [ intro; reflexivity | ];
+ cases n2; [ intro; reflexivity | ];
+ cases n3; [ intro; reflexivity | ];
+ cases n4; [ intro; reflexivity | ];
+ cases n5; [ intro; reflexivity | ]; 
+ cases n6; [ intro; reflexivity | ]; 
+ cases n7; [ intro; reflexivity | ];
+ cases n8; [ intro; reflexivity | ];
+ cases n9; [ intro; reflexivity | ];
+ cases n10; [ intro; reflexivity | ];
+ cases n11 [ intro; reflexivity | ];
+ cases n12; [ intro; reflexivity | ];
+ cases n13; [ intro; reflexivity | ];
+ cases n14; [ intro; reflexivity | ];
+ cases n15; [ intro; reflexivity | ];
+ cases n16; [ intro; reflexivity | ];
+ intro;
+ unfold lt in H;
+ cut False;
+  [ elim Hcut
+  | autobatch
+  ]
+qed.
+
+lemma exadecim_of_nat_nat_of_exadecim:
+ ∀e.exadecim_of_nat (nat_of_exadecim e) = e.
+ intro;
+ elim e;
+ reflexivity.
+qed.
+
+lemma plusex_ok:
+ ∀b1,b2,c.
+  match plus_ex b1 b2 c with
+   [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
+ intros;
+ elim b1; (elim b2; (elim c; normalize; reflexivity)).
+qed.
+
+lemma eq_eqex_S_x0_false:
+ ∀n. n < 15 → eq_ex x0 (exadecim_of_nat (S n)) = false.
+ intro;
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ intro;
+ unfold lt in H;
+ cut (S n1 ≤ 0);
+  [ elim (not_le_Sn_O ? Hcut)
+  | do 15 (apply le_S_S_to_le);
+    assumption
+  ]
+qed.
+
+lemma eqex_true_to_eq: ∀b,b'. eq_ex b b' = true → b=b'.
+ intros 2;
+ elim b 0;
+ elim b' 0;
+ simplify;
+ intro;
+ first [ reflexivity | destruct H ].
+qed.
+
+lemma eqex_false_to_not_eq: ∀b,b'. eq_ex b b' = false → b ≠ b'.
+ intros 2;
+ elim b 0;
+ elim b' 0;
+ simplify;
+ intro;
+ try (destruct H);
+ intro K;
+ destruct K.
+qed.
+
+(* nuovi *)
+
+lemma ok_lt_ex : ∀e1,e2:exadecim.
+ lt_ex e1 e2 = ltb e1 e2.
+ intros;
+ elim e1;
+ elim e2;
+ simplify;
+ reflexivity.
+ qed.
+
+lemma ok_le_ex : ∀e1,e2:exadecim.
+ le_ex e1 e2 = leb e1 e2.
+ intros;
+ elim e1;
+ elim e2;
+ simplify;
+ reflexivity.
+ qed.
+
+lemma ok_gt_ex : ∀e1,e2:exadecim.
+ gt_ex e1 e2 = notb (leb e1 e2).
+ intros;
+ elim e1;
+ elim e2;
+ simplify;
+ reflexivity.
+ qed.
+
+lemma ok_ge_ex : ∀e1,e2:exadecim.
+ ge_ex e1 e2 = notb (ltb e1 e2).
+ intros;
+ elim e1;
+ elim e2;
+ simplify;
+ reflexivity.
+ qed.
+
+lemma ok_pred_ex : ∀e:exadecim.
+ pred_ex e = plus_exnc e xF.
+ intros;
+ elim e;
+ simplify;
+ reflexivity.
+ qed.
+
+lemma ok_succ_ex : ∀e:exadecim.
+ succ_ex e = plus_exnc e x1.
+ intros;
+ elim e;
+ simplify;
+ reflexivity.
+ qed.
+
+lemma ok_rcr_ex : ∀e:exadecim.∀b:bool.
+ rcr_ex e b = 
+ pair exadecim bool
+  (exadecim_of_nat ((e/2)+match b with [ true ⇒ 8 | false ⇒ 0]))
+  (eqb (mod e 2) 1).
+ intros;
+ elim e;
+ elim b;
+ simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
+ simplify in ⊢ (? ? ? (? ? ? ? %));
+ simplify in ⊢ (? ? ? (? ? ? % ?));
+ simplify in ⊢ (? ? % ?);
+ reflexivity;
+qed.
+
+lemma ok_rcl_ex : ∀e:exadecim.∀b:bool.
+ rcl_ex e b =
+ pair exadecim bool
+  (exadecim_of_nat ((mod (e*2) 16)+match b with [ true ⇒ 1 | false ⇒ 0]))
+  (notb (ltb e 8)).
+ intros;
+ elim e;
+ elim b;
+ simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
+ simplify in ⊢ (? ? ? (? ? ? % ?));
+ simplify in ⊢ (? ? ? (? ? ? ? (? %)));
+ simplify in ⊢ (? ? ? (? ? ? ? %));
+ simplify in ⊢ (? ? % ?);
+ reflexivity.
+ qed.
+
+lemma ok_shr_ex : ∀e:exadecim.
+ shr_ex e =
+ pair exadecim bool
+  (exadecim_of_nat (e/2))
+  (eqb (mod e 2) 1).
+ intros;
+ elim e;
+ simplify in ⊢ (? ? ? (? ? ? % ?));
+ simplify in ⊢ (? ? ? (? ? ? ? %));
+ simplify in ⊢ (? ? % ?);
+ reflexivity.
+qed.
+
+lemma ok_shl_ex : ∀e:exadecim.
+ shl_ex e =
+ pair exadecim bool
+  (exadecim_of_nat (mod (e*2) 16))
+  (notb (ltb e 8)).
+ intros;
+ elim e;
+ simplify in ⊢ (? ? ? (? ? ? % ?));
+ simplify in ⊢ (? ? ? (? ? ? ? (? %)));
+ simplify in ⊢ (? ? ? (? ? ? ? %));
+ simplify in ⊢ (? ? % ?);
+ reflexivity.
+qed.
+
+lemma ok_not_ex : ∀e:exadecim.
+ e + (not_ex e) = 15.
+ intros;
+ elim e;
+ simplify;
+ reflexivity.
+qed.
+
+lemma ok_compl_ex : ∀e:exadecim.
+ e + (compl_ex e) = match gt_ex e x0 with [ true ⇒ 16 | false ⇒ 0 ].
+ intros;
+ elim e;
+ simplify;
+ reflexivity.
+qed.
+
+lemma ok_MSB_ex : ∀e:exadecim.
+ MSB_ex e = notb (ltb e 8).
+ intros;
+ elim e;
+ simplify;
+ reflexivity.
+qed.