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.
-
-definition nat_of_bool ≝
- λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
-
-(* Way too slow. Handles 2^32 goals!
-lemma plusbyte_ok:
- ∀b1,b2,c.
- match plusbyte b1 b2 c with
- [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c'
- ].
- intros;
- elim c;
- elim b1;
- elim e;
- elim e1;
- elim b2;
- elim e2;
- elim e3;
- reflexivity.
-qed.
-*)
-
-notation "14" non associative with precedence 80 for @{ 'x14 }.
-interpretation "natural number" 'x14 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
+notation "14" non associative with precedence 80 for @{ 'x14 }.
+interpretation "natural number" 'x14 =
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
notation "22" non associative with precedence 80 for @{ 'x22 }.
interpretation "natural number" 'x22 =
(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
+
+inductive exadecimal : Type ≝
+ x0: exadecimal
+ | x1: exadecimal
+ | x2: exadecimal
+ | x3: exadecimal
+ | x4: exadecimal
+ | x5: exadecimal
+ | x6: exadecimal
+ | x7: exadecimal
+ | x8: exadecimal
+ | x9: exadecimal
+ | xA: exadecimal
+ | xB: exadecimal
+ | xC: exadecimal
+ | xD: exadecimal
+ | xE: exadecimal
+ | xF: exadecimal.
+
+record byte : Type ≝ {
+ bh: exadecimal;
+ bl: exadecimal
+}.
+
+definition eqex ≝
+ λb1,b2.
+ match b1 with
+ [ x0 ⇒
+ match b2 with
+ [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x1 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x2 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x3 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x4 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x5 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x6 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x7 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x8 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x9 ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xA ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xB ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xC ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xD ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
+ | xE ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ false ]
+ | xF ⇒
+ match b2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]].
+
+
+definition eqbyte ≝
+ λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b').
+
+inductive cartesian_product (A,B: Type) : Type ≝
+ couple: ∀a:A.∀b:B. cartesian_product A B.
+
+definition plusex ≝
+ λb1,b2,c.
+ match c with
+ [ true ⇒
+ match b1 with
+ [ x0 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x1 false
+ | x1 ⇒ couple exadecimal bool x2 false
+ | x2 ⇒ couple exadecimal bool x3 false
+ | x3 ⇒ couple exadecimal bool x4 false
+ | x4 ⇒ couple exadecimal bool x5 false
+ | x5 ⇒ couple exadecimal bool x6 false
+ | x6 ⇒ couple exadecimal bool x7 false
+ | x7 ⇒ couple exadecimal bool x8 false
+ | x8 ⇒ couple exadecimal bool x9 false
+ | x9 ⇒ couple exadecimal bool xA false
+ | xA ⇒ couple exadecimal bool xB false
+ | xB ⇒ couple exadecimal bool xC false
+ | xC ⇒ couple exadecimal bool xD false
+ | xD ⇒ couple exadecimal bool xE false
+ | xE ⇒ couple exadecimal bool xF false
+ | xF ⇒ couple exadecimal bool x0 true ]
+ | x1 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x2 false
+ | x1 ⇒ couple exadecimal bool x3 false
+ | x2 ⇒ couple exadecimal bool x4 false
+ | x3 ⇒ couple exadecimal bool x5 false
+ | x4 ⇒ couple exadecimal bool x6 false
+ | x5 ⇒ couple exadecimal bool x7 false
+ | x6 ⇒ couple exadecimal bool x8 false
+ | x7 ⇒ couple exadecimal bool x9 false
+ | x8 ⇒ couple exadecimal bool xA false
+ | x9 ⇒ couple exadecimal bool xB false
+ | xA ⇒ couple exadecimal bool xC false
+ | xB ⇒ couple exadecimal bool xD false
+ | xC ⇒ couple exadecimal bool xE false
+ | xD ⇒ couple exadecimal bool xF false
+ | xE ⇒ couple exadecimal bool x0 true
+ | xF ⇒ couple exadecimal bool x1 true ]
+ | x2 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x3 false
+ | x1 ⇒ couple exadecimal bool x4 false
+ | x2 ⇒ couple exadecimal bool x5 false
+ | x3 ⇒ couple exadecimal bool x6 false
+ | x4 ⇒ couple exadecimal bool x7 false
+ | x5 ⇒ couple exadecimal bool x8 false
+ | x6 ⇒ couple exadecimal bool x9 false
+ | x7 ⇒ couple exadecimal bool xA false
+ | x8 ⇒ couple exadecimal bool xB false
+ | x9 ⇒ couple exadecimal bool xC false
+ | xA ⇒ couple exadecimal bool xD false
+ | xB ⇒ couple exadecimal bool xE false
+ | xC ⇒ couple exadecimal bool xF false
+ | xD ⇒ couple exadecimal bool x0 true
+ | xE ⇒ couple exadecimal bool x1 true
+ | xF ⇒ couple exadecimal bool x2 true ]
+ | x3 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x4 false
+ | x1 ⇒ couple exadecimal bool x5 false
+ | x2 ⇒ couple exadecimal bool x6 false
+ | x3 ⇒ couple exadecimal bool x7 false
+ | x4 ⇒ couple exadecimal bool x8 false
+ | x5 ⇒ couple exadecimal bool x9 false
+ | x6 ⇒ couple exadecimal bool xA false
+ | x7 ⇒ couple exadecimal bool xB false
+ | x8 ⇒ couple exadecimal bool xC false
+ | x9 ⇒ couple exadecimal bool xD false
+ | xA ⇒ couple exadecimal bool xE false
+ | xB ⇒ couple exadecimal bool xF false
+ | xC ⇒ couple exadecimal bool x0 true
+ | xD ⇒ couple exadecimal bool x1 true
+ | xE ⇒ couple exadecimal bool x2 true
+ | xF ⇒ couple exadecimal bool x3 true ]
+ | x4 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x5 false
+ | x1 ⇒ couple exadecimal bool x6 false
+ | x2 ⇒ couple exadecimal bool x7 false
+ | x3 ⇒ couple exadecimal bool x8 false
+ | x4 ⇒ couple exadecimal bool x9 false
+ | x5 ⇒ couple exadecimal bool xA false
+ | x6 ⇒ couple exadecimal bool xB false
+ | x7 ⇒ couple exadecimal bool xC false
+ | x8 ⇒ couple exadecimal bool xD false
+ | x9 ⇒ couple exadecimal bool xE false
+ | xA ⇒ couple exadecimal bool xF false
+ | xB ⇒ couple exadecimal bool x0 true
+ | xC ⇒ couple exadecimal bool x1 true
+ | xD ⇒ couple exadecimal bool x2 true
+ | xE ⇒ couple exadecimal bool x3 true
+ | xF ⇒ couple exadecimal bool x4 true ]
+ | x5 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x6 false
+ | x1 ⇒ couple exadecimal bool x7 false
+ | x2 ⇒ couple exadecimal bool x8 false
+ | x3 ⇒ couple exadecimal bool x9 false
+ | x4 ⇒ couple exadecimal bool xA false
+ | x5 ⇒ couple exadecimal bool xB false
+ | x6 ⇒ couple exadecimal bool xC false
+ | x7 ⇒ couple exadecimal bool xD false
+ | x8 ⇒ couple exadecimal bool xE false
+ | x9 ⇒ couple exadecimal bool xF false
+ | xA ⇒ couple exadecimal bool x0 true
+ | xB ⇒ couple exadecimal bool x1 true
+ | xC ⇒ couple exadecimal bool x2 true
+ | xD ⇒ couple exadecimal bool x3 true
+ | xE ⇒ couple exadecimal bool x4 true
+ | xF ⇒ couple exadecimal bool x5 true ]
+ | x6 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x7 false
+ | x1 ⇒ couple exadecimal bool x8 false
+ | x2 ⇒ couple exadecimal bool x9 false
+ | x3 ⇒ couple exadecimal bool xA false
+ | x4 ⇒ couple exadecimal bool xB false
+ | x5 ⇒ couple exadecimal bool xC false
+ | x6 ⇒ couple exadecimal bool xD false
+ | x7 ⇒ couple exadecimal bool xE false
+ | x8 ⇒ couple exadecimal bool xF false
+ | x9 ⇒ couple exadecimal bool x0 true
+ | xA ⇒ couple exadecimal bool x1 true
+ | xB ⇒ couple exadecimal bool x2 true
+ | xC ⇒ couple exadecimal bool x3 true
+ | xD ⇒ couple exadecimal bool x4 true
+ | xE ⇒ couple exadecimal bool x5 true
+ | xF ⇒ couple exadecimal bool x6 true ]
+ | x7 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x8 false
+ | x1 ⇒ couple exadecimal bool x9 false
+ | x2 ⇒ couple exadecimal bool xA false
+ | x3 ⇒ couple exadecimal bool xB false
+ | x4 ⇒ couple exadecimal bool xC false
+ | x5 ⇒ couple exadecimal bool xD false
+ | x6 ⇒ couple exadecimal bool xE false
+ | x7 ⇒ couple exadecimal bool xF false
+ | x8 ⇒ couple exadecimal bool x0 true
+ | x9 ⇒ couple exadecimal bool x1 true
+ | xA ⇒ couple exadecimal bool x2 true
+ | xB ⇒ couple exadecimal bool x3 true
+ | xC ⇒ couple exadecimal bool x4 true
+ | xD ⇒ couple exadecimal bool x5 true
+ | xE ⇒ couple exadecimal bool x6 true
+ | xF ⇒ couple exadecimal bool x7 true ]
+ | x8 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x9 false
+ | x1 ⇒ couple exadecimal bool xA false
+ | x2 ⇒ couple exadecimal bool xB false
+ | x3 ⇒ couple exadecimal bool xC false
+ | x4 ⇒ couple exadecimal bool xD false
+ | x5 ⇒ couple exadecimal bool xE false
+ | x6 ⇒ couple exadecimal bool xF false
+ | x7 ⇒ couple exadecimal bool x0 true
+ | x8 ⇒ couple exadecimal bool x1 true
+ | x9 ⇒ couple exadecimal bool x2 true
+ | xA ⇒ couple exadecimal bool x3 true
+ | xB ⇒ couple exadecimal bool x4 true
+ | xC ⇒ couple exadecimal bool x5 true
+ | xD ⇒ couple exadecimal bool x6 true
+ | xE ⇒ couple exadecimal bool x7 true
+ | xF ⇒ couple exadecimal bool x8 true ]
+ | x9 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xA false
+ | x1 ⇒ couple exadecimal bool xB false
+ | x2 ⇒ couple exadecimal bool xC false
+ | x3 ⇒ couple exadecimal bool xD false
+ | x4 ⇒ couple exadecimal bool xE false
+ | x5 ⇒ couple exadecimal bool xF false
+ | x6 ⇒ couple exadecimal bool x0 true
+ | x7 ⇒ couple exadecimal bool x1 true
+ | x8 ⇒ couple exadecimal bool x2 true
+ | x9 ⇒ couple exadecimal bool x3 true
+ | xA ⇒ couple exadecimal bool x4 true
+ | xB ⇒ couple exadecimal bool x5 true
+ | xC ⇒ couple exadecimal bool x6 true
+ | xD ⇒ couple exadecimal bool x7 true
+ | xE ⇒ couple exadecimal bool x8 true
+ | xF ⇒ couple exadecimal bool x9 true ]
+ | xA ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xB false
+ | x1 ⇒ couple exadecimal bool xC false
+ | x2 ⇒ couple exadecimal bool xD false
+ | x3 ⇒ couple exadecimal bool xE false
+ | x4 ⇒ couple exadecimal bool xF false
+ | x5 ⇒ couple exadecimal bool x0 true
+ | x6 ⇒ couple exadecimal bool x1 true
+ | x7 ⇒ couple exadecimal bool x2 true
+ | x8 ⇒ couple exadecimal bool x3 true
+ | x9 ⇒ couple exadecimal bool x4 true
+ | xA ⇒ couple exadecimal bool x5 true
+ | xB ⇒ couple exadecimal bool x6 true
+ | xC ⇒ couple exadecimal bool x7 true
+ | xD ⇒ couple exadecimal bool x8 true
+ | xE ⇒ couple exadecimal bool x9 true
+ | xF ⇒ couple exadecimal bool xA true ]
+ | xB ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xC false
+ | x1 ⇒ couple exadecimal bool xD false
+ | x2 ⇒ couple exadecimal bool xE false
+ | x3 ⇒ couple exadecimal bool xF false
+ | x4 ⇒ couple exadecimal bool x0 true
+ | x5 ⇒ couple exadecimal bool x1 true
+ | x6 ⇒ couple exadecimal bool x2 true
+ | x7 ⇒ couple exadecimal bool x3 true
+ | x8 ⇒ couple exadecimal bool x4 true
+ | x9 ⇒ couple exadecimal bool x5 true
+ | xA ⇒ couple exadecimal bool x6 true
+ | xB ⇒ couple exadecimal bool x7 true
+ | xC ⇒ couple exadecimal bool x8 true
+ | xD ⇒ couple exadecimal bool x9 true
+ | xE ⇒ couple exadecimal bool xA true
+ | xF ⇒ couple exadecimal bool xB true ]
+ | xC ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xD false
+ | x1 ⇒ couple exadecimal bool xE false
+ | x2 ⇒ couple exadecimal bool xF false
+ | x3 ⇒ couple exadecimal bool x0 true
+ | x4 ⇒ couple exadecimal bool x1 true
+ | x5 ⇒ couple exadecimal bool x2 true
+ | x6 ⇒ couple exadecimal bool x3 true
+ | x7 ⇒ couple exadecimal bool x4 true
+ | x8 ⇒ couple exadecimal bool x5 true
+ | x9 ⇒ couple exadecimal bool x6 true
+ | xA ⇒ couple exadecimal bool x7 true
+ | xB ⇒ couple exadecimal bool x8 true
+ | xC ⇒ couple exadecimal bool x9 true
+ | xD ⇒ couple exadecimal bool xA true
+ | xE ⇒ couple exadecimal bool xB true
+ | xF ⇒ couple exadecimal bool xC true ]
+ | xD ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xE false
+ | x1 ⇒ couple exadecimal bool xF false
+ | x2 ⇒ couple exadecimal bool x0 true
+ | x3 ⇒ couple exadecimal bool x1 true
+ | x4 ⇒ couple exadecimal bool x2 true
+ | x5 ⇒ couple exadecimal bool x3 true
+ | x6 ⇒ couple exadecimal bool x4 true
+ | x7 ⇒ couple exadecimal bool x5 true
+ | x8 ⇒ couple exadecimal bool x6 true
+ | x9 ⇒ couple exadecimal bool x7 true
+ | xA ⇒ couple exadecimal bool x8 true
+ | xB ⇒ couple exadecimal bool x9 true
+ | xC ⇒ couple exadecimal bool xA true
+ | xD ⇒ couple exadecimal bool xB true
+ | xE ⇒ couple exadecimal bool xC true
+ | xF ⇒ couple exadecimal bool xD true ]
+ | xE ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xF false
+ | x1 ⇒ couple exadecimal bool x0 true
+ | x2 ⇒ couple exadecimal bool x1 true
+ | x3 ⇒ couple exadecimal bool x2 true
+ | x4 ⇒ couple exadecimal bool x3 true
+ | x5 ⇒ couple exadecimal bool x4 true
+ | x6 ⇒ couple exadecimal bool x5 true
+ | x7 ⇒ couple exadecimal bool x6 true
+ | x8 ⇒ couple exadecimal bool x7 true
+ | x9 ⇒ couple exadecimal bool x8 true
+ | xA ⇒ couple exadecimal bool x9 true
+ | xB ⇒ couple exadecimal bool xA true
+ | xC ⇒ couple exadecimal bool xB true
+ | xD ⇒ couple exadecimal bool xC true
+ | xE ⇒ couple exadecimal bool xD true
+ | xF ⇒ couple exadecimal bool xE true ]
+ | xF ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x0 true
+ | x1 ⇒ couple exadecimal bool x1 true
+ | x2 ⇒ couple exadecimal bool x2 true
+ | x3 ⇒ couple exadecimal bool x3 true
+ | x4 ⇒ couple exadecimal bool x4 true
+ | x5 ⇒ couple exadecimal bool x5 true
+ | x6 ⇒ couple exadecimal bool x6 true
+ | x7 ⇒ couple exadecimal bool x7 true
+ | x8 ⇒ couple exadecimal bool x8 true
+ | x9 ⇒ couple exadecimal bool x9 true
+ | xA ⇒ couple exadecimal bool xA true
+ | xB ⇒ couple exadecimal bool xB true
+ | xC ⇒ couple exadecimal bool xC true
+ | xD ⇒ couple exadecimal bool xD true
+ | xE ⇒ couple exadecimal bool xE true
+ | xF ⇒ couple exadecimal bool xF true ]
+ ]
+ | false ⇒
+ match b1 with
+ [ x0 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x0 false
+ | x1 ⇒ couple exadecimal bool x1 false
+ | x2 ⇒ couple exadecimal bool x2 false
+ | x3 ⇒ couple exadecimal bool x3 false
+ | x4 ⇒ couple exadecimal bool x4 false
+ | x5 ⇒ couple exadecimal bool x5 false
+ | x6 ⇒ couple exadecimal bool x6 false
+ | x7 ⇒ couple exadecimal bool x7 false
+ | x8 ⇒ couple exadecimal bool x8 false
+ | x9 ⇒ couple exadecimal bool x9 false
+ | xA ⇒ couple exadecimal bool xA false
+ | xB ⇒ couple exadecimal bool xB false
+ | xC ⇒ couple exadecimal bool xC false
+ | xD ⇒ couple exadecimal bool xD false
+ | xE ⇒ couple exadecimal bool xE false
+ | xF ⇒ couple exadecimal bool xF false ]
+ | x1 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x1 false
+ | x1 ⇒ couple exadecimal bool x2 false
+ | x2 ⇒ couple exadecimal bool x3 false
+ | x3 ⇒ couple exadecimal bool x4 false
+ | x4 ⇒ couple exadecimal bool x5 false
+ | x5 ⇒ couple exadecimal bool x6 false
+ | x6 ⇒ couple exadecimal bool x7 false
+ | x7 ⇒ couple exadecimal bool x8 false
+ | x8 ⇒ couple exadecimal bool x9 false
+ | x9 ⇒ couple exadecimal bool xA false
+ | xA ⇒ couple exadecimal bool xB false
+ | xB ⇒ couple exadecimal bool xC false
+ | xC ⇒ couple exadecimal bool xD false
+ | xD ⇒ couple exadecimal bool xE false
+ | xE ⇒ couple exadecimal bool xF false
+ | xF ⇒ couple exadecimal bool x0 true ]
+ | x2 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x2 false
+ | x1 ⇒ couple exadecimal bool x3 false
+ | x2 ⇒ couple exadecimal bool x4 false
+ | x3 ⇒ couple exadecimal bool x5 false
+ | x4 ⇒ couple exadecimal bool x6 false
+ | x5 ⇒ couple exadecimal bool x7 false
+ | x6 ⇒ couple exadecimal bool x8 false
+ | x7 ⇒ couple exadecimal bool x9 false
+ | x8 ⇒ couple exadecimal bool xA false
+ | x9 ⇒ couple exadecimal bool xB false
+ | xA ⇒ couple exadecimal bool xC false
+ | xB ⇒ couple exadecimal bool xD false
+ | xC ⇒ couple exadecimal bool xE false
+ | xD ⇒ couple exadecimal bool xF false
+ | xE ⇒ couple exadecimal bool x0 true
+ | xF ⇒ couple exadecimal bool x1 true ]
+ | x3 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x3 false
+ | x1 ⇒ couple exadecimal bool x4 false
+ | x2 ⇒ couple exadecimal bool x5 false
+ | x3 ⇒ couple exadecimal bool x6 false
+ | x4 ⇒ couple exadecimal bool x7 false
+ | x5 ⇒ couple exadecimal bool x8 false
+ | x6 ⇒ couple exadecimal bool x9 false
+ | x7 ⇒ couple exadecimal bool xA false
+ | x8 ⇒ couple exadecimal bool xB false
+ | x9 ⇒ couple exadecimal bool xC false
+ | xA ⇒ couple exadecimal bool xD false
+ | xB ⇒ couple exadecimal bool xE false
+ | xC ⇒ couple exadecimal bool xF false
+ | xD ⇒ couple exadecimal bool x0 true
+ | xE ⇒ couple exadecimal bool x1 true
+ | xF ⇒ couple exadecimal bool x2 true ]
+ | x4 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x4 false
+ | x1 ⇒ couple exadecimal bool x5 false
+ | x2 ⇒ couple exadecimal bool x6 false
+ | x3 ⇒ couple exadecimal bool x7 false
+ | x4 ⇒ couple exadecimal bool x8 false
+ | x5 ⇒ couple exadecimal bool x9 false
+ | x6 ⇒ couple exadecimal bool xA false
+ | x7 ⇒ couple exadecimal bool xB false
+ | x8 ⇒ couple exadecimal bool xC false
+ | x9 ⇒ couple exadecimal bool xD false
+ | xA ⇒ couple exadecimal bool xE false
+ | xB ⇒ couple exadecimal bool xF false
+ | xC ⇒ couple exadecimal bool x0 true
+ | xD ⇒ couple exadecimal bool x1 true
+ | xE ⇒ couple exadecimal bool x2 true
+ | xF ⇒ couple exadecimal bool x3 true ]
+ | x5 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x5 false
+ | x1 ⇒ couple exadecimal bool x6 false
+ | x2 ⇒ couple exadecimal bool x7 false
+ | x3 ⇒ couple exadecimal bool x8 false
+ | x4 ⇒ couple exadecimal bool x9 false
+ | x5 ⇒ couple exadecimal bool xA false
+ | x6 ⇒ couple exadecimal bool xB false
+ | x7 ⇒ couple exadecimal bool xC false
+ | x8 ⇒ couple exadecimal bool xD false
+ | x9 ⇒ couple exadecimal bool xE false
+ | xA ⇒ couple exadecimal bool xF false
+ | xB ⇒ couple exadecimal bool x0 true
+ | xC ⇒ couple exadecimal bool x1 true
+ | xD ⇒ couple exadecimal bool x2 true
+ | xE ⇒ couple exadecimal bool x3 true
+ | xF ⇒ couple exadecimal bool x4 true ]
+ | x6 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x6 false
+ | x1 ⇒ couple exadecimal bool x7 false
+ | x2 ⇒ couple exadecimal bool x8 false
+ | x3 ⇒ couple exadecimal bool x9 false
+ | x4 ⇒ couple exadecimal bool xA false
+ | x5 ⇒ couple exadecimal bool xB false
+ | x6 ⇒ couple exadecimal bool xC false
+ | x7 ⇒ couple exadecimal bool xD false
+ | x8 ⇒ couple exadecimal bool xE false
+ | x9 ⇒ couple exadecimal bool xF false
+ | xA ⇒ couple exadecimal bool x0 true
+ | xB ⇒ couple exadecimal bool x1 true
+ | xC ⇒ couple exadecimal bool x2 true
+ | xD ⇒ couple exadecimal bool x3 true
+ | xE ⇒ couple exadecimal bool x4 true
+ | xF ⇒ couple exadecimal bool x5 true ]
+ | x7 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x7 false
+ | x1 ⇒ couple exadecimal bool x8 false
+ | x2 ⇒ couple exadecimal bool x9 false
+ | x3 ⇒ couple exadecimal bool xA false
+ | x4 ⇒ couple exadecimal bool xB false
+ | x5 ⇒ couple exadecimal bool xC false
+ | x6 ⇒ couple exadecimal bool xD false
+ | x7 ⇒ couple exadecimal bool xE false
+ | x8 ⇒ couple exadecimal bool xF false
+ | x9 ⇒ couple exadecimal bool x0 true
+ | xA ⇒ couple exadecimal bool x1 true
+ | xB ⇒ couple exadecimal bool x2 true
+ | xC ⇒ couple exadecimal bool x3 true
+ | xD ⇒ couple exadecimal bool x4 true
+ | xE ⇒ couple exadecimal bool x5 true
+ | xF ⇒ couple exadecimal bool x6 true ]
+ | x8 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x8 false
+ | x1 ⇒ couple exadecimal bool x9 false
+ | x2 ⇒ couple exadecimal bool xA false
+ | x3 ⇒ couple exadecimal bool xB false
+ | x4 ⇒ couple exadecimal bool xC false
+ | x5 ⇒ couple exadecimal bool xD false
+ | x6 ⇒ couple exadecimal bool xE false
+ | x7 ⇒ couple exadecimal bool xF false
+ | x8 ⇒ couple exadecimal bool x0 true
+ | x9 ⇒ couple exadecimal bool x1 true
+ | xA ⇒ couple exadecimal bool x2 true
+ | xB ⇒ couple exadecimal bool x3 true
+ | xC ⇒ couple exadecimal bool x4 true
+ | xD ⇒ couple exadecimal bool x5 true
+ | xE ⇒ couple exadecimal bool x6 true
+ | xF ⇒ couple exadecimal bool x7 true ]
+ | x9 ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool x9 false
+ | x1 ⇒ couple exadecimal bool xA false
+ | x2 ⇒ couple exadecimal bool xB false
+ | x3 ⇒ couple exadecimal bool xC false
+ | x4 ⇒ couple exadecimal bool xD false
+ | x5 ⇒ couple exadecimal bool xE false
+ | x6 ⇒ couple exadecimal bool xF false
+ | x7 ⇒ couple exadecimal bool x0 true
+ | x8 ⇒ couple exadecimal bool x1 true
+ | x9 ⇒ couple exadecimal bool x2 true
+ | xA ⇒ couple exadecimal bool x3 true
+ | xB ⇒ couple exadecimal bool x4 true
+ | xC ⇒ couple exadecimal bool x5 true
+ | xD ⇒ couple exadecimal bool x6 true
+ | xE ⇒ couple exadecimal bool x7 true
+ | xF ⇒ couple exadecimal bool x8 true ]
+ | xA ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xA false
+ | x1 ⇒ couple exadecimal bool xB false
+ | x2 ⇒ couple exadecimal bool xC false
+ | x3 ⇒ couple exadecimal bool xD false
+ | x4 ⇒ couple exadecimal bool xE false
+ | x5 ⇒ couple exadecimal bool xF false
+ | x6 ⇒ couple exadecimal bool x0 true
+ | x7 ⇒ couple exadecimal bool x1 true
+ | x8 ⇒ couple exadecimal bool x2 true
+ | x9 ⇒ couple exadecimal bool x3 true
+ | xA ⇒ couple exadecimal bool x4 true
+ | xB ⇒ couple exadecimal bool x5 true
+ | xC ⇒ couple exadecimal bool x6 true
+ | xD ⇒ couple exadecimal bool x7 true
+ | xE ⇒ couple exadecimal bool x8 true
+ | xF ⇒ couple exadecimal bool x9 true ]
+ | xB ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xB false
+ | x1 ⇒ couple exadecimal bool xC false
+ | x2 ⇒ couple exadecimal bool xD false
+ | x3 ⇒ couple exadecimal bool xE false
+ | x4 ⇒ couple exadecimal bool xF false
+ | x5 ⇒ couple exadecimal bool x0 true
+ | x6 ⇒ couple exadecimal bool x1 true
+ | x7 ⇒ couple exadecimal bool x2 true
+ | x8 ⇒ couple exadecimal bool x3 true
+ | x9 ⇒ couple exadecimal bool x4 true
+ | xA ⇒ couple exadecimal bool x5 true
+ | xB ⇒ couple exadecimal bool x6 true
+ | xC ⇒ couple exadecimal bool x7 true
+ | xD ⇒ couple exadecimal bool x8 true
+ | xE ⇒ couple exadecimal bool x9 true
+ | xF ⇒ couple exadecimal bool xA true ]
+ | xC ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xC false
+ | x1 ⇒ couple exadecimal bool xD false
+ | x2 ⇒ couple exadecimal bool xE false
+ | x3 ⇒ couple exadecimal bool xF false
+ | x4 ⇒ couple exadecimal bool x0 true
+ | x5 ⇒ couple exadecimal bool x1 true
+ | x6 ⇒ couple exadecimal bool x2 true
+ | x7 ⇒ couple exadecimal bool x3 true
+ | x8 ⇒ couple exadecimal bool x4 true
+ | x9 ⇒ couple exadecimal bool x5 true
+ | xA ⇒ couple exadecimal bool x6 true
+ | xB ⇒ couple exadecimal bool x7 true
+ | xC ⇒ couple exadecimal bool x8 true
+ | xD ⇒ couple exadecimal bool x9 true
+ | xE ⇒ couple exadecimal bool xA true
+ | xF ⇒ couple exadecimal bool xB true ]
+ | xD ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xD false
+ | x1 ⇒ couple exadecimal bool xE false
+ | x2 ⇒ couple exadecimal bool xF false
+ | x3 ⇒ couple exadecimal bool x0 true
+ | x4 ⇒ couple exadecimal bool x1 true
+ | x5 ⇒ couple exadecimal bool x2 true
+ | x6 ⇒ couple exadecimal bool x3 true
+ | x7 ⇒ couple exadecimal bool x4 true
+ | x8 ⇒ couple exadecimal bool x5 true
+ | x9 ⇒ couple exadecimal bool x6 true
+ | xA ⇒ couple exadecimal bool x7 true
+ | xB ⇒ couple exadecimal bool x8 true
+ | xC ⇒ couple exadecimal bool x9 true
+ | xD ⇒ couple exadecimal bool xA true
+ | xE ⇒ couple exadecimal bool xB true
+ | xF ⇒ couple exadecimal bool xC true ]
+ | xE ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xE false
+ | x1 ⇒ couple exadecimal bool xF false
+ | x2 ⇒ couple exadecimal bool x0 true
+ | x3 ⇒ couple exadecimal bool x1 true
+ | x4 ⇒ couple exadecimal bool x2 true
+ | x5 ⇒ couple exadecimal bool x3 true
+ | x6 ⇒ couple exadecimal bool x4 true
+ | x7 ⇒ couple exadecimal bool x5 true
+ | x8 ⇒ couple exadecimal bool x6 true
+ | x9 ⇒ couple exadecimal bool x7 true
+ | xA ⇒ couple exadecimal bool x8 true
+ | xB ⇒ couple exadecimal bool x9 true
+ | xC ⇒ couple exadecimal bool xA true
+ | xD ⇒ couple exadecimal bool xB true
+ | xE ⇒ couple exadecimal bool xC true
+ | xF ⇒ couple exadecimal bool xD true ]
+ | xF ⇒
+ match b2 with
+ [ x0 ⇒ couple exadecimal bool xF false
+ | x1 ⇒ couple exadecimal bool x0 true
+ | x2 ⇒ couple exadecimal bool x1 true
+ | x3 ⇒ couple exadecimal bool x2 true
+ | x4 ⇒ couple exadecimal bool x3 true
+ | x5 ⇒ couple exadecimal bool x4 true
+ | x6 ⇒ couple exadecimal bool x5 true
+ | x7 ⇒ couple exadecimal bool x6 true
+ | x8 ⇒ couple exadecimal bool x7 true
+ | x9 ⇒ couple exadecimal bool x8 true
+ | xA ⇒ couple exadecimal bool x9 true
+ | xB ⇒ couple exadecimal bool xA true
+ | xC ⇒ couple exadecimal bool xB true
+ | xD ⇒ couple exadecimal bool xC true
+ | xE ⇒ couple exadecimal bool xD true
+ | xF ⇒ couple exadecimal bool xE true ]
+ ]
+ ]
+.
+
+definition plusbyte ≝
+ λb1,b2,c.
+ match plusex (bl b1) (bl b2) c with
+ [ couple l c' ⇒
+ match plusex (bh b1) (bh b2) c' with
+ [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]].
+
+alias num (instance 0) = "natural number".
+definition nat_of_exadecimal ≝
+ λb.
+ match b with
+ [ x0 ⇒ 0
+ | x1 ⇒ 1
+ | x2 ⇒ 2
+ | x3 ⇒ 3
+ | x4 ⇒ 4
+ | x5 ⇒ 5
+ | x6 ⇒ 6
+ | x7 ⇒ 7
+ | x8 ⇒ 8
+ | x9 ⇒ 9
+ | xA ⇒ 10
+ | xB ⇒ 11
+ | xC ⇒ 12
+ | xD ⇒ 13
+ | xE ⇒ 14
+ | xF ⇒ 15
+ ].
+
+coercion cic:/matita/assembly/nat_of_exadecimal.con.
+
+definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b).
+
+coercion cic:/matita/assembly/nat_of_byte.con.
+
+let rec exadecimal_of_nat b ≝
+ match b with [ O ⇒ x0 | S b ⇒
+ match b with [ O ⇒ x1 | S b ⇒
+ match b with [ O ⇒ x2 | S b ⇒
+ match b with [ O ⇒ x3 | S b ⇒
+ match b with [ O ⇒ x4 | S b ⇒
+ match b with [ O ⇒ x5 | S b ⇒
+ match b with [ O ⇒ x6 | S b ⇒
+ match b with [ O ⇒ x7 | S b ⇒
+ match b with [ O ⇒ x8 | S b ⇒
+ match b with [ O ⇒ x9 | S b ⇒
+ match b with [ O ⇒ xA | S b ⇒
+ match b with [ O ⇒ xB | S b ⇒
+ match b with [ O ⇒ xC | S b ⇒
+ match b with [ O ⇒ xD | S b ⇒
+ match b with [ O ⇒ xE | S b ⇒
+ match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]].
+
+definition byte_of_nat ≝
+ λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
+
+lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
+ intros;
+ elim b;
+ elim e;
+ elim e1;
+ reflexivity.
+qed.
+
+axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n.
+(* intros;
+ unfold byte_of_nat;
+*)
+
+definition nat_of_bool ≝
+ λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
+
+(* Way too slow. Handles 2^32 goals!
+lemma plusbyte_ok:
+ ∀b1,b2,c.
+ match plusbyte b1 b2 c with
+ [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c'
+ ].
+ intros;
+ elim c;
+ elim b1;
+ elim e;
+ elim e1;
+ elim b2;
+ elim e2;
+ elim e3;
+ reflexivity.
+qed.
+*)
(*
lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
| S n' ⇒ execute (tick s) n'
].
-lemma foo: ∀s,n. execute s (S n) = execute (tick s) n.
- intros; reflexivity.
+lemma breakpoint:
+ ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2.
+ intros;
+ generalize in match s; clear s;
+ elim n1;
+ [ reflexivity
+ | simplify;
+ apply H;
+ ]
qed.
notation "hvbox(# break a)"
#BRA; mk_byte xF x2; (* goto l1 *)
#LDAd; mk_byte x2 x0].(* (l2) *)
-definition mult_status ≝
- λx,y.
- mk_status (mk_byte x0 x0) 0 0 false false
- (λa:addr.
+definition mult_memory ≝
+ λx,y.λa:addr.
match leb a 29 with
[ true ⇒ nth ? mult_source (mk_byte x0 x0) a
| false ⇒
[ true ⇒ x
| false ⇒ y
]
- ]) 0.
+ ].
+
+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.
].
qed.
+axiom byte_elim:
+ ∀P:byte → Prop.
+ (P (mk_byte x0 x0)) →
+ (∀i:nat. i < 255 → P (byte_of_nat i) → P (byte_of_nat (S i))) →
+ ∀b:byte. P b.
+(* Tedious proof, easy to automate but not trivial
+ intros;
+ elim b;
+ elim e;
+ [ elim e1;
+ [ assumption
+ | apply (H1 0);
+ [ apply lt_O_S
+ | assumption
+ ]
+ | apply (H1 1);
+ [ alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
+ apply lt_S_S;
+ apply lt_O_S
+ | apply (H1 0);
+*)
+
+theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
+ unfold lt;
+ intros;
+ autobatch.
+qed.
+
+axiom daemon: False.
+
+axiom loop_invariant:
+ ∀x,y:byte.∀j:nat. j ≤ y →
+ let s ≝ execute (mult_status x y) (5 + 23*j) in
+ pc s = 4 ∧
+ mem s 30 = x ∧
+ mem s 31 = byte_of_nat (y - j) ∧
+ mem s 32 = byte_of_nat (x * j).
(*
-lemma test_x_y:
+ intros 2;
+ apply (byte_elim ? ? ? y);
+ [ intros;
+ simplify in H;
+ cut (j=O);
+ [ unfold s; clear s;
+ rewrite > Hcut;
+ reflexivity
+ | (* easy *) elim daemon
+ ]
+ | intros;
+ unfold s;
+ cut (j < S i ∨ j = S i);
+ [ elim Hcut;
+ [ rewrite > nat_of_byte_byte_of_nat in H1;
+ [2: apply (lt_trans ? 255);
+ [ assumption
+ | unfold lt;
+ (* ???????? *)
+ ]
+ | generalize in match (H1 j); clear H1;
+ intros;
+ unfold lt in H3;
+ cut (j ≤ i);
+ [ generalize in match (H4 Hcut1); clear H4; clear Hcut1; intro;
+ apply H1
+ | letin xxx ≝ H3;
+ inversion xxx;
+ [ intro;
+ rewrite > (injective_S ? ? H1);
+ autobatch
+ | intros;
+ (* facile *) elim daemon
+ ]
+ ]
+ ]
+ |
+ ]
+ | (* easy *)
+ ]
+ ].
+qed.
+*)
+
+axiom loop_invariant':
+ ∀x,y:byte.∀j:nat. j ≤ y →
+ let s ≝ execute (mult_status x y) (5 + 23*j) in
+ s =
+ mk_status (byte_of_nat (x * j)) 4 0 true false
+ (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
+ (byte_of_nat (x * j)))
+ 0.
+
+theorem test_x_y:
∀x,y.
let i ≝ 14 + 23 * nat_of_byte y in
let s ≝ execute (mult_status x y) i in
pc s = 20 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y).
intros;
-
+ generalize in match (loop_invariant' x y y (le_n y)); intro;
+ generalize in match (breakpoint (mult_status x y) (5 + 23*y) 9); intro;
+ cut (5 + 23*y +9 = 14 + 23* y);
+ [2: autobatch paramodulation
+ | rewrite > Hcut in H1;
+ change in H1:(? ? % ?) with s;
+ letin s0 ≝ (execute (mult_status x y) (S (S (S (S (S O))))+S 22*y));
+ generalize in match H; intro K; clear H;
+ change in K with
+ (s0 =
+ mk_status (byte_of_nat (x*y)) 4 0 true false
+ (update
+ (update
+ (update (mult_memory x y) 30 x)
+ 31 (byte_of_nat (y-y)))
+ 32 (byte_of_nat (x*y))) O);
+ clear Hcut;
+ generalize in match H1; intro K1; clear H1;
+ change in K1 with (s = execute s0 9);
+ rewrite > K in K1;
+ clear K; clear s0; clearbody s; clear i;
+ rewrite < minus_n_n in K1;
+ split;
+ rewrite > K1;
+ reflexivity
+ ]
qed.
-*)
(*
letin w ≝ 22;
projects / helm.git / commitdiff