corrected axiom mod_plus

[helm.git] / helm / software / matita / library / assembly / assembly.ma

diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/assembly.ma
index 6a349426748faa22a220b1e281aaae016cf5ece4..4e2326de08023d7581783fd70c7608e7865c8405 100644 (file)
--- a/helm/software/matita/library/assembly/assembly.ma
+++ b/helm/software/matita/library/assembly/assembly.ma
@@ -17,682 +17,6 @@ set "baseuri" "cic:/matita/assembly/".
 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
@@ -1475,31 +799,204 @@ lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
  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.
@@ -1643,6 +1140,34 @@ definition update ≝
    [ 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 ≝
@@ -1664,6 +1189,7 @@ definition tick ≝
            acc
            (match zf with
              [ true ⇒ mmod16 (2 + op1 + pc) (*\mod 256*)   (* signed!!! *)
+                      (* FIXME: can't work - address truncated to 8 bits *)
              | false ⇒ 2 + pc
              ])
            spc
@@ -1674,6 +1200,7 @@ definition tick ≝
        | BRA ⇒
           mk_status
            acc (mmod16 (2 + op1 + pc) (*\mod 256*)) (* signed!!! *)
+                                      (* FIXME: same as above *)
            spc
            zf
            cf
@@ -1775,6 +1302,38 @@ lemma plusbytenc_O_x:
  reflexivity.
 qed.
 
+(*axiom mod_plus: ∀a,b,m. (a + b) \mod m = a \mod m + b \mod m.*)
+axiom mod_plus: \forall a1,a2,b1,b2,m.
+              a1 \mod m = b1 \mod m \to
+              a2 \mod m = b2 \mod m \to
+              (a1 + a2) \mod m = (b1 + b2) \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;
+ letin K ≝ (eq_nat_of_byte_mod t); clearbody K;
+ rewrite > K in ⊢ (? ? % ?); 
+ letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K';
+    [ autobatch
+    | cut (O =  O \mod 256);
+       [ rewrite > Hcut in K':(? ? ? %);
+         rewrite > K in K:(? ? % ?);
+         rewrite > (mod_plus ? ? ? ? ? K K') in ⊢ (? ? ? %);
+         rewrite < plus_n_O;reflexivity
+       |simplify;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
@@ -1827,88 +1386,12 @@ lemma test_x_2:
   ].
 qed.
 
-axiom byte_elim:
- ∀P:byte → Prop.
-  (P (mk_byte x0 x0)) →
-   (∀i:nat. i < 255 → P (byte_of_nat i) → P (byte_of_nat (S i))) →
-    ∀b:byte. P b.
-(* Tedious proof, easy to automate but not trivial
- intros;
- elim b;
- elim e;
-  [ elim e1;
-     [ assumption
-     | apply (H1 0);
-        [ apply lt_O_S
-        | assumption
-        ]
-     | apply (H1 1);
-        [ alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
-          apply lt_S_S;
-          apply lt_O_S
-        | apply (H1 0);
-*)
-
 theorem lt_trans: ∀x,y,z. x < y → y < z → x < z.
  unfold lt;
  intros;
  autobatch.
 qed.
 
-axiom daemon: False.
-
-(*axiom loop_invariant:
- ∀x,y:byte.∀j:nat. j ≤ y →
-  let s ≝ execute (mult_status x y) (5 + 23*j) in
-   pc s = 4 ∧
-   mem s 30 = x ∧
-   mem s 31 = byte_of_nat (y - j) ∧
-   mem s 32 = byte_of_nat (x * j).
-
- 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' →
@@ -1992,8 +1475,12 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
     [ unfold eqbyte;
       change in ⊢ (? ? (? ? %) ?) with (eqex x0 (exadecimal_of_nat (S b))); 
       rewrite > eq_eqex_S_x0_false;
-       [ alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
+       [ elim (eqex (bh (mk_byte x0 x0))
+(bh (mk_byte (exadecimal_of_nat (S b/16)) (exadecimal_of_nat (S b)))));simplify;
+(*
+ alias id "andb_sym" = "cic:/matita/nat/propr_div_mod_lt_le_totient1_aux/andb_sym.con".
          rewrite > andb_sym;
+*)
          reflexivity
        | assumption
        ]
@@ -2021,77 +1508,6 @@ lemma eq_eqbyte_x0_x0_byte_of_nat_S_false:
   ].
 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. (*
@@ -2109,15 +1525,34 @@ qed.
 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.
@@ -2125,7 +1560,10 @@ lemma loop_invariant':
  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
     ]
@@ -2145,32 +1583,29 @@ lemma loop_invariant':
          [ 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;
@@ -2180,11 +1615,12 @@ lemma loop_invariant':
            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;
@@ -2198,7 +1634,8 @@ lemma loop_invariant':
            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;
@@ -2216,7 +1653,8 @@ lemma loop_invariant':
            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
@@ -2230,21 +1668,15 @@ lemma loop_invariant':
            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
@@ -2257,11 +1689,14 @@ lemma loop_invariant':
            (* 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)
@@ -2275,41 +1710,35 @@ lemma loop_invariant':
             ]
          ]
       ]
-    | 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.