X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fexadecim.ma;h=9400d90741ef7b6130c109f048a68331b349f109;hb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;hp=10019b37920956383f5e148294d9ac6b9047bb23;hpb=d3c72253769956a8af10e6ea990ed34c92999e58;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
index 10019b379..9400d9074 100755
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -47,6 +47,11 @@ ninductive exadecim : Type ≝
 | xE: exadecim
 | xF: exadecim.
 
+(* 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.
+
 (* operatore = *)
 ndefinition eq_ex ≝
 λe1,e2:exadecim.
@@ -668,40 +673,84 @@ ndefinition xor_ex ≝
   | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ] 
  ].
 
+(* operatore Most Significant Bit *)
+ndefinition getMSB_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 ].
+
+ndefinition setMSB_ex ≝
+λe:exadecim.match e 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 ].
+
+ndefinition clrMSB_ex ≝
+λe:exadecim.match e 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 ].
+
+(* operatore Least Significant Bit *)
+ndefinition getLSB_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ true
+ | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ true
+ | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ true ].
+
+ndefinition setLSB_ex ≝
+λe:exadecim.match e 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 ].
+
+ndefinition clrLSB_ex ≝
+λe:exadecim.match e 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 ].
+
 (* operatore rotazione destra con carry *)
 ndefinition rcr_ex ≝
-λe:exadecim.λc:bool.match c with
+λc:bool.λe:exadecim.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 ]
+  [ x0 ⇒ pair … false x8 | x1 ⇒ pair … true x8
+  | x2 ⇒ pair … false x9 | x3 ⇒ pair … true x9
+  | x4 ⇒ pair … false xA | x5 ⇒ pair … true xA
+  | x6 ⇒ pair … false xB | x7 ⇒ pair … true xB
+  | x8 ⇒ pair … false xC | x9 ⇒ pair … true xC
+  | xA ⇒ pair … false xD | xB ⇒ pair … true xD
+  | xC ⇒ pair … false xE | xD ⇒ pair … true xE
+  | xE ⇒ pair … false xF | xF ⇒ pair … true xF ]
  | 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 ]
+  [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
+  | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
+  | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
+  | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
+  | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
+  | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
+  | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
+  | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ]
  ].
 
 (* 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 ].
+ [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0
+ | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1
+ | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2
+ | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3
+ | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4
+ | xA ⇒ pair … false x5 | xB ⇒ pair … true x5
+ | xC ⇒ pair … false x6 | xD ⇒ pair … true x6
+ | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ].
 
 (* operatore rotazione destra *)
 ndefinition ror_ex ≝
@@ -711,46 +760,40 @@ ndefinition ror_ex ≝
  | 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
+λc:bool.λe:exadecim.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 ]
+  [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x3
+  | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x7
+  | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xB
+  | x6 ⇒ pair … false xD | x7 ⇒ pair … false xF
+  | x8 ⇒ pair … true x1  | x9 ⇒ pair … true x3
+  | xA ⇒ pair … true x5  | xB ⇒ pair … true x7
+  | xC ⇒ pair … true x9  | xD ⇒ pair … true xB
+  | xE ⇒ pair … true xD  | xF ⇒ pair … true xF ]
  | 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 ]
+  [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
+  | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
+  | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
+  | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
+  | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x2
+  | xA ⇒ pair … true x4  | xB ⇒ pair … true x6
+  | xC ⇒ pair … true x8  | xD ⇒ pair … true xA
+  | xE ⇒ pair … true xC  | xF ⇒ pair … true xE ]
  ].
 
 (* 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 ].
+ [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2
+ | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6
+ | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA
+ | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE
+ | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x2
+ | xA ⇒ pair … true x4  | xB ⇒ pair … true x6
+ | xC ⇒ pair … true x8  | xD ⇒ pair … true xA
+ | xE ⇒ pair … true xC  | xF ⇒ pair … true xE ].
 
 (* operatore rotazione sinistra *)
 ndefinition rol_ex ≝
@@ -760,12 +803,6 @@ ndefinition rol_ex ≝
  | 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
@@ -776,171 +813,171 @@ ndefinition not_ex ≝
 
 (* operatore somma con data+carry → data+carry *)
 ndefinition plus_ex_dc_dc ≝
-λe1,e2:exadecim.λc:bool.
+λc:bool.λe1,e2:exadecim.
  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 ] 
