Examples
Examples -> PeanoArithmetic -> PA-TwoToTheN.prf
2 [] x*0=0.
5 [] x^s(y)=x*x^y.
9 [] -ap(y,0)|ap(y,g(y))|ap(y,z).
10 [] -ap(y,0)| -ap(y,s(g(y)))|ap(y,z).
13 [] -(u<v)|x*u<x*v| -(0<x).
15 [] 0<s(0).
17 [] 0<a.
19 [] x<y|y<=x.
20 [] -(y<=x)| -(x<y).
21 [] -(u<v)| -(v<=w)|u<w.
22 [] -(s(0)<z)| -(0<y)|s(y)<=z*y.
24 [] -(x<=0)|x=0.
25 [] s(0)<a.
26 [] x*s(y)=x*y+x.
28 [] 0+x=x.
29 [] x^0=s(0).
30 [] -(n<a^n).
32 [binary,30.1,10.3,demod,beta,29,beta,5,unit_del,15] -(s(g(lambda(x,x<a^x)))<a*a^g(lambda(x,x<a^x))).
33 [binary,30.1,9.3,demod,beta,29,beta,unit_del,15] g(lambda(x,x<a^x))<a^g(lambda(x,x<a^x)).
35 [hyper,33,13,17] a*g(lambda(x,x<a^x))<a*a^g(lambda(x,x<a^x)).
37 [binary,32.1,19.1] a*a^g(lambda(x,x<a^x))<=s(g(lambda(x,x<a^x))).
41 [hyper,37,21,35] a*g(lambda(x,x<a^x))<s(g(lambda(y,y<a^y))).
42 [binary,41.1,20.2] -(s(g(lambda(x,x<a^x)))<=a*g(lambda(y,y<a^y))).
45 [binary,42.1,22.3,unit_del,25] -(0<g(lambda(x,x<a^x))).
46 [binary,45.1,19.1] g(lambda(x,x<a^x))<=0.
52 [binary,46.1,24.1] g(lambda(x,x<a^x))=0.
67 [para_from,52.1.1,32.1.2.2.2,demod,29,26,2,28] -(s(g(lambda(x,x<a^x)))<a).
76 [para_from,52.1.2,25.1.1.1] s(g(lambda(x,x<a^x)))<a.
77 [binary,76.1,67.1] $F.
