From c1e4ed1c5c7789a6b9020914da16de876c5b3ecc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 13 Jul 2007 18:08:28 +0000 Subject: [PATCH] 1. requires the new pretty printer for natural numbers 2. important properties of plusbyte proved 3. all important conjectures almost proved --- .../matita/library/assembly/assembly.ma | 758 ++---------------- 1 file changed, 71 insertions(+), 687 deletions(-) diff --git a/helm/software/matita/library/assembly/assembly.ma b/helm/software/matita/library/assembly/assembly.ma index c9582c830..87d9006c9 100644 --- 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. -- 2.39.2