--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+include "num/quatern.ma".
+include "num/oct.ma".
+include "common/prod.ma".
+
+(* *********** *)
+(* ESADECIMALI *)
+(* *********** *)
+
+ninductive exadecim : Type ≝
+ x0: exadecim
+| x1: exadecim
+| x2: exadecim
+| x3: exadecim
+| x4: exadecim
+| x5: exadecim
+| x6: exadecim
+| x7: exadecim
+| x8: exadecim
+| x9: exadecim
+| xA: exadecim
+| xB: exadecim
+| xC: exadecim
+| xD: exadecim
+| xE: exadecim
+| xF: exadecim.
+
+(* operatore = *)
+ndefinition eq_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ]
+ | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ]
+ | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ]
+ | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ]
+ | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ]
+ | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ]
+ | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ]
+ | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ]
+ | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ]
+ | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ]
+ | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ]
+ | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ]
+ | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ]
+ | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ]
+ | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ]
+ | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ]
+ ].
+
+(* operatore < *)
+ndefinition lt_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ ].
+
+(* operatore ≤ *)
+ndefinition le_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+ ].
+
+(* operatore > *)
+ndefinition gt_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
+ ].
+
+(* operatore ≥ *)
+ndefinition ge_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ ].
+
+(* operatore and *)
+ndefinition and_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
+ | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
+ | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
+ | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
+ | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
+ | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
+ | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
+ | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
+ | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
+ | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
+ | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
+ | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
+ | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
+ | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
+ | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
+ | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
+ | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
+ | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
+ | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
+ | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ ].
+
+(* operatore or *)
+ndefinition or_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
+ | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
+ | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
+ | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
+ | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
+ | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
+ | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
+ | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
+ | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
+ | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
+ | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
+ | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
+ | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
+ | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
+ | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
+ | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
+ | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
+ | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
+ | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
+ | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
+ | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
+ | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
+ | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
+ | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
+ | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
+ | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
+ | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
+ | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
+ | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
+ | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ ].
+
+(* operatore xor *)
+ndefinition xor_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
+ | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
+ | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
+ | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
+ | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
+ | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
+ | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
+ | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
+ | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
+ | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
+ | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
+ | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
+ | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
+ | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
+ | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
+ | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
+ | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
+ | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
+ | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
+ | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
+ | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
+ | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
+ | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
+ | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
+ | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
+ | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
+ | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+ | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
+ | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
+ | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
+ | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
+ | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
+ | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
+ | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
+ | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
+ | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
+ | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
+ | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
+ ].
+
+(* operatore rotazione destra con carry *)
+ndefinition rcr_ex ≝
+λe:exadecim.λc:bool.match c with
+ [ true ⇒ match e with
+ [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
+ | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
+ | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
+ | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
+ | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
+ | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
+ | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
+ | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
+ | false ⇒ match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
+ ].
+
+(* operatore shift destro *)
+ndefinition shr_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
+
+(* operatore rotazione destra *)
+ndefinition ror_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
+ | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
+ | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
+ | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
+
+(* operatore rotazione destra n-volte *)
+nlet rec ror_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
+ match r with
+ [ qu_O ⇒ e
+ | qu_S t n' ⇒ ror_ex_n (ror_ex e) t n' ].
+
+(* operatore rotazione sinistra con carry *)
+ndefinition rcl_ex ≝
+λe:exadecim.λc:bool.match c with
+ [ true ⇒ match e with
+ [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
+ | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
+ | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
+ | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
+ | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true
+ | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true
+ | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true
+ | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ]
+ | false ⇒ match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]
+ ].
+
+(* operatore shift sinistro *)
+ndefinition shl_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ].
+
+(* operatore rotazione sinistra *)
+ndefinition rol_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
+ | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
+ | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
+ | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
+
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
+ match r with
+ [ qu_O ⇒ e
+ | qu_S t n' ⇒ rol_ex_n (rol_ex e) t n' ].
+
+(* operatore not/complemento a 1 *)
+ndefinition not_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
+ | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
+ | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
+ | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
+
+(* operatore somma con data+carry → data+carry *)
+ndefinition plus_ex_dc_dc ≝
+λe1,e2:exadecim.λc:bool.
+ match c with
+ [ true ⇒ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
+ | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
+ | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
+ | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
+ | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
+ | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
+ | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
+ | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
+ | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
+ | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
+ | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
+ | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
+ | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
+ | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
+ | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
+ | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
+ | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
+ | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
+ | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
+ | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
+ | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
+ | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
+ | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
+ | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
+ | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
+ | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
+ | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
+ | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
+ | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
+ | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
+ | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
+ | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
+ | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
+ | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
+ | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
+ | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
+ | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
+ | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
+ | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
+ | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
+ | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
+ | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
+ | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
+ | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
+ | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
+ | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ pair … x0 true | x1 ⇒ pair … x1 true | x2 ⇒ pair … x2 true | x3 ⇒ pair … x3 true
+ | x4 ⇒ pair … x4 true | x5 ⇒ pair … x5 true | x6 ⇒ pair … x6 true | x7 ⇒ pair … x7 true
+ | x8 ⇒ pair … x8 true | x9 ⇒ pair … x9 true | xA ⇒ pair … xA true | xB ⇒ pair … xB true
+ | xC ⇒ pair … xC true | xD ⇒ pair … xD true | xE ⇒ pair … xE true | xF ⇒ pair … xF true ]
+ ]
+ | false ⇒ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false
+ | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false
+ | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false
+ | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
+ | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
+ | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
+ | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
+ | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
+ | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
+ | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
+ | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
+ | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
+ | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
+ | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
+ | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
+ | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
+ | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
+ | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
+ | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
+ | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
+ | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
+ | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
+ | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
+ | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
+ | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
+ | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
+ | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
+ | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
+ | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
+ | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
+ | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
+ | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
+ | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
+ | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
+ | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
+ | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
+ | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
+ | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
+ | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
+ | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
+ | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
+ | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
+ | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
+ | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
+ | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
+ | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
+ | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
+ | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
+ | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
+ ]].
+
+(* operatore somma con data → data+carry *)
+ndefinition plus_ex_d_dc ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false
+ | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false
+ | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false
+ | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
+ | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
+ | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
+ | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
+ | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
+ | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
+ | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
+ | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
+ | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
+ | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
+ | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
+ | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
+ | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
+ | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
+ | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
+ | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
+ | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
+ | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
+ | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
+ | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
+ | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
+ | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
+ | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
+ | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
+ | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
+ | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
+ | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
+ | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
+ | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
+ | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
+ | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
+ | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
+ | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
+ | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
+ | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
+ | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
+ | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
+ | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
+ | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
+ | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
+ | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
+ | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
+ | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
+ | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
+ | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
+ | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
+ ].
+
+(* operatore somma con data+carry → data *)
+ndefinition plus_ex_dc_d ≝
+λe1,e2:exadecim.λc:bool.
+ match c with
+ [ true ⇒ match e1 with
+ [ x0 ⇒ match e2 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 ]
+ | x1 ⇒ match e2 with
+ [ 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 ⇒ x0 | xF ⇒ x1 ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+ | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+ | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+ | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+ | x7 ⇒ 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 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+ | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+ | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+ | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+ | xE ⇒ match e2 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 ]
+ | 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 ]
+ ]
+ | false ⇒ 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 ⇒ 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 ]
+ | x2 ⇒ match e2 with
+ [ 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 ⇒ x0 | xF ⇒ x1 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+ | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+ | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+ | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+ | 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 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+ | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+ | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+ | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+ | xF ⇒ match e2 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 somma con data → data *)
+ndefinition plus_ex_d_d ≝
+λ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 ⇒ 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 ]
+ | x2 ⇒ match e2 with
+ [ 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 ⇒ x0 | xF ⇒ x1 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+ | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+ | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+ | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+ | 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 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+ | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+ | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+ | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+ | xF ⇒ match e2 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 somma con data+carry → carry *)
+ndefinition plus_ex_dc_c ≝
+λe1,e2:exadecim.λc:bool.
+ match c with
+ [ true ⇒ 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 ⇒ true ]
+ | x1 ⇒ 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 ]
+ | x2 ⇒ 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 ]
+ | x3 ⇒ 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 ]
+ | x4 ⇒ 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 ]
+ | x5 ⇒ 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 ]
+ | x6 ⇒ 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 ]
+ | 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 ⇒ true
+ | 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 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | 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 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | 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 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ 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 ]
+ | xD ⇒ 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 ]
+ | xE ⇒ 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 ]
+ | 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 ]
+ ]
+ | false ⇒ 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 ⇒ 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 ]
+ | x2 ⇒ 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 ]
+ | x3 ⇒ 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 ]
+ | x4 ⇒ 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 ]
+ | x5 ⇒ 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 ]
+ | x6 ⇒ 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 ]
+ | x7 ⇒ 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 ]
+ | 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 ⇒ true
+ | x8 ⇒ true | 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 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | 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 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ 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 ]
+ | xD ⇒ 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 ]
+ | xE ⇒ 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 ]
+ | xF ⇒ 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 ]
+ ]].
+
+(* operatore somma con data → carry *)
+ndefinition plus_ex_d_c ≝
+λ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 ⇒ 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 ]
+ | x2 ⇒ 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 ]
+ | x3 ⇒ 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 ]
+ | x4 ⇒ 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 ]
+ | x5 ⇒ 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 ]
+ | x6 ⇒ 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 ]
+ | x7 ⇒ 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 ]
+ | 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 ⇒ true
+ | x8 ⇒ true | 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 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | 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 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ 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 ]
+ | xD ⇒ 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 ]
+ | xE ⇒ 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 ]
+ | xF ⇒ 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 ]
+ ].
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
+
+(* operatore predecessore *)
+ndefinition pred_ex ≝
+λe:exadecim.
+ match e with
+ [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+ | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
+
+(* operatore successore *)
+ndefinition succ_ex ≝
+λe:exadecim.
+ match e with
+ [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+ | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
+
+(* operatore neg/complemento a 2 *)
+ndefinition compl_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
+ | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
+ | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
+ | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
+
+(* iteratore sugli esadecimali *)
+ndefinition forall_ex ≝ λ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.
+
+(* esadecimali ricorsivi *)
+ninductive rec_exadecim : exadecim → Type ≝
+ ex_O : rec_exadecim x0
+| ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
+
+(* esadecimali → esadecimali ricorsivi *)
+ndefinition ex_to_recex ≝
+λn.match n return λx.rec_exadecim x with
+ [ x0 ⇒ ex_O
+ | x1 ⇒ ex_S ? ex_O
+ | x2 ⇒ ex_S ? (ex_S ? ex_O)
+ | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
+ | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
+ | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
+ | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
+ | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
+ | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
+ | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
+ | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
+ | xB ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))
+ | xC ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))
+ | xD ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))
+ | xE ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))))
+ | xF ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))))
+ ].
+
+(* quaternari → esadecimali *)
+ndefinition ex_of_qu ≝
+λn.match n with
+ [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].
+
+(* ottali → esadecimali *)
+ndefinition ex_of_oct ≝
+λn.match n with
+ [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].