1. requires the new pretty printer for natural numbers

2. important properties of plusbyte proved
3. all important conjectures almost proved

diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/assembly.ma
index c9582c8304f476f0989c60fca0b793b0e2e4025a..87d9006c90b893f30b505c76102af844b32a2cd2 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
@@ -1483,23 +807,56 @@ axiom nat_of_byte_byte_of_nat: ∀n. n < 256 → nat_of_byte (byte_of_nat n) = n
 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.
@@ -1775,6 +1132,28 @@ lemma plusbytenc_O_x:
  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
@@ -2108,7 +1487,12 @@ qed.
  
 lemma plusbyteenc_S:
  ∀x:byte.∀n.plusbytenc (byte_of_nat (x*n)) x = byte_of_nat (x * S n).
+(*CSC*)
  intros;
+ unfold byte_of_nat;
+ unfold plusbytenc;
+ unfold plusbyte;
+ 
  elim daemon.
 qed. 
 
@@ -2315,4 +1699,4 @@ theorem test_x_y:
         ]
      ]
   ].
-qed.
\ No newline at end of file
+qed.