+    [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
+    | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
+    | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
+    | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
+    | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
+    | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
+    | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0  | xF ⇒ pair … true x1 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
+    | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
+    | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
+    | xC ⇒ pair … false xF | xD ⇒ pair … true x0  | xE ⇒ pair … true x1  | xF ⇒ pair … true x2 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
+    | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
+    | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
+    | xC ⇒ pair … true x0  | xD ⇒ pair … true x1  | xE ⇒ pair … true x2  | xF ⇒ pair … true x3 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
+    | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
+    | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
+    | xC ⇒ pair … true x1  | xD ⇒ pair … true x2  | xE ⇒ pair … true x3  | xF ⇒ pair … true x4 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
+    | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
+    | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0  | xB ⇒ pair … true x1
+    | xC ⇒ pair … true x2  | xD ⇒ pair … true x3  | xE ⇒ pair … true x4  | xF ⇒ pair … true x5 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
+    | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
+    | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0  | xA ⇒ pair … true x1  | xB ⇒ pair … true x2
+    | xC ⇒ pair … true x3  | xD ⇒ pair … true x4  | xE ⇒ pair … true x5  | xF ⇒ pair … true x6 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
+    | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
+    | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x1  | xA ⇒ pair … true x2  | xB ⇒ pair … true x3
+    | xC ⇒ pair … true x4  | xD ⇒ pair … true x5  | xE ⇒ pair … true x6  | xF ⇒ pair … true x7 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
+    | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
+    | x8 ⇒ pair … true x1  | x9 ⇒ pair … true x2  | xA ⇒ pair … true x3  | xB ⇒ pair … true x4
+    | xC ⇒ pair … true x5  | xD ⇒ pair … true x6  | xE ⇒ pair … true x7  | xF ⇒ pair … true x8 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
+    | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0  | x7 ⇒ pair … true x1
+    | x8 ⇒ pair … true x2  | x9 ⇒ pair … true x3  | xA ⇒ pair … true x4  | xB ⇒ pair … true x5
+    | xC ⇒ pair … true x6  | xD ⇒ pair … true x7  | xE ⇒ pair … true x8  | xF ⇒ pair … true x9 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
+    | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0  | x6 ⇒ pair … true x1  | x7 ⇒ pair … true x2
+    | x8 ⇒ pair … true x3  | x9 ⇒ pair … true x4  | xA ⇒ pair … true x5  | xB ⇒ pair … true x6
+    | xC ⇒ pair … true x7  | xD ⇒ pair … true x8  | xE ⇒ pair … true x9  | xF ⇒ pair … true xA ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
+    | x4 ⇒ pair … true x0  | x5 ⇒ pair … true x1  | x6 ⇒ pair … true x2  | x7 ⇒ pair … true x3
+    | x8 ⇒ pair … true x4  | x9 ⇒ pair … true x5  | xA ⇒ pair … true x6  | xB ⇒ pair … true x7
+    | xC ⇒ pair … true x8  | xD ⇒ pair … true x9  | xE ⇒ pair … true xA  | xF ⇒ pair … true xB ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
+    | x4 ⇒ pair … true x1  | x5 ⇒ pair … true x2  | x6 ⇒ pair … true x3  | x7 ⇒ pair … true x4
+    | x8 ⇒ pair … true x5  | x9 ⇒ pair … true x6  | xA ⇒ pair … true x7  | xB ⇒ pair … true x8
+    | xC ⇒ pair … true x9  | xD ⇒ pair … true xA  | xE ⇒ pair … true xB  | xF ⇒ pair … true xC ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0  | x3 ⇒ pair … true x1
+    | x4 ⇒ pair … true x2  | x5 ⇒ pair … true x3  | x6 ⇒ pair … true x4  | x7 ⇒ pair … true x5
+    | x8 ⇒ pair … true x6  | x9 ⇒ pair … true x7  | xA ⇒ pair … true x8  | xB ⇒ pair … true x9
+    | xC ⇒ pair … true xA  | xD ⇒ pair … true xB  | xE ⇒ pair … true xC  | xF ⇒ pair … true xD ] 
    | 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 ]
