X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fassembly.ma;h=5a3398db00f5ddf6af7c8d4d8ef75eefd8e23baa;hb=cc3629bdd8e527c98c30ba3133269de2a72d703e;hp=6cdf4091569624430db6be1bac1ca849c622892d;hpb=105e895dd735c2f1ceed588026346e168908ce3a;p=helm.git diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/assembly.ma index 6cdf40915..5a3398db0 100644 --- a/helm/software/matita/library/assembly/assembly.ma +++ b/helm/software/matita/library/assembly/assembly.ma @@ -14,24 +14,1441 @@ set "baseuri" "cic:/matita/assembly/". -include "nat/times.ma". -include "nat/compare.ma". +include "nat/div_and_mod.ma". include "list/list.ma". -alias id "OO" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". -alias id "SS" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". +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/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/2) +(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) +(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))). + +notation "255" non associative with precedence 80 for @{ 'x255 }. +interpretation "natural number" 'x255 = +(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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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 "256" non associative with precedence 80 for @{ 'x256 }. +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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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/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) +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). + +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'' ]]. -let rec matita_nat_of_coq_nat n ≝ - match n with - [ OO ⇒ O - | SS y ⇒ S (matita_nat_of_coq_nat y) - ]. -coercion cic:/matita/assembly/matita_nat_of_coq_nat.con. 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. + intros; elim n; [ reflexivity | unfold byte_of_nat. +qed. +*) -definition byte ≝ nat. definition addr ≝ nat. +definition xpred ≝ + λb. + match b with + [ x0 ⇒ xF + | x1 ⇒ x0 + | x2 ⇒ x1 + | x3 ⇒ x2 + | x4 ⇒ x3 + | x5 ⇒ x4 + | x6 ⇒ x5 + | x7 ⇒ x6 + | x8 ⇒ x7 + | x9 ⇒ x8 + | xA ⇒ x9 + | xB ⇒ xA + | xC ⇒ xB + | xD ⇒ xC + | xE ⇒ xD + | xF ⇒ xE ]. + +definition bpred ≝ + λb. + match eqex (bl b) x0 with + [ true ⇒ mk_byte (xpred (bh b)) (xpred (bl b)) + | false ⇒ mk_byte (bh b) (xpred (bl b)) + ]. + +(* Way too slow and subsumed by previous theorem +lemma bpred_pred: + ∀b. + match eqbyte b (mk_byte x0 x0) with + [ true ⇒ nat_of_byte (bpred b) = mk_byte xF xF + | false ⇒ nat_of_byte (bpred b) = pred (nat_of_byte b)]. + intros; + elim b; + elim e; + elim e1; + reflexivity. +qed. +*) + +definition addr_of_byte : byte → addr ≝ λb. nat_of_byte b. + +coercion cic:/matita/assembly/addr_of_byte.con. + inductive opcode: Type ≝ ADDd: opcode (* 3 clock, 171 *) | BEQ: opcode (* 3, 55 *) @@ -41,28 +1458,25 @@ inductive opcode: Type ≝ | LDAd: opcode (* 3, 182 *) | STAd: opcode. (* 3, 183 *) -let rec cycles_of_opcode op ≝ +let rec cycles_of_opcode op : nat ≝ match op with - [ ADDd ⇒ matita_nat_of_coq_nat 3 - | BEQ ⇒ matita_nat_of_coq_nat 3 - | BRA ⇒ matita_nat_of_coq_nat 3 - | DECd ⇒ matita_nat_of_coq_nat 5 - | LDAi ⇒ matita_nat_of_coq_nat 2 - | LDAd ⇒ matita_nat_of_coq_nat 3 - | STAd ⇒ matita_nat_of_coq_nat 3 + [ ADDd ⇒ 3 + | BEQ ⇒ 3 + | BRA ⇒ 3 + | DECd ⇒ 5 + | LDAi ⇒ 2 + | LDAd ⇒ 3 + | STAd ⇒ 3 ]. -inductive cartesian_product (A,B: Type) : Type ≝ - couple: ∀a:A.∀b:B. cartesian_product A B. - definition opcodemap ≝ - [ couple ? ? ADDd 171; - couple ? ? BEQ 55; - couple ? ? BRA 48; - couple ? ? DECd 58; - couple ? ? LDAi 166; - couple ? ? LDAd 182; - couple ? ? STAd 183 ]. + [ couple ? ? ADDd (mk_byte xA xB); + couple ? ? BEQ (mk_byte x3 x7); + couple ? ? BRA (mk_byte x3 x0); + couple ? ? DECd (mk_byte x3 xA); + couple ? ? LDAi (mk_byte xA x6); + couple ? ? LDAd (mk_byte xB x6); + couple ? ? STAd (mk_byte xB x7) ]. definition opcode_of_byte ≝ λb. @@ -72,7 +1486,7 @@ definition opcode_of_byte ≝ | cons c tl ⇒ match c with [ couple op n ⇒ - match eqb (matita_nat_of_coq_nat n) b with + match eqbyte n b with [ true ⇒ op | false ⇒ aux tl ]]] @@ -97,46 +1511,17 @@ definition byte_of_opcode : opcode → byte ≝ λop. let rec aux l ≝ match l with - [ nil ⇒ matita_nat_of_coq_nat 0 + [ nil ⇒ mk_byte x0 x0 | cons c tl ⇒ match c with [ couple op' n ⇒ match opcodeeqb op op' with - [ true ⇒ matita_nat_of_coq_nat n + [ true ⇒ n | false ⇒ aux tl ]]] in aux opcodemap. -notation "hvbox(# break a)" - non associative with precedence 80 -for @{ 'byte_of_opcode $a }. -interpretation "byte_of_opcode" 'byte_of_opcode a = - (cic:/matita/assembly/byte_of_opcode.con a). - -definition byte_of_coq_nat : nat → byte ≝ matita_nat_of_coq_nat. - -notation "hvbox(@ break a)" - non associative with precedence 80 -for @{ 'matita_nat_of_coq_nat $a }. -interpretation "matita_nat_of_coq_nat" 'matita_nat_of_coq_nat a = - (cic:/matita/assembly/byte_of_coq_nat.con a). - -definition mult_source : list byte ≝ - [#LDAi; @0; - #STAd; @18; (* 18 = locazione $12 *) - #LDAd; @17; (* 17 = locazione $11 *) - #BEQ; @14; - #LDAd; @18; - #DECd; @17; - #ADDd; @16; (* 16 = locazione $10 *) - #STAd; @18; - #LDAd; @17; - #BRA; @246; (* 246 = -10 *) - #LDAd; @18]. - -definition mult_source' : list byte. - record status : Type ≝ { acc : byte; pc : addr; @@ -147,42 +1532,66 @@ record status : Type ≝ { clk : nat }. -definition mult_status : status ≝ - mk_status @0 @0 @0 false false (λa:addr. nth ? mult_source @0 a) 0. +definition update ≝ + λf: addr → byte.λa.λv.λx. + match eqb x a with + [ true ⇒ v + | false ⇒ f x ]. + +definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n). definition tick ≝ - λs:status. - (* fetch *) - let opc ≝ opcode_of_byte (mem s (pc s)) in - let op1 ≝ mem s (S (pc s)) in - let op2 ≝ mem s (S (S (pc s))) in + λs:status. match s with [ mk_status acc pc spc zf cf mem clk ⇒ + let opc ≝ opcode_of_byte (mem pc) in + let op1 ≝ mem (S pc) in let clk' ≝ cycles_of_opcode opc in - match eqb (S (clk s)) clk' with - [ false ⇒ - mk_status - (acc s) (pc s) (spc s) (zf s) (cf s) (mem s) (S (clk s)) - | true ⇒ + match eqb (S clk) clk' with + [ true ⇒ match opc with - [ ADDd ⇒ s + [ ADDd ⇒ + let res ≝ plusbyte acc (mem op1) false in (* verify carrier! *) + let acc' ≝ match res with [ couple acc' _ ⇒ acc' ] in + let c' ≝ match res with [ couple _ c' ⇒ c'] in + mk_status acc' (2 + pc) spc + (eqb O (nat_of_byte acc')) c' mem 0 (* verify carrier! *) | BEQ ⇒ mk_status - (acc s) - (match zf s with - [ true ⇒ op1 + pc s (* signed!!! *) - | false ⇒ 2 + pc s + acc + (match zf with + [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*) (* signed!!! *) + | false ⇒ 2 + pc ]) - (spc s) - (zf s) - (cf s) - (mem s) + spc + zf + cf + mem + 0 + | BRA ⇒ + mk_status + acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *) + spc + zf + cf + mem 0 - | BRA ⇒ s - | DECd ⇒ s - | LDAi ⇒ s - | LDAd ⇒ s - | STAd ⇒ s + | DECd ⇒ + let x ≝ bpred (mem op1) in (* signed!!! *) + let mem' ≝ update mem op1 x in + mk_status acc (2 + pc) spc + (eqb O x) cf mem' 0 (* check zb!!! *) + | LDAi ⇒ + mk_status op1 (2 + pc) spc (eqb O op1) cf mem 0 + | LDAd ⇒ + let x ≝ mem op1 in + mk_status x (2 + pc) spc (eqb O x) cf mem 0 + | STAd ⇒ + mk_status acc (2 + pc) spc zf cf + (update mem op1 acc) 0 ] - ]. + | false ⇒ + mk_status + acc pc spc zf cf mem (S clk) + ]]. let rec execute s n on n ≝ match n with @@ -190,85 +1599,413 @@ 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. -lemma goo: execute mult_status (matita_nat_of_coq_nat 4) = mult_status. - simplify; - change with (tick (tick (tick mult_status)) = mult_status); - change with (tick (tick mult_status) = mult_status); - change with (tick mult_status = mult_status); - change with (mult_status = mult_status); +notation "hvbox(# break a)" + non associative with precedence 80 +for @{ 'byte_of_opcode $a }. +interpretation "byte_of_opcode" 'byte_of_opcode a = + (cic:/matita/assembly/byte_of_opcode.con a). + +definition mult_source : list byte ≝ + [#LDAi; mk_byte x0 x0; (* A := 0 *) + #STAd; mk_byte x2 x0; (* Z := A *) + #LDAd; mk_byte x1 xF; (* (l1) A := Y *) + #BEQ; mk_byte x0 xA; (* if A == 0 then goto l2 *) + #LDAd; mk_byte x2 x0; (* A := Z *) + #DECd; mk_byte x1 xF; (* Y := Y - 1 *) + #ADDd; mk_byte x1 xE; (* A += X *) + #STAd; mk_byte x2 x0; (* Z := A *) + #BRA; mk_byte xF x2; (* goto l1 *) + #LDAd; mk_byte x2 x0].(* (l2) *) + +definition mult_memory ≝ + λx,y.λa:addr. + match leb a 29 with + [ true ⇒ nth ? mult_source (mk_byte x0 x0) a + | false ⇒ + match eqb a 30 with + [ true ⇒ x + | false ⇒ y + ] + ]. + +definition mult_status ≝ + λx,y. + mk_status (mk_byte x0 x0) 0 0 false false (mult_memory x y) 0. + +lemma plusbyte_O_x: + ∀b. plusbyte (mk_byte x0 x0) b false = couple ? ? b false. + intros; + elim b; + elim e; + elim e1; reflexivity. qed. +definition plusbytenc ≝ + λx,y. + match plusbyte x y false with + [couple res _ ⇒ res]. + +lemma plusbytenc_O_x: + ∀x. plusbytenc (mk_byte x0 x0) x = x. + intros; + unfold plusbytenc; + rewrite > plusbyte_O_x; + reflexivity. +qed. + +lemma test_O_O: + let i ≝ 14 in + let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in + pc s = 20 ∧ mem s 32 = byte_of_nat 0. + normalize; + split; + reflexivity. +qed. + + +lemma test_0_2: + let x ≝ mk_byte x0 x0 in + let y ≝ mk_byte x0 x2 in + let i ≝ 14 + 23 * nat_of_byte y in + let s ≝ execute (mult_status x y) i in + pc s = 20 ∧ mem s 32 = plusbytenc x x. + intros; + split; + reflexivity. +qed. + +lemma test_x_1: + ∀x. + let y ≝ mk_byte x0 x1 in + let i ≝ 14 + 23 * nat_of_byte y in + let s ≝ execute (mult_status x y) i in + pc s = 20 ∧ mem s 32 = x. + intros; + split; + [ reflexivity + | change in ⊢ (? ? % ?) with (plusbytenc (mk_byte x0 x0) x); + rewrite > plusbytenc_O_x; + reflexivity + ]. +qed. + +lemma test_x_2: + ∀x. + let y ≝ mk_byte x0 x2 in + let i ≝ 14 + 23 * nat_of_byte y in + let s ≝ execute (mult_status x y) i in + pc s = 20 ∧ mem s 32 = plusbytenc x x. + intros; + split; + [ reflexivity + | change in ⊢ (? ? % ?) with + (plusbytenc (plusbytenc (mk_byte x0 x0) x) x); + rewrite > plusbytenc_O_x; + reflexivity + ]. +qed. + +axiom byte_elim: + ∀P:byte → Prop. + (P (mk_byte x0 x0)) → + (∀i:nat. i < 255 → P (byte_of_nat i) → P (byte_of_nat (S i))) → + ∀b:byte. P b. +(* Tedious proof, easy to automate but not trivial + intros; + elim b; + elim e; + [ elim e1; + [ assumption + | apply (H1 0); + [ apply lt_O_S + | assumption + ] + | apply (H1 1); + [ alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con". + apply lt_S_S; + apply lt_O_S + | apply (H1 0); +*) + +theorem lt_trans: ∀x,y,z. x < y → y < z → x < z. + unfold lt; + intros; + autobatch. +qed. + +axiom daemon: False. + +(*axiom loop_invariant: + ∀x,y:byte.∀j:nat. j ≤ y → + let s ≝ execute (mult_status x y) (5 + 23*j) in + pc s = 4 ∧ + mem s 30 = x ∧ + mem s 31 = byte_of_nat (y - j) ∧ + mem s 32 = byte_of_nat (x * j). + + intros 2; + apply (byte_elim ? ? ? y); + [ intros; + simplify in H; + cut (j=O); + [ unfold s; clear s; + rewrite > Hcut; + reflexivity + | (* easy *) elim daemon + ] + | intros; + unfold s; + cut (j < S i ∨ j = S i); + [ elim Hcut; + [ rewrite > nat_of_byte_byte_of_nat in H1; + [2: apply (lt_trans ? 255); + [ assumption + | unfold lt; + (* ???????? *) + ] + | generalize in match (H1 j); clear H1; + intros; + unfold lt in H3; + cut (j ≤ i); + [ generalize in match (H4 Hcut1); clear H4; clear Hcut1; intro; + apply H1 + | letin xxx ≝ H3; + inversion xxx; + [ intro; + rewrite > (injective_S ? ? H1); + autobatch + | intros; + (* facile *) elim daemon + ] + ] + ] + | + ] + | (* easy *) + ] + ]. +qed. +*) + +axiom status_eq: + ∀s,s'. + acc s = acc s' → + pc s = pc s' → + spc s = spc s' → + zf s = zf s' → + cf s = cf s' → + (∀a. mem s a = mem s' a) → + clk s = clk s' → + s=s'. +(* +lemma loop_invariant': + ∀x,y:byte.∀j:nat. j ≤ y → + execute (mult_status x y) (5 + 23*j) + = + mk_status (byte_of_nat (x * j)) 4 0 true false + (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32 + (byte_of_nat (x * j))) + 0. + intros 3; + elim j; + [ do 2 (rewrite < times_n_O); + apply status_eq; + [1,2,3,4,5,7: normalize; reflexivity + | intro; + elim daemon + ] + | cut (5 + 23 * S n = 5 + 23 * n + 23); + [ letin K ≝ (breakpoint (mult_status x y) (5 + 23 * n) 23); clearbody K; + letin H' ≝ (H ?); clearbody H'; clear H; + [ autobatch + | letin xxx ≝ (eq_f ? ? (λz. execute (mult_status x y) z) ? ? Hcut); clearbody xxx; + clear Hcut; + rewrite > xxx; + clear xxx; + apply (transitive_eq ? ? ? ? K); + clear K; + rewrite > H'; + clear H'; + TO BE FINISHED; + ] + | autobatch paramodulation + ] + ] +(* + intros 2; + apply (byte_elim ? ? ? y); + [ intros; + simplify in H; + generalize in match (le_n_O_to_eq ? H); intro; + unfold s; clear s; + rewrite < H1; + rewrite < times_n_O; + rewrite < times_n_O; + apply status_eq; + [1,2,3,4,5,7: normalize; reflexivity + | intros; + whd in ⊢ (? ? % %); + normalize in ⊢ (? ? match ? ? % in bool return ? with [true\rArr ?|false\rArr ?] ?); + elim (eqb a 32) in ⊢ (? ? % match % in bool return ? with [true\rArr ?|false\rArr ?]); + simplify; + [ reflexivity + | whd in ⊢ (? ? % %); + elim daemon + ] + ] + | intros; + cut (j = byte_of_nat (S i) ∨ j ≤ byte_of_nat i); + ]. +*) +qed. + +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. + (* - unfold mult_status; - simplify; - whd in ⊢ (? ? -(? - (? - (? - match match ? % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ? - with - [true\rArr ?|false\rArr ?]))) ?); - simplify; - whd in ⊢ (? ? -(? - (? - (? - match % in opcode return ? with - [ADDd\rArr ? - |BEQ\rArr ? - |BRA\rArr ? - |DECd\rArr ? - |LDAi\rArr ? - |LDAd\rArr ? - |STAd\rArr ?]))) ?); - simplify; - whd in \vdash (? ? -(? - (? - match match % in nat return ? with [O\rArr ?|S\rArr ?] in bool return ? with - [true\rArr ?|false\rArr ?])) ?); - simplify; - whd in \vdash (? ? -(? - (? - match % in opcode return ? with - [ADDd\rArr ? - |BEQ\rArr ? - |BRA\rArr ? - |DECd\rArr ? - |LDAi\rArr ? - |LDAd\rArr ? - |STAd\rArr ?])) ?); - simplify; - whd in \vdash (? ? (? match % in bool return ? with [true\rArr ?|false\rArr ?]) ?); - simplify; - whd in \vdash (? ? -(? - match % in opcode return ? with - [ADDd\rArr ? - |BEQ\rArr ? - |BRA\rArr ? - |DECd\rArr ? - |LDAi\rArr ? - |LDAd\rArr ? - |STAd\rArr ?]) ?); - simplify; - whd in \vdash (? ? match % in bool return ? with [true\rArr ?|false\rArr ?] ?); - simplify; - whd in \vdash (? ? -match % in opcode return ? with -[ADDd\rArr ? -|BEQ\rArr ? -|BRA\rArr ? -|DECd\rArr ? -|LDAi\rArr ? -|LDAd\rArr ? -|STAd\rArr ?] ?); - simplify; + letin w ≝ 22; + letin opc ≝ (let s ≝ execute (mult_status x y) w in opcode_of_byte (mem s (pc s))); whd in opc; + letin acc' ≝ (acc (execute (mult_status x y) w)); + normalize in acc'; + change in acc' with x; + letin z ≝ (let s ≝ (execute (mult_status x y) w) in mem s 32); whd in z; + letin x ≝ (let s ≝ (execute (mult_status x y) w) in mem s 30); whd in x; + (*letin xxx ≝ (byte_of_nat (x+y)); normalize in xxx;*) + split; + [ normalize; reflexivity + | change with (byte_of_nat x = x); + normalize; + split; + [ reflexivity + | change with (byte_of_nat (x + 0)); + letin www ≝ (nat_of_byte (byte_of_nat 260)); whd in www; + letin xxx ≝ (260 \mod 256); reduce in xxx; + letin xxx ≝ ((18 + 242) \mod 256); + whd in xxx; + letin pc' ≝ (pc s); + normalize in pc'; + letin opcode ≝ (let s ≝ s in opcode_of_byte (mem s (pc s))); + normalize in opcode; + csc. + split; + reduce in s; reflexivity. -*) \ No newline at end of file +qed. + +lemma goo1: + ∀x,y. + let i ≝ 14 + 23 * nat_of_byte y in + let s ≝ execute (mult_status x y) i in + pc s = 22 ∧ mem s 32 = byte_of_nat (nat_of_byte x * nat_of_byte y). + intros; +qed. + +lemma goo: True. + letin s0 ≝ mult_status; + letin pc0 ≝ (pc s0); + reduce in pc0; + letin i0 ≝ (opcode_of_byte (mem s0 pc0)); + reduce in i0; + + letin s1 ≝ (execute s0 (cycles_of_opcode i0)); + letin pc1 ≝ (pc s1); + reduce in pc1; + letin i1 ≝ (opcode_of_byte (mem s1 pc1)); + reduce in i1; + + letin s2 ≝ (execute s1 (cycles_of_opcode i1)); + letin pc2 ≝ (pc s2); + reduce in pc2; + letin i2 ≝ (opcode_of_byte (mem s2 pc2)); + reduce in i2; + + letin s3 ≝ (execute s2 (cycles_of_opcode i2)); + letin pc3 ≝ (pc s3); + reduce in pc3; + letin i3 ≝ (opcode_of_byte (mem s3 pc3)); + reduce in i3; + letin zf3 ≝ (zf s3); + reduce in zf3; + + letin s4 ≝ (execute s3 (cycles_of_opcode i3)); + letin pc4 ≝ (pc s4); + reduce in pc4; + letin i4 ≝ (opcode_of_byte (mem s4 pc4)); + reduce in i4; + + letin s5 ≝ (execute s4 (cycles_of_opcode i4)); + letin pc5 ≝ (pc s5); + reduce in pc5; + letin i5 ≝ (opcode_of_byte (mem s5 pc5)); + reduce in i5; + + letin s6 ≝ (execute s5 (cycles_of_opcode i5)); + letin pc6 ≝ (pc s6); + reduce in pc6; + letin i6 ≝ (opcode_of_byte (mem s6 pc6)); + reduce in i6; + + letin s7 ≝ (execute s6 (cycles_of_opcode i6)); + letin pc7 ≝ (pc s7); + reduce in pc7; + letin i7 ≝ (opcode_of_byte (mem s7 pc7)); + reduce in i7; + + letin s8 ≝ (execute s7 (cycles_of_opcode i7)); + letin pc8 ≝ (pc s8); + reduce in pc8; + letin i8 ≝ (opcode_of_byte (mem s8 pc8)); + reduce in i8; + + letin s9 ≝ (execute s8 (cycles_of_opcode i8)); + letin pc9 ≝ (pc s9); + reduce in pc9; + letin i9 ≝ (opcode_of_byte (mem s9 pc9)); + reduce in i9; + + exact I. +qed. +*)*)