From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Jul 2007 14:51:18 +0000 (+0000)
Subject: assembly.ma splitted into many files
X-Git-Tag: 0.4.95@7852~324
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5fe5171fa142cdd9370819e233c013b599b5d76c;p=helm.git

assembly.ma splitted into many files
---

diff --git a/matita/library/assembly/assembly.ma b/matita/library/assembly/assembly.ma
deleted file mode 100644
index 4e2326de0..000000000
--- a/matita/library/assembly/assembly.ma
+++ /dev/null
@@ -1,1744 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/assembly/".
-
-include "nat/div_and_mod.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').
-
-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.
-
-lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
- intro;
- elim b;
- simplify;
- autobatch.
-qed.
-
-lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
- intro;
- unfold nat_of_byte;
- letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
- letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
- unfold lt in H K ⊢ %;
- letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
- letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
- apply le_S_S;
- cut (16*bh b ≤ 16*15);
-  [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
-    simplify in Hf:(? ? %);
-    assumption
-  | autobatch
-  ]
-qed.
-
-lemma le_to_lt: ∀n,m. n ≤ m → n < S m.
- intros;
- autobatch.
-qed.
-
-axiom daemon: False.
-
-lemma exadecimal_of_nat_mod:
- ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
- elim daemon.
-(*
- intros;
- cases n; [ reflexivity | ];
- cases n1; [ reflexivity | ];
- cases n2; [ reflexivity | ];
- cases n3; [ reflexivity | ];
- cases n4; [ reflexivity | ];
- cases n5; [ reflexivity | ];
- cases n6; [ reflexivity | ];  
- cases n7; [ reflexivity | ];
- cases n8; [ reflexivity | ];
- cases n9; [ reflexivity | ];
- cases n10; [ reflexivity | ];
- cases n11; [ reflexivity | ];
- cases n12; [ reflexivity | ];
- cases n13; [ reflexivity | ];
- cases n14; [ reflexivity | ];
- cases n15; [ reflexivity | ];
- change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
- cut ((16 + n16) \mod 16 = n16 \mod 16);
-  [ rewrite > Hcut;
-    simplify in ⊢ (? ? % ?);
-    
-  | unfold mod;
-    change with (mod_aux (16+n16) (16+n16) 15 = n16);
-    unfold mod_aux;
-    change with
-     (match leb (16+n16) 15 with
-       [true ⇒ 16+n16
-       | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
-       ] = n16);
-    cut (leb (16+n16) 15 = false);
-     [ rewrite > Hcut;
-       change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
-       cut (16+n16-16 = n16);
-        [ rewrite > Hcut1; clear Hcut1;
-          
-        |
-        ]
-     |
-     ]
-  ]*)
-qed.
-
-(*lemma exadecimal_of_nat_elim:
- ∀P:exadecimal → Prop.
-  (∀m. m < 16 → P (exadecimal_of_nat m)) →
-    ∀n. P (exadecimal_of_nat n).
- intros;
- cases n; [ apply H; autobatch | ]; clear n;
- cases n1; [ apply H; autobatch | ]; clear n1;
- cases n; [ apply H; autobatch | ]; clear n;
- cases n1; [ apply H; autobatch | ]; clear n1; 
- cases n; [ apply H; autobatch | ]; clear n;
- cases n1; [ apply H; autobatch | ]; clear n1;
- cases n; [ apply H; autobatch | ]; clear n;
- cases n1; [ apply H; autobatch | ]; clear n1;
- cases n; [ apply H; autobatch | ]; clear n;
- cases n1; [ apply H; autobatch | ]; clear n1;
- cases n; [ apply H; autobatch | ]; clear n;
- cases n1; [ apply H; autobatch | ]; clear n1;
- cases n; [ apply H; autobatch | ]; clear n;
- cases n1; [ apply H; autobatch | ]; clear n1;
- cases n; [ apply H; autobatch | ]; clear n;
- cases n1; [ apply H; autobatch | ]; clear n1;
- simplify;
- elim daemon.
-qed.
-*)
-      
-axiom nat_of_exadecimal_exadecimal_of_nat:
- ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16.
-(*
- intro;
- apply (exadecimal_of_nat_elim (λn.;
- 
- 
- 
- elim n 0; [ reflexivity | intro ];
- elim n1 0; [ intros; reflexivity | intros 2 ];
- elim n2 0; [ intros; reflexivity | intros 2 ];
- elim n3 0; [ intros; reflexivity | intros 2 ];
- elim n4 0; [ intros; reflexivity | intros 2 ];
- elim n5 0; [ intros; reflexivity | intros 2 ];
- elim n6 0; [ intros; reflexivity | intros 2 ];
- elim n7 0; [ intros; reflexivity | intros 2 ];
- elim n8 0; [ intros; reflexivity | intros 2 ];
- elim n9 0; [ intros; reflexivity | intros 2 ];
- elim n10 0; [ intros; reflexivity | intros 2 ];
- elim n11 0; [ intros; reflexivity | intros 2 ];
- elim n12 0; [ intros; reflexivity | intros 2 ];
- elim n13 0; [ intros; reflexivity | intros 2 ];
- elim n14 0; [ intros; reflexivity | intros 2 ];
- elim n15 0; [ intros; reflexivity | intros 2 ];
- intro;
- simplify;
- rewrite < H15;
- change in ⊢ (? ? % ?) with (nat_of_exadecimal (exadecimal_of_nat n16));
-qed.
-*)
-
-lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
- intro;
- unfold byte_of_nat;
- unfold nat_of_byte;
- change with (16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n = n \mod 256);
- rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
- rewrite > nat_of_exadecimal_exadecimal_of_nat;
- elim daemon.
-qed.
-
-definition nat_of_bool ≝
- λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
-
-lemma plusex_ok:
- ∀b1,b2,c.
-  match plusex b1 b2 c with
-   [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
- intros;
- elim c;
- elim b1;
- elim b2;
- normalize;
- reflexivity.
-qed.
-
-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' * 256
-   ].
- intros;
- unfold plusbyte;
- generalize in match (plusex_ok (bl b1) (bl b2) c);
- elim (plusex (bl b1) (bl b2) c);
- simplify in H ⊢ %;
- generalize in match (plusex_ok (bh b1) (bh b2) t1);
- elim (plusex (bh b1) (bh b2) t1);
- simplify in H1 ⊢ %;
- change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
- unfold nat_of_byte;
- letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
- rewrite > distr_times_plus in K:(? ? ? %);
- rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
- rewrite < associative_times in K:(? ? ? (? ? %));
- normalize in K:(? ? ? (? ? (? % ?)));
- rewrite > symmetric_times in K:(? ? ? (? ? %));
- rewrite > sym_plus in ⊢ (? ? ? (? % ?));
- rewrite > associative_plus in ⊢ (? ? ? %);
- letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
-  apply transitive_eq; [3: apply K' | skip | ];
- clear K';
- rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
- rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
- rewrite > associative_plus in ⊢ (? ? % ?);
- rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
- rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
- rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
- rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
- rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
- rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
- rewrite > H; clear H;
- autobatch paramodulation.
-qed.
-
-(*
-lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
- intros; elim n; [ reflexivity | unfold byte_of_nat. 
-qed.
-*)
-
-definition addr ≝ nat.
-
-definition xpred ≝
- λb.
-  match b with
-   [ x0 ⇒ xF
-   | x1 ⇒ x0
-   | x2 ⇒ x1
-   | x3 ⇒ x2
-   | x4 ⇒ x3
-   | x5 ⇒ x4
-   | x6 ⇒ x5
-   | x7 ⇒ x6
-   | x8 ⇒ x7
-   | x9 ⇒ x8
-   | xA ⇒ x9
-   | xB ⇒ xA
-   | xC ⇒ xB
-   | xD ⇒ xC
-   | xE ⇒ xD
-   | xF ⇒ xE ].
-
-definition bpred ≝
- λb.
-  match eqex (bl b) x0 with
-   [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
-   | false ⇒ mk_byte (bh b) (xpred (bl b))
-   ]. 
-
-(* Way too slow and subsumed by previous theorem
-lemma bpred_pred:
- ∀b.
-  match eqbyte b (mk_byte x0 x0) with
-   [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
-   | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
- intros;
- elim b;
- elim e;
- elim e1;
- reflexivity.
-qed.
-*)
-
-definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
-
-coercion cic:/matita/assembly/addr_of_byte.con.
-
-inductive opcode: Type ≝
-   ADDd: opcode  (* 3 clock, 171 *)
- | BEQ: opcode   (* 3, 55 *)
- | BRA: opcode   (* 3, 48 *)
- | DECd: opcode  (* 5, 58 *)
- | LDAi: opcode  (* 2, 166 *)
- | LDAd: opcode  (* 3, 182 *)
- | STAd: opcode. (* 3, 183 *)
-
-let rec cycles_of_opcode op : nat ≝
- match op with
-  [ ADDd ⇒ 3
-  | BEQ ⇒ 3
-  | BRA ⇒ 3
-  | DECd ⇒ 5
-  | LDAi ⇒ 2
-  | LDAd ⇒ 3
-  | STAd ⇒ 3
-  ].
-
-definition opcodemap ≝
- [ couple ? ? ADDd (mk_byte xA xB);
-   couple ? ? BEQ (mk_byte x3 x7);
-   couple ? ? BRA (mk_byte x3 x0);
-   couple ? ? DECd (mk_byte x3 xA);
-   couple ? ? LDAi (mk_byte xA x6);
-   couple ? ? LDAd (mk_byte xB x6);
-   couple ? ? STAd (mk_byte xB x7) ].
-
-definition opcode_of_byte ≝
- λb.
-  let rec aux l ≝
-   match l with
-    [ nil ⇒ ADDd
-    | cons c tl ⇒
-       match c with
-        [ couple op n ⇒
-           match eqbyte n b with
-            [ true ⇒ op
-            | false ⇒ aux tl
-            ]]]
-  in
-   aux opcodemap.
-
-definition magic_of_opcode ≝
- λop1.
-  match op1 with
-   [ ADDd ⇒ 0
-   | BEQ ⇒  1 
-   | BRA ⇒  2
-   | DECd ⇒ 3
-   | LDAi ⇒ 4
-   | LDAd ⇒ 5
-   | STAd ⇒ 6 ].
-   
-definition opcodeeqb ≝
- λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
-
-definition byte_of_opcode : opcode → byte ≝
- λop.
-  let rec aux l ≝
-   match l with
-    [ nil ⇒ mk_byte x0 x0
-    | cons c tl ⇒
-       match c with
-        [ couple op' n ⇒
-           match opcodeeqb op op' with
-            [ true ⇒ n
-            | false ⇒ aux tl
-            ]]]
-  in
-   aux opcodemap.
-
-record status : Type ≝ {
-  acc : byte;
-  pc  : addr;
-  spc : addr;
-  zf  : bool;
-  cf  : bool;
-  mem : addr → byte;
-  clk : nat
-}.
-
-definition update ≝
- λf: addr → byte.λa.λv.λx.
-  match eqb x a with
-   [ true ⇒ v
-   | false ⇒ f x ].
-
-lemma update_update_a_a:
- ∀s,a,v1,v2,b.
-  update (update s a v1) a v2 b = update s a v2 b.
- intros;
- unfold update;
- unfold update;
- elim (eqb b a);
- reflexivity.
-qed. 
-
-lemma update_update_a_b:
- ∀s,a1,v1,a2,v2,b.
-  a1 ≠ a2 →
-   update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
- intros;
- unfold update;
- unfold update;
- apply (bool_elim ? (eqb b a1)); intros;
- apply (bool_elim ? (eqb b a2)); intros;
- simplify;
- [ elim H;
-   rewrite < (eqb_true_to_eq ? ? H1);
-   apply eqb_true_to_eq;
-   assumption
- |*: reflexivity
- ].
-qed.
-
-definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
-
-definition tick ≝
- λ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) clk' with
-   [ true ⇒
-      match opc with
-       [ ADDd ⇒
-          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
-            (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
-       | BEQ ⇒
-          mk_status
-           acc
-           (match zf with
-             [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
-                      (* FIXME: can't work - address truncated to 8 bits *)
-             | false ⇒ 2 + pc
-             ])
-           spc
-           zf
-           cf
-           mem
-           0
-       | BRA ⇒
-          mk_status
-           acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
-                                      (* FIXME: same as above *)
-           spc
-           zf
-           cf
-           mem
-           0
-       | DECd ⇒
-          let x ≝ bpred (mem op1) in (* signed!!! *)
-          let mem' ≝ update mem op1 x in
-           mk_status acc (2 + pc) spc
-            (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
-       | LDAi ⇒
-          mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
-       | LDAd ⇒
-          let x ≝ mem op1 in
-           mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
-       | STAd ⇒
-          mk_status acc (2 + pc) spc zf cf
-           (update mem op1 acc) 0
-       ]
-   | false ⇒
-       mk_status
-        acc pc spc zf cf mem (S clk)
-   ]].
-
-let rec execute s n on n ≝
- match n with
-  [ O ⇒ s
-  | S n' ⇒ execute (tick s) n'
-  ].
-  
-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)"
-  non associative with precedence 80
-for @{ 'byte_of_opcode $a }.
-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; (* 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_memory ≝
- λx,y.λa:addr.
-     match leb a 29 with
-      [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
-      | false ⇒
-         match eqb a 30 with
-          [ true ⇒ x
-          | false ⇒ y
-          ]
-      ].
-
-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].
-
-definition plusbytec ≝
- λx,y.
-  match plusbyte x y false with
-   [couple _ c ⇒ c].
-
-lemma plusbytenc_O_x:
- ∀x. plusbytenc (mk_byte x0 x0) x = x.
- intros;
- unfold plusbytenc;
- rewrite > plusbyte_O_x;
- reflexivity.
-qed.
-
-(*axiom mod_plus: ∀a,b,m. (a + b) \mod m = a \mod m + b \mod m.*)
-axiom mod_plus: \forall a1,a2,b1,b2,m.
-              a1 \mod m = b1 \mod m \to
-              a2 \mod m = b2 \mod m \to
-              (a1 + a2) \mod m = (b1 + b2) \mod m.
-              
-axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O.
-
-axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
-
-theorem plusbytenc_ok:
- ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
- intros;
- unfold plusbytenc;
- generalize in match (plusbyte_ok b1 b2 false);
- elim (plusbyte b1 b2 false);
- simplify in H ⊢ %;
- change with (nat_of_byte t = (b1 + b2) \mod 256);
- rewrite < plus_n_O in H;
- rewrite > H; clear H;
- letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
- rewrite > K in ⊢ (? ? % ?); 
- letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
-    [ autobatch
-    | cut (O =  O \mod 256);
-       [ rewrite > Hcut in K':(? ? ? %);
-         rewrite > K in K:(? ? % ?);
-         rewrite > (mod_plus ? ? ? ? ? K K') in ⊢ (? ? ? %);
-         rewrite < plus_n_O;reflexivity
-       |simplify;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.
-  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;
- split;
-  [ reflexivity
-  | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
-    rewrite > plusbytenc_O_x;
-    reflexivity
-  ].
-qed.
-
-lemma test_x_2:
- ∀x.
-  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
-  | change in ⊢ (? ? % ?) with
-     (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
-    rewrite > plusbytenc_O_x;
-    reflexivity
-  ].
-qed.
-
-theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
- unfold lt;
- intros;
- autobatch.
-qed.
-
-axiom status_eq:
- ∀s,s'.
-  acc s = acc s' →
-  pc s = pc s' →
-  spc s = spc s' →
-  zf s = zf s' →
-  cf s = cf s' →
-  (∀a. mem s a = mem s' a) →
-  clk s = clk s' →
-   s=s'.
-
-lemma eq_eqex_S_x0_false:
- ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
- intro;
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- intro;
- unfold lt in H;
- cut (S n1 ≤ 0);
-  [ elim (not_le_Sn_O ? Hcut)
-  | do 15 (apply le_S_S_to_le);
-    assumption
-  ]
-qed.
-
-lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z.
- intros;
- unfold div;
- apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m)));
- cut (∃w.m = S w);
-  [ elim Hcut;
-    rewrite > H2;
-    rewrite > H2 in H1;
-    clear Hcut; clear H2; clear H; (*clear m;*)
-    simplify;
-    unfold in ⊢ (? ? % ?);
-    cut (∃z.n = S z);
-     [ elim Hcut; clear Hcut;
-       rewrite > H in H1;
-       rewrite > H; clear m;
-       change in ⊢ (? ? % ?)  with
-        (match leb (S a1) a with
-         [ true ⇒ O
-         | false ⇒ S (div_aux a1 ((S a1) - S a) a)]);
-       cut (S a1 ≰ a);
-        [ apply (leb_elim (S a1) a);
-           [ intro;
-             elim (Hcut H2)
-           | intro;
-             simplify;
-             reflexivity
-           ]
-        | intro;
-          autobatch
-        ]
-     | elim H1; autobatch
-     ]
-  | autobatch
-  ].
-qed.
-
-lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
- ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
- intros;
- unfold byte_of_nat;
- cut (b < 15 ∨ b ≥ 15);
-  [ elim Hcut;
-    [ unfold eqbyte;
-      change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b))); 
-      rewrite > eq_eqex_S_x0_false;
-       [ elim (eqex (bh (mk_byte x0 x0))
-(bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify;
-(*
- alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
-         rewrite > andb_sym;
-*)
-         reflexivity
-       | assumption
-       ]
-    | unfold eqbyte;
-      change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
-      letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
-       [ autobatch
-       | unfold in H1;
-         apply le_S_S;
-         assumption
-       | clearbody K;
-         elim K; clear K;
-         rewrite > H2;
-         rewrite > eq_eqex_S_x0_false;
-          [ reflexivity
-          | unfold lt;
-            unfold lt in H;
-            rewrite < H2;
-            clear H2; clear a; clear H1; clear Hcut;
-            elim daemon (* trivial arithmetic property over <= and div *)
-          ] 
-       ]
-    ]
-  | elim daemon
-  ].
-qed.
-
-lemma eq_bpred_S_a_a:
- ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
-elim daemon. (*
- intros;
- unfold byte_of_nat;
- cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
-  [ elim Hcut;
-     [ 
-     |
-     ]
-  | autobatch
-  ].*)
-qed.
- 
-lemma plusbyteenc_S:
- ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
- intros;
- rewrite < byte_of_nat_nat_of_byte;
- rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
- rewrite > na
-  
-(*CSC*)
- intros;
- unfold byte_of_nat;
- unfold plusbytenc;
- unfold plusbyte;
- 
- elim daemon.
-qed. 
-
-lemma eq_plusbytec_x0_x0_x_false:
- ∀x.plusbytec (mk_byte x0 x0) x = false.
- intro;
- elim x;
- elim e;
- elim e1;
- reflexivity.
-qed.
-
-lemma loop_invariant':
- ∀x,y:byte.∀j:nat. j ≤ y →
-  execute (mult_status x y) (5 + 23*j)
-   =
-    mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
-     (plusbytec (byte_of_nat (x*pred j)) x)
-     (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
-      (byte_of_nat (x * j)))
-     0.
- intros 3;
- elim j;
-  [ do 2 (rewrite < times_n_O);
-    apply status_eq;
-    [1,2,3,4,7: normalize; reflexivity
-    | rewrite > eq_plusbytec_x0_x0_x_false;
-      normalize;
-      reflexivity 
-    | intro;
-      elim daemon
-    ]
-  | cut (5 + 23 * S n = 5 + 23 * n + 23);
-    [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
-      letin H' ≝ (H ?); clearbody H'; clear H;
-      [ autobatch
-      | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
-        clear Hcut;
-        rewrite > xxx;
-        clear xxx;
-        apply (transitive_eq ? ? ? ? K);
-        clear K; 
-        rewrite > H';
-        clear H';
-        cut (∃z.y-n=S z ∧ z < 255);
-         [ elim Hcut; clear Hcut;
-           elim H; clear H;
-           rewrite > H2;
-           (* instruction LDAd *)
-           letin K ≝
-            (breakpoint
-              (mk_status (byte_of_nat (x*n)) 4 O
-               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
-               (plusbytec (byte_of_nat (x*pred n)) x)
-               (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
-               (byte_of_nat (x*n))) O)
-              3 20); clearbody K;
-           normalize in K:(? ? (? ? %) ?);
-           apply transitive_eq; [2: apply K | skip | ]; clear K;
-           whd in ⊢ (? ? (? % ?) ?);
-           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
-           change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
-            with (byte_of_nat (S a));
-           change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
-            (byte_of_nat (S a));
-           (* instruction BEQ *)
-           letin K ≝
-            (breakpoint
-              (mk_status (byte_of_nat (S a)) 6 O
-               (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
-               (plusbytec (byte_of_nat (x*pred n)) x)
-                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
-                 (byte_of_nat (x*n))) O)
-              3 17); clearbody K;
-           normalize in K:(? ? (? ? %) ?);
-           apply transitive_eq; [2: apply K | skip | ]; clear K;
-           whd in ⊢ (? ? (? % ?) ?);
-           letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
-           rewrite > K; clear K;
-           simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
-           (* instruction LDAd *)
-           letin K ≝
-            (breakpoint
-              (mk_status (byte_of_nat (S a)) 8 O
-               (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
-               (plusbytec (byte_of_nat (x*pred n)) x)
-                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
-                 (byte_of_nat (x*n))) O)
-              3 14); clearbody K;
-           normalize in K:(? ? (? ? %) ?);
-           apply transitive_eq; [2: apply K | skip | ]; clear K;
-           whd in ⊢ (? ? (? % ?) ?);
-           change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
-           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
-           change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
-           (* instruction DECd *)
-           letin K ≝
-            (breakpoint
-             (mk_status (byte_of_nat (x*n)) 10 O
-              (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
-              (plusbytec (byte_of_nat (x*pred n)) x)
-               (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
-                (byte_of_nat (x*n))) O)
-             5 9); clearbody K;
-           normalize in K:(? ? (? ? %) ?);
-           apply transitive_eq; [2: apply K | skip | ]; clear K;
-           whd in ⊢ (? ? (? % ?) ?);
-           change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
-           rewrite > (eq_bpred_S_a_a ? H3);
-           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
-           normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
-           cut (y - S n = a);
-            [2: elim daemon | ];
-           rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;          
-           (* instruction ADDd *)
-           letin K ≝
-            (breakpoint
-             (mk_status (byte_of_nat (x*n)) 12
-              O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
-              (plusbytec (byte_of_nat (x*pred n)) x)
-              (update
-               (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
-               32 (byte_of_nat (x*n))) 31
-               (byte_of_nat (y-S n))) O)
-             3 6); clearbody K;
-           normalize in K:(? ? (? ? %) ?);            
-           apply transitive_eq; [2: apply K | skip | ]; clear K;
-           whd in ⊢ (? ? (? % ?) ?);
-           change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
-            (plusbytenc (byte_of_nat (x*n)) x);
-           change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
-            (plusbytenc (byte_of_nat (x*n)) x);
-           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
-           change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
-            with (plusbytec (byte_of_nat (x*n)) x);
-           rewrite > plusbyteenc_S;
-           (* instruction STAd *)
-           letin K ≝
-            (breakpoint
-             (mk_status (byte_of_nat (x*S n)) 14 O
-              (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
-              (plusbytec (byte_of_nat (x*n)) x)
-               (update
-                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
-                32 (byte_of_nat (x*n))) 31
-                (byte_of_nat (y-S n))) O)
-            3 3); clearbody K;
-           normalize in K:(? ? (? ? %) ?);            
-           apply transitive_eq; [2: apply K | skip | ]; clear K;
-           whd in ⊢ (? ? (? % ?) ?);
-           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
-           (* instruction BRA *)
-           whd in ⊢ (? ? % ?);
-           normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
-           rewrite < pred_Sn;        
-           apply status_eq;
-            [1,2,3,4,7: normalize; reflexivity
-            | change with (plusbytec (byte_of_nat (x*n)) x =
-                             plusbytec (byte_of_nat (x*n)) x);
-              reflexivity
-            |6: intro;
-              elim daemon
-            ]
-         | exists;
-            [ apply (y - S n)
-            | split;
-               [ rewrite < (minus_S_S y n);
-                 autobatch
-               | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
-                 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
-                 autobatch
-               ]
-            ]
-         ]
-      ]
-    | rewrite > associative_plus;
-      autobatch paramodulation
-    ] 
-  ]   
-qed.
-
-theorem test_x_y:
- ∀x,y:byte.
-  let i ≝ 14 + 23 * y in
-   execute (mult_status x y) i =
-    mk_status (byte_of_nat (x*y)) 20 0
-     (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
-     (plusbytec (byte_of_nat (x*pred y)) x)
-     (update
-       (update (mult_memory x y) 31 (mk_byte x0 x0))
-       32 (byte_of_nat (x*y)))
-     0.
- intros;
- cut (14 + 23 * y = 5 + 23*y + 9);
-  [2: autobatch paramodulation;
-  | rewrite > Hcut; (* clear Hcut; *)
-    rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
-    rewrite > loop_invariant';
-     [2: apply le_n
-     | rewrite < minus_n_n;
-       apply status_eq;
-        [1,2,3,4,5,7: normalize; reflexivity
-        | elim daemon
-        ]
-     ]
-  ].
-qed.
diff --git a/matita/library/assembly/byte.ma b/matita/library/assembly/byte.ma
new file mode 100644
index 000000000..f18effeab
--- /dev/null
+++ b/matita/library/assembly/byte.ma
@@ -0,0 +1,261 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/assembly/byte".
+
+include "exadecimal.ma".
+
+record byte : Type ≝ {
+ bh: exadecimal;
+ bl: exadecimal
+}.
+
+definition eqbyte ≝
+ λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
+
+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'' ]].
+
+definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
+
+coercion cic:/matita/assembly/byte/nat_of_byte.con.
+
+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.
+
+lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
+ intro;
+ unfold nat_of_byte;
+ letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
+ letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
+ unfold lt in H K ⊢ %;
+ letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
+ letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
+ apply le_S_S;
+ cut (16*bh b ≤ 16*15);
+  [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
+    simplify in Hf:(? ? %);
+    assumption
+  | autobatch
+  ]
+qed.
+
+lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
+ intro;
+ letin H ≝ (lt_nat_of_byte_256 (byte_of_nat n)); clearbody H;
+ rewrite < (lt_to_eq_mod ? ? H); clear H;
+ unfold byte_of_nat;
+ unfold nat_of_byte;
+ change with ((16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n) \mod 256 = n \mod 256);
+ letin H ≝ (div_mod n 16 ?); clearbody H; [ autobatch | ];
+ rewrite > symmetric_times in H;
+ rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? % ?) ?) ?);
+ rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > H in ⊢ (? ? ? (? % ?)); clear H;
+ rewrite > mod_plus in ⊢ (? ? % ?);
+ rewrite > mod_plus in ⊢ (? ? ? %);
+ apply eq_mod_to_eq_plus_mod;
+ rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch];
+ rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch];
+ rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ];
+ rewrite < mod_mod in ⊢ (? ? % ?);
+  [ reflexivity
+  | autobatch
+  ].
+qed.
+
+axiom eq_nat_of_byte_n_nat_of_byte_mod_n_256:
+ ∀n. byte_of_nat n = byte_of_nat (n \mod 256).
+
+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' * 256
+   ].
+ intros;
+ unfold plusbyte;
+ generalize in match (plusex_ok (bl b1) (bl b2) c);
+ elim (plusex (bl b1) (bl b2) c);
+ simplify in H ⊢ %;
+ generalize in match (plusex_ok (bh b1) (bh b2) t1);
+ elim (plusex (bh b1) (bh b2) t1);
+ simplify in H1 ⊢ %;
+ change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
+ unfold nat_of_byte;
+ letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
+ rewrite > distr_times_plus in K:(? ? ? %);
+ rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
+ rewrite < associative_times in K:(? ? ? (? ? %));
+ normalize in K:(? ? ? (? ? (? % ?)));
+ rewrite > symmetric_times in K:(? ? ? (? ? %));
+ rewrite > sym_plus in ⊢ (? ? ? (? % ?));
+ rewrite > associative_plus in ⊢ (? ? ? %);
+ letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
+  apply transitive_eq; [3: apply K' | skip | ];
+ clear K';
+ rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
+ rewrite > associative_plus in ⊢ (? ? % ?);
+ rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
+ rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
+ rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
+ rewrite > H; clear H;
+ autobatch paramodulation.
+qed.
+
+definition bpred ≝
+ λb.
+  match eqex (bl b) x0 with
+   [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b))
+   | false ⇒ mk_byte (bh b) (xpred (bl b))
+   ]. 
+
+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].
+
+definition plusbytec ≝
+ λx,y.
+  match plusbyte x y false with
+   [couple _ c ⇒ c].
+
+lemma plusbytenc_O_x:
+ ∀x. plusbytenc (mk_byte x0 x0) x = x.
+ intros;
+ unfold plusbytenc;
+ rewrite > plusbyte_O_x;
+ reflexivity.
+qed.
+
+axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
+
+theorem plusbytenc_ok:
+ ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
+ intros;
+ unfold plusbytenc;
+ generalize in match (plusbyte_ok b1 b2 false);
+ elim (plusbyte b1 b2 false);
+ simplify in H ⊢ %;
+ change with (nat_of_byte t = (b1 + b2) \mod 256);
+ rewrite < plus_n_O in H;
+ rewrite > H; clear H;
+ rewrite > mod_plus;
+ letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
+ letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
+  [ autobatch | ];
+ autobatch paramodulation.
+qed.
+
+lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
+ ∀b. b < 255 → eqbyte (mk_byte x0 x0) (byte_of_nat (S b)) = false.
+ intros;
+ unfold byte_of_nat;
+ cut (b < 15 ∨ b ≥ 15);
+  [ elim Hcut;
+    [ unfold eqbyte;
+      change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b))); 
+      rewrite > eq_eqex_S_x0_false;
+       [ elim (eqex (bh (mk_byte x0 x0))
+(bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify;
+(*
+ alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
+         rewrite > andb_sym;
+*)
+         reflexivity
+       | assumption
+       ]
+    | unfold eqbyte;
+      change in ⊢ (? ? (? % ?) ?) with (eqex x0 (exadecimal_of_nat (S b/16)));
+      letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
+       [ autobatch
+       | unfold in H1;
+         apply le_S_S;
+         assumption
+       | clearbody K;
+         elim K; clear K;
+         rewrite > H2;
+         rewrite > eq_eqex_S_x0_false;
+          [ reflexivity
+          | unfold lt;
+            unfold lt in H;
+            rewrite < H2;
+            clear H2; clear a; clear H1; clear Hcut;
+            elim daemon (* trivial arithmetic property over <= and div *)
+          ] 
+       ]
+    ]
+  | elim daemon
+  ].
+qed.
+
+lemma eq_bpred_S_a_a:
+ ∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
+elim daemon. (*
+ intros;
+ unfold byte_of_nat;
+ cut (a \mod 16 = 15 ∨ a \mod 16 < 15);
+  [ elim Hcut;
+     [ 
+     |
+     ]
+  | autobatch
+  ].*)
+qed.
+ 
+lemma plusbytenc_S:
+ ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
+ intros;
+ rewrite < byte_of_nat_nat_of_byte;
+ rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
+ rewrite < times_n_Sm;
+ rewrite > mod_plus;
+ rewrite < eq_nat_of_byte_mod in ⊢ (? ? (? (? (? ? %) ?)) ?);
+ rewrite > nat_of_byte_byte_of_nat;
+ rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?);
+elim daemon.
+qed. 
+
+lemma eq_plusbytec_x0_x0_x_false:
+ ∀x.plusbytec (mk_byte x0 x0) x = false.
+ intro;
+ elim x;
+ elim e;
+ elim e1;
+ reflexivity.
+qed.
diff --git a/matita/library/assembly/exadecimal.ma b/matita/library/assembly/exadecimal.ma
new file mode 100644
index 000000000..bf689de00
--- /dev/null
+++ b/matita/library/assembly/exadecimal.ma
@@ -0,0 +1,926 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/assembly/exadecimal/".
+
+include "extra.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.
+
+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 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 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/exadecimal/nat_of_exadecimal.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 ]]]]]]]]]]]]]]]]. 
+
+lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
+ intro;
+ elim b;
+ simplify;
+ [
+ |*: alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
+   repeat (apply lt_S_S)
+ ];
+ autobatch.
+qed.
+
+lemma exadecimal_of_nat_mod:
+ ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
+ elim daemon.
+(*
+ intros;
+ cases n; [ reflexivity | ];
+ cases n1; [ reflexivity | ];
+ cases n2; [ reflexivity | ];
+ cases n3; [ reflexivity | ];
+ cases n4; [ reflexivity | ];
+ cases n5; [ reflexivity | ];
+ cases n6; [ reflexivity | ];  
+ cases n7; [ reflexivity | ];
+ cases n8; [ reflexivity | ];
+ cases n9; [ reflexivity | ];
+ cases n10; [ reflexivity | ];
+ cases n11; [ reflexivity | ];
+ cases n12; [ reflexivity | ];
+ cases n13; [ reflexivity | ];
+ cases n14; [ reflexivity | ];
+ cases n15; [ reflexivity | ];
+ change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
+ cut ((16 + n16) \mod 16 = n16 \mod 16);
+  [ rewrite > Hcut;
+    simplify in ⊢ (? ? % ?);
+    
+  | unfold mod;
+    change with (mod_aux (16+n16) (16+n16) 15 = n16);
+    unfold mod_aux;
+    change with
+     (match leb (16+n16) 15 with
+       [true ⇒ 16+n16
+       | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
+       ] = n16);
+    cut (leb (16+n16) 15 = false);
+     [ rewrite > Hcut;
+       change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
+       cut (16+n16-16 = n16);
+        [ rewrite > Hcut1; clear Hcut1;
+          
+        |
+        ]
+     |
+     ]
+  ]*)
+qed.
+
+axiom nat_of_exadecimal_exadecimal_of_nat:
+ ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16.
+(*
+ intro;
+ apply (exadecimal_of_nat_elim (λn.;
+ 
+ 
+ 
+ elim n 0; [ reflexivity | intro ];
+ elim n1 0; [ intros; reflexivity | intros 2 ];
+ elim n2 0; [ intros; reflexivity | intros 2 ];
+ elim n3 0; [ intros; reflexivity | intros 2 ];
+ elim n4 0; [ intros; reflexivity | intros 2 ];
+ elim n5 0; [ intros; reflexivity | intros 2 ];
+ elim n6 0; [ intros; reflexivity | intros 2 ];
+ elim n7 0; [ intros; reflexivity | intros 2 ];
+ elim n8 0; [ intros; reflexivity | intros 2 ];
+ elim n9 0; [ intros; reflexivity | intros 2 ];
+ elim n10 0; [ intros; reflexivity | intros 2 ];
+ elim n11 0; [ intros; reflexivity | intros 2 ];
+ elim n12 0; [ intros; reflexivity | intros 2 ];
+ elim n13 0; [ intros; reflexivity | intros 2 ];
+ elim n14 0; [ intros; reflexivity | intros 2 ];
+ elim n15 0; [ intros; reflexivity | intros 2 ];
+ intro;
+ simplify;
+ rewrite < H15;
+ change in ⊢ (? ? % ?) with (nat_of_exadecimal (exadecimal_of_nat n16));
+qed.
+*)
+
+lemma plusex_ok:
+ ∀b1,b2,c.
+  match plusex b1 b2 c with
+   [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
+ intros;
+ elim c;
+ elim b1;
+ elim b2;
+ normalize;
+ reflexivity.
+qed.
+
+definition xpred ≝
+ λb.
+  match b with
+   [ x0 ⇒ xF
+   | x1 ⇒ x0
+   | x2 ⇒ x1
+   | x3 ⇒ x2
+   | x4 ⇒ x3
+   | x5 ⇒ x4
+   | x6 ⇒ x5
+   | x7 ⇒ x6
+   | x8 ⇒ x7
+   | x9 ⇒ x8
+   | xA ⇒ x9
+   | xB ⇒ xA
+   | xC ⇒ xB
+   | xD ⇒ xC
+   | xE ⇒ xD
+   | xF ⇒ xE ].
+
+(* Way too slow and subsumed by previous theorem
+lemma bpred_pred:
+ ∀b.
+  match eqbyte b (mk_byte x0 x0) with
+   [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF
+   | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)].
+ intros;
+ elim b;
+ elim e;
+ elim e1;
+ reflexivity.
+qed.
+*)
+
+lemma eq_eqex_S_x0_false:
+ ∀n. n < 15 → eqex x0 (exadecimal_of_nat (S n)) = false.
+ intro;
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ cases n1 0; [ intro; simplify; reflexivity | clear n1];
+ cases n 0; [ intro; simplify; reflexivity | clear n];
+ intro;
+ unfold lt in H;
+ cut (S n1 ≤ 0);
+  [ elim (not_le_Sn_O ? Hcut)
+  | do 15 (apply le_S_S_to_le);
+    assumption
+  ]
+qed.
diff --git a/matita/library/assembly/extra.ma b/matita/library/assembly/extra.ma
new file mode 100644
index 000000000..70b43bb1e
--- /dev/null
+++ b/matita/library/assembly/extra.ma
@@ -0,0 +1,81 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/assembly/extra".
+
+include "nat/div_and_mod.ma".
+include "nat/primes.ma".
+include "list/list.ma".
+
+axiom mod_plus: ∀a,b,m. (a + b) \mod m = (a \mod m + b \mod m) \mod m.
+axiom mod_mod: ∀a,n,m. n∣m → a \mod n = a \mod n \mod m.
+axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O.
+axiom eq_mod_to_eq_plus_mod: ∀a,b,c,m. a \mod m = b \mod m → (a+c) \mod m = (b+c) \mod m.
+axiom eq_mod_times_times_mod: ∀a,b,n,m. m = a*n → (a*b) \mod m = a * (b \mod n).
+
+inductive cartesian_product (A,B: Type) : Type ≝
+ couple: ∀a:A.∀b:B. cartesian_product A B.
+
+lemma le_to_lt: ∀n,m. n ≤ m → n < S m.
+ intros;
+ autobatch.
+qed.
+
+alias num (instance 0) = "natural number".
+definition nat_of_bool ≝
+ λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
+
+theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
+ unfold lt;
+ intros;
+ autobatch.
+qed.
+
+lemma leq_m_n_to_eq_div_n_m_S: ∀n,m:nat. 0 < m → m ≤ n → ∃z. n/m = S z.
+ intros;
+ unfold div;
+ apply (ex_intro ? ? (div_aux (pred n) (n-m) (pred m)));
+ cut (∃w.m = S w);
+  [ elim Hcut;
+    rewrite > H2;
+    rewrite > H2 in H1;
+    clear Hcut; clear H2; clear H; (*clear m;*)
+    simplify;
+    unfold in ⊢ (? ? % ?);
+    cut (∃z.n = S z);
+     [ elim Hcut; clear Hcut;
+       rewrite > H in H1;
+       rewrite > H; clear m;
+       change in ⊢ (? ? % ?)  with
+        (match leb (S a1) a with
+         [ true ⇒ O
+         | false ⇒ S (div_aux a1 ((S a1) - S a) a)]);
+       cut (S a1 ≰ a);
+        [ apply (leb_elim (S a1) a);
+           [ intro;
+             elim (Hcut H2)
+           | intro;
+             simplify;
+             reflexivity
+           ]
+        | intro;
+          autobatch
+        ]
+     | elim H1; autobatch
+     ]
+  | autobatch
+  ].
+qed.
+
+axiom daemon: False.
diff --git a/matita/library/assembly/test.ma b/matita/library/assembly/test.ma
new file mode 100644
index 000000000..98eb48d91
--- /dev/null
+++ b/matita/library/assembly/test.ma
@@ -0,0 +1,297 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/assembly/test/".
+
+include "vm.ma".
+
+notation "hvbox(# break a)"
+  non associative with precedence 80
+for @{ 'byte_of_opcode $a }.
+interpretation "byte_of_opcode" 'byte_of_opcode a =
+ (cic:/matita/assembly/vm/byte_of_opcode.con a).
+
+definition mult_source : list byte ≝
+  [#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_memory ≝
+ λx,y.λa:addr.
+     match leb a 29 with
+      [ true ⇒ nth ? mult_source (mk_byte x0 x0) a
+      | false ⇒
+         match eqb a 30 with
+          [ true ⇒ x
+          | false ⇒ y
+          ]
+      ].
+
+definition mult_status ≝
+ λx,y.
+  mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0.
+
+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.
+  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;
+ split;
+  [ reflexivity
+  | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x);
+    rewrite > plusbytenc_O_x;
+    reflexivity
+  ].
+qed.
+
+lemma test_x_2:
+ ∀x.
+  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
+  | change in ⊢ (? ? % ?) with
+     (plusbytenc (plusbytenc (mk_byte x0 x0) x) x);
+    rewrite > plusbytenc_O_x;
+    reflexivity
+  ].
+qed.
+
+lemma loop_invariant':
+ ∀x,y:byte.∀j:nat. j ≤ y →
+  execute (mult_status x y) (5 + 23*j)
+   =
+    mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
+     (plusbytec (byte_of_nat (x*pred j)) x)
+     (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
+      (byte_of_nat (x * j)))
+     0.
+ intros 3;
+ elim j;
+  [ do 2 (rewrite < times_n_O);
+    apply status_eq;
+    [1,2,3,4,7: normalize; reflexivity
+    | rewrite > eq_plusbytec_x0_x0_x_false;
+      normalize;
+      reflexivity 
+    | intro;
+      elim daemon
+    ]
+  | cut (5 + 23 * S n = 5 + 23 * n + 23);
+    [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K;
+      letin H' ≝ (H ?); clearbody H'; clear H;
+      [ autobatch
+      | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx;
+        clear Hcut;
+        rewrite > xxx;
+        clear xxx;
+        apply (transitive_eq ? ? ? ? K);
+        clear K; 
+        rewrite > H';
+        clear H';
+        cut (∃z.y-n=S z ∧ z < 255);
+         [ elim Hcut; clear Hcut;
+           elim H; clear H;
+           rewrite > H2;
+           (* instruction LDAd *)
+           letin K ≝
+            (breakpoint
+              (mk_status (byte_of_nat (x*n)) 4 O
+               (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
+               (plusbytec (byte_of_nat (x*pred n)) x)
+               (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
+               (byte_of_nat (x*n))) O)
+              3 20); clearbody K;
+           normalize in K:(? ? (? ? %) ?);
+           apply transitive_eq; [2: apply K | skip | ]; clear K;
+           whd in ⊢ (? ? (? % ?) ?);
+           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+           change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
+            with (byte_of_nat (S a));
+           change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
+            (byte_of_nat (S a));
+           (* instruction BEQ *)
+           letin K ≝
+            (breakpoint
+              (mk_status (byte_of_nat (S a)) 6 O
+               (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
+               (plusbytec (byte_of_nat (x*pred n)) x)
+                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
+                 (byte_of_nat (x*n))) O)
+              3 17); clearbody K;
+           normalize in K:(? ? (? ? %) ?);
+           apply transitive_eq; [2: apply K | skip | ]; clear K;
+           whd in ⊢ (? ? (? % ?) ?);
+           letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
+           rewrite > K; clear K;
+           simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+           (* instruction LDAd *)
+           letin K ≝
+            (breakpoint
+              (mk_status (byte_of_nat (S a)) 8 O
+               (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
+               (plusbytec (byte_of_nat (x*pred n)) x)
+                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
+                 (byte_of_nat (x*n))) O)
+              3 14); clearbody K;
+           normalize in K:(? ? (? ? %) ?);
+           apply transitive_eq; [2: apply K | skip | ]; clear K;
+           whd in ⊢ (? ? (? % ?) ?);
+           change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with (byte_of_nat (x*n));
+           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+           change in ⊢ (? ? (? (? ? ? ? % ? ? ?) ?) ?) with (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)));
+           (* instruction DECd *)
+           letin K ≝
+            (breakpoint
+             (mk_status (byte_of_nat (x*n)) 10 O
+              (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
+              (plusbytec (byte_of_nat (x*pred n)) x)
+               (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
+                (byte_of_nat (x*n))) O)
+             5 9); clearbody K;
+           normalize in K:(? ? (? ? %) ?);
+           apply transitive_eq; [2: apply K | skip | ]; clear K;
+           whd in ⊢ (? ? (? % ?) ?);
+           change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with (bpred (byte_of_nat (S a)));
+           rewrite > (eq_bpred_S_a_a ? H3);
+           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+           normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
+           cut (y - S n = a);
+            [2: elim daemon | ];
+           rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;          
+           (* instruction ADDd *)
+           letin K ≝
+            (breakpoint
+             (mk_status (byte_of_nat (x*n)) 12
+              O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
+              (plusbytec (byte_of_nat (x*pred n)) x)
+              (update
+               (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
+               32 (byte_of_nat (x*n))) 31
+               (byte_of_nat (y-S n))) O)
+             3 6); clearbody K;
+           normalize in K:(? ? (? ? %) ?);            
+           apply transitive_eq; [2: apply K | skip | ]; clear K;
+           whd in ⊢ (? ? (? % ?) ?);
+           change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?) with
+            (plusbytenc (byte_of_nat (x*n)) x);
+           change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
+            (plusbytenc (byte_of_nat (x*n)) x);
+           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+           change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
+            with (plusbytec (byte_of_nat (x*n)) x);
+           rewrite > plusbytenc_S;
+           (* instruction STAd *)
+           letin K ≝
+            (breakpoint
+             (mk_status (byte_of_nat (x*S n)) 14 O
+              (eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
+              (plusbytec (byte_of_nat (x*n)) x)
+               (update
+                (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
+                32 (byte_of_nat (x*n))) 31
+                (byte_of_nat (y-S n))) O)
+            3 3); clearbody K;
+           normalize in K:(? ? (? ? %) ?);            
+           apply transitive_eq; [2: apply K | skip | ]; clear K;
+           whd in ⊢ (? ? (? % ?) ?);
+           normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+           (* instruction BRA *)
+           whd in ⊢ (? ? % ?);
+           normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
+           rewrite < pred_Sn;        
+           apply status_eq;
+            [1,2,3,4,7: normalize; reflexivity
+            | change with (plusbytec (byte_of_nat (x*n)) x =
+                             plusbytec (byte_of_nat (x*n)) x);
+              reflexivity
+            |6: intro;
+              elim daemon
+            ]
+         | exists;
+            [ apply (y - S n)
+            | split;
+               [ rewrite < (minus_S_S y n);
+                 autobatch
+               | letin K ≝ (lt_nat_of_byte_256 y); clearbody K;
+                 letin K' ≝ (lt_minus_m y (S n) ? ?); clearbody K';
+                 autobatch
+               ]
+            ]
+         ]
+      ]
+    | rewrite > associative_plus;
+      autobatch paramodulation
+    ] 
+  ]   
+qed.
+
+theorem test_x_y:
+ ∀x,y:byte.
+  let i ≝ 14 + 23 * y in
+   execute (mult_status x y) i =
+    mk_status (byte_of_nat (x*y)) 20 0
+     (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
+     (plusbytec (byte_of_nat (x*pred y)) x)
+     (update
+       (update (mult_memory x y) 31 (mk_byte x0 x0))
+       32 (byte_of_nat (x*y)))
+     0.
+ intros;
+ cut (14 + 23 * y = 5 + 23*y + 9);
+  [2: autobatch paramodulation;
+  | rewrite > Hcut; (* clear Hcut; *)
+    rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
+    rewrite > loop_invariant';
+     [2: apply le_n
+     | rewrite < minus_n_n;
+       apply status_eq;
+        [1,2,3,4,5,7: normalize; reflexivity
+        | elim daemon
+        ]
+     ]
+  ].
+qed.
diff --git a/matita/library/assembly/vm.ma b/matita/library/assembly/vm.ma
new file mode 100644
index 000000000..dac755c82
--- /dev/null
+++ b/matita/library/assembly/vm.ma
@@ -0,0 +1,225 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/assembly/vm/".
+
+include "byte.ma".
+
+definition addr ≝ nat.
+
+definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b.
+
+coercion cic:/matita/assembly/vm/addr_of_byte.con.
+
+inductive opcode: Type ≝
+   ADDd: opcode  (* 3 clock, 171 *)
+ | BEQ: opcode   (* 3, 55 *)
+ | BRA: opcode   (* 3, 48 *)
+ | DECd: opcode  (* 5, 58 *)
+ | LDAi: opcode  (* 2, 166 *)
+ | LDAd: opcode  (* 3, 182 *)
+ | STAd: opcode. (* 3, 183 *)
+
+let rec cycles_of_opcode op : nat ≝
+ match op with
+  [ ADDd ⇒ 3
+  | BEQ ⇒ 3
+  | BRA ⇒ 3
+  | DECd ⇒ 5
+  | LDAi ⇒ 2
+  | LDAd ⇒ 3
+  | STAd ⇒ 3
+  ].
+
+definition opcodemap ≝
+ [ couple ? ? ADDd (mk_byte xA xB);
+   couple ? ? BEQ (mk_byte x3 x7);
+   couple ? ? BRA (mk_byte x3 x0);
+   couple ? ? DECd (mk_byte x3 xA);
+   couple ? ? LDAi (mk_byte xA x6);
+   couple ? ? LDAd (mk_byte xB x6);
+   couple ? ? STAd (mk_byte xB x7) ].
+
+definition opcode_of_byte ≝
+ λb.
+  let rec aux l ≝
+   match l with
+    [ nil ⇒ ADDd
+    | cons c tl ⇒
+       match c with
+        [ couple op n ⇒
+           match eqbyte n b with
+            [ true ⇒ op
+            | false ⇒ aux tl
+            ]]]
+  in
+   aux opcodemap.
+
+definition magic_of_opcode ≝
+ λop1.
+  match op1 with
+   [ ADDd ⇒ 0
+   | BEQ ⇒  1 
+   | BRA ⇒  2
+   | DECd ⇒ 3
+   | LDAi ⇒ 4
+   | LDAd ⇒ 5
+   | STAd ⇒ 6 ].
+   
+definition opcodeeqb ≝
+ λop1,op2. eqb (magic_of_opcode op1) (magic_of_opcode op2).
+
+definition byte_of_opcode : opcode → byte ≝
+ λop.
+  let rec aux l ≝
+   match l with
+    [ nil ⇒ mk_byte x0 x0
+    | cons c tl ⇒
+       match c with
+        [ couple op' n ⇒
+           match opcodeeqb op op' with
+            [ true ⇒ n
+            | false ⇒ aux tl
+            ]]]
+  in
+   aux opcodemap.
+
+record status : Type ≝ {
+  acc : byte;
+  pc  : addr;
+  spc : addr;
+  zf  : bool;
+  cf  : bool;
+  mem : addr → byte;
+  clk : nat
+}.
+
+definition update ≝
+ λf: addr → byte.λa.λv.λx.
+  match eqb x a with
+   [ true ⇒ v
+   | false ⇒ f x ].
+
+lemma update_update_a_a:
+ ∀s,a,v1,v2,b.
+  update (update s a v1) a v2 b = update s a v2 b.
+ intros;
+ unfold update;
+ unfold update;
+ elim (eqb b a);
+ reflexivity.
+qed. 
+
+lemma update_update_a_b:
+ ∀s,a1,v1,a2,v2,b.
+  a1 ≠ a2 →
+   update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
+ intros;
+ unfold update;
+ unfold update;
+ apply (bool_elim ? (eqb b a1)); intros;
+ apply (bool_elim ? (eqb b a2)); intros;
+ simplify;
+ [ elim H;
+   rewrite < (eqb_true_to_eq ? ? H1);
+   apply eqb_true_to_eq;
+   assumption
+ |*: reflexivity
+ ].
+qed.
+
+definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
+
+definition tick ≝
+ λ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) clk' with
+   [ true ⇒
+      match opc with
+       [ ADDd ⇒
+          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
+            (eqbyte (mk_byte x0 x0) acc') c' mem 0 (* verify carrier! *)
+       | BEQ ⇒
+          mk_status
+           acc
+           (match zf with
+             [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
+                      (* FIXME: can't work - address truncated to 8 bits *)
+             | false ⇒ 2 + pc
+             ])
+           spc
+           zf
+           cf
+           mem
+           0
+       | BRA ⇒
+          mk_status
+           acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
+                                      (* FIXME: same as above *)
+           spc
+           zf
+           cf
+           mem
+           0
+       | DECd ⇒
+          let x ≝ bpred (mem op1) in (* signed!!! *)
+          let mem' ≝ update mem op1 x in
+           mk_status acc (2 + pc) spc
+            (eqbyte (mk_byte x0 x0) x) cf mem' 0 (* check zb!!! *)
+       | LDAi ⇒
+          mk_status op1 (2 + pc) spc (eqbyte (mk_byte x0 x0) op1) cf mem 0
+       | LDAd ⇒
+          let x ≝ mem op1 in
+           mk_status x (2 + pc) spc (eqbyte (mk_byte x0 x0) x) cf mem 0
+       | STAd ⇒
+          mk_status acc (2 + pc) spc zf cf
+           (update mem op1 acc) 0
+       ]
+   | false ⇒
+       mk_status
+        acc pc spc zf cf mem (S clk)
+   ]].
+
+let rec execute s n on n ≝
+ match n with
+  [ O ⇒ s
+  | S n' ⇒ execute (tick s) n'
+  ].
+  
+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.
+
+axiom status_eq:
+ ∀s,s'.
+  acc s = acc s' →
+  pc s = pc s' →
+  spc s = spc s' →
+  zf s = zf s' →
+  cf s = cf s' →
+  (∀a. mem s a = mem s' a) →
+  clk s = clk s' →
+   s=s'.