X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fassembly.ma;h=c7ecd595b21f5ceef69cc4848118ef1c37541a23;hb=016036e00c941eeeea7a3301d11c363dd888248e;hp=875e6da8d4b0cb4c6ad5ad22245fabaf55a06406;hpb=f1a376f6a60e9b65d8e7a82458ab217de23e5214;p=helm.git

diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/assembly.ma
index 875e6da8d..c7ecd595b 100644
--- a/helm/software/matita/library/assembly/assembly.ma
+++ b/helm/software/matita/library/assembly/assembly.ma
@@ -15,193 +15,8 @@
 set "baseuri" "cic:/matita/assembly/".
 
 include "nat/div_and_mod.ma".
-(*include "nat/compare.ma".*)
 include "list/list.ma".
 
-inductive exadecimal : Type ≝
-   x0: exadecimal
- | x1: exadecimal
- | x2: exadecimal
- | x3: exadecimal
- | x4: exadecimal
- | x5: exadecimal
- | x6: exadecimal
- | x7: exadecimal
- | x8: exadecimal
- | x9: exadecimal
- | xA: exadecimal
- | xB: exadecimal
- | xC: exadecimal
- | xD: exadecimal
- | xE: exadecimal
- | xF: exadecimal.
- 
-record byte : Type ≝ {
- bh: exadecimal;
- bl: exadecimal
-}.
-
-definition eqex ≝
- λb1,b2.
-  match b1 with
-   [ x0 ⇒
-       match b2 with
-        [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x1 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x2 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x3 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true 
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x4 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x5 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x6 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x7 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true 
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x8 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | x9 ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | xA ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | xB ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true 
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | xC ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
-   | xD ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ] 
-   | xE ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ] 
-   | xF ⇒
-       match b2 with
-        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
-        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
-        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
-        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]]. 
-
-
-definition eqbyte ≝
- λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
-
-alias num (instance 0) = "natural number".
-definition nat_of_exadecimal ≝
- λb.
-  match b with
-   [ x0 ⇒ 0
-   | x1 ⇒ 1
-   | x2 ⇒ 2
-   | x3 ⇒ 3
-   | x4 ⇒ 4
-   | x5 ⇒ 5
-   | x6 ⇒ 6
-   | x7 ⇒ 7
-   | x8 ⇒ 8
-   | x9 ⇒ 9
-   | xA ⇒ 10
-   | xB ⇒ 11
-   | xC ⇒ 12
-   | xD ⇒ 13
-   | xE ⇒ 14
-   | xF ⇒ 15
-   ].
-
-coercion cic:/matita/assembly/nat_of_exadecimal.con.
-
-definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
-
-coercion cic:/matita/assembly/nat_of_byte.con.
-
-let rec exadecimal_of_nat b ≝
-  match b with [ O ⇒ x0 | S b ⇒
-  match b with [ O ⇒ x1 | S b ⇒
-  match b with [ O ⇒ x2 | S b ⇒ 
-  match b with [ O ⇒ x3 | S b ⇒ 
-  match b with [ O ⇒ x4 | S b ⇒ 
-  match b with [ O ⇒ x5 | S b ⇒ 
-  match b with [ O ⇒ x6 | S b ⇒ 
-  match b with [ O ⇒ x7 | S b ⇒ 
-  match b with [ O ⇒ x8 | S b ⇒ 
-  match b with [ O ⇒ x9 | S b ⇒ 
-  match b with [ O ⇒ xA | S b ⇒ 
-  match b with [ O ⇒ xB | S b ⇒ 
-  match b with [ O ⇒ xC | S b ⇒ 
-  match b with [ O ⇒ xD | S b ⇒ 
-  match b with [ O ⇒ xE | S b ⇒ 
-  match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]]. 
-
-definition byte_of_nat ≝
- λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
- (*
-lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
- intros;
- elim b;
- elim e;
- elim e1;
- reflexivity.
-qed. *)
-
 notation "14" non associative with precedence 80 for @{ 'x14 }.
 interpretation "natural number" 'x14 = 
 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
@@ -501,11 +316,822 @@ interpretation "natural number" 'x256 =
 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) 
 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1) 
 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
+
+inductive exadecimal : Type ≝
+   x0: exadecimal
+ | x1: exadecimal
+ | x2: exadecimal
+ | x3: exadecimal
+ | x4: exadecimal
+ | x5: exadecimal
+ | x6: exadecimal
+ | x7: exadecimal
+ | x8: exadecimal
+ | x9: exadecimal
+ | xA: exadecimal
+ | xB: exadecimal
+ | xC: exadecimal
+ | xD: exadecimal
+ | xE: exadecimal
+ | xF: exadecimal.
+ 
+record byte : Type ≝ {
+ bh: exadecimal;
+ bl: exadecimal
+}.
+
+definition eqex ≝
+ λb1,b2.
+  match b1 with
+   [ x0 ⇒
+       match b2 with
+        [ x0 ⇒ true  | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x1 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x2 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x3 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true 
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x4 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x5 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x6 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x7 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true 
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x8 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x9 ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ true  | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | xA ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | xB ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true 
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | xC ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ true  | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | xD ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ true  | xE ⇒ false | xF ⇒ false ] 
+   | xE ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ false ] 
+   | xF ⇒
+       match b2 with
+        [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+        | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+        | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+        | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ]]. 
+
+
+definition eqbyte ≝
+ λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
+
+inductive cartesian_product (A,B: Type) : Type ≝
+ couple: ∀a:A.∀b:B. cartesian_product A B.
+
+definition plusex ≝
+ λb1,b2,c.
+  match c with
+   [ true ⇒
+      match b1 with
+       [ x0 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x1 false
+            | x1 ⇒ couple exadecimal bool x2 false
+            | x2 ⇒ couple exadecimal bool x3 false
+            | x3 ⇒ couple exadecimal bool x4 false
+            | x4 ⇒ couple exadecimal bool x5 false
+            | x5 ⇒ couple exadecimal bool x6 false
+            | x6 ⇒ couple exadecimal bool x7 false
+            | x7 ⇒ couple exadecimal bool x8 false
+            | x8 ⇒ couple exadecimal bool x9 false
+            | x9 ⇒ couple exadecimal bool xA false
+            | xA ⇒ couple exadecimal bool xB false
+            | xB ⇒ couple exadecimal bool xC false
+            | xC ⇒ couple exadecimal bool xD false
+            | xD ⇒ couple exadecimal bool xE false
+            | xE ⇒ couple exadecimal bool xF false
+            | xF ⇒ couple exadecimal bool x0 true ] 
+       | x1 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x2 false
+            | x1 ⇒ couple exadecimal bool x3 false
+            | x2 ⇒ couple exadecimal bool x4 false
+            | x3 ⇒ couple exadecimal bool x5 false
+            | x4 ⇒ couple exadecimal bool x6 false
+            | x5 ⇒ couple exadecimal bool x7 false
+            | x6 ⇒ couple exadecimal bool x8 false
+            | x7 ⇒ couple exadecimal bool x9 false
+            | x8 ⇒ couple exadecimal bool xA false
+            | x9 ⇒ couple exadecimal bool xB false
+            | xA ⇒ couple exadecimal bool xC false
+            | xB ⇒ couple exadecimal bool xD false
+            | xC ⇒ couple exadecimal bool xE false
+            | xD ⇒ couple exadecimal bool xF false
+            | xE ⇒ couple exadecimal bool x0 true
+            | xF ⇒ couple exadecimal bool x1 true ] 
+       | x2 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x3 false
+            | x1 ⇒ couple exadecimal bool x4 false
+            | x2 ⇒ couple exadecimal bool x5 false
+            | x3 ⇒ couple exadecimal bool x6 false
+            | x4 ⇒ couple exadecimal bool x7 false
+            | x5 ⇒ couple exadecimal bool x8 false
+            | x6 ⇒ couple exadecimal bool x9 false
+            | x7 ⇒ couple exadecimal bool xA false
+            | x8 ⇒ couple exadecimal bool xB false
+            | x9 ⇒ couple exadecimal bool xC false
+            | xA ⇒ couple exadecimal bool xD false
+            | xB ⇒ couple exadecimal bool xE false
+            | xC ⇒ couple exadecimal bool xF false
+            | xD ⇒ couple exadecimal bool x0 true
+            | xE ⇒ couple exadecimal bool x1 true
+            | xF ⇒ couple exadecimal bool x2 true ] 
+       | x3 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x4 false
+            | x1 ⇒ couple exadecimal bool x5 false
+            | x2 ⇒ couple exadecimal bool x6 false
+            | x3 ⇒ couple exadecimal bool x7 false
+            | x4 ⇒ couple exadecimal bool x8 false
+            | x5 ⇒ couple exadecimal bool x9 false
+            | x6 ⇒ couple exadecimal bool xA false
+            | x7 ⇒ couple exadecimal bool xB false
+            | x8 ⇒ couple exadecimal bool xC false
+            | x9 ⇒ couple exadecimal bool xD false
+            | xA ⇒ couple exadecimal bool xE false
+            | xB ⇒ couple exadecimal bool xF false
+            | xC ⇒ couple exadecimal bool x0 true
+            | xD ⇒ couple exadecimal bool x1 true
+            | xE ⇒ couple exadecimal bool x2 true
+            | xF ⇒ couple exadecimal bool x3 true ] 
+       | x4 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x5 false
+            | x1 ⇒ couple exadecimal bool x6 false
+            | x2 ⇒ couple exadecimal bool x7 false
+            | x3 ⇒ couple exadecimal bool x8 false
+            | x4 ⇒ couple exadecimal bool x9 false
+            | x5 ⇒ couple exadecimal bool xA false
+            | x6 ⇒ couple exadecimal bool xB false
+            | x7 ⇒ couple exadecimal bool xC false
+            | x8 ⇒ couple exadecimal bool xD false
+            | x9 ⇒ couple exadecimal bool xE false
+            | xA ⇒ couple exadecimal bool xF false
+            | xB ⇒ couple exadecimal bool x0 true
+            | xC ⇒ couple exadecimal bool x1 true
+            | xD ⇒ couple exadecimal bool x2 true
+            | xE ⇒ couple exadecimal bool x3 true
+            | xF ⇒ couple exadecimal bool x4 true ] 
+       | x5 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x6 false
+            | x1 ⇒ couple exadecimal bool x7 false
+            | x2 ⇒ couple exadecimal bool x8 false
+            | x3 ⇒ couple exadecimal bool x9 false
+            | x4 ⇒ couple exadecimal bool xA false
+            | x5 ⇒ couple exadecimal bool xB false
+            | x6 ⇒ couple exadecimal bool xC false
+            | x7 ⇒ couple exadecimal bool xD false
+            | x8 ⇒ couple exadecimal bool xE false
+            | x9 ⇒ couple exadecimal bool xF false
+            | xA ⇒ couple exadecimal bool x0 true
+            | xB ⇒ couple exadecimal bool x1 true
+            | xC ⇒ couple exadecimal bool x2 true
+            | xD ⇒ couple exadecimal bool x3 true
+            | xE ⇒ couple exadecimal bool x4 true
+            | xF ⇒ couple exadecimal bool x5 true ] 
+       | x6 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x7 false
+            | x1 ⇒ couple exadecimal bool x8 false
+            | x2 ⇒ couple exadecimal bool x9 false
+            | x3 ⇒ couple exadecimal bool xA false
+            | x4 ⇒ couple exadecimal bool xB false
+            | x5 ⇒ couple exadecimal bool xC false
+            | x6 ⇒ couple exadecimal bool xD false
+            | x7 ⇒ couple exadecimal bool xE false
+            | x8 ⇒ couple exadecimal bool xF false
+            | x9 ⇒ couple exadecimal bool x0 true
+            | xA ⇒ couple exadecimal bool x1 true
+            | xB ⇒ couple exadecimal bool x2 true
+            | xC ⇒ couple exadecimal bool x3 true
+            | xD ⇒ couple exadecimal bool x4 true
+            | xE ⇒ couple exadecimal bool x5 true
+            | xF ⇒ couple exadecimal bool x6 true ] 
+       | x7 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x8 false
+            | x1 ⇒ couple exadecimal bool x9 false
+            | x2 ⇒ couple exadecimal bool xA false
+            | x3 ⇒ couple exadecimal bool xB false
+            | x4 ⇒ couple exadecimal bool xC false
+            | x5 ⇒ couple exadecimal bool xD false
+            | x6 ⇒ couple exadecimal bool xE false
+            | x7 ⇒ couple exadecimal bool xF false
+            | x8 ⇒ couple exadecimal bool x0 true
+            | x9 ⇒ couple exadecimal bool x1 true
+            | xA ⇒ couple exadecimal bool x2 true
+            | xB ⇒ couple exadecimal bool x3 true
+            | xC ⇒ couple exadecimal bool x4 true
+            | xD ⇒ couple exadecimal bool x5 true
+            | xE ⇒ couple exadecimal bool x6 true
+            | xF ⇒ couple exadecimal bool x7 true ] 
+       | x8 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x9 false
+            | x1 ⇒ couple exadecimal bool xA false
+            | x2 ⇒ couple exadecimal bool xB false
+            | x3 ⇒ couple exadecimal bool xC false
+            | x4 ⇒ couple exadecimal bool xD false
+            | x5 ⇒ couple exadecimal bool xE false
+            | x6 ⇒ couple exadecimal bool xF false
+            | x7 ⇒ couple exadecimal bool x0 true
+            | x8 ⇒ couple exadecimal bool x1 true
+            | x9 ⇒ couple exadecimal bool x2 true
+            | xA ⇒ couple exadecimal bool x3 true
+            | xB ⇒ couple exadecimal bool x4 true
+            | xC ⇒ couple exadecimal bool x5 true
+            | xD ⇒ couple exadecimal bool x6 true
+            | xE ⇒ couple exadecimal bool x7 true
+            | xF ⇒ couple exadecimal bool x8 true ] 
+       | x9 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xA false
+            | x1 ⇒ couple exadecimal bool xB false
+            | x2 ⇒ couple exadecimal bool xC false
+            | x3 ⇒ couple exadecimal bool xD false
+            | x4 ⇒ couple exadecimal bool xE false
+            | x5 ⇒ couple exadecimal bool xF false
+            | x6 ⇒ couple exadecimal bool x0 true
+            | x7 ⇒ couple exadecimal bool x1 true
+            | x8 ⇒ couple exadecimal bool x2 true
+            | x9 ⇒ couple exadecimal bool x3 true
+            | xA ⇒ couple exadecimal bool x4 true
+            | xB ⇒ couple exadecimal bool x5 true
+            | xC ⇒ couple exadecimal bool x6 true
+            | xD ⇒ couple exadecimal bool x7 true
+            | xE ⇒ couple exadecimal bool x8 true
+            | xF ⇒ couple exadecimal bool x9 true ] 
+       | xA ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xB false
+            | x1 ⇒ couple exadecimal bool xC false
+            | x2 ⇒ couple exadecimal bool xD false
+            | x3 ⇒ couple exadecimal bool xE false
+            | x4 ⇒ couple exadecimal bool xF false
+            | x5 ⇒ couple exadecimal bool x0 true
+            | x6 ⇒ couple exadecimal bool x1 true
+            | x7 ⇒ couple exadecimal bool x2 true
+            | x8 ⇒ couple exadecimal bool x3 true
+            | x9 ⇒ couple exadecimal bool x4 true
+            | xA ⇒ couple exadecimal bool x5 true
+            | xB ⇒ couple exadecimal bool x6 true
+            | xC ⇒ couple exadecimal bool x7 true
+            | xD ⇒ couple exadecimal bool x8 true
+            | xE ⇒ couple exadecimal bool x9 true
+            | xF ⇒ couple exadecimal bool xA true ] 
+       | xB ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xC false
+            | x1 ⇒ couple exadecimal bool xD false
+            | x2 ⇒ couple exadecimal bool xE false
+            | x3 ⇒ couple exadecimal bool xF false
+            | x4 ⇒ couple exadecimal bool x0 true
+            | x5 ⇒ couple exadecimal bool x1 true
+            | x6 ⇒ couple exadecimal bool x2 true
+            | x7 ⇒ couple exadecimal bool x3 true
+            | x8 ⇒ couple exadecimal bool x4 true
+            | x9 ⇒ couple exadecimal bool x5 true
+            | xA ⇒ couple exadecimal bool x6 true
+            | xB ⇒ couple exadecimal bool x7 true
+            | xC ⇒ couple exadecimal bool x8 true
+            | xD ⇒ couple exadecimal bool x9 true
+            | xE ⇒ couple exadecimal bool xA true
+            | xF ⇒ couple exadecimal bool xB true ] 
+       | xC ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xD false
+            | x1 ⇒ couple exadecimal bool xE false
+            | x2 ⇒ couple exadecimal bool xF false
+            | x3 ⇒ couple exadecimal bool x0 true
+            | x4 ⇒ couple exadecimal bool x1 true
+            | x5 ⇒ couple exadecimal bool x2 true
+            | x6 ⇒ couple exadecimal bool x3 true
+            | x7 ⇒ couple exadecimal bool x4 true
+            | x8 ⇒ couple exadecimal bool x5 true
+            | x9 ⇒ couple exadecimal bool x6 true
+            | xA ⇒ couple exadecimal bool x7 true
+            | xB ⇒ couple exadecimal bool x8 true
+            | xC ⇒ couple exadecimal bool x9 true
+            | xD ⇒ couple exadecimal bool xA true
+            | xE ⇒ couple exadecimal bool xB true
+            | xF ⇒ couple exadecimal bool xC true ] 
+       | xD ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xE false
+            | x1 ⇒ couple exadecimal bool xF false
+            | x2 ⇒ couple exadecimal bool x0 true
+            | x3 ⇒ couple exadecimal bool x1 true
+            | x4 ⇒ couple exadecimal bool x2 true
+            | x5 ⇒ couple exadecimal bool x3 true
+            | x6 ⇒ couple exadecimal bool x4 true
+            | x7 ⇒ couple exadecimal bool x5 true
+            | x8 ⇒ couple exadecimal bool x6 true
+            | x9 ⇒ couple exadecimal bool x7 true
+            | xA ⇒ couple exadecimal bool x8 true
+            | xB ⇒ couple exadecimal bool x9 true
+            | xC ⇒ couple exadecimal bool xA true
+            | xD ⇒ couple exadecimal bool xB true
+            | xE ⇒ couple exadecimal bool xC true
+            | xF ⇒ couple exadecimal bool xD true ] 
+       | xE ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xF false
+            | x1 ⇒ couple exadecimal bool x0 true
+            | x2 ⇒ couple exadecimal bool x1 true
+            | x3 ⇒ couple exadecimal bool x2 true
+            | x4 ⇒ couple exadecimal bool x3 true
+            | x5 ⇒ couple exadecimal bool x4 true
+            | x6 ⇒ couple exadecimal bool x5 true
+            | x7 ⇒ couple exadecimal bool x6 true
+            | x8 ⇒ couple exadecimal bool x7 true
+            | x9 ⇒ couple exadecimal bool x8 true
+            | xA ⇒ couple exadecimal bool x9 true
+            | xB ⇒ couple exadecimal bool xA true
+            | xC ⇒ couple exadecimal bool xB true
+            | xD ⇒ couple exadecimal bool xC true
+            | xE ⇒ couple exadecimal bool xD true
+            | xF ⇒ couple exadecimal bool xE true ]
+       | xF ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x0 true
+            | x1 ⇒ couple exadecimal bool x1 true
+            | x2 ⇒ couple exadecimal bool x2 true
+            | x3 ⇒ couple exadecimal bool x3 true
+            | x4 ⇒ couple exadecimal bool x4 true
+            | x5 ⇒ couple exadecimal bool x5 true
+            | x6 ⇒ couple exadecimal bool x6 true
+            | x7 ⇒ couple exadecimal bool x7 true
+            | x8 ⇒ couple exadecimal bool x8 true
+            | x9 ⇒ couple exadecimal bool x9 true
+            | xA ⇒ couple exadecimal bool xA true
+            | xB ⇒ couple exadecimal bool xB true
+            | xC ⇒ couple exadecimal bool xC true
+            | xD ⇒ couple exadecimal bool xD true
+            | xE ⇒ couple exadecimal bool xE true
+            | xF ⇒ couple exadecimal bool xF true ] 
+       ]
+   | false ⇒
+      match b1 with
+       [ x0 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x0 false
+            | x1 ⇒ couple exadecimal bool x1 false
+            | x2 ⇒ couple exadecimal bool x2 false
+            | x3 ⇒ couple exadecimal bool x3 false
+            | x4 ⇒ couple exadecimal bool x4 false
+            | x5 ⇒ couple exadecimal bool x5 false
+            | x6 ⇒ couple exadecimal bool x6 false
+            | x7 ⇒ couple exadecimal bool x7 false
+            | x8 ⇒ couple exadecimal bool x8 false
+            | x9 ⇒ couple exadecimal bool x9 false
+            | xA ⇒ couple exadecimal bool xA false
+            | xB ⇒ couple exadecimal bool xB false
+            | xC ⇒ couple exadecimal bool xC false
+            | xD ⇒ couple exadecimal bool xD false
+            | xE ⇒ couple exadecimal bool xE false
+            | xF ⇒ couple exadecimal bool xF false ] 
+       | x1 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x1 false
+            | x1 ⇒ couple exadecimal bool x2 false
+            | x2 ⇒ couple exadecimal bool x3 false
+            | x3 ⇒ couple exadecimal bool x4 false
+            | x4 ⇒ couple exadecimal bool x5 false
+            | x5 ⇒ couple exadecimal bool x6 false
+            | x6 ⇒ couple exadecimal bool x7 false
+            | x7 ⇒ couple exadecimal bool x8 false
+            | x8 ⇒ couple exadecimal bool x9 false
+            | x9 ⇒ couple exadecimal bool xA false
+            | xA ⇒ couple exadecimal bool xB false
+            | xB ⇒ couple exadecimal bool xC false
+            | xC ⇒ couple exadecimal bool xD false
+            | xD ⇒ couple exadecimal bool xE false
+            | xE ⇒ couple exadecimal bool xF false
+            | xF ⇒ couple exadecimal bool x0 true ] 
+       | x2 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x2 false
+            | x1 ⇒ couple exadecimal bool x3 false
+            | x2 ⇒ couple exadecimal bool x4 false
+            | x3 ⇒ couple exadecimal bool x5 false
+            | x4 ⇒ couple exadecimal bool x6 false
+            | x5 ⇒ couple exadecimal bool x7 false
+            | x6 ⇒ couple exadecimal bool x8 false
+            | x7 ⇒ couple exadecimal bool x9 false
+            | x8 ⇒ couple exadecimal bool xA false
+            | x9 ⇒ couple exadecimal bool xB false
+            | xA ⇒ couple exadecimal bool xC false
+            | xB ⇒ couple exadecimal bool xD false
+            | xC ⇒ couple exadecimal bool xE false
+            | xD ⇒ couple exadecimal bool xF false
+            | xE ⇒ couple exadecimal bool x0 true
+            | xF ⇒ couple exadecimal bool x1 true ] 
+       | x3 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x3 false
+            | x1 ⇒ couple exadecimal bool x4 false
+            | x2 ⇒ couple exadecimal bool x5 false
+            | x3 ⇒ couple exadecimal bool x6 false
+            | x4 ⇒ couple exadecimal bool x7 false
+            | x5 ⇒ couple exadecimal bool x8 false
+            | x6 ⇒ couple exadecimal bool x9 false
+            | x7 ⇒ couple exadecimal bool xA false
+            | x8 ⇒ couple exadecimal bool xB false
+            | x9 ⇒ couple exadecimal bool xC false
+            | xA ⇒ couple exadecimal bool xD false
+            | xB ⇒ couple exadecimal bool xE false
+            | xC ⇒ couple exadecimal bool xF false
+            | xD ⇒ couple exadecimal bool x0 true
+            | xE ⇒ couple exadecimal bool x1 true
+            | xF ⇒ couple exadecimal bool x2 true ] 
+       | x4 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x4 false
+            | x1 ⇒ couple exadecimal bool x5 false
+            | x2 ⇒ couple exadecimal bool x6 false
+            | x3 ⇒ couple exadecimal bool x7 false
+            | x4 ⇒ couple exadecimal bool x8 false
+            | x5 ⇒ couple exadecimal bool x9 false
+            | x6 ⇒ couple exadecimal bool xA false
+            | x7 ⇒ couple exadecimal bool xB false
+            | x8 ⇒ couple exadecimal bool xC false
+            | x9 ⇒ couple exadecimal bool xD false
+            | xA ⇒ couple exadecimal bool xE false
+            | xB ⇒ couple exadecimal bool xF false
+            | xC ⇒ couple exadecimal bool x0 true
+            | xD ⇒ couple exadecimal bool x1 true
+            | xE ⇒ couple exadecimal bool x2 true
+            | xF ⇒ couple exadecimal bool x3 true ] 
+       | x5 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x5 false
+            | x1 ⇒ couple exadecimal bool x6 false
+            | x2 ⇒ couple exadecimal bool x7 false
+            | x3 ⇒ couple exadecimal bool x8 false
+            | x4 ⇒ couple exadecimal bool x9 false
+            | x5 ⇒ couple exadecimal bool xA false
+            | x6 ⇒ couple exadecimal bool xB false
+            | x7 ⇒ couple exadecimal bool xC false
+            | x8 ⇒ couple exadecimal bool xD false
+            | x9 ⇒ couple exadecimal bool xE false
+            | xA ⇒ couple exadecimal bool xF false
+            | xB ⇒ couple exadecimal bool x0 true
+            | xC ⇒ couple exadecimal bool x1 true
+            | xD ⇒ couple exadecimal bool x2 true
+            | xE ⇒ couple exadecimal bool x3 true
+            | xF ⇒ couple exadecimal bool x4 true ] 
+       | x6 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x6 false
+            | x1 ⇒ couple exadecimal bool x7 false
+            | x2 ⇒ couple exadecimal bool x8 false
+            | x3 ⇒ couple exadecimal bool x9 false
+            | x4 ⇒ couple exadecimal bool xA false
+            | x5 ⇒ couple exadecimal bool xB false
+            | x6 ⇒ couple exadecimal bool xC false
+            | x7 ⇒ couple exadecimal bool xD false
+            | x8 ⇒ couple exadecimal bool xE false
+            | x9 ⇒ couple exadecimal bool xF false
+            | xA ⇒ couple exadecimal bool x0 true
+            | xB ⇒ couple exadecimal bool x1 true
+            | xC ⇒ couple exadecimal bool x2 true
+            | xD ⇒ couple exadecimal bool x3 true
+            | xE ⇒ couple exadecimal bool x4 true
+            | xF ⇒ couple exadecimal bool x5 true ] 
+       | x7 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x7 false
+            | x1 ⇒ couple exadecimal bool x8 false
+            | x2 ⇒ couple exadecimal bool x9 false
+            | x3 ⇒ couple exadecimal bool xA false
+            | x4 ⇒ couple exadecimal bool xB false
+            | x5 ⇒ couple exadecimal bool xC false
+            | x6 ⇒ couple exadecimal bool xD false
+            | x7 ⇒ couple exadecimal bool xE false
+            | x8 ⇒ couple exadecimal bool xF false
+            | x9 ⇒ couple exadecimal bool x0 true
+            | xA ⇒ couple exadecimal bool x1 true
+            | xB ⇒ couple exadecimal bool x2 true
+            | xC ⇒ couple exadecimal bool x3 true
+            | xD ⇒ couple exadecimal bool x4 true
+            | xE ⇒ couple exadecimal bool x5 true
+            | xF ⇒ couple exadecimal bool x6 true ] 
+       | x8 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x8 false
+            | x1 ⇒ couple exadecimal bool x9 false
+            | x2 ⇒ couple exadecimal bool xA false
+            | x3 ⇒ couple exadecimal bool xB false
+            | x4 ⇒ couple exadecimal bool xC false
+            | x5 ⇒ couple exadecimal bool xD false
+            | x6 ⇒ couple exadecimal bool xE false
+            | x7 ⇒ couple exadecimal bool xF false
+            | x8 ⇒ couple exadecimal bool x0 true
+            | x9 ⇒ couple exadecimal bool x1 true
+            | xA ⇒ couple exadecimal bool x2 true
+            | xB ⇒ couple exadecimal bool x3 true
+            | xC ⇒ couple exadecimal bool x4 true
+            | xD ⇒ couple exadecimal bool x5 true
+            | xE ⇒ couple exadecimal bool x6 true
+            | xF ⇒ couple exadecimal bool x7 true ] 
+       | x9 ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool x9 false
+            | x1 ⇒ couple exadecimal bool xA false
+            | x2 ⇒ couple exadecimal bool xB false
+            | x3 ⇒ couple exadecimal bool xC false
+            | x4 ⇒ couple exadecimal bool xD false
+            | x5 ⇒ couple exadecimal bool xE false
+            | x6 ⇒ couple exadecimal bool xF false
+            | x7 ⇒ couple exadecimal bool x0 true
+            | x8 ⇒ couple exadecimal bool x1 true
+            | x9 ⇒ couple exadecimal bool x2 true
+            | xA ⇒ couple exadecimal bool x3 true
+            | xB ⇒ couple exadecimal bool x4 true
+            | xC ⇒ couple exadecimal bool x5 true
+            | xD ⇒ couple exadecimal bool x6 true
+            | xE ⇒ couple exadecimal bool x7 true
+            | xF ⇒ couple exadecimal bool x8 true ] 
+       | xA ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xA false
+            | x1 ⇒ couple exadecimal bool xB false
+            | x2 ⇒ couple exadecimal bool xC false
+            | x3 ⇒ couple exadecimal bool xD false
+            | x4 ⇒ couple exadecimal bool xE false
+            | x5 ⇒ couple exadecimal bool xF false
+            | x6 ⇒ couple exadecimal bool x0 true
+            | x7 ⇒ couple exadecimal bool x1 true
+            | x8 ⇒ couple exadecimal bool x2 true
+            | x9 ⇒ couple exadecimal bool x3 true
+            | xA ⇒ couple exadecimal bool x4 true
+            | xB ⇒ couple exadecimal bool x5 true
+            | xC ⇒ couple exadecimal bool x6 true
+            | xD ⇒ couple exadecimal bool x7 true
+            | xE ⇒ couple exadecimal bool x8 true
+            | xF ⇒ couple exadecimal bool x9 true ] 
+       | xB ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xB false
+            | x1 ⇒ couple exadecimal bool xC false
+            | x2 ⇒ couple exadecimal bool xD false
+            | x3 ⇒ couple exadecimal bool xE false
+            | x4 ⇒ couple exadecimal bool xF false
+            | x5 ⇒ couple exadecimal bool x0 true
+            | x6 ⇒ couple exadecimal bool x1 true
+            | x7 ⇒ couple exadecimal bool x2 true
+            | x8 ⇒ couple exadecimal bool x3 true
+            | x9 ⇒ couple exadecimal bool x4 true
+            | xA ⇒ couple exadecimal bool x5 true
+            | xB ⇒ couple exadecimal bool x6 true
+            | xC ⇒ couple exadecimal bool x7 true
+            | xD ⇒ couple exadecimal bool x8 true
+            | xE ⇒ couple exadecimal bool x9 true
+            | xF ⇒ couple exadecimal bool xA true ] 
+       | xC ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xC false
+            | x1 ⇒ couple exadecimal bool xD false
+            | x2 ⇒ couple exadecimal bool xE false
+            | x3 ⇒ couple exadecimal bool xF false
+            | x4 ⇒ couple exadecimal bool x0 true
+            | x5 ⇒ couple exadecimal bool x1 true
+            | x6 ⇒ couple exadecimal bool x2 true
+            | x7 ⇒ couple exadecimal bool x3 true
+            | x8 ⇒ couple exadecimal bool x4 true
+            | x9 ⇒ couple exadecimal bool x5 true
+            | xA ⇒ couple exadecimal bool x6 true
+            | xB ⇒ couple exadecimal bool x7 true
+            | xC ⇒ couple exadecimal bool x8 true
+            | xD ⇒ couple exadecimal bool x9 true
+            | xE ⇒ couple exadecimal bool xA true
+            | xF ⇒ couple exadecimal bool xB true ] 
+       | xD ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xD false
+            | x1 ⇒ couple exadecimal bool xE false
+            | x2 ⇒ couple exadecimal bool xF false
+            | x3 ⇒ couple exadecimal bool x0 true
+            | x4 ⇒ couple exadecimal bool x1 true
+            | x5 ⇒ couple exadecimal bool x2 true
+            | x6 ⇒ couple exadecimal bool x3 true
+            | x7 ⇒ couple exadecimal bool x4 true
+            | x8 ⇒ couple exadecimal bool x5 true
+            | x9 ⇒ couple exadecimal bool x6 true
+            | xA ⇒ couple exadecimal bool x7 true
+            | xB ⇒ couple exadecimal bool x8 true
+            | xC ⇒ couple exadecimal bool x9 true
+            | xD ⇒ couple exadecimal bool xA true
+            | xE ⇒ couple exadecimal bool xB true
+            | xF ⇒ couple exadecimal bool xC true ] 
+       | xE ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xE false
+            | x1 ⇒ couple exadecimal bool xF false
+            | x2 ⇒ couple exadecimal bool x0 true
+            | x3 ⇒ couple exadecimal bool x1 true
+            | x4 ⇒ couple exadecimal bool x2 true
+            | x5 ⇒ couple exadecimal bool x3 true
+            | x6 ⇒ couple exadecimal bool x4 true
+            | x7 ⇒ couple exadecimal bool x5 true
+            | x8 ⇒ couple exadecimal bool x6 true
+            | x9 ⇒ couple exadecimal bool x7 true
+            | xA ⇒ couple exadecimal bool x8 true
+            | xB ⇒ couple exadecimal bool x9 true
+            | xC ⇒ couple exadecimal bool xA true
+            | xD ⇒ couple exadecimal bool xB true
+            | xE ⇒ couple exadecimal bool xC true
+            | xF ⇒ couple exadecimal bool xD true ] 
+       | xF ⇒
+           match b2 with
+            [ x0 ⇒ couple exadecimal bool xF false
+            | x1 ⇒ couple exadecimal bool x0 true
+            | x2 ⇒ couple exadecimal bool x1 true
+            | x3 ⇒ couple exadecimal bool x2 true
+            | x4 ⇒ couple exadecimal bool x3 true
+            | x5 ⇒ couple exadecimal bool x4 true
+            | x6 ⇒ couple exadecimal bool x5 true
+            | x7 ⇒ couple exadecimal bool x6 true
+            | x8 ⇒ couple exadecimal bool x7 true
+            | x9 ⇒ couple exadecimal bool x8 true
+            | xA ⇒ couple exadecimal bool x9 true
+            | xB ⇒ couple exadecimal bool xA true
+            | xC ⇒ couple exadecimal bool xB true
+            | xD ⇒ couple exadecimal bool xC true
+            | xE ⇒ couple exadecimal bool xD true
+            | xF ⇒ couple exadecimal bool xE true ]
+       ]
+   ]
+.
+
+definition plusbyte ≝
+ λb1,b2,c.
+  match plusex (bl b1) (bl b2) c with
+   [ couple l c' ⇒
+      match plusex (bh b1) (bh b2) c' with
+       [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
+
+alias num (instance 0) = "natural number".
+definition nat_of_exadecimal ≝
+ λb.
+  match b with
+   [ x0 ⇒ 0
+   | x1 ⇒ 1
+   | x2 ⇒ 2
+   | x3 ⇒ 3
+   | x4 ⇒ 4
+   | x5 ⇒ 5
+   | x6 ⇒ 6
+   | x7 ⇒ 7
+   | x8 ⇒ 8
+   | x9 ⇒ 9
+   | xA ⇒ 10
+   | xB ⇒ 11
+   | xC ⇒ 12
+   | xD ⇒ 13
+   | xE ⇒ 14
+   | xF ⇒ 15
+   ].
+
+coercion cic:/matita/assembly/nat_of_exadecimal.con.
+
+definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
+
+coercion cic:/matita/assembly/nat_of_byte.con.
+
+let rec exadecimal_of_nat b ≝
+  match b with [ O ⇒ x0 | S b ⇒
+  match b with [ O ⇒ x1 | S b ⇒
+  match b with [ O ⇒ x2 | S b ⇒ 
+  match b with [ O ⇒ x3 | S b ⇒ 
+  match b with [ O ⇒ x4 | S b ⇒ 
+  match b with [ O ⇒ x5 | S b ⇒ 
+  match b with [ O ⇒ x6 | S b ⇒ 
+  match b with [ O ⇒ x7 | S b ⇒ 
+  match b with [ O ⇒ x8 | S b ⇒ 
+  match b with [ O ⇒ x9 | S b ⇒ 
+  match b with [ O ⇒ xA | S b ⇒ 
+  match b with [ O ⇒ xB | S b ⇒ 
+  match b with [ O ⇒ xC | S b ⇒ 
+  match b with [ O ⇒ xD | S b ⇒ 
+  match b with [ O ⇒ xE | S b ⇒ 
+  match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]]. 
+
+definition byte_of_nat ≝
+ λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
+
+lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
+ intros;
+ elim b;
+ elim e;
+ elim e1;
+ reflexivity.
+qed.
+
+axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n.
+(* intros;
+ unfold byte_of_nat;
+*) 
+
+definition nat_of_bool ≝
+ λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
+
+(* Way too slow. Handles 2^32 goals!
+lemma plusbyte_ok:
+ ∀b1,b2,c.
+  match plusbyte b1 b2 c with
+   [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c'
+   ].
+ intros;
+ elim c;
+ elim b1;
+ elim e;
+ elim e1;
+ elim b2;
+ elim e2;
+ elim e3;
+ reflexivity.
+qed.
+*)
 
 (*
 lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
@@ -542,7 +1168,7 @@ definition bpred ≝
    | false ⇒ mk_byte (bh b) (xpred (bl b))
    ]. 
 
-(* way too slow! 
+(* Way too slow and subsumed by previous theorem
 lemma bpred_pred:
  ∀b.
   match eqbyte b (mk_byte x0 x0) with
@@ -552,7 +1178,6 @@ lemma bpred_pred:
  elim b;
  elim e;
  elim e1;
- whd;
  reflexivity.
 qed.
 *)
@@ -581,9 +1206,6 @@ let rec cycles_of_opcode op : nat ≝
   | STAd ⇒ 3
   ].
 
-inductive cartesian_product (A,B: Type) : Type ≝
- couple: ∀a:A.∀b:B. cartesian_product A B.
-
 definition opcodemap ≝
  [ couple ? ? ADDd (mk_byte xA xB);
    couple ? ? BEQ (mk_byte x3 x7);
@@ -653,58 +1275,60 @@ definition update ≝
    [ true ⇒ v
    | false ⇒ f x ].
 
+definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
+
 definition tick ≝
- λs:status.
-  (* fetch *)
-  let opc ≝ opcode_of_byte (mem s (pc s)) in
-  let op1 ≝ mem s (S (pc s)) in
+ λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒
+  let opc ≝ opcode_of_byte (mem pc) in
+  let op1 ≝ mem (S pc) in
   let clk' ≝ cycles_of_opcode opc in
-  match eqb (S (clk s)) clk' with
+  match eqb (S clk) clk' with
    [ true ⇒
       match opc with
        [ ADDd ⇒
-          let x ≝ nat_of_byte (mem s op1) in
-          let acc' ≝ x + acc s in (* signed!!! *)
-           mk_status (byte_of_nat acc') (2 + pc s) (spc s)
-            (eqb O acc') (cf s) (mem s) 0
+          let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *)
+          let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in
+          let c' ≝ match res with [ couple _ c' ⇒ c'] in
+           mk_status acc' (2 + pc) spc
+            (eqb O (nat_of_byte acc')) c' mem 0 (* verify carrier! *)
        | BEQ ⇒
           mk_status
-           (acc s)
-           (match zf s with
-             [ true ⇒ 2 + op1 + pc s   (* signed!!! *)
-             | false ⇒ 2 + pc s
+           acc
+           (match zf with
+             [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
+             | false ⇒ 2 + pc
              ])
-           (spc s)
-           (zf s)
-           (cf s)
-           (mem s)
+           spc
+           zf
+           cf
+           mem
            0
        | BRA ⇒
           mk_status
-           (acc s) (2 + op1 + pc s) (* signed!!! *)
-           (spc s)
-           (zf s)
-           (cf s)
-           (mem s)
+           acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
+           spc
+           zf
+           cf
+           mem
            0
        | DECd ⇒
-          let x ≝ bpred (mem s op1) in (* signed!!! *)
-          let mem' ≝ update (mem s) op1 x in
-           mk_status (acc s) (2 + pc s) (spc s)
-            (eqb O x) (cf s) mem' 0 (* check zb!!! *)
+          let x ≝ bpred (mem op1) in (* signed!!! *)
+          let mem' ≝ update mem op1 x in
+           mk_status acc (2 + pc) spc
+            (eqb O x) cf mem' 0 (* check zb!!! *)
        | LDAi ⇒
-          mk_status op1 (2 + pc s) (spc s) (eqb O op1) (cf s) (mem s) 0
+          mk_status op1 (2 + pc) spc (eqb O op1) cf mem 0
        | LDAd ⇒
-          let x ≝ mem s op1 in
-           mk_status x (2 + pc s) (spc s) (eqb O x) (cf s) (mem s) 0
+          let x ≝ mem op1 in
+           mk_status x (2 + pc) spc (eqb O x) cf mem 0
        | STAd ⇒
-          mk_status (acc s) (2 + pc s) (spc s) (zf s) (cf s)
-           (update (mem s) op1 (acc s)) 0
+          mk_status acc (2 + pc) spc zf cf
+           (update mem op1 acc) 0
        ]
    | false ⇒
        mk_status
-        (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s))
-   ].
+        acc pc spc zf cf mem (S clk)
+   ]].
 
 let rec execute s n on n ≝
  match n with
@@ -712,8 +1336,15 @@ let rec execute s n on n ≝
   | S n' ⇒ execute (tick s) n'
   ].
   
-lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
- intros; reflexivity.
+lemma breakpoint:
+ ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
+ intros;
+ generalize in match s; clear s;
+ elim n1;
+  [ reflexivity
+  | simplify;
+    apply H;
+  ]
 qed.
 
 notation "hvbox(# break a)"
@@ -723,22 +1354,19 @@ interpretation "byte_of_opcode" 'byte_of_opcode a =
  (cic:/matita/assembly/byte_of_opcode.con a).
 
 definition mult_source : list byte ≝
-  [#LDAi; mk_byte x0 x0;
-   #STAd; mk_byte x2 x0; (* 18 = locazione $12 *)
-   #LDAd; mk_byte x1 xF; (* 17 = locazione $11 *)
-   #BEQ;  mk_byte x0 xC;
-   #LDAd; mk_byte x1 x2;
-   #DECd; mk_byte x1 xF;
-   #ADDd; mk_byte x1 xE; (* 16 = locazione $10 *)
-   #STAd; mk_byte x2 x0;
-   #LDAd; mk_byte x1 xF;
-   #BRA;  mk_byte xF x2; (* 242 = -14 *)
-   #LDAd; mk_byte x2 x0].
+  [#LDAi; mk_byte x0 x0; (* A := 0 *)
+   #STAd; mk_byte x2 x0; (* Z := A *)
+   #LDAd; mk_byte x1 xF; (* (l1) A := Y *)
+   #BEQ;  mk_byte x0 xA; (* if A == 0 then goto l2 *)
+   #LDAd; mk_byte x2 x0; (* A := Z *)
+   #DECd; mk_byte x1 xF; (* Y := Y - 1 *)
+   #ADDd; mk_byte x1 xE; (* A += X *)
+   #STAd; mk_byte x2 x0; (* Z := A *)
+   #BRA;  mk_byte xF x2; (* goto l1 *)
+   #LDAd; mk_byte x2 x0].(* (l2) *)
 
-definition mult_status ≝
- λx,y.
-  mk_status (mk_byte x0 x0) 0 0 false false
-   (λa:addr.
+definition mult_memory ≝
+ λx,y.λa:addr.
      match leb a 29 with
       [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
       | false ⇒
@@ -746,45 +1374,241 @@ definition mult_status ≝
           [ true ⇒ x
           | false ⇒ y
           ]
-      ]) 0.
-      
-(*      
-lemma foobar:
+      ].
+
+definition mult_status ≝
+ λx,y.
+  mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
+
+lemma plusbyte_O_x:
+ ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false.
+ intros;
+ elim b;
+ elim e;
+ elim e1;
+ reflexivity.
+qed.
+
+definition plusbytenc ≝
+ λx,y.
+  match plusbyte x y false with
+   [couple res _ ⇒ res].
+
+lemma plusbytenc_O_x:
+ ∀x. plusbytenc (mk_byte x0 x0) x = x.
+ intros;
+ unfold plusbytenc;
+ rewrite > plusbyte_O_x;
+ reflexivity.
+qed.
+
+lemma test_O_O:
+  let i ≝ 14 in
+  let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
+   pc s = 20 ∧ mem s 32 = byte_of_nat 0.
+ normalize;
+ split;
+ reflexivity.
+qed.
+
+
+lemma test_0_2:
+  let x ≝ mk_byte x0 x0 in
+  let y ≝ mk_byte x0 x2 in
+  let i ≝ 14 + 23 * nat_of_byte y in
+  let s ≝ execute (mult_status x y) i in
+   pc s = 20 ∧ mem s 32 = plusbytenc x x.
+ intros;
+ split;
+ reflexivity.
+qed.
+
+lemma test_x_1:
  ∀x.
-  (λi.
-    let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
-     (* pc s = 22 ∧*) mem s 32 = byte_of_nat 0) 14.
+  let y ≝ mk_byte x0 x1 in
+  let i ≝ 14 + 23 * nat_of_byte y in
+  let s ≝ execute (mult_status x y) i in
+   pc s = 20 ∧ mem s 32 = x.
  intros;
- letin foo ≝ (execute (mult_status x (mk_byte x0 x0)) 8);
- whd in foo;
-reduce in foo:(? ? ? ? ? ? ? ?);
- whd in foo;
-
-  xxx.
- change with 
-   (let s ≝ execute (mult_status x (mk_byte x0 x0)) 14 in
-    (* pc s = 22 ∧*)  eq ? (mem s 32) (byte_of_nat 0)).
-    xxxxxxxxx
- whd in ⊢ ((\lambda i:?.(let s \def ? in ? ? % %)) ?).
- 
- reduce;
- (* split; *)
- reflexivity;
+ split;
+  [ reflexivity
+  | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
+    rewrite > plusbytenc_O_x;
+    reflexivity
+  ].
 qed.
 
-lemma goo1:
+lemma test_x_2:
  ∀x.
-  let i ≝ 14 in
-  let s ≝ execute (mult_status x (mk_byte x0 x0)) i in
-   pc s = 22 ∧ mem s 32 = byte_of_nat 0.
+  let y ≝ mk_byte x0 x2 in
+  let i ≝ 14 + 23 * nat_of_byte y in
+  let s ≝ execute (mult_status x y) i in
+   pc s = 20 ∧ mem s 32 = plusbytenc x x.
  intros;
  split;
-  [ reduce;
-    
-  |
+  [ reflexivity
+  | change in ⊢ (? ? % ?) with
+     (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
+    rewrite > plusbytenc_O_x;
+    reflexivity
   ].
 qed.
 
+axiom byte_elim:
+ ∀P:byte → Prop.
+  (P (mk_byte x0 x0)) →
+   (∀i:nat. i < 255 → P (byte_of_nat i) → P (byte_of_nat (S i))) →
+    ∀b:byte. P b.
+(* Tedious proof, easy to automate but not trivial
+ intros;
+ elim b;
+ elim e;
+  [ elim e1;
+     [ assumption
+     | apply (H1 0);
+        [ apply lt_O_S
+        | assumption
+        ]
+     | apply (H1 1);
+        [ alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
+          apply lt_S_S;
+          apply lt_O_S
+        | apply (H1 0);
+*)
+
+theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
+ unfold lt;
+ intros;
+ autobatch.
+qed.
+
+axiom daemon: False.
+
+axiom loop_invariant:
+ ∀x,y:byte.∀j:nat. j ≤ y →
+  let s ≝ execute (mult_status x y) (5 + 23*j) in
+   pc s = 4 ∧
+   mem s 30 = x ∧
+   mem s 31 = byte_of_nat (y - j) ∧
+   mem s 32 = byte_of_nat (x * j).
+(*
+ intros 2;
+ apply (byte_elim ? ? ? y);
+  [ intros;
+    simplify in H;
+    cut (j=O);
+     [ unfold s; clear s;
+       rewrite > Hcut;
+       reflexivity
+     | (* easy *) elim daemon
+     ]
+  | intros;
+    unfold s;
+    cut (j < S i ∨ j = S i);
+    [ elim Hcut;
+       [ rewrite > nat_of_byte_byte_of_nat in H1;
+         [2: apply (lt_trans ? 255);
+             [ assumption
+             | unfold lt;
+               (* ???????? *)
+             ]
+         | generalize in match (H1 j); clear H1;
+           intros;
+           unfold lt in H3;
+           cut (j ≤ i);
+            [ generalize in match (H4 Hcut1); clear H4; clear Hcut1; intro;
+              apply H1
+            | letin xxx ≝ H3;
+              inversion xxx;
+               [ intro;
+                 rewrite > (injective_S ? ? H1);
+                 autobatch
+               | intros;
+                 (* facile *) elim daemon
+               ] 
+            ]
+         ]
+       |
+       ]
+    | (* easy *)
+    ]
+  ].
+qed.  
+*)
+
+axiom loop_invariant':
+ ∀x,y:byte.∀j:nat. j ≤ y →
+  let s ≝ execute (mult_status x y) (5 + 23*j) in
+   s =
+    mk_status (byte_of_nat (x * j)) 4 0 true false
+     (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
+      (byte_of_nat (x * j)))
+     0.
+
+theorem test_x_y:
+ ∀x,y.
+  let i ≝ 14 + 23 * nat_of_byte y in
+  let s ≝ execute (mult_status x y) i in
+   pc s = 20 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
+ intros;
+ generalize in match (loop_invariant' x y y (le_n y)); intro;
+ generalize in match (breakpoint (mult_status x y) (5 + 23*y) 9); intro;
+ cut (5 + 23*y +9 = 14 + 23* y);
+  [2: autobatch paramodulation
+  | rewrite > Hcut in H1;
+    change in H1:(? ? % ?) with s;
+    letin s0 ≝ (execute (mult_status x y) (S (S (S (S (S O))))+S 22*y));
+    generalize in match H; intro K; clear H;
+    change in K with
+     (s0 =
+      mk_status (byte_of_nat (x*y)) 4 0 true false
+       (update
+        (update
+         (update (mult_memory x y) 30 x)
+         31 (byte_of_nat (y-y)))
+         32 (byte_of_nat (x*y))) O);
+    clear Hcut;
+    generalize in match H1; intro K1; clear H1;
+    change in K1 with (s = execute s0 9);
+    rewrite > K in K1;
+    clear K; clear s0; clearbody s; clear i;
+    rewrite < minus_n_n in K1;
+    split;
+    rewrite > K1;
+    reflexivity
+  ]
+qed.
+
+(*
+ letin w ≝ 22;
+ letin opc ≝ (let s ≝ execute (mult_status x y) w in opcode_of_byte (mem s (pc s))); whd in opc;
+ letin acc' ≝ (acc (execute (mult_status x y) w)); 
+ normalize in acc';
+ change in acc' with x;
+ letin z ≝ (let s ≝ (execute (mult_status x y) w) in mem s 32); whd in z;
+ letin x ≝ (let s ≝ (execute (mult_status x y) w) in mem s 30); whd in x;
+ (*letin xxx ≝ (byte_of_nat (x+y)); normalize in xxx;*)
+ split;
+  [ normalize; reflexivity
+  | change with (byte_of_nat x = x);
+ normalize;
+ split;
+  [ reflexivity
+  | change with (byte_of_nat (x + 0));
+ letin www ≝ (nat_of_byte (byte_of_nat 260)); whd in www;
+ letin xxx ≝ (260 \mod 256); reduce in xxx;
+ letin xxx ≝ ((18 + 242) \mod 256);
+ whd in xxx;
+ letin pc' ≝ (pc s);
+ normalize in pc';
+ letin opcode ≝ (let s ≝ s in opcode_of_byte (mem s (pc s)));
+ normalize in opcode;
+ csc.
+ split;
+ reduce in s;
+ reflexivity.
+qed.
+
 lemma goo1:
  ∀x,y.
   let i ≝ 14 + 23 * nat_of_byte y in
@@ -858,4 +1682,4 @@ lemma goo: True.
  
  exact I.
 qed.
-*)
\ No newline at end of file
+*)