+    [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0  | x2 ⇒ pair … true x1  | x3 ⇒ pair … true x2
+    | x4 ⇒ pair … true x3  | x5 ⇒ pair … true x4  | x6 ⇒ pair … true x5  | x7 ⇒ pair … true x6
+    | x8 ⇒ pair … true x7  | x9 ⇒ pair … true x8  | xA ⇒ pair … true x9  | xB ⇒ pair … true xA
+    | xC ⇒ pair … true xB  | xD ⇒ pair … true xC  | xE ⇒ pair … true xD  | xF ⇒ pair … true xE ]
    | 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 ] 
+    [ x0 ⇒ pair … true x0  | x1 ⇒ pair … true x1  | x2 ⇒ pair … true x2  | x3 ⇒ pair … true x3
+    | x4 ⇒ pair … true x4  | x5 ⇒ pair … true x5  | x6 ⇒ pair … true x6  | x7 ⇒ pair … true x7
+    | x8 ⇒ pair … true x8  | x9 ⇒ pair … true x9  | xA ⇒ pair … true xA  | xB ⇒ pair … true xB
+    | xC ⇒ pair … true xC  | xD ⇒ pair … true xD  | xE ⇒ pair … true xE  | xF ⇒ pair … true xF ] 
    ]
   | 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 ] 
+    [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
+    | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
+    | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
+    | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
+    | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
+    | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
+    | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
+    | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
+    | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
+    | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0  | xF ⇒ pair … true x1 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
+    | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
+    | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
+    | xC ⇒ pair … false xF | xD ⇒ pair … true x0  | xE ⇒ pair … true x1  | xF ⇒ pair … true x2 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
+    | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
+    | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
+    | xC ⇒ pair … true x0  | xD ⇒ pair … true x1  | xE ⇒ pair … true x2  | xF ⇒ pair … true x3 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
+    | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
+    | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
+    | xC ⇒ pair … true x1  | xD ⇒ pair … true x2  | xE ⇒ pair … true x3  | xF ⇒ pair … true x4 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
+    | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
+    | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0  | xB ⇒ pair … true x1
+    | xC ⇒ pair … true x2  | xD ⇒ pair … true x3  | xE ⇒ pair … true x4  | xF ⇒ pair … true x5 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
+    | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
+    | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0  | xA ⇒ pair … true x1  | xB ⇒ pair … true x2
+    | xC ⇒ pair … true x3  | xD ⇒ pair … true x4  | xE ⇒ pair … true x5  | xF ⇒ pair … true x6 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
+    | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
+    | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x1  | xA ⇒ pair … true x2  | xB ⇒ pair … true x3
+    | xC ⇒ pair … true x4  | xD ⇒ pair … true x5  | xE ⇒ pair … true x6  | xF ⇒ pair … true x7 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
+    | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
+    | x8 ⇒ pair … true x1  | x9 ⇒ pair … true x2  | xA ⇒ pair … true x3  | xB ⇒ pair … true x4
+    | xC ⇒ pair … true x5  | xD ⇒ pair … true x6  | xE ⇒ pair … true x7  | xF ⇒ pair … true x8 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
+    | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0  | x7 ⇒ pair … true x1
+    | x8 ⇒ pair … true x2  | x9 ⇒ pair … true x3  | xA ⇒ pair … true x4  | xB ⇒ pair … true x5
+    | xC ⇒ pair … true x6  | xD ⇒ pair … true x7  | xE ⇒ pair … true x8  | xF ⇒ pair … true x9 ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
+    | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0  | x6 ⇒ pair … true x1  | x7 ⇒ pair … true x2
+    | x8 ⇒ pair … true x3  | x9 ⇒ pair … true x4  | xA ⇒ pair … true x5  | xB ⇒ pair … true x6
+    | xC ⇒ pair … true x7  | xD ⇒ pair … true x8  | xE ⇒ pair … true x9  | xF ⇒ pair … true xA ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
+    | x4 ⇒ pair … true x0  | x5 ⇒ pair … true x1  | x6 ⇒ pair … true x2  | x7 ⇒ pair … true x3
+    | x8 ⇒ pair … true x4  | x9 ⇒ pair … true x5  | xA ⇒ pair … true x6  | xB ⇒ pair … true x7
+    | xC ⇒ pair … true x8  | xD ⇒ pair … true x9  | xE ⇒ pair … true xA  | xF ⇒ pair … true xB ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
+    | x4 ⇒ pair … true x1  | x5 ⇒ pair … true x2  | x6 ⇒ pair … true x3  | x7 ⇒ pair … true x4
+    | x8 ⇒ pair … true x5  | x9 ⇒ pair … true x6  | xA ⇒ pair … true x7  | xB ⇒ pair … true x8
+    | xC ⇒ pair … true x9  | xD ⇒ pair … true xA  | xE ⇒ pair … true xB  | xF ⇒ pair … true xC ] 
    | 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 ] 
+    [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0  | x3 ⇒ pair … true x1
+    | x4 ⇒ pair … true x2  | x5 ⇒ pair … true x3  | x6 ⇒ pair … true x4  | x7 ⇒ pair … true x5
+    | x8 ⇒ pair … true x6  | x9 ⇒ pair … true x7  | xA ⇒ pair … true x8  | xB ⇒ pair … true x9
+    | xC ⇒ pair … true xA  | xD ⇒ pair … true xB  | xE ⇒ pair … true xC  | xF ⇒ pair … true xD ] 
    | 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 ]
+    [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0  | x2 ⇒ pair … true x1  | x3 ⇒ pair … true x2
+    | x4 ⇒ pair … true x3  | x5 ⇒ pair … true x4  | x6 ⇒ pair … true x5  | x7 ⇒ pair … true x6
+    | x8 ⇒ pair … true x7  | x9 ⇒ pair … true x8  | xA ⇒ pair … true x9  | xB ⇒ pair … true xA
+    | xC ⇒ pair … true xB  | xD ⇒ pair … true xC  | xE ⇒ pair … true xD  | xF ⇒ pair … true xE ]
    ]].
 
 (* operatore somma con data → data+carry *)
@@ -948,90 +985,90 @@ 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 ]  
+   [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3
+   | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7
+   | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB
+   | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ]  
   | 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 ] 
+   [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4
+   | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8
+   | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC
+   | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5
+   | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9
+   | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD
+   | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0  | xF ⇒ pair … true x1 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6
+   | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA
+   | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE
+   | xC ⇒ pair … false xF | xD ⇒ pair … true x0  | xE ⇒ pair … true x1  | xF ⇒ pair … true x2 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7
+   | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB
+   | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF
+   | xC ⇒ pair … true x0  | xD ⇒ pair … true x1  | xE ⇒ pair … true x2  | xF ⇒ pair … true x3 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8
+   | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC
+   | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0
+   | xC ⇒ pair … true x1  | xD ⇒ pair … true x2  | xE ⇒ pair … true x3  | xF ⇒ pair … true x4 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9
+   | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD
+   | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0  | xB ⇒ pair … true x1
+   | xC ⇒ pair … true x2  | xD ⇒ pair … true x3  | xE ⇒ pair … true x4  | xF ⇒ pair … true x5 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA
+   | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE
+   | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0  | xA ⇒ pair … true x1  | xB ⇒ pair … true x2
+   | xC ⇒ pair … true x3  | xD ⇒ pair … true x4  | xE ⇒ pair … true x5  | xF ⇒ pair … true x6 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB
+   | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF
+   | x8 ⇒ pair … true x0  | x9 ⇒ pair … true x1  | xA ⇒ pair … true x2  | xB ⇒ pair … true x3
+   | xC ⇒ pair … true x4  | xD ⇒ pair … true x5  | xE ⇒ pair … true x6  | xF ⇒ pair … true x7 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC
+   | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0
+   | x8 ⇒ pair … true x1  | x9 ⇒ pair … true x2  | xA ⇒ pair … true x3  | xB ⇒ pair … true x4
+   | xC ⇒ pair … true x5  | xD ⇒ pair … true x6  | xE ⇒ pair … true x7  | xF ⇒ pair … true x8 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD
+   | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0  | x7 ⇒ pair … true x1
+   | x8 ⇒ pair … true x2  | x9 ⇒ pair … true x3  | xA ⇒ pair … true x4  | xB ⇒ pair … true x5
+   | xC ⇒ pair … true x6  | xD ⇒ pair … true x7  | xE ⇒ pair … true x8  | xF ⇒ pair … true x9 ] 
   | 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 ] 
+   [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE
+   | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0  | x6 ⇒ pair … true x1  | x7 ⇒ pair … true x2
+   | x8 ⇒ pair … true x3  | x9 ⇒ pair … true x4  | xA ⇒ pair … true x5  | xB ⇒ pair … true x6
+   | xC ⇒ pair … true x7  | xD ⇒ pair … true x8  | xE ⇒ pair … true x9  | xF ⇒ pair … true xA ] 
   | 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 ] 
+   [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF
+   | x4 ⇒ pair … true x0  | x5 ⇒ pair … true x1  | x6 ⇒ pair … true x2  | x7 ⇒ pair … true x3
+   | x8 ⇒ pair … true x4  | x9 ⇒ pair … true x5  | xA ⇒ pair … true x6  | xB ⇒ pair … true x7
+   | xC ⇒ pair … true x8  | xD ⇒ pair … true x9  | xE ⇒ pair … true xA  | xF ⇒ pair … true xB ] 
   | 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 ] 
+   [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0
+   | x4 ⇒ pair … true x1  | x5 ⇒ pair … true x2  | x6 ⇒ pair … true x3  | x7 ⇒ pair … true x4
+   | x8 ⇒ pair … true x5  | x9 ⇒ pair … true x6  | xA ⇒ pair … true x7  | xB ⇒ pair … true x8
+   | xC ⇒ pair … true x9  | xD ⇒ pair … true xA  | xE ⇒ pair … true xB  | xF ⇒ pair … true xC ] 
   | 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 ] 
+   [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0  | x3 ⇒ pair … true x1
+   | x4 ⇒ pair … true x2  | x5 ⇒ pair … true x3  | x6 ⇒ pair … true x4  | x7 ⇒ pair … true x5
+   | x8 ⇒ pair … true x6  | x9 ⇒ pair … true x7  | xA ⇒ pair … true x8  | xB ⇒ pair … true x9
+   | xC ⇒ pair … true xA  | xD ⇒ pair … true xB  | xE ⇒ pair … true xC  | xF ⇒ pair … true xD ] 
   | 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 ]
+   [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0  | x2 ⇒ pair … true x1  | x3 ⇒ pair … true x2
+   | x4 ⇒ pair … true x3  | x5 ⇒ pair … true x4  | x6 ⇒ pair … true x5  | x7 ⇒ pair … true x6
+   | x8 ⇒ pair … true x7  | x9 ⇒ pair … true x8  | xA ⇒ pair … true x9  | xB ⇒ pair … true xA
+   | xC ⇒ pair … true xB  | xD ⇒ pair … true xC  | xE ⇒ pair … true xD  | xF ⇒ pair … true xE ]
   ].
 
 (* operatore somma con data+carry → data *)
 ndefinition plus_ex_dc_d ≝
-λe1,e2:exadecim.λc:bool.
+λc:bool.λe1,e2:exadecim.
  match c with
   [ true ⇒ match e1 with
    [ x0 ⇒ match e2 with
@@ -1190,7 +1227,7 @@ ndefinition plus_ex_d_d ≝
 
 (* operatore somma con data+carry → carry *)
 ndefinition plus_ex_dc_c ≝
-λe1,e2:exadecim.λc:bool.
+λc:bool.λe1,e2:exadecim.
  match c with
   [ true ⇒ match e1 with
    [ x0 ⇒ match e2 with
@@ -1347,14 +1384,6 @@ ndefinition plus_ex_d_c ≝
    | 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.
@@ -1377,10 +1406,12 @@ ndefinition compl_ex ≝
  | 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.
+(* operatore x in [inf,sup] o in sup],[inf *)
+ndefinition inrange_ex ≝
+λx,inf,sup:exadecim.
+ match le_ex inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_ex inf x) (le_ex x sup).
 
 (* esadecimali ricorsivi *)
 ninductive rec_exadecim : exadecim → Type ≝
@@ -1417,3 +1448,15 @@ ndefinition ex_of_qu ≝
 ndefinition ex_of_oct ≝
 λn.match n with
  [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
+
+(* esadecimali xNNNN → ottali *)
+ndefinition oct_of_exL ≝
+λn.match n with
+  [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
+  | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
+
+(* esadecimali NNNNx → ottali *)
+ndefinition oct_of_exH ≝
+λn.match n with
+  [ x0 ⇒ o0 | x1 ⇒ o0 | x2 ⇒ o1 | x3 ⇒ o1 | x4 ⇒ o2 | x5 ⇒ o2 | x6 ⇒ o3 | x7 ⇒ o3
+  | x8 ⇒ o4 | x9 ⇒ o4 | xA ⇒ o5 | xB ⇒ o5 | xC ⇒ o6 | xD ⇒ o6 | xE ⇒ o7 | xF ⇒ o7 ].