X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fexadecim.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fexadecim.ma;h=0000000000000000000000000000000000000000;hb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;hp=246ab983eef67519ce572b32909c6f352b8b8f0b;hpb=c78a913e4e45c1128b59ca8be9d53fc0c36fc9e0;p=helm.git

diff --git a/helm/software/matita/library/freescale/exadecim.ma b/helm/software/matita/library/freescale/exadecim.ma
deleted file mode 100644
index 246ab983e..000000000
--- a/helm/software/matita/library/freescale/exadecim.ma
+++ /dev/null
@@ -1,1823 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
-(*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   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.