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 *)
| 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.
| 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
]]]
λ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;
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
| 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.
+*)*)
projects / helm.git / blobdiff