-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 "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/1)
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).