ax0E	: 0=0;
succE	: !n.!m.(n=m)->(n'=m');
predE	: !n.!m.(n'=m')->(n=m);
transE	: !n.!m.!k.(n=m)&(m=k)->(n=k);
symmE	: !n.!m.(n=m)->(m=n);

transE4 : !x1.!x2.!x3.!x4.(x1=x2)&(x2=x3)&(x3=x4)->(x1=x4);
transE5 : !x1.!x2.!x3.!x4.!x5.(x1=x2)&(x2=x3)&(x3=x4)&(x4=x5)->(x1=x5);
transE6 : !x1.!x2.!x3.!x4.!x5.!x6.
	  (x1=x2)&(x2=x3)&(x3=x4)&(x4=x5)&(x5=x6)->(x1=x6);
transE7 : !x1.!x2.!x3.!x4.!x5.!x6.!x7.
	  (x1=x2)&(x2=x3)&(x3=x4)&(x4=x5)&(x5=x6)&(x6=x7)->(x1=x7);
transE8 : !x1.!x2.!x3.!x4.!x5.!x6.!x7.!x8.
	  (x1=x2)&(x2=x3)&(x3=x4)&(x4=x5)&(x5=x6)&(x6=x7)&(x7=x8)->(x1=x8);

axLS	: !n.n<n';
transL	: !n.!m.!k.(n<m)&(m<k)->(n<k);

defP0	: !n.n+0=n;
defPS	: !n.!m.n+m'=(n+m)';

thmE	: !x.x=x;
thm0LS	: !x.0<x';

thm0P	: !x.0+x=x;
thm1P	: !x.0'+x=x';
assocP	: !a.!b.!c.(a+b)+c=a+(b+c);
commP	: !a.!b.a+b=b+a;
thmPE	: !n.!a.!b.(a=b)->(n+a)=(n+b);
thmPE2	: !n.!a.!b.(a=b)->(a+n)=(b+n);