From 016036e00c941eeeea7a3301d11c363dd888248e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Jul 2007 14:54:04 +0000 Subject: [PATCH] 1. loop invariant stated, but not proved 2. final theorem stated and proved --- .../matita/library/assembly/assembly.ma | 1793 +++++++++-------- 1 file changed, 962 insertions(+), 831 deletions(-) diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/assembly.ma index 9966482e3..c7ecd595b 100644 --- a/helm/software/matita/library/assembly/assembly.ma +++ b/helm/software/matita/library/assembly/assembly.ma @@ -17,826 +17,23 @@ 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. - -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 = @@ -1119,11 +316,822 @@ interpretation "natural number" 'x256 = (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) +(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) +(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) +(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) -)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). + +inductive exadecimal : Type ≝ + x0: exadecimal + | x1: exadecimal + | x2: exadecimal + | x3: exadecimal + | x4: exadecimal + | x5: exadecimal + | x6: exadecimal + | x7: exadecimal + | x8: exadecimal + | x9: exadecimal + | xA: exadecimal + | xB: exadecimal + | xC: exadecimal + | xD: exadecimal + | xE: exadecimal + | xF: exadecimal. + +record byte : Type ≝ { + bh: exadecimal; + bl: exadecimal +}. + +definition eqex ≝ + λb1,b2. + match b1 with + [ x0 ⇒ + match b2 with + [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x1 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x2 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x3 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x4 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x5 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x6 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x7 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x8 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | x9 ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xA ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xB ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xC ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ] + | xD ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ false ] + | xE ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ false ] + | xF ⇒ + match b2 with + [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false + | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false + | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false + | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]]. + + +definition eqbyte ≝ + λb,b'. eqex (bh b) (bh b') ∧ eqex (bl b) (bl b'). + +inductive cartesian_product (A,B: Type) : Type ≝ + couple: ∀a:A.∀b:B. cartesian_product A B. + +definition plusex ≝ + λb1,b2,c. + match c with + [ true ⇒ + match b1 with + [ x0 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x1 false + | x1 ⇒ couple exadecimal bool x2 false + | x2 ⇒ couple exadecimal bool x3 false + | x3 ⇒ couple exadecimal bool x4 false + | x4 ⇒ couple exadecimal bool x5 false + | x5 ⇒ couple exadecimal bool x6 false + | x6 ⇒ couple exadecimal bool x7 false + | x7 ⇒ couple exadecimal bool x8 false + | x8 ⇒ couple exadecimal bool x9 false + | x9 ⇒ couple exadecimal bool xA false + | xA ⇒ couple exadecimal bool xB false + | xB ⇒ couple exadecimal bool xC false + | xC ⇒ couple exadecimal bool xD false + | xD ⇒ couple exadecimal bool xE false + | xE ⇒ couple exadecimal bool xF false + | xF ⇒ couple exadecimal bool x0 true ] + | x1 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x2 false + | x1 ⇒ couple exadecimal bool x3 false + | x2 ⇒ couple exadecimal bool x4 false + | x3 ⇒ couple exadecimal bool x5 false + | x4 ⇒ couple exadecimal bool x6 false + | x5 ⇒ couple exadecimal bool x7 false + | x6 ⇒ couple exadecimal bool x8 false + | x7 ⇒ couple exadecimal bool x9 false + | x8 ⇒ couple exadecimal bool xA false + | x9 ⇒ couple exadecimal bool xB false + | xA ⇒ couple exadecimal bool xC false + | xB ⇒ couple exadecimal bool xD false + | xC ⇒ couple exadecimal bool xE false + | xD ⇒ couple exadecimal bool xF false + | xE ⇒ couple exadecimal bool x0 true + | xF ⇒ couple exadecimal bool x1 true ] + | x2 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x3 false + | x1 ⇒ couple exadecimal bool x4 false + | x2 ⇒ couple exadecimal bool x5 false + | x3 ⇒ couple exadecimal bool x6 false + | x4 ⇒ couple exadecimal bool x7 false + | x5 ⇒ couple exadecimal bool x8 false + | x6 ⇒ couple exadecimal bool x9 false + | x7 ⇒ couple exadecimal bool xA false + | x8 ⇒ couple exadecimal bool xB false + | x9 ⇒ couple exadecimal bool xC false + | xA ⇒ couple exadecimal bool xD false + | xB ⇒ couple exadecimal bool xE false + | xC ⇒ couple exadecimal bool xF false + | xD ⇒ couple exadecimal bool x0 true + | xE ⇒ couple exadecimal bool x1 true + | xF ⇒ couple exadecimal bool x2 true ] + | x3 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x4 false + | x1 ⇒ couple exadecimal bool x5 false + | x2 ⇒ couple exadecimal bool x6 false + | x3 ⇒ couple exadecimal bool x7 false + | x4 ⇒ couple exadecimal bool x8 false + | x5 ⇒ couple exadecimal bool x9 false + | x6 ⇒ couple exadecimal bool xA false + | x7 ⇒ couple exadecimal bool xB false + | x8 ⇒ couple exadecimal bool xC false + | x9 ⇒ couple exadecimal bool xD false + | xA ⇒ couple exadecimal bool xE false + | xB ⇒ couple exadecimal bool xF false + | xC ⇒ couple exadecimal bool x0 true + | xD ⇒ couple exadecimal bool x1 true + | xE ⇒ couple exadecimal bool x2 true + | xF ⇒ couple exadecimal bool x3 true ] + | x4 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x5 false + | x1 ⇒ couple exadecimal bool x6 false + | x2 ⇒ couple exadecimal bool x7 false + | x3 ⇒ couple exadecimal bool x8 false + | x4 ⇒ couple exadecimal bool x9 false + | x5 ⇒ couple exadecimal bool xA false + | x6 ⇒ couple exadecimal bool xB false + | x7 ⇒ couple exadecimal bool xC false + | x8 ⇒ couple exadecimal bool xD false + | x9 ⇒ couple exadecimal bool xE false + | xA ⇒ couple exadecimal bool xF false + | xB ⇒ couple exadecimal bool x0 true + | xC ⇒ couple exadecimal bool x1 true + | xD ⇒ couple exadecimal bool x2 true + | xE ⇒ couple exadecimal bool x3 true + | xF ⇒ couple exadecimal bool x4 true ] + | x5 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x6 false + | x1 ⇒ couple exadecimal bool x7 false + | x2 ⇒ couple exadecimal bool x8 false + | x3 ⇒ couple exadecimal bool x9 false + | x4 ⇒ couple exadecimal bool xA false + | x5 ⇒ couple exadecimal bool xB false + | x6 ⇒ couple exadecimal bool xC false + | x7 ⇒ couple exadecimal bool xD false + | x8 ⇒ couple exadecimal bool xE false + | x9 ⇒ couple exadecimal bool xF false + | xA ⇒ couple exadecimal bool x0 true + | xB ⇒ couple exadecimal bool x1 true + | xC ⇒ couple exadecimal bool x2 true + | xD ⇒ couple exadecimal bool x3 true + | xE ⇒ couple exadecimal bool x4 true + | xF ⇒ couple exadecimal bool x5 true ] + | x6 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x7 false + | x1 ⇒ couple exadecimal bool x8 false + | x2 ⇒ couple exadecimal bool x9 false + | x3 ⇒ couple exadecimal bool xA false + | x4 ⇒ couple exadecimal bool xB false + | x5 ⇒ couple exadecimal bool xC false + | x6 ⇒ couple exadecimal bool xD false + | x7 ⇒ couple exadecimal bool xE false + | x8 ⇒ couple exadecimal bool xF false + | x9 ⇒ couple exadecimal bool x0 true + | xA ⇒ couple exadecimal bool x1 true + | xB ⇒ couple exadecimal bool x2 true + | xC ⇒ couple exadecimal bool x3 true + | xD ⇒ couple exadecimal bool x4 true + | xE ⇒ couple exadecimal bool x5 true + | xF ⇒ couple exadecimal bool x6 true ] + | x7 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x8 false + | x1 ⇒ couple exadecimal bool x9 false + | x2 ⇒ couple exadecimal bool xA false + | x3 ⇒ couple exadecimal bool xB false + | x4 ⇒ couple exadecimal bool xC false + | x5 ⇒ couple exadecimal bool xD false + | x6 ⇒ couple exadecimal bool xE false + | x7 ⇒ couple exadecimal bool xF false + | x8 ⇒ couple exadecimal bool x0 true + | x9 ⇒ couple exadecimal bool x1 true + | xA ⇒ couple exadecimal bool x2 true + | xB ⇒ couple exadecimal bool x3 true + | xC ⇒ couple exadecimal bool x4 true + | xD ⇒ couple exadecimal bool x5 true + | xE ⇒ couple exadecimal bool x6 true + | xF ⇒ couple exadecimal bool x7 true ] + | x8 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x9 false + | x1 ⇒ couple exadecimal bool xA false + | x2 ⇒ couple exadecimal bool xB false + | x3 ⇒ couple exadecimal bool xC false + | x4 ⇒ couple exadecimal bool xD false + | x5 ⇒ couple exadecimal bool xE false + | x6 ⇒ couple exadecimal bool xF false + | x7 ⇒ couple exadecimal bool x0 true + | x8 ⇒ couple exadecimal bool x1 true + | x9 ⇒ couple exadecimal bool x2 true + | xA ⇒ couple exadecimal bool x3 true + | xB ⇒ couple exadecimal bool x4 true + | xC ⇒ couple exadecimal bool x5 true + | xD ⇒ couple exadecimal bool x6 true + | xE ⇒ couple exadecimal bool x7 true + | xF ⇒ couple exadecimal bool x8 true ] + | x9 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xA false + | x1 ⇒ couple exadecimal bool xB false + | x2 ⇒ couple exadecimal bool xC false + | x3 ⇒ couple exadecimal bool xD false + | x4 ⇒ couple exadecimal bool xE false + | x5 ⇒ couple exadecimal bool xF false + | x6 ⇒ couple exadecimal bool x0 true + | x7 ⇒ couple exadecimal bool x1 true + | x8 ⇒ couple exadecimal bool x2 true + | x9 ⇒ couple exadecimal bool x3 true + | xA ⇒ couple exadecimal bool x4 true + | xB ⇒ couple exadecimal bool x5 true + | xC ⇒ couple exadecimal bool x6 true + | xD ⇒ couple exadecimal bool x7 true + | xE ⇒ couple exadecimal bool x8 true + | xF ⇒ couple exadecimal bool x9 true ] + | xA ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xB false + | x1 ⇒ couple exadecimal bool xC false + | x2 ⇒ couple exadecimal bool xD false + | x3 ⇒ couple exadecimal bool xE false + | x4 ⇒ couple exadecimal bool xF false + | x5 ⇒ couple exadecimal bool x0 true + | x6 ⇒ couple exadecimal bool x1 true + | x7 ⇒ couple exadecimal bool x2 true + | x8 ⇒ couple exadecimal bool x3 true + | x9 ⇒ couple exadecimal bool x4 true + | xA ⇒ couple exadecimal bool x5 true + | xB ⇒ couple exadecimal bool x6 true + | xC ⇒ couple exadecimal bool x7 true + | xD ⇒ couple exadecimal bool x8 true + | xE ⇒ couple exadecimal bool x9 true + | xF ⇒ couple exadecimal bool xA true ] + | xB ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xC false + | x1 ⇒ couple exadecimal bool xD false + | x2 ⇒ couple exadecimal bool xE false + | x3 ⇒ couple exadecimal bool xF false + | x4 ⇒ couple exadecimal bool x0 true + | x5 ⇒ couple exadecimal bool x1 true + | x6 ⇒ couple exadecimal bool x2 true + | x7 ⇒ couple exadecimal bool x3 true + | x8 ⇒ couple exadecimal bool x4 true + | x9 ⇒ couple exadecimal bool x5 true + | xA ⇒ couple exadecimal bool x6 true + | xB ⇒ couple exadecimal bool x7 true + | xC ⇒ couple exadecimal bool x8 true + | xD ⇒ couple exadecimal bool x9 true + | xE ⇒ couple exadecimal bool xA true + | xF ⇒ couple exadecimal bool xB true ] + | xC ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xD false + | x1 ⇒ couple exadecimal bool xE false + | x2 ⇒ couple exadecimal bool xF false + | x3 ⇒ couple exadecimal bool x0 true + | x4 ⇒ couple exadecimal bool x1 true + | x5 ⇒ couple exadecimal bool x2 true + | x6 ⇒ couple exadecimal bool x3 true + | x7 ⇒ couple exadecimal bool x4 true + | x8 ⇒ couple exadecimal bool x5 true + | x9 ⇒ couple exadecimal bool x6 true + | xA ⇒ couple exadecimal bool x7 true + | xB ⇒ couple exadecimal bool x8 true + | xC ⇒ couple exadecimal bool x9 true + | xD ⇒ couple exadecimal bool xA true + | xE ⇒ couple exadecimal bool xB true + | xF ⇒ couple exadecimal bool xC true ] + | xD ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xE false + | x1 ⇒ couple exadecimal bool xF false + | x2 ⇒ couple exadecimal bool x0 true + | x3 ⇒ couple exadecimal bool x1 true + | x4 ⇒ couple exadecimal bool x2 true + | x5 ⇒ couple exadecimal bool x3 true + | x6 ⇒ couple exadecimal bool x4 true + | x7 ⇒ couple exadecimal bool x5 true + | x8 ⇒ couple exadecimal bool x6 true + | x9 ⇒ couple exadecimal bool x7 true + | xA ⇒ couple exadecimal bool x8 true + | xB ⇒ couple exadecimal bool x9 true + | xC ⇒ couple exadecimal bool xA true + | xD ⇒ couple exadecimal bool xB true + | xE ⇒ couple exadecimal bool xC true + | xF ⇒ couple exadecimal bool xD true ] + | xE ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xF false + | x1 ⇒ couple exadecimal bool x0 true + | x2 ⇒ couple exadecimal bool x1 true + | x3 ⇒ couple exadecimal bool x2 true + | x4 ⇒ couple exadecimal bool x3 true + | x5 ⇒ couple exadecimal bool x4 true + | x6 ⇒ couple exadecimal bool x5 true + | x7 ⇒ couple exadecimal bool x6 true + | x8 ⇒ couple exadecimal bool x7 true + | x9 ⇒ couple exadecimal bool x8 true + | xA ⇒ couple exadecimal bool x9 true + | xB ⇒ couple exadecimal bool xA true + | xC ⇒ couple exadecimal bool xB true + | xD ⇒ couple exadecimal bool xC true + | xE ⇒ couple exadecimal bool xD true + | xF ⇒ couple exadecimal bool xE true ] + | xF ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x0 true + | x1 ⇒ couple exadecimal bool x1 true + | x2 ⇒ couple exadecimal bool x2 true + | x3 ⇒ couple exadecimal bool x3 true + | x4 ⇒ couple exadecimal bool x4 true + | x5 ⇒ couple exadecimal bool x5 true + | x6 ⇒ couple exadecimal bool x6 true + | x7 ⇒ couple exadecimal bool x7 true + | x8 ⇒ couple exadecimal bool x8 true + | x9 ⇒ couple exadecimal bool x9 true + | xA ⇒ couple exadecimal bool xA true + | xB ⇒ couple exadecimal bool xB true + | xC ⇒ couple exadecimal bool xC true + | xD ⇒ couple exadecimal bool xD true + | xE ⇒ couple exadecimal bool xE true + | xF ⇒ couple exadecimal bool xF true ] + ] + | false ⇒ + match b1 with + [ x0 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x0 false + | x1 ⇒ couple exadecimal bool x1 false + | x2 ⇒ couple exadecimal bool x2 false + | x3 ⇒ couple exadecimal bool x3 false + | x4 ⇒ couple exadecimal bool x4 false + | x5 ⇒ couple exadecimal bool x5 false + | x6 ⇒ couple exadecimal bool x6 false + | x7 ⇒ couple exadecimal bool x7 false + | x8 ⇒ couple exadecimal bool x8 false + | x9 ⇒ couple exadecimal bool x9 false + | xA ⇒ couple exadecimal bool xA false + | xB ⇒ couple exadecimal bool xB false + | xC ⇒ couple exadecimal bool xC false + | xD ⇒ couple exadecimal bool xD false + | xE ⇒ couple exadecimal bool xE false + | xF ⇒ couple exadecimal bool xF false ] + | x1 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x1 false + | x1 ⇒ couple exadecimal bool x2 false + | x2 ⇒ couple exadecimal bool x3 false + | x3 ⇒ couple exadecimal bool x4 false + | x4 ⇒ couple exadecimal bool x5 false + | x5 ⇒ couple exadecimal bool x6 false + | x6 ⇒ couple exadecimal bool x7 false + | x7 ⇒ couple exadecimal bool x8 false + | x8 ⇒ couple exadecimal bool x9 false + | x9 ⇒ couple exadecimal bool xA false + | xA ⇒ couple exadecimal bool xB false + | xB ⇒ couple exadecimal bool xC false + | xC ⇒ couple exadecimal bool xD false + | xD ⇒ couple exadecimal bool xE false + | xE ⇒ couple exadecimal bool xF false + | xF ⇒ couple exadecimal bool x0 true ] + | x2 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x2 false + | x1 ⇒ couple exadecimal bool x3 false + | x2 ⇒ couple exadecimal bool x4 false + | x3 ⇒ couple exadecimal bool x5 false + | x4 ⇒ couple exadecimal bool x6 false + | x5 ⇒ couple exadecimal bool x7 false + | x6 ⇒ couple exadecimal bool x8 false + | x7 ⇒ couple exadecimal bool x9 false + | x8 ⇒ couple exadecimal bool xA false + | x9 ⇒ couple exadecimal bool xB false + | xA ⇒ couple exadecimal bool xC false + | xB ⇒ couple exadecimal bool xD false + | xC ⇒ couple exadecimal bool xE false + | xD ⇒ couple exadecimal bool xF false + | xE ⇒ couple exadecimal bool x0 true + | xF ⇒ couple exadecimal bool x1 true ] + | x3 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x3 false + | x1 ⇒ couple exadecimal bool x4 false + | x2 ⇒ couple exadecimal bool x5 false + | x3 ⇒ couple exadecimal bool x6 false + | x4 ⇒ couple exadecimal bool x7 false + | x5 ⇒ couple exadecimal bool x8 false + | x6 ⇒ couple exadecimal bool x9 false + | x7 ⇒ couple exadecimal bool xA false + | x8 ⇒ couple exadecimal bool xB false + | x9 ⇒ couple exadecimal bool xC false + | xA ⇒ couple exadecimal bool xD false + | xB ⇒ couple exadecimal bool xE false + | xC ⇒ couple exadecimal bool xF false + | xD ⇒ couple exadecimal bool x0 true + | xE ⇒ couple exadecimal bool x1 true + | xF ⇒ couple exadecimal bool x2 true ] + | x4 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x4 false + | x1 ⇒ couple exadecimal bool x5 false + | x2 ⇒ couple exadecimal bool x6 false + | x3 ⇒ couple exadecimal bool x7 false + | x4 ⇒ couple exadecimal bool x8 false + | x5 ⇒ couple exadecimal bool x9 false + | x6 ⇒ couple exadecimal bool xA false + | x7 ⇒ couple exadecimal bool xB false + | x8 ⇒ couple exadecimal bool xC false + | x9 ⇒ couple exadecimal bool xD false + | xA ⇒ couple exadecimal bool xE false + | xB ⇒ couple exadecimal bool xF false + | xC ⇒ couple exadecimal bool x0 true + | xD ⇒ couple exadecimal bool x1 true + | xE ⇒ couple exadecimal bool x2 true + | xF ⇒ couple exadecimal bool x3 true ] + | x5 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x5 false + | x1 ⇒ couple exadecimal bool x6 false + | x2 ⇒ couple exadecimal bool x7 false + | x3 ⇒ couple exadecimal bool x8 false + | x4 ⇒ couple exadecimal bool x9 false + | x5 ⇒ couple exadecimal bool xA false + | x6 ⇒ couple exadecimal bool xB false + | x7 ⇒ couple exadecimal bool xC false + | x8 ⇒ couple exadecimal bool xD false + | x9 ⇒ couple exadecimal bool xE false + | xA ⇒ couple exadecimal bool xF false + | xB ⇒ couple exadecimal bool x0 true + | xC ⇒ couple exadecimal bool x1 true + | xD ⇒ couple exadecimal bool x2 true + | xE ⇒ couple exadecimal bool x3 true + | xF ⇒ couple exadecimal bool x4 true ] + | x6 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x6 false + | x1 ⇒ couple exadecimal bool x7 false + | x2 ⇒ couple exadecimal bool x8 false + | x3 ⇒ couple exadecimal bool x9 false + | x4 ⇒ couple exadecimal bool xA false + | x5 ⇒ couple exadecimal bool xB false + | x6 ⇒ couple exadecimal bool xC false + | x7 ⇒ couple exadecimal bool xD false + | x8 ⇒ couple exadecimal bool xE false + | x9 ⇒ couple exadecimal bool xF false + | xA ⇒ couple exadecimal bool x0 true + | xB ⇒ couple exadecimal bool x1 true + | xC ⇒ couple exadecimal bool x2 true + | xD ⇒ couple exadecimal bool x3 true + | xE ⇒ couple exadecimal bool x4 true + | xF ⇒ couple exadecimal bool x5 true ] + | x7 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x7 false + | x1 ⇒ couple exadecimal bool x8 false + | x2 ⇒ couple exadecimal bool x9 false + | x3 ⇒ couple exadecimal bool xA false + | x4 ⇒ couple exadecimal bool xB false + | x5 ⇒ couple exadecimal bool xC false + | x6 ⇒ couple exadecimal bool xD false + | x7 ⇒ couple exadecimal bool xE false + | x8 ⇒ couple exadecimal bool xF false + | x9 ⇒ couple exadecimal bool x0 true + | xA ⇒ couple exadecimal bool x1 true + | xB ⇒ couple exadecimal bool x2 true + | xC ⇒ couple exadecimal bool x3 true + | xD ⇒ couple exadecimal bool x4 true + | xE ⇒ couple exadecimal bool x5 true + | xF ⇒ couple exadecimal bool x6 true ] + | x8 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x8 false + | x1 ⇒ couple exadecimal bool x9 false + | x2 ⇒ couple exadecimal bool xA false + | x3 ⇒ couple exadecimal bool xB false + | x4 ⇒ couple exadecimal bool xC false + | x5 ⇒ couple exadecimal bool xD false + | x6 ⇒ couple exadecimal bool xE false + | x7 ⇒ couple exadecimal bool xF false + | x8 ⇒ couple exadecimal bool x0 true + | x9 ⇒ couple exadecimal bool x1 true + | xA ⇒ couple exadecimal bool x2 true + | xB ⇒ couple exadecimal bool x3 true + | xC ⇒ couple exadecimal bool x4 true + | xD ⇒ couple exadecimal bool x5 true + | xE ⇒ couple exadecimal bool x6 true + | xF ⇒ couple exadecimal bool x7 true ] + | x9 ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool x9 false + | x1 ⇒ couple exadecimal bool xA false + | x2 ⇒ couple exadecimal bool xB false + | x3 ⇒ couple exadecimal bool xC false + | x4 ⇒ couple exadecimal bool xD false + | x5 ⇒ couple exadecimal bool xE false + | x6 ⇒ couple exadecimal bool xF false + | x7 ⇒ couple exadecimal bool x0 true + | x8 ⇒ couple exadecimal bool x1 true + | x9 ⇒ couple exadecimal bool x2 true + | xA ⇒ couple exadecimal bool x3 true + | xB ⇒ couple exadecimal bool x4 true + | xC ⇒ couple exadecimal bool x5 true + | xD ⇒ couple exadecimal bool x6 true + | xE ⇒ couple exadecimal bool x7 true + | xF ⇒ couple exadecimal bool x8 true ] + | xA ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xA false + | x1 ⇒ couple exadecimal bool xB false + | x2 ⇒ couple exadecimal bool xC false + | x3 ⇒ couple exadecimal bool xD false + | x4 ⇒ couple exadecimal bool xE false + | x5 ⇒ couple exadecimal bool xF false + | x6 ⇒ couple exadecimal bool x0 true + | x7 ⇒ couple exadecimal bool x1 true + | x8 ⇒ couple exadecimal bool x2 true + | x9 ⇒ couple exadecimal bool x3 true + | xA ⇒ couple exadecimal bool x4 true + | xB ⇒ couple exadecimal bool x5 true + | xC ⇒ couple exadecimal bool x6 true + | xD ⇒ couple exadecimal bool x7 true + | xE ⇒ couple exadecimal bool x8 true + | xF ⇒ couple exadecimal bool x9 true ] + | xB ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xB false + | x1 ⇒ couple exadecimal bool xC false + | x2 ⇒ couple exadecimal bool xD false + | x3 ⇒ couple exadecimal bool xE false + | x4 ⇒ couple exadecimal bool xF false + | x5 ⇒ couple exadecimal bool x0 true + | x6 ⇒ couple exadecimal bool x1 true + | x7 ⇒ couple exadecimal bool x2 true + | x8 ⇒ couple exadecimal bool x3 true + | x9 ⇒ couple exadecimal bool x4 true + | xA ⇒ couple exadecimal bool x5 true + | xB ⇒ couple exadecimal bool x6 true + | xC ⇒ couple exadecimal bool x7 true + | xD ⇒ couple exadecimal bool x8 true + | xE ⇒ couple exadecimal bool x9 true + | xF ⇒ couple exadecimal bool xA true ] + | xC ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xC false + | x1 ⇒ couple exadecimal bool xD false + | x2 ⇒ couple exadecimal bool xE false + | x3 ⇒ couple exadecimal bool xF false + | x4 ⇒ couple exadecimal bool x0 true + | x5 ⇒ couple exadecimal bool x1 true + | x6 ⇒ couple exadecimal bool x2 true + | x7 ⇒ couple exadecimal bool x3 true + | x8 ⇒ couple exadecimal bool x4 true + | x9 ⇒ couple exadecimal bool x5 true + | xA ⇒ couple exadecimal bool x6 true + | xB ⇒ couple exadecimal bool x7 true + | xC ⇒ couple exadecimal bool x8 true + | xD ⇒ couple exadecimal bool x9 true + | xE ⇒ couple exadecimal bool xA true + | xF ⇒ couple exadecimal bool xB true ] + | xD ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xD false + | x1 ⇒ couple exadecimal bool xE false + | x2 ⇒ couple exadecimal bool xF false + | x3 ⇒ couple exadecimal bool x0 true + | x4 ⇒ couple exadecimal bool x1 true + | x5 ⇒ couple exadecimal bool x2 true + | x6 ⇒ couple exadecimal bool x3 true + | x7 ⇒ couple exadecimal bool x4 true + | x8 ⇒ couple exadecimal bool x5 true + | x9 ⇒ couple exadecimal bool x6 true + | xA ⇒ couple exadecimal bool x7 true + | xB ⇒ couple exadecimal bool x8 true + | xC ⇒ couple exadecimal bool x9 true + | xD ⇒ couple exadecimal bool xA true + | xE ⇒ couple exadecimal bool xB true + | xF ⇒ couple exadecimal bool xC true ] + | xE ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xE false + | x1 ⇒ couple exadecimal bool xF false + | x2 ⇒ couple exadecimal bool x0 true + | x3 ⇒ couple exadecimal bool x1 true + | x4 ⇒ couple exadecimal bool x2 true + | x5 ⇒ couple exadecimal bool x3 true + | x6 ⇒ couple exadecimal bool x4 true + | x7 ⇒ couple exadecimal bool x5 true + | x8 ⇒ couple exadecimal bool x6 true + | x9 ⇒ couple exadecimal bool x7 true + | xA ⇒ couple exadecimal bool x8 true + | xB ⇒ couple exadecimal bool x9 true + | xC ⇒ couple exadecimal bool xA true + | xD ⇒ couple exadecimal bool xB true + | xE ⇒ couple exadecimal bool xC true + | xF ⇒ couple exadecimal bool xD true ] + | xF ⇒ + match b2 with + [ x0 ⇒ couple exadecimal bool xF false + | x1 ⇒ couple exadecimal bool x0 true + | x2 ⇒ couple exadecimal bool x1 true + | x3 ⇒ couple exadecimal bool x2 true + | x4 ⇒ couple exadecimal bool x3 true + | x5 ⇒ couple exadecimal bool x4 true + | x6 ⇒ couple exadecimal bool x5 true + | x7 ⇒ couple exadecimal bool x6 true + | x8 ⇒ couple exadecimal bool x7 true + | x9 ⇒ couple exadecimal bool x8 true + | xA ⇒ couple exadecimal bool x9 true + | xB ⇒ couple exadecimal bool xA true + | xC ⇒ couple exadecimal bool xB true + | xD ⇒ couple exadecimal bool xC true + | xE ⇒ couple exadecimal bool xD true + | xF ⇒ couple exadecimal bool xE true ] + ] + ] +. + +definition plusbyte ≝ + λb1,b2,c. + match plusex (bl b1) (bl b2) c with + [ couple l c' ⇒ + match plusex (bh b1) (bh b2) c' with + [ couple h c'' ⇒ couple ? ? (mk_byte h l) c'' ]]. + +alias num (instance 0) = "natural number". +definition nat_of_exadecimal ≝ + λb. + match b with + [ x0 ⇒ 0 + | x1 ⇒ 1 + | x2 ⇒ 2 + | x3 ⇒ 3 + | x4 ⇒ 4 + | x5 ⇒ 5 + | x6 ⇒ 6 + | x7 ⇒ 7 + | x8 ⇒ 8 + | x9 ⇒ 9 + | xA ⇒ 10 + | xB ⇒ 11 + | xC ⇒ 12 + | xD ⇒ 13 + | xE ⇒ 14 + | xF ⇒ 15 + ]. + +coercion cic:/matita/assembly/nat_of_exadecimal.con. + +definition nat_of_byte ≝ λb:byte. 16*(bh b) + (bl b). + +coercion cic:/matita/assembly/nat_of_byte.con. + +let rec exadecimal_of_nat b ≝ + match b with [ O ⇒ x0 | S b ⇒ + match b with [ O ⇒ x1 | S b ⇒ + match b with [ O ⇒ x2 | S b ⇒ + match b with [ O ⇒ x3 | S b ⇒ + match b with [ O ⇒ x4 | S b ⇒ + match b with [ O ⇒ x5 | S b ⇒ + match b with [ O ⇒ x6 | S b ⇒ + match b with [ O ⇒ x7 | S b ⇒ + match b with [ O ⇒ x8 | S b ⇒ + match b with [ O ⇒ x9 | S b ⇒ + match b with [ O ⇒ xA | S b ⇒ + match b with [ O ⇒ xB | S b ⇒ + match b with [ O ⇒ xC | S b ⇒ + match b with [ O ⇒ xD | S b ⇒ + match b with [ O ⇒ xE | S b ⇒ + match b with [ O ⇒ xF | S b ⇒ exadecimal_of_nat b ]]]]]]]]]]]]]]]]. + +definition byte_of_nat ≝ + λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n). + +lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b. + intros; + elim b; + elim e; + elim e1; + reflexivity. +qed. + +axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n. +(* intros; + unfold byte_of_nat; +*) + +definition nat_of_bool ≝ + λb. match b with [ true ⇒ 1 | false ⇒ 0 ]. + +(* Way too slow. Handles 2^32 goals! +lemma plusbyte_ok: + ∀b1,b2,c. + match plusbyte b1 b2 c with + [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' + ]. + intros; + elim c; + elim b1; + elim e; + elim e1; + elim b2; + elim e2; + elim e3; + reflexivity. +qed. +*) (* lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256. @@ -1328,8 +1336,15 @@ let rec execute s n on n ≝ | S n' ⇒ execute (tick s) n' ]. -lemma foo: ∀s,n. execute s (S n) = execute (tick s) n. - intros; reflexivity. +lemma breakpoint: + ∀s,n1,n2. execute s (n1 + n2) = execute (execute s n1) n2. + intros; + generalize in match s; clear s; + elim n1; + [ reflexivity + | simplify; + apply H; + ] qed. notation "hvbox(# break a)" @@ -1350,10 +1365,8 @@ definition mult_source : list byte ≝ #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 ⇒ @@ -1361,7 +1374,11 @@ definition mult_status ≝ [ 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. @@ -1437,16 +1454,130 @@ lemma test_x_2: ]. 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; -- 2.39.2