include "nat/div_and_mod.ma".
include "list/list.ma".
-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 "30" non associative with precedence 80 for @{ 'x30 }.
-interpretation "natural number" 'x30 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.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 "31" non associative with precedence 80 for @{ 'x31 }.
-interpretation "natural number" 'x31 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.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 "32" non associative with precedence 80 for @{ 'x32 }.
-interpretation "natural number" 'x32 =
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
-(cic:/matita/nat/nat/nat.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
reflexivity.
qed.
-axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n.
-(* intros;
+lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
+ intro;
+ elim b;
+ simplify;
+ autobatch.
+qed.
+
+lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
+ intro;
+ unfold nat_of_byte;
+ letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
+ letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
+ unfold lt in H K ⊢ %;
+ letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
+ letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
+ apply le_S_S;
+ cut (16*bh b ≤ 16*15);
+ [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
+ simplify in Hf:(? ? %);
+ assumption
+ | autobatch
+ ]
+qed.
+
+lemma le_to_lt: ∀n,m. n ≤ m → n < S m.
+ intros;
+ autobatch.
+qed.
+
+axiom daemon: False.
+
+lemma exadecimal_of_nat_mod:
+ ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
+ elim daemon.
+(*
+ intros;
+ cases n; [ reflexivity | ];
+ cases n1; [ reflexivity | ];
+ cases n2; [ reflexivity | ];
+ cases n3; [ reflexivity | ];
+ cases n4; [ reflexivity | ];
+ cases n5; [ reflexivity | ];
+ cases n6; [ reflexivity | ];
+ cases n7; [ reflexivity | ];
+ cases n8; [ reflexivity | ];
+ cases n9; [ reflexivity | ];
+ cases n10; [ reflexivity | ];
+ cases n11; [ reflexivity | ];
+ cases n12; [ reflexivity | ];
+ cases n13; [ reflexivity | ];
+ cases n14; [ reflexivity | ];
+ cases n15; [ reflexivity | ];
+ change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
+ cut ((16 + n16) \mod 16 = n16 \mod 16);
+ [ rewrite > Hcut;
+ simplify in ⊢ (? ? % ?);
+
+ | unfold mod;
+ change with (mod_aux (16+n16) (16+n16) 15 = n16);
+ unfold mod_aux;
+ change with
+ (match leb (16+n16) 15 with
+ [true ⇒ 16+n16
+ | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
+ ] = n16);
+ cut (leb (16+n16) 15 = false);
+ [ rewrite > Hcut;
+ change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
+ cut (16+n16-16 = n16);
+ [ rewrite > Hcut1; clear Hcut1;
+
+ |
+ ]
+ |
+ ]
+ ]*)
+qed.
+
+(*lemma exadecimal_of_nat_elim:
+ ∀P:exadecimal → Prop.
+ (∀m. m < 16 → P (exadecimal_of_nat m)) →
+ ∀n. P (exadecimal_of_nat n).
+ intros;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ cases n; [ apply H; autobatch | ]; clear n;
+ cases n1; [ apply H; autobatch | ]; clear n1;
+ simplify;
+ elim daemon.
+qed.
+*)
+
+axiom nat_of_exadecimal_exadecimal_of_nat:
+ ∀n. nat_of_exadecimal (exadecimal_of_nat n) = n \mod 16.
+(*
+ intro;
+ apply (exadecimal_of_nat_elim (λn.;
+
+
+
+ elim n 0; [ reflexivity | intro ];
+ elim n1 0; [ intros; reflexivity | intros 2 ];
+ elim n2 0; [ intros; reflexivity | intros 2 ];
+ elim n3 0; [ intros; reflexivity | intros 2 ];
+ elim n4 0; [ intros; reflexivity | intros 2 ];
+ elim n5 0; [ intros; reflexivity | intros 2 ];
+ elim n6 0; [ intros; reflexivity | intros 2 ];
+ elim n7 0; [ intros; reflexivity | intros 2 ];
+ elim n8 0; [ intros; reflexivity | intros 2 ];
+ elim n9 0; [ intros; reflexivity | intros 2 ];
+ elim n10 0; [ intros; reflexivity | intros 2 ];
+ elim n11 0; [ intros; reflexivity | intros 2 ];
+ elim n12 0; [ intros; reflexivity | intros 2 ];
+ elim n13 0; [ intros; reflexivity | intros 2 ];
+ elim n14 0; [ intros; reflexivity | intros 2 ];
+ elim n15 0; [ intros; reflexivity | intros 2 ];
+ intro;
+ simplify;
+ rewrite < H15;
+ change in ⊢ (? ? % ?) with (nat_of_exadecimal (exadecimal_of_nat n16));
+qed.
+*)
+
+lemma nat_of_byte_byte_of_nat: ∀n. nat_of_byte (byte_of_nat n) = n \mod 256.
+ intro;
unfold byte_of_nat;
-*)
+ unfold nat_of_byte;
+ change with (16*(exadecimal_of_nat (n/16)) + exadecimal_of_nat n = n \mod 256);
+ rewrite > nat_of_exadecimal_exadecimal_of_nat in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > nat_of_exadecimal_exadecimal_of_nat;
+ elim daemon.
+qed.
definition nat_of_bool ≝
λb. match b with [ true ⇒ 1 | false ⇒ 0 ].
-(* Way too slow. Handles 2^32 goals!
-lemma plusbyte_ok:
+lemma plusex_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'
- ].
+ match plusex b1 b2 c with
+ [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
intros;
elim c;
elim b1;
- elim e;
- elim e1;
elim b2;
- elim e2;
- elim e3;
+ normalize;
reflexivity.
qed.
-*)
+
+lemma plusbyte_ok:
+ ∀b1,b2,c.
+ match plusbyte b1 b2 c with
+ [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
+ ].
+ intros;
+ unfold plusbyte;
+ generalize in match (plusex_ok (bl b1) (bl b2) c);
+ elim (plusex (bl b1) (bl b2) c);
+ simplify in H ⊢ %;
+ generalize in match (plusex_ok (bh b1) (bh b2) t1);
+ elim (plusex (bh b1) (bh b2) t1);
+ simplify in H1 ⊢ %;
+ change in ⊢ (? ? ? (? (? % ?) ?)) with (16 * t2);
+ unfold nat_of_byte;
+ letin K ≝ (eq_f ? ? (λy.16*y) ? ? H1); clearbody K; clear H1;
+ rewrite > distr_times_plus in K:(? ? ? %);
+ rewrite > symmetric_times in K:(? ? ? (? ? (? ? %)));
+ rewrite < associative_times in K:(? ? ? (? ? %));
+ normalize in K:(? ? ? (? ? (? % ?)));
+ rewrite > symmetric_times in K:(? ? ? (? ? %));
+ rewrite > sym_plus in ⊢ (? ? ? (? % ?));
+ rewrite > associative_plus in ⊢ (? ? ? %);
+ letin K' ≝ (eq_f ? ? (plus t) ? ? K); clearbody K'; clear K;
+ apply transitive_eq; [3: apply K' | skip | ];
+ clear K';
+ rewrite > sym_plus in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > associative_plus in ⊢ (? ? (? % ?) ?);
+ rewrite > associative_plus in ⊢ (? ? % ?);
+ rewrite > associative_plus in ⊢ (? ? (? ? %) ?);
+ rewrite > associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
+ rewrite > sym_plus in ⊢ (? ? (? ? (? ? (? ? %))) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? (? ? %)) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? %) ?);
+ rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
+ rewrite > H; clear H;
+ autobatch paramodulation.
+qed.
(*
lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
[ true ⇒ v
| false ⇒ f x ].
+lemma update_update_a_a:
+ ∀s,a,v1,v2,b.
+ update (update s a v1) a v2 b = update s a v2 b.
+ intros;
+ unfold update;
+ unfold update;
+ elim (eqb b a);
+ reflexivity.
+qed.
+
+lemma update_update_a_b:
+ ∀s,a1,v1,a2,v2,b.
+ a1 ≠ a2 →
+ update (update s a1 v1) a2 v2 b = update (update s a2 v2) a1 v1 b.
+ intros;
+ unfold update;
+ unfold update;
+ apply (bool_elim ? (eqb b a1)); intros;
+ apply (bool_elim ? (eqb b a2)); intros;
+ simplify;
+ [ elim H;
+ rewrite < (eqb_true_to_eq ? ? H1);
+ apply eqb_true_to_eq;
+ assumption
+ |*: reflexivity
+ ].
+qed.
+
definition mmod16 ≝ λn. nat_of_byte (byte_of_nat n).
definition tick ≝
reflexivity.
qed.
+axiom mod_plus: ∀a,b,m. (a + b) \mod m = a \mod m + b \mod m.
+axiom eq_mod_times_n_m_m_O: ∀n,m. O < m → n * m \mod m = O.
+
+axiom eq_nat_of_byte_mod: ∀b. nat_of_byte b = nat_of_byte b \mod 256.
+
+theorem plusbytenc_ok:
+ ∀b1,b2:byte. nat_of_byte (plusbytenc b1 b2) = (b1 + b2) \mod 256.
+ intros;
+ unfold plusbytenc;
+ generalize in match (plusbyte_ok b1 b2 false);
+ elim (plusbyte b1 b2 false);
+ simplify in H ⊢ %;
+ change with (nat_of_byte t = (b1 + b2) \mod 256);
+ rewrite < plus_n_O in H;
+ rewrite > H; clear H;
+ rewrite > mod_plus;
+ letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
+ letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
+ [ autobatch | ];
+ autobatch paramodulation.
+qed.
+
lemma test_O_O:
let i ≝ 14 in
let s ≝ execute (mult_status (mk_byte x0 x0) (mk_byte x0 x0)) i in
].
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' →
].
qed.
-lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
- intro;
- elim b;
- simplify;
- autobatch.
-qed.
-
-lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
- intro;
- unfold nat_of_byte;
- letin H ≝ (lt_nat_of_exadecimal_16 (bh b)); clearbody H;
- letin K ≝ (lt_nat_of_exadecimal_16 (bl b)); clearbody K;
- unfold lt in H K ⊢ %;
- letin H' ≝ (le_S_S_to_le ? ? H); clearbody H'; clear H;
- letin K' ≝ (le_S_S_to_le ? ? K); clearbody K'; clear K;
- apply le_S_S;
- cut (16*bh b ≤ 16*15);
- [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
- simplify in Hf:(? ? %);
- assumption
- | autobatch
- ]
-qed.
-
-lemma exadecimal_of_nat_mod:
- ∀n.exadecimal_of_nat n = exadecimal_of_nat (n \mod 16).
- elim daemon.
-(*
- intros;
- cases n; [ reflexivity | ];
- cases n1; [ reflexivity | ];
- cases n2; [ reflexivity | ];
- cases n3; [ reflexivity | ];
- cases n4; [ reflexivity | ];
- cases n5; [ reflexivity | ];
- cases n6; [ reflexivity | ];
- cases n7; [ reflexivity | ];
- cases n8; [ reflexivity | ];
- cases n9; [ reflexivity | ];
- cases n10; [ reflexivity | ];
- cases n11; [ reflexivity | ];
- cases n12; [ reflexivity | ];
- cases n13; [ reflexivity | ];
- cases n14; [ reflexivity | ];
- cases n15; [ reflexivity | ];
- change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
- cut ((16 + n16) \mod 16 = n16 \mod 16);
- [ rewrite > Hcut;
- simplify in ⊢ (? ? % ?);
-
- | unfold mod;
- change with (mod_aux (16+n16) (16+n16) 15 = n16);
- unfold mod_aux;
- change with
- (match leb (16+n16) 15 with
- [true ⇒ 16+n16
- | false ⇒ mod_aux (15+n16) ((16+n16) - 16) 15
- ] = n16);
- cut (leb (16+n16) 15 = false);
- [ rewrite > Hcut;
- change with (mod_aux (15+n16) (16+n16-16) 15 = n16);
- cut (16+n16-16 = n16);
- [ rewrite > Hcut1; clear Hcut1;
-
- |
- ]
- |
- ]
- ]*)
-qed.
-
lemma eq_bpred_S_a_a:
∀a. a < 255 → bpred (byte_of_nat (S a)) = byte_of_nat a.
elim daemon. (*
lemma plusbyteenc_S:
∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
intros;
+ rewrite < byte_of_nat_nat_of_byte;
+ rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x);
+ rewrite > na
+
+(*CSC*)
+ intros;
+ unfold byte_of_nat;
+ unfold plusbytenc;
+ unfold plusbyte;
+
elim daemon.
qed.
-(*
+lemma eq_plusbytec_x0_x0_x_false:
+ ∀x.plusbytec (mk_byte x0 x0) x = false.
+ intro;
+ elim x;
+ elim e;
+ elim e1;
+ reflexivity.
+qed.
+
lemma loop_invariant':
∀x,y:byte.∀j:nat. j ≤ y →
execute (mult_status x y) (5 + 23*j)
=
- mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j))) false
+ mk_status (byte_of_nat (x * j)) 4 0 (eqbyte (mk_byte x0 x0) (byte_of_nat (x*j)))
+ (plusbytec (byte_of_nat (x*pred j)) x)
(update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (y - j))) 32
(byte_of_nat (x * j)))
0.
elim j;
[ do 2 (rewrite < times_n_O);
apply status_eq;
- [1,2,3,4,5,7: normalize; reflexivity
+ [1,2,3,4,7: normalize; reflexivity
+ | rewrite > eq_plusbytec_x0_x0_x_false;
+ normalize;
+ reflexivity
| intro;
elim daemon
]
[ elim Hcut; clear Hcut;
elim H; clear H;
rewrite > H2;
- (* instruction 1 *)
+ (* instruction LDAd *)
letin K ≝
(breakpoint
- (mk_status (byte_of_nat (x*n)) 4 O true false
+ (mk_status (byte_of_nat (x*n)) 4 O
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
(update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
(byte_of_nat (x*n))) O)
3 20); clearbody K;
normalize in K:(? ? (? ? %) ?);
apply transitive_eq; [2: apply K | skip | ]; clear K;
- change in ⊢ (? ? (? % ?) ?) with
- (mk_status
- (byte_of_nat (S a))
- 6
- 0
- (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
- false
- (update
- (update (update (mult_memory x y) 30 x)
- 31 (byte_of_nat (S a)))
- 32 (byte_of_nat (x*n)))
- 0);
- (* instruction 2 *)
+ whd in ⊢ (? ? (? % ?) ?);
+ normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
+ change in ⊢ (? ? (? (? % ? ? ? ? ? ?) ?) ?)
+ with (byte_of_nat (S a));
+ change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
+ (byte_of_nat (S a));
+ (* instruction BEQ *)
letin K ≝
(breakpoint
(mk_status (byte_of_nat (S a)) 6 O
- (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) false
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
(update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
(byte_of_nat (x*n))) O)
3 17); clearbody K;
letin K ≝ (eq_eqbyte_x0_x0_byte_of_nat_S_false ? H3); clearbody K;
rewrite > K; clear K;
simplify in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
- (* instruction 3 *)
+ (* instruction LDAd *)
letin K ≝
(breakpoint
(mk_status (byte_of_nat (S a)) 8 O
- (eqbyte (mk_byte x0 x0) (byte_of_nat (S a))) false
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (S a)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
(update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
(byte_of_nat (x*n))) O)
3 14); clearbody K;
letin K ≝
(breakpoint
(mk_status (byte_of_nat (x*n)) 10 O
- (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n))) false
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (x*n)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
(update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S a))) 32
(byte_of_nat (x*n))) O)
5 9); clearbody K;
letin K ≝
(breakpoint
(mk_status (byte_of_nat (x*n)) 12
- O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n))) false
+ O (eqbyte (mk_byte x0 x0) (byte_of_nat (y-S n)))
+ (plusbytec (byte_of_nat (x*pred n)) x)
(update
(update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
32 (byte_of_nat (x*n))) 31
change in ⊢ (? ? (? (? ? ? ? (? ? %) ? ? ?) ?) ?) with
(plusbytenc (byte_of_nat (x*n)) x);
normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
- normalize in \vdash (? ?
- (?
- (? ? ? ? ? match ? ? % ? in cartesian_product return ? with [couple\rArr ?] ? ?)
- ?) ?);
+ change in ⊢ (? ? (? (? ? ? ? ? % ? ?) ?) ?)
+ with (plusbytec (byte_of_nat (x*n)) x);
rewrite > plusbyteenc_S;
(* instruction STAd *)
letin K ≝
(breakpoint
(mk_status (byte_of_nat (x*S n)) 14 O
(eqbyte (mk_byte x0 x0) (byte_of_nat (x*S n)))
- match plusbyte (byte_of_nat (x*n)) x false
- in cartesian_product
- return \lambda c:(cartesian_product byte bool).bool
- with
- [couple (_:byte) (c':bool)\rArr c']
+ (plusbytec (byte_of_nat (x*n)) x)
(update
(update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat (S (y-S n))))
32 (byte_of_nat (x*n))) 31
(* instruction BRA *)
whd in ⊢ (? ? % ?);
normalize in ⊢ (? ? (? ? % ? ? ? ? ?) ?);
+ rewrite < pred_Sn;
apply status_eq;
[1,2,3,4,7: normalize; reflexivity
+ | change with (plusbytec (byte_of_nat (x*n)) x =
+ plusbytec (byte_of_nat (x*n)) x);
+ reflexivity
|6: intro;
elim daemon
- |5: FALSO!
]
| exists;
[ apply (y - S n)
]
]
]
- | autobatch paramodulation
+ | rewrite > associative_plus;
+ autobatch paramodulation
]
]
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).
+ ∀x,y:byte.
+ let i ≝ 14 + 23 * y in
+ execute (mult_status x y) i =
+ mk_status (byte_of_nat (x*y)) 20 0
+ (eqbyte (mk_byte x0 x0) (byte_of_nat (x*y)))
+ (plusbytec (byte_of_nat (x*pred y)) x)
+ (update
+ (update (mult_memory x y) 31 (mk_byte x0 x0))
+ 32 (byte_of_nat (x*y)))
+ 0.
intros;
- 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.*)
\ No newline at end of file
+ cut (14 + 23 * y = 5 + 23*y + 9);
+ [2: autobatch paramodulation;
+ | rewrite > Hcut; (* clear Hcut; *)
+ rewrite > (breakpoint (mult_status x y) (5 + 23*y) 9);
+ rewrite > loop_invariant';
+ [2: apply le_n
+ | rewrite < minus_n_n;
+ apply status_eq;
+ [1,2,3,4,5,7: normalize; reflexivity
+ | elim daemon
+ ]
+ ]
+ ].
+qed.