(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Sviluppo: 2008-2010 *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
include "num/quatern.ma".
include "num/oct.ma".
include "common/prod.ma".
+include "common/nat.ma".
(* *********** *)
(* ESADECIMALI *)
| 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.
| 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 ≝
-λc:bool.λe:exadecim.match c with
+λe:exadecim.λc:bool.match c with
[ true ⇒ match e with
- [ 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ].
+ [ 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 ≝
| x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
| xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
+(* operatore rotazione destra n-volte *)
+nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
+ match n with
+ [ O ⇒ e
+ | S n' ⇒ ror_ex_n (ror_ex e) n' ].
+
(* operatore rotazione sinistra con carry *)
ndefinition rcl_ex ≝
-λc:bool.λe:exadecim.match c with
+λe:exadecim.λc:bool.match c with
[ true ⇒ match e with
- [ 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ].
+ [ 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 ≝
| x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
| xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
+ match n with
+ [ O ⇒ e
+ | S n' ⇒ rol_ex_n (rol_ex e) n' ].
+
(* operatore not/complemento a 1 *)
ndefinition not_ex ≝
λe:exadecim.match e with
(* operatore somma con data+carry → data+carry *)
ndefinition plus_ex_dc_dc ≝
-λc:bool.λe1,e2:exadecim.
+λe1,e2:exadecim.λc:bool.
match c with
[ true ⇒ match e1 with
[ x0 ⇒ match e2 with
- [ 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 *)
λe1,e2:exadecim.
match e1 with
[ x0 ⇒ match e2 with
- [ 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 … 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 ]
+ [ 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 ≝
-λc:bool.λe1,e2:exadecim.
+λe1,e2:exadecim.λc:bool.
match c with
[ true ⇒ match e1 with
[ x0 ⇒ match e2 with
(* operatore somma con data+carry → carry *)
ndefinition plus_ex_dc_c ≝
-λc:bool.λe1,e2:exadecim.
+λe1,e2:exadecim.λc:bool.
match c with
[ true ⇒ match e1 with
[ x0 ⇒ match e2 with
| 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.
| x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
| xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
-(* operatore abs *)
-ndefinition abs_ex ≝
-λe:exadecim.match getMSB_ex e with
- [ true ⇒ compl_ex e | false ⇒ e ].
-
-(* operatore x in [inf,sup] o in sup],[inf *)
+(* operatore x in [inf,sup] *)
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).
+λx,inf,sup:exadecim.(le_ex inf x) ⊗ (le_ex x sup).
+
+(* 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 ≝
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 ].