+landau
+n
@nat:='prim':'type'
[x:nat][y:nat]
is:=is"e"(nat,x,y):'prop'
nis:=not(is(x,y)):'prop'
x@[s:set(nat)]
in:=esti(nat,x,s):'prop'
@[p:[x:nat]'prop']
some:=some"l"(nat,p):'prop'
all:=all"l"(nat,p):'prop'
one:=one"e"(nat,p):'prop'
@1:='prim':nat
suc:='prim':[x:nat]nat
[x:nat][y:nat][i:is(x,y)]
ax2:=isf(nat,nat,suc,x,y,i):is(<x>suc,<y>suc)
@ax3:='prim':[x:nat]nis(<x>suc,1)
ax4:='prim':[x:nat][y:nat][u:is(<x>suc,<y>suc)]is(x,y)
[s:set(nat)]
cond1:=in(1,s):'prop'
cond2:=all([x:nat]imp(in(x,s),in(<x>suc,s))):'prop'
@ax5:='prim':[s:set(nat)][u:cond1(s)][v:cond2(s)][x:nat]in(x,s)
[p:[x:nat]'prop'][1p:<1>p][xsp:[x:nat][y:<x>p]<<x>suc>p][x:nat]
+i1
s:=setof(nat,p):set(nat)
t1:=estii(nat,p,1,1p):cond1(s)
[y:nat][yes:in(y,s)]
t2:=estie(nat,p,y,yes):<y>p
t3:=estii(nat,p,<y>suc,<t2><y>xsp):in(<y>suc,s)
x@t4:=<x><[y:nat][u:in(y,s)]t3(y,u)><t1><s>ax5:in(x,s)
-i1
induction:=estie(nat,p,x,t4".i1"):<x>p
@[x:nat][y:nat][n:nis(x,y)]
+21
[i:is(<x>suc,<y>suc)]
t1:=<i><y><x>ax4:is(x,y)
-21
satz1:=th3"l.imp"(is(<x>suc,<y>suc),is(x,y),n,[u:is(<x>suc,<y>suc)]t1".21"(u)):nis(<x>suc,<y>suc)
+22
x@prop1:=nis(<x>suc,x):'prop'
@t1:=<1>ax3:prop1(1)
x@[p:prop1(x)]
t2:=satz1(<x>suc,x,p):prop1(<x>suc)
-22
x@satz2:=induction([y:nat]prop1".22"(y),t1".22",[y:nat][u:prop1".22"(y)]t2".22"(y,u),x):nis(<x>suc,x)
+23
prop1:=or(is(x,1),some([u:nat]is(x,<u>suc))):'prop'
@t1:=ori1(is(1,1),some([u:nat]is(1,<u>suc)),refis(nat,1)):prop1(1)
x@t2:=somei(nat,[u:nat]is(<x>suc,<u>suc),x,refis(nat,<x>suc)):some([u:nat]is(<x>suc,<u>suc))
t3:=ori2(is(<x>suc,1),some([u:nat]is(<x>suc,<u>suc)),t2):prop1(<x>suc)
t4:=induction([y:nat]prop1(y),t1,[y:nat][u:prop1(y)]t3(y),x):prop1(x)
-23
[n:nis(x,1)]
satz3:=ore2(is(x,1),some([u:nat]is(x,<u>suc)),t4".23",n):some([u:nat]is(x,<u>suc))
y@[z:nat][i:is(x,<y>suc)][j:is(x,<z>suc)]
+*23
j@t5:=<tris1(nat,<y>suc,<z>suc,x,i,j)><z><y>ax4:is(y,z)
x@t6:=[y:nat][z:nat][u:is(x,<y>suc)][v:is(x,<z>suc)]t5(y,z,u,v):amone(nat,[u:nat]is(x,<u>suc))
-23
n@satz3a:=onei(nat,[u:nat]is(x,<u>suc),t6".23",satz3):one([u:nat]is(x,<u>suc))
+24
x@[f:[y:nat]nat]
prop1:=all([y:nat]is(<<y>suc>f,<<y>f>suc)):'prop'
prop2:=and(is(<1>f,<x>suc),prop1):'prop'
x@[a:[y:nat]nat][b:[y:nat]nat][pa:prop2(a)][pb:prop2(b)][y:nat]
prop3:=is(<y>a,<y>b):'prop'
pb@t1:=ande1(is(<1>a,<x>suc),prop1(a),pa):is(<1>a,<x>suc)
t2:=ande1(is(<1>b,<x>suc),prop1(b),pb):is(<1>b,<x>suc)
t3:=tris2(nat,<1>a,<1>b,<x>suc,t1,t2):prop3(1)
y@[p:prop3(y)]
t4:=ax2(<y>a,<y>b,p):is(<<y>a>suc,<<y>b>suc)
t5:=ande2(is(<1>a,<x>suc),prop1(a),pa):prop1(a)
t6:=ande2(is(<1>b,<x>suc),prop1(b),pb):prop1(b)
t7:=<y>t5:is(<<y>suc>a,<<y>a>suc)
t8:=<y>t6:is(<<y>suc>b,<<y>b>suc)
t9:=tr3is(nat,<<y>suc>a,<<y>a>suc,<<y>b>suc,<<y>suc>b,t7,t4,symis"e"(nat,<<y>suc>b,<<y>b>suc,t8)):prop3(<y>suc)
y@t10:=induction([z:nat]prop3(z),t3,[z:nat][u:prop3(z)]t9(z,u),y):prop3(y)
pb@t11:=fisi(nat,nat,a,b,[y:nat]t10(y)):is"e"([y:nat]nat,a,b)
x@aa:=[z:[y:nat]nat][u:[y:nat]nat][v:prop2(z)][w:prop2(u)]t11(z,u,v,w):amone([y:nat]nat,[z:[y:nat]nat]prop2(z))
prop4:=some"l"([y:nat]nat,[z:[y:nat]nat]prop2(z)):'prop'
@t12:=[x:nat]refis(nat,<<x>suc>suc):prop1(1,suc)
t13:=andi(is(<1>suc,<1>suc),prop1(1,suc),refis(nat,<1>suc),t12):prop2(1,suc)
t14:=somei([y:nat]nat,[z:[y:nat]nat]prop2(1,z),suc,t13):prop4(1)
x@[p:prop4(x)][f:[y:nat]nat][pf:prop2(f)]
g:=[y:nat]<<y>f>suc:[y:nat]nat
[y:nat]
t15:=refis(nat,<y>g):is(<y>g,<<y>f>suc)
pf@t16:=ande1(is(<1>f,<x>suc),prop1(f),pf):is(<1>f,<x>suc)
t17:=tris(nat,<1>g,<<1>f>suc,<<x>suc>suc,t15(1),ax2(<1>f,<x>suc,t16)):is(<1>g,<<x>suc>suc)
y@t18:=ande2(is(<1>f,<x>suc),prop1(f),pf):prop1(f)
t19:=<y>t18:is(<<y>suc>f,<<y>f>suc)
t20:=tris2(nat,<<y>suc>f,<y>g,<<y>f>suc,t19,t15):is(<<y>suc>f,<y>g)
t21:=tris(nat,<<y>suc>g,<<<y>suc>f>suc,<<y>g>suc,t15(<y>suc),ax2(<<y>suc>f,<y>g,t20)):is(<<y>suc>g,<<y>g>suc)
pf@t22:=[y:nat]t21(y):prop1(<x>suc,g)
t23:=andi(is(<1>g,<<x>suc>suc),prop1(<x>suc,g),t17,t22):prop2(<x>suc,g)
t24:=somei([y:nat]nat,[z:[y:nat]nat]prop2(<x>suc,z),g,t23):prop4(<x>suc)
p@t25:=someapp([y:nat]nat,[z:[y:nat]nat]prop2(z),p,prop4(<x>suc),[z:[y:nat]nat][u:prop2(z)]t24(z,u)):prop4(<x>suc)
x@bb:=induction([y:nat]prop4(y),t14,[y:nat][u:prop4(y)]t25(y,u),x):prop4(x)
-24
x@satz4:=onei([y:nat]nat,[z:[y:nat]nat]prop2".24"(z),aa".24",bb".24"):one"e"([y:nat]nat,[z:[y:nat]nat]and(is(<1>z,<x>suc),all([y:nat]is(<<y>suc>z,<<y>z>suc))))
plus:=ind([y:nat]nat,[z:[y:nat]nat]prop2".24"(z),satz4):[y:nat]nat
y@pl:=<y>plus:nat
+*24
x@t26:=oneax([y:nat]nat,[z:[y:nat]nat]prop2(z),satz4):prop2(plus)
-24
x@satz4a:=ande1(is(<1>plus,<x>suc),prop1".24"(plus),t26".24"):is(pl(x,1),<x>suc)
+*24
x@t27:=ande2(is(<1>plus,<x>suc),prop1(plus),t26):prop1(plus)
-24
y@satz4b:=<y>t27".24":is(pl(x,<y>suc),<pl(x,y)>suc)
+*24
@t28:=t11(1,plus(1),suc,t26(1),t13):is"e"([y:nat]nat,plus(1),suc)
-24
x@satz4c:=fise(nat,nat,plus(1),suc,t28".24",x):is(pl(1,x),<x>suc)
+*24
x@t29:=t11(<x>suc,plus(<x>suc),[y:nat]<<y>plus>suc,t26(<x>suc),t23(bb,plus,t26)):is"e"([y:nat]nat,plus(<x>suc),[y:nat]<<y>plus>suc)
-24
y@satz4d:=fise(nat,nat,plus(<x>suc),[z:nat]<<z>plus>suc,t29".24",y):is(pl(<x>suc,y),<pl(x,y)>suc)
x@satz4e:=symis(nat,pl(x,1),<x>suc,satz4a):is(<x>suc,pl(x,1))
y@satz4f:=symis(nat,pl(x,<y>suc),<pl(x,y)>suc,satz4b):is(<pl(x,y)>suc,pl(x,<y>suc))
x@satz4g:=symis(nat,pl(1,x),<x>suc,satz4c):is(<x>suc,pl(1,x))
y@satz4h:=symis(nat,pl(<x>suc,y),<pl(x,y)>suc,satz4d):is(<pl(x,y)>suc,pl(<x>suc,y))
z@[i:is(x,y)]
ispl1:=isf(nat,nat,[u:nat]pl(u,z),x,y,i):is(pl(x,z),pl(y,z))
ispl2:=isf(nat,nat,[u:nat]pl(z,u),x,y,i):is(pl(z,x),pl(z,y))
z@[u:nat][i:is(x,y)][j:is(z,u)]
ispl12:=tris(nat,pl(x,z),pl(y,z),pl(y,u),ispl1(i),ispl2(z,u,y,j)):is(pl(x,z),pl(y,u))
+25
z@prop1:=is(pl(pl(x,y),z),pl(x,pl(y,z))):'prop'
y@t1:=tr3is(nat,pl(pl(x,y),1),<pl(x,y)>suc,pl(x,<y>suc),pl(x,pl(y,1)),satz4a(pl(x,y)),satz4f,ispl2(<y>suc,pl(y,1),x,satz4e(y))):prop1(1)
z@[p:prop1(z)]
t2:=ax2(pl(pl(x,y),z),pl(x,pl(y,z)),p):is(<pl(pl(x,y),z)>suc,<pl(x,pl(y,z))>suc)
t3:=tr4is(nat,pl(pl(x,y),<z>suc),<pl(pl(x,y),z)>suc,<pl(x,pl(y,z))>suc,pl(x,<pl(y,z)>suc),pl(x,pl(y,<z>suc)),satz4b(pl(x,y),z),t2,satz4f(x,pl(y,z)),ispl2(<pl(y,z)>suc,pl(y,<z>suc),x,satz4f(y,z))):prop1(<z>suc)
-25
z@satz5:=induction([u:nat]prop1".25"(u),t1".25",[u:nat][v:prop1".25"(u)]t3".25"(u,v),z):is(pl(pl(x,y),z),pl(x,pl(y,z)))
asspl1:=satz5:is(pl(pl(x,y),z),pl(x,pl(y,z)))
asspl2:=symis(nat,pl(pl(x,y),z),pl(x,pl(y,z)),satz5):is(pl(x,pl(y,z)),pl(pl(x,y),z))
+26
y@prop1:=is(pl(x,y),pl(y,x)):'prop'
t1:=satz4a(y):is(pl(y,1),<y>suc)
t2:=satz4c(y):is(pl(1,y),<y>suc)
t3:=tris2(nat,pl(1,y),pl(y,1),<y>suc,t2,t1):prop1(1,y)
[p:prop1(x,y)]
t4:=tris(nat,<pl(x,y)>suc,<pl(y,x)>suc,pl(y,<x>suc),ax2(pl(x,y),pl(y,x),p),satz4f(y,x)):is(<pl(x,y)>suc,pl(y,<x>suc))
t5:=satz4d:is(pl(<x>suc,y),<pl(x,y)>suc)
t6:=tris(nat,pl(<x>suc,y),<pl(x,y)>suc,pl(y,<x>suc),t5,t4):prop1(<x>suc,y)
-26
y@satz6:=induction([z:nat]prop1".26"(z,y),t3".26",[z:nat][u:prop1".26"(z,y)]t6".26"(z,y,u),x):is(pl(x,y),pl(y,x))
compl:=satz6:is(pl(x,y),pl(y,x))
+*26
x@t7:=tris(nat,pl(x,1),<x>suc,pl(1,x),satz4a,satz4g):prop1(1)
y@[p:prop1(y)]
t8:=tr3is(nat,pl(x,<y>suc),<pl(x,y)>suc,<pl(y,x)>suc,pl(<y>suc,x),satz4b,ax2(pl(x,y),pl(y,x),p),satz4h(y,x)):prop1(<y>suc)
y@anders:=induction([z:nat]prop1(z),t7,[z:nat][u:prop1(z)]t8(z,u),y):is(pl(x,y),pl(y,x))
-26
+27
y@prop1:=nis(y,pl(x,y)):'prop'
x@t1:=symnotis(nat,<x>suc,1,<x>ax3):nis(1,<x>suc)
t2:=th4"e.notis"(nat,1,<x>suc,pl(x,1),t1,satz4a):prop1(1)
y@[p:prop1(y)]
t3:=satz1(y,pl(x,y),p):nis(<y>suc,<pl(x,y)>suc)
t4:=th4"e.notis"(nat,<y>suc,<pl(x,y)>suc,pl(x,<y>suc),t3,satz4b):prop1(<y>suc)
-27
y@satz7:=induction([z:nat]prop1".27"(z),t2".27",[z:nat][u:prop1".27"(z)]t4".27"(z,u),y):nis(y,pl(x,y))
z@[n:nis(y,z)]
+28
prop1:=nis(pl(x,y),pl(x,z)):'prop'
t1:=satz1(y,z,n):nis(<y>suc,<z>suc)
t2:=th5"e.notis"(nat,<y>suc,<z>suc,pl(1,y),pl(1,z),t1,satz4g(y),satz4g(z)):prop1(1,y,z,n)
[p:prop1(x,y,z,n)]
t3:=satz1(pl(x,y),pl(x,z),p):nis(<pl(x,y)>suc,<pl(x,z)>suc)
t4:=th5"e.notis"(nat,<pl(x,y)>suc,<pl(x,z)>suc,pl(<x>suc,y),pl(<x>suc,z),t3,satz4h,satz4h(z)):prop1(<x>suc,y,z,n)
-28
satz8:=induction([u:nat]prop1".28"(u,y,z,n),t2".28",[u:nat][v:prop1".28"(u,y,z,n)]t4".28"(u,y,z,n,v),x):nis(pl(x,y),pl(x,z))
z@[i:is(pl(x,y),pl(x,z))]
satz8a:=th7"l.imp"(is(y,z),nis(pl(x,y),pl(x,z)),weli(is(pl(x,y),pl(x,z)),i),[u:nis(y,z)]satz8(u)):is(y,z)
z@diffprop:=is(x,pl(y,z)):'prop'
+*28
y@[u:nat][v:nat][du:diffprop(u)][dv:diffprop(v)]
t5:=satz8a(y,u,v,tris1(nat,pl(y,u),pl(y,v),x,du,dv)):is(u,v)
-28
y@satz8b:=[u:nat][v:nat][du:diffprop(u)][dv:diffprop(v)]t5".28"(u,v,du,dv):amone(nat,[z:nat]is(x,pl(y,z)))
+29
i:=is(x,y):'prop'
ii:=some([u:nat]diffprop(x,y,u)):'prop'
iii:=some([v:nat]diffprop(y,x,v)):'prop'
[one1:i][u:nat]
t1:=tris(nat,pl(u,x),pl(x,u),pl(y,u),compl(u,x),ispl1(u,one1)):is(pl(u,x),pl(y,u))
t2:=th3"e.notis"(nat,x,pl(u,x),pl(y,u),satz7(u,x),t1):nis(x,pl(y,u))
one1@t3:=th5"l.some"(nat,[u:nat]diffprop(u),[u:nat]t2(u)):not(ii)
y@t4:=th1"l.ec"(i,ii,[z:i]t3(z)):ec(i,ii)
one1@t5:=t3(y,x,symis(nat,x,y,one1)):not(iii)
y@t6:=th2"l.ec"(iii,i,[z:i]t5(z)):ec(iii,i)
[two1:ii][three1:iii][u:nat][du:diffprop(x,y,u)][v:nat][dv:diffprop(y,x,v)]
t6a:=tr4is(nat,x,pl(y,u),pl(pl(x,v),u),pl(x,pl(v,u)),pl(pl(v,u),x),du,ispl1(y,pl(x,v),u,dv),asspl1(x,v,u),compl(x,pl(v,u))):is(x,pl(pl(v,u),x))
t7:=mp(is(x,pl(pl(v,u),x)),con,t6a,satz7(pl(v,u),x)):con
du@t8:=someapp(nat,[v:nat]diffprop(y,x,v),three1,con,[v:nat][dv:diffprop(y,x,v)]t7(v,dv)):con
three1@t9:=someapp(nat,[u:nat]diffprop(u),two1,con,[u:nat][du:diffprop(u)]t8(u,du)):con
two1@t10:=[z:iii]t9(z):not(iii)
y@t11:=th1"l.ec"(ii,iii,[z:ii]t10(z)):ec(ii,iii)
a:=th6"l.ec3"(i,ii,iii,t4,t11,t6):ec3(i,ii,iii)
prop1:=or3(i,ii,iii):'prop'
x@[j:is(x,1)]
t12:=or3i1(i(1),ii(1),iii(1),j):prop1(1)
x@[n:nis(x,1)][u:nat][j:is(x,<u>suc)]
t13:=tris(nat,x,<u>suc,pl(1,u),j,satz4g(u)):is(x,pl(1,u))
t14:=somei(nat,[z:nat]diffprop(x,1,z),u,t13):ii(1)
t15:=someapp(nat,[u1:nat]is(x,<u1>suc),satz3(x,n),ii(1),[u1:nat][z:is(x,<u1>suc)]t14(u1,z)):ii(1)
t16:=or3i2(i(1),ii(1),iii(1),t15):prop1(1)
n@t16a:=someapp(nat,[u:nat]is(x,<u>suc),satz3(x,n),prop1(1),[u:nat][v:is(x,<u>suc)]t16(u,v)):prop1(1)
x@t17:=th1"l.imp"(is(x,1),prop1(1),[z:is(x,1)]t12(z),[z:nis(x,1)]t16a(z)):prop1(1)
y@[p:prop1(y)][one1:i(y)]
t18:=tris(nat,<y>suc,pl(y,1),pl(x,1),satz4e(y),ispl1(y,x,1,symis(nat,x,y,one1))):is(<y>suc,pl(x,1))
t19:=somei(nat,[z:nat]diffprop(<y>suc,x,z),1,t18):iii(<y>suc)
t20:=or3i3(i(<y>suc),ii(<y>suc),iii(<y>suc),t19):prop1(<y>suc)
p@[two1:ii(y)][u:nat][du:diffprop(x,y,u)][j:is(u,1)]
t21:=tr3is(nat,x,pl(y,u),pl(y,1),<y>suc,du,ispl2(u,1,y,j),satz4a(y)):is(x,<y>suc)
t22:=or3i1(i(<y>suc),ii(<y>suc),iii(<y>suc),t21):prop1(<y>suc)
du@[n:nis(u,1)][w:nat][j:is(u,<w>suc)]
t23:=tris(nat,u,<w>suc,pl(1,w),j,satz4g(w)):is(u,pl(1,w))
t24:=tr4is(nat,x,pl(y,u),pl(y,pl(1,w)),pl(pl(y,1),w),pl(<y>suc,w),du,ispl2(u,pl(1,w),y,t23),asspl2(y,1,w),ispl1(pl(y,1),<y>suc,w,satz4a(y))):is(x,pl(<y>suc,w))
t25:=somei(nat,[z:nat]diffprop(x,<y>suc,z),w,t24):ii(<y>suc)
n@t26:=someapp(nat,[z:nat]is(u,<z>suc),satz3(u,n),ii(<y>suc),[z:nat][v:is(u,<z>suc)]t25(z,v)):ii(<y>suc)
t27:=or3i2(i(<y>suc),ii(<y>suc),iii(<y>suc),t26):prop1(<y>suc)
du@t28:=th1"l.imp"(is(u,1),prop1(<y>suc),[z:is(u,1)]t22(z),[z:nis(u,1)]t27(z)):prop1(<y>suc)
two1@t28a:=someapp(nat,[u:nat]diffprop(u),two1,prop1(<y>suc),[u:nat][du:diffprop(u)]t28(u,du)):prop1(<y>suc)
p@[three1:iii(y)][v:nat][dv:diffprop(y,x,v)]
t29:=tris(nat,<y>suc,<pl(x,v)>suc,pl(x,<v>suc),ax2(y,pl(x,v),dv),satz4f(x,v)):is(<y>suc,pl(x,<v>suc))
t30:=somei(nat,[z:nat]diffprop(<y>suc,x,z),<v>suc,t29):iii(<y>suc)
three1@t31:=someapp(nat,[v:nat]diffprop(y,x,v),three1,iii(<y>suc),[v:nat][dv:diffprop(y,x,v)]t30(v,dv)):iii(<y>suc)
t32:=or3i3(i(<y>suc),ii(<y>suc),iii(<y>suc),t31):prop1(<y>suc)
p@t33:=or3app(i(y),ii(y),iii(y),prop1(<y>suc),p,[z:i(y)]t20(z),[z:ii(y)]t28a(z),[z:iii(y)]t32(z)):prop1(<y>suc)
y@b:=induction([z:nat]prop1(z),t17,[z:nat][u:prop1(z)]t33(z,u),y):or3(i,ii,iii)
-29
satz9:=orec3i(i".29",ii".29",iii".29",b".29",a".29"):orec3(is(x,y),some([u:nat]is(x,pl(y,u))),some([v:nat]is(y,pl(x,v))))
satz9a:=b".29":or3(is(x,y),some([u:nat]diffprop(x,y,u)),some([v:nat]diffprop(y,x,v)))
satz9b:=a".29":ec3(is(x,y),some([u:nat]diffprop(x,y,u)),some([v:nat]diffprop(y,x,v)))
more:=some([u:nat]diffprop(x,y,u)):'prop'
less:=some([v:nat]diffprop(y,x,v)):'prop'
satz10:=satz9:orec3(is(x,y),more(x,y),less(x,y))
satz10a:=satz9a:or3(is(x,y),more(x,y),less(x,y))
satz10b:=satz9b:ec3(is(x,y),more(x,y),less(x,y))
[m:more(x,y)]
satz11:=m:less(y,x)
y@[l:less(x,y)]
satz12:=l:more(y,x)
y@moreis:=or(more,is(x,y)):'prop'
lessis:=or(less,is(x,y)):'prop'
[m:moreis(x,y)]
satz13:=th9"l.or"(more,is(x,y),less(y,x),is(y,x),m,[z:more]satz11(z),[z:is(x,y)]symis(nat,x,y,z)):lessis(y,x)
y@[l:lessis(x,y)]
satz14:=th9"l.or"(less,is(x,y),more(y,x),is(y,x),l,[z:less]satz12(z),[z:is(x,y)]symis(nat,x,y,z)):moreis(y,x)
z@[i:is(x,y)][m:more(x,z)]
ismore1:=isp(nat,[u:nat]more(u,z),x,y,m,i):more(y,z)
i@[m:more(z,x)]
ismore2:=isp(nat,[u:nat]more(z,u),x,y,m,i):more(z,y)
i@[l:less(x,z)]
isless1:=isp(nat,[u:nat]less(u,z),x,y,l,i):less(y,z)
i@[l:less(z,x)]
isless2:=isp(nat,[u:nat]less(z,u),x,y,l,i):less(z,y)
i@[m:moreis(x,z)]
ismoreis1:=isp(nat,[u:nat]moreis(u,z),x,y,m,i):moreis(y,z)
i@[m:moreis(z,x)]
ismoreis2:=isp(nat,[u:nat]moreis(z,u),x,y,m,i):moreis(z,y)
i@[l:lessis(x,z)]
islessis1:=isp(nat,[u:nat]lessis(u,z),x,y,l,i):lessis(y,z)
i@[l:lessis(z,x)]
islessis2:=isp(nat,[u:nat]lessis(z,u),x,y,l,i):lessis(z,y)
y@[i:is(x,y)]
moreisi2:=ori2(more(x,y),is(x,y),i):moreis(x,y)
lessisi2:=ori2(less(x,y),is(x,y),i):lessis(x,y)
y@[m:more(x,y)]
moreisi1:=ori1(more(x,y),is(x,y),m):moreis(x,y)
y@[l:less(x,y)]
lessisi1:=ori1(less(x,y),is(x,y),l):lessis(x,y)
z@[u:nat][i:is(x,y)][j:is(z,u)][m:more(x,z)]
ismore12:=ismore2(z,u,y,j,ismore1(x,y,z,i,m)):more(y,u)
j@[l:less(x,z)]
isless12:=isless2(z,u,y,j,isless1(x,y,z,i,l)):less(y,u)
j@[m:moreis(x,z)]
ismoreis12:=ismoreis2(z,u,y,j,ismoreis1(x,y,z,i,m)):moreis(y,u)
j@[l:lessis(x,z)]
islessis12:=islessis2(z,u,y,j,islessis1(x,y,z,i,l)):lessis(y,u)
y@[m:moreis(x,y)]
satz10c:=th7"l.ec3"(is(x,y),more(x,y),less(x,y),satz10b,comor(more(x,y),is(x,y),m)):not(less(x,y))
y@[l:lessis(x,y)]
satz10d:=th9"l.ec3"(is(x,y),more(x,y),less(x,y),satz10b,l):not(more(x,y))
y@[n:not(more(x,y))]
satz10e:=th2"l.or3"(is(x,y),more(x,y),less(x,y),satz10a,n):lessis(x,y)
y@[n:not(less(x,y))]
satz10f:=comor(is(x,y),more(x,y),th3"l.or3"(is(x,y),more(x,y),less(x,y),satz10a,n)):moreis(x,y)
y@[m:more(x,y)]
satz10g:=th3"l.or"(less(x,y),is(x,y),ec3e23(is(x,y),more(x,y),less(x,y),satz10b,m),ec3e21(is(x,y),more(x,y),less(x,y),satz10b,m)):not(lessis(x,y))
y@[l:less(x,y)]
satz10h:=th3"l.or"(more(x,y),is(x,y),ec3e32(is(x,y),more(x,y),less(x,y),satz10b,l),ec3e31(is(x,y),more(x,y),less(x,y),satz10b,l)):not(moreis(x,y))
y@[n:not(moreis(x,y))]
satz10j:=or3e3(is(x,y),more(x,y),less(x,y),satz10a,th5"l.or"(more(x,y),is(x,y),n),th4"l.or"(more(x,y),is(x,y),n)):less(x,y)
y@[n:not(lessis(x,y))]
satz10k:=or3e2(is(x,y),more(x,y),less(x,y),satz10a,th4"l.or"(less(x,y),is(x,y),n),th5"l.or"(less(x,y),is(x,y),n)):more(x,y)
z@[l:less(x,y)][k:less(y,z)]
+315
[v:nat][dv:diffprop(y,x,v)][w:nat][dw:diffprop(z,y,w)]
t1:=tr3is(nat,z,pl(y,w),pl(pl(x,v),w),pl(x,pl(v,w)),dw,ispl1(y,pl(x,v),w,dv),asspl1(x,v,w)):is(z,pl(x,pl(v,w)))
t2:=somei(nat,[u:nat]diffprop(z,x,u),pl(v,w),t1):less(x,z)
dv@t3:=someapp(nat,[w:nat]diffprop(z,y,w),k,less(x,z),[w:nat][dw:diffprop(z,y,w)]t2(w,dw)):less(x,z)
-315
satz15:=someapp(nat,[v:nat]diffprop(y,x,v),l,less(x,z),[v:nat][dv:diffprop(y,x,v)]t3".315"(v,dv)):less(x,z)
trless:=satz15:less(x,z)
z@[m:more(x,y)][n:more(y,z)]
trmore:=satz15(z,y,x,n,m):more(x,z)
+*315
n@anders:=satz12(z,x,satz15(z,y,x,satz11(y,z,n),satz11(m))):more(x,z)
-315
z@[l:lessis(x,y)][k:less(y,z)]
satz16a:=orapp(less(x,y),is(x,y),less(x,z),l,[u:less(x,y)]trless(u,k),[u:is(x,y)]isless1(y,x,z,symis(nat,x,y,u),k)):less(x,z)
z@[l:less(x,y)][k:lessis(y,z)]
satz16b:=orapp(less(y,z),is(y,z),less(x,z),k,[u:less(y,z)]trless(l,u),[u:is(y,z)]isless2(y,z,x,u,l)):less(x,z)
z@[m:moreis(x,y)][n:more(y,z)]
satz16c:=satz16b(z,y,x,n,satz13(m)):more(x,z)
z@[m:more(x,y)][n:moreis(y,z)]
satz16d:=satz16a(z,y,x,satz13(y,z,n),m):more(x,z)
z@[l:lessis(x,y)][k:lessis(y,z)]
+317
[i:is(x,y)][j:is(y,z)]
t1:=lessisi2(x,z,tris(nat,x,y,z,i,j)):lessis(x,z)
i@[j:less(y,z)]
t2:=lessisi1(x,z,satz16a(l,j)):lessis(x,z)
i@t3:=orapp(less(y,z),is(y,z),lessis(x,z),k,[u:less(y,z)]t2(u),[u:is(y,z)]t1(u)):lessis(x,z)
k@[j:less(x,y)]
t4:=lessisi1(x,z,satz16b(j,k)):lessis(x,z)
-317
satz17:=orapp(less(x,y),is(x,y),lessis(x,z),l,[u:less(x,y)]t4".317"(u),[u:is(x,y)]t3".317"(u)):lessis(x,z)
+*317
k@[j:less(x,y)]
t5:=lessisi1(x,z,satz16b(j,k)):lessis(x,z)
k@[i:is(x,y)]
t6:=islessis1(y,x,z,symis(nat,x,y,i),k):lessis(x,z)
k@anders:=orapp(less(x,y),is(x,y),lessis(x,z),l,[u:less(x,y)]t5(u),[u:is(x,y)]t6(u)):lessis(x,z)
-317
k@trlessis:=satz17:lessis(x,z)
z@[m:moreis(x,y)][n:moreis(y,z)]
trmoreis:=satz14(z,x,satz17(z,y,x,satz13(y,z,n),satz13(m))):moreis(x,z)
y@satz18:=somei(nat,[u:nat]diffprop(pl(x,y),x,u),y,refis(nat,pl(x,y))):more(pl(x,y),x)
satz18a:=satz18:less(x,pl(x,y))
x@satz18b:=ismore1(pl(x,1),<x>suc,x,satz4a,satz18(1)):more(<x>suc,x)
satz18c:=satz18b:less(x,<x>suc)
z@[m:more(x,y)]
+319
[u:nat][du:diffprop(u)]
t1:=tris(nat,x,pl(y,u),pl(u,y),du,compl(y,u)):is(x,pl(u,y))
t2:=tr3is(nat,pl(x,z),pl(pl(u,y),z),pl(u,pl(y,z)),pl(pl(y,z),u),ispl1(x,pl(u,y),z,t1),asspl1(u,y,z),compl(u,pl(y,z))):is(pl(x,z),pl(pl(y,z),u))
t3:=somei(nat,[v:nat]diffprop(pl(x,z),pl(y,z),v),u,t2):more(pl(x,z),pl(y,z))
-319
satz19a:=someapp(nat,[u:nat]diffprop(u),m,more(pl(x,z),pl(y,z)),[u:nat][v:diffprop(u)]t3".319"(u,v)):more(pl(x,z),pl(y,z))
z@[i:is(x,y)]
satz19b:=ispl1(x,y,z,i):is(pl(x,z),pl(y,z))
z@[l:less(x,y)]
satz19c:=satz11(pl(y,z),pl(x,z),satz19a(y,x,z,satz12(x,y,l))):less(pl(x,z),pl(y,z))
+*319
l@anders1:=satz19a(y,x,z,l):less(pl(x,z),pl(y,z))
-319
m@satz19d:=ismore12(pl(x,z),pl(z,x),pl(y,z),pl(z,y),compl(x,z),compl(y,z),satz19a):more(pl(z,x),pl(z,y))
i@satz19e:=ispl2(x,y,z,i):is(pl(z,x),pl(z,y))
l@satz19f:=isless12(pl(x,z),pl(z,x),pl(y,z),pl(z,y),compl(x,z),compl(y,z),satz19c):less(pl(z,x),pl(z,y))
+*319
l@anders2:=satz19d(y,x,z,l):less(pl(z,x),pl(z,y))
-319
z@[u:nat][i:is(x,y)][m:more(z,u)]
satz19g:=ismore2(pl(x,u),pl(y,u),pl(x,z),ispl1(x,y,u,i),satz19d(z,u,x,m)):more(pl(x,z),pl(y,u))
satz19h:=ismore12(pl(x,z),pl(z,x),pl(y,u),pl(u,y),compl(x,z),compl(y,u),satz19g):more(pl(z,x),pl(u,y))
i@[l:less(z,u)]
satz19j:=isless2(pl(x,u),pl(y,u),pl(x,z),ispl1(x,y,u,i),satz19f(z,u,x,l)):less(pl(x,z),pl(y,u))
satz19k:=isless12(pl(x,z),pl(z,x),pl(y,u),pl(u,y),compl(x,z),compl(y,u),satz19j):less(pl(z,x),pl(u,y))
z@[m:moreis(x,y)]
+*319
m@[n:more(x,y)]
t4:=moreisi1(pl(x,z),pl(y,z),satz19a(n)):moreis(pl(x,z),pl(y,z))
m@[i:is(x,y)]
t5:=moreisi2(pl(x,z),pl(y,z),ispl1(x,y,z,i)):moreis(pl(x,z),pl(y,z))
-319
m@satz19l:=orapp(more(x,y),is(x,y),moreis(pl(x,z),pl(y,z)),m,[u:more(x,y)]t4".319"(u),[u:is(x,y)]t5".319"(u)):moreis(pl(x,z),pl(y,z))
satz19m:=ismoreis12(pl(x,z),pl(z,x),pl(y,z),pl(z,y),compl(x,z),compl(y,z),satz19l):moreis(pl(z,x),pl(z,y))
z@[l:lessis(x,y)]
satz19n:=satz13(pl(y,z),pl(x,z),satz19l(y,x,z,satz14(l))):lessis(pl(x,z),pl(y,z))
satz19o:=satz13(pl(z,y),pl(z,x),satz19m(y,x,z,satz14(l))):lessis(pl(z,x),pl(z,y))
+320
z@t1:=satz10a(x,y):or3(is(x,y),more(x,y),less(x,y))
t2:=satz10b(pl(x,z),pl(y,z)):ec3(is(pl(x,z),pl(y,z)),more(pl(x,z),pl(y,z)),less(pl(x,z),pl(y,z)))
-320
z@[m:more(pl(x,z),pl(y,z))]
satz20a:=th11"l.ec3"(is(x,y),more(x,y),less(x,y),is(pl(x,z),pl(y,z)),more(pl(x,z),pl(y,z)),less(pl(x,z),pl(y,z)),t1".320",t2".320",[u:is(x,y)]satz19b(x,y,z,u),[u:more(x,y)]satz19a(x,y,z,u),[u:less(x,y)]satz19c(x,y,z,u),m):more(x,y)
z@[i:is(pl(x,z),pl(y,z))]
satz20b:=th10"l.ec3"(is(x,y),more(x,y),less(x,y),is(pl(x,z),pl(y,z)),more(pl(x,z),pl(y,z)),less(pl(x,z),pl(y,z)),t1".320",t2".320",[u:is(x,y)]satz19b(x,y,z,u),[u:more(x,y)]satz19a(x,y,z,u),[u:less(x,y)]satz19c(x,y,z,u),i):is(x,y)
z@[l:less(pl(x,z),pl(y,z))]
satz20c:=th12"l.ec3"(is(x,y),more(x,y),less(x,y),is(pl(x,z),pl(y,z)),more(pl(x,z),pl(y,z)),less(pl(x,z),pl(y,z)),t1".320",t2".320",[u:is(x,y)]satz19b(x,y,z,u),[u:more(x,y)]satz19a(x,y,z,u),[u:less(x,y)]satz19c(x,y,z,u),l):less(x,y)
+*320
i@t3:=tr3is(nat,pl(z,x),pl(x,z),pl(y,z),pl(z,y),compl(z,x),i,compl(y,z)):is(pl(z,x),pl(z,y))
andersb:=satz8a(z,x,y,t3):is(x,y)
l@andersc:=satz20a(y,x,z,l):less(x,y)
-320
z@[m:more(pl(z,x),pl(z,y))]
satz20d:=satz20a(ismore12(pl(z,x),pl(x,z),pl(z,y),pl(y,z),compl(z,x),compl(z,y),m)):more(x,y)
z@[i:is(pl(z,x),pl(z,y))]
satz20e:=satz20b(tr3is(nat,pl(x,z),pl(z,x),pl(z,y),pl(y,z),compl(x,z),i,compl(z,y))):is(x,y)
z@[l:less(pl(z,x),pl(z,y))]
satz20f:=satz20c(isless12(pl(z,x),pl(x,z),pl(z,y),pl(y,z),compl(z,x),compl(z,y),l)):less(x,y)
u@[m:more(x,y)][n:more(z,u)]
+321
t1:=satz19a(x,y,z,m):more(pl(x,z),pl(y,z))
t2:=ismore12(pl(z,y),pl(y,z),pl(u,y),pl(y,u),compl(z,y),compl(u,y),satz19a(z,u,y,n)):more(pl(y,z),pl(y,u))
-321
satz21:=trmore(pl(x,z),pl(y,z),pl(y,u),t1".321",t2".321"):more(pl(x,z),pl(y,u))
+*321
n@anders:=trmore(pl(x,z),pl(y,z),pl(y,u),satz19a(x,y,z,m),satz19d(z,u,y,n)):more(pl(x,z),pl(y,u))
-321
u@[l:less(x,y)][k:less(z,u)]
satz21a:=satz21(y,x,u,z,l,k):less(pl(x,z),pl(y,u))
+*321
k@andersa:=satz11(pl(y,u),pl(x,z),satz21(y,x,u,z,satz12(x,y,l),satz12(z,u,k))):less(pl(x,z),pl(y,u))
-321
u@[m:moreis(x,y)][n:more(z,u)]
satz22a:=orapp(more(x,y),is(x,y),more(pl(x,z),pl(y,u)),m,[v:more(x,y)]satz21(v,n),[v:is(x,y)]satz19g(u,v,n)):more(pl(x,z),pl(y,u))
u@[m:more(x,y)][n:moreis(z,u)]
satz22b:=orapp(more(z,u),is(z,u),more(pl(x,z),pl(y,u)),n,[v:more(z,u)]satz21(m,v),[v:is(z,u)]satz19h(z,u,x,y,v,m)):more(pl(x,z),pl(y,u))
u@[l:lessis(x,y)][k:less(z,u)]
satz22c:=satz22a(y,x,u,z,satz14(x,y,l),k):less(pl(x,z),pl(y,u))
u@[l:less(x,y)][k:lessis(z,u)]
satz22d:=satz22b(y,x,u,z,l,satz14(z,u,k)):less(pl(x,z),pl(y,u))
u@[m:moreis(x,y)][n:moreis(z,u)]
+323
[i:is(x,y)][j:is(z,u)]
t1:=moreisi2(pl(x,z),pl(y,u),tris(nat,pl(x,z),pl(y,z),pl(y,u),ispl1(x,y,z,i),ispl2(z,u,y,j))):moreis(pl(x,z),pl(y,u))
i@[o:more(z,u)]
t2:=moreisi1(pl(x,z),pl(y,u),satz22a(m,o)):moreis(pl(x,z),pl(y,u))
i@t3:=orapp(more(z,u),is(z,u),moreis(pl(x,z),pl(y,u)),n,[v:more(z,u)]t2(v),[v:is(z,u)]t1(v)):moreis(pl(x,z),pl(y,u))
n@[o:more(x,y)]
t4:=moreisi1(pl(x,z),pl(y,u),satz22b(o,n)):moreis(pl(x,z),pl(y,u))
-323
satz23:=orapp(more(x,y),is(x,y),moreis(pl(x,z),pl(y,u)),m,[v:more(x,y)]t4".323"(v),[v:is(x,y)]t3".323"(v)):moreis(pl(x,z),pl(y,u))
+*323
n@[o:more(x,y)]
t5:=moreisi1(pl(x,z),pl(y,u),satz22b(o,n)):moreis(pl(x,z),pl(y,u))
n@[i:is(x,y)]
t6:=ismoreis2(pl(x,u),pl(y,u),pl(x,z),ispl1(u,i),satz19m(z,u,x,n)):moreis(pl(x,z),pl(y,u))
n@anders:=orapp(more(x,y),is(x,y),moreis(pl(x,z),pl(y,u)),m,[v:more(x,y)]t5(v),[v:is(x,y)]t6(v)):moreis(pl(x,z),pl(y,u))
-323
u@[l:lessis(x,y)][k:lessis(z,u)]
satz23a:=satz13(pl(y,u),pl(x,z),satz23(y,x,u,z,satz14(l),satz14(z,u,k))):lessis(pl(x,z),pl(y,u))
+324
x@[n:nis(x,1)][u:nat][i:is(x,<u>suc)]
t1:=tris(nat,x,<u>suc,pl(1,u),i,satz4g(u)):is(x,pl(1,u))
t2:=ismore1(pl(1,u),x,1,symis(nat,x,pl(1,u),t1),satz18(1,u)):more(x,1)
n@t3:=someapp(nat,[u:nat]is(x,<u>suc),satz3(x,n),more(x,1),[u:nat][v:is(x,<u>suc)]t2(u,v)):more(x,1)
-324
x@satz24:=th2"l.or"(more(x,1),is(x,1),[u:nis(x,1)]t3".324"(u)):moreis(x,1)
satz24a:=satz13(x,1,satz24):lessis(1,x)
satz24b:=t3".324"(<x>suc,<x>ax3):more(<x>suc,1)
satz24c:=satz24b:less(1,<x>suc)
y@[m:more(y,x)]
+325
[u:nat][du:diffprop(y,x,u)]
t1:=satz19m(u,1,x,satz24(u)):moreis(pl(x,u),pl(x,1))
t2:=ismoreis1(pl(x,u),y,pl(x,1),symis(nat,y,pl(x,u),du),t1):moreis(y,pl(x,1))
-325
satz25:=someapp(nat,[u:nat]diffprop(y,x,u),m,moreis(y,pl(x,1)),[u:nat][v:diffprop(y,x,u)]t2".325"(u,v)):moreis(y,pl(x,1))
satz25a:=ismoreis2(pl(x,1),<x>suc,y,satz4a,satz25):moreis(y,<x>suc)
y@[l:less(y,x)]
satz25b:=satz13(x,pl(y,1),satz25(y,x,l)):lessis(pl(y,1),x)
satz25c:=islessis1(pl(y,1),<y>suc,x,satz4a(y),satz25b):lessis(<y>suc,x)
y@[l:less(y,pl(x,1))]
+326
[m:more(y,x)]
t1:=satz25(m):moreis(y,pl(x,1))
l@t2:=th3"l.imp"(more(y,x),moreis(y,pl(x,1)),satz10h(y,pl(x,1),l),[v:more(y,x)]t1(v)):not(more(y,x))
-326
satz26:=satz10e(y,x,t2".326"):lessis(y,x)
y@[l:less(y,<x>suc)]
satz26a:=satz26(isless2(<x>suc,pl(x,1),y,satz4e,l)):lessis(y,x)
y@[m:more(pl(y,1),x)]
satz26b:=satz14(x,y,satz26(y,x,m)):moreis(y,x)
y@[m:more(<y>suc,x)]
satz26c:=satz26b(ismore1(<y>suc,pl(y,1),x,satz4e(y),m)):moreis(y,x)
@[p:[x:nat]'prop'][n:nat]
+327
[m:nat]
lbprop:=imp(<m>p,lessis(n,m)):'prop'
-327
lb:=all([x:nat]lbprop".327"(x)):'prop'
min:=and(lb,<n>p):'prop'
p@[s:some(p)]
+*327
s@[n:nat]
t1:=[x:<n>p]satz24a(n):lbprop(1,n)
s@t2:=[x:nat]t1(x):lb(1)
[l:[x:nat]lb(x)][y:nat][yp:<y>p]
t3:=satz18(y,1):more(pl(y,1),y)
t4:=satz10g(pl(y,1),y,t3):not(lessis(pl(y,1),y))
t5:=th4"l.imp"(<y>p,lessis(pl(y,1),y),yp,t4):not(lbprop(pl(y,1),y))
t6:=th1"l.all"(nat,[x:nat]lbprop(pl(y,1),x),y,t5):not(lb(pl(y,1)))
t7:=mp(lb(pl(y,1)),con,<pl(y,1)>l,t6):con
l@t8:=someapp(nat,p,s,con,[x:nat][y:<x>p]t7(x,y)):con
s@[n:non(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))))][m:nat][l:lb(m)]
t9:=<m>n:not(and(lb(m),not(lb(pl(m,1)))))
t10:=et(lb(pl(m,1)),th3"l.and"(lb(m),not(lb(pl(m,1))),t9,l)):lb(pl(m,1))
t11:=isp(nat,[x:nat]lb(x),pl(m,1),<m>suc,t10,satz4a(m)):lb(<m>suc)
n@t12:=[x:nat]induction([y:nat]lb(y),t2,[y:nat][z:lb(y)]t11(y,z),x):[x:nat]lb(x)
s@t13:=[x:non(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))))]t8(t12(x)):some([x:nat]and(lb(x),not(lb(pl(x,1)))))
[m:nat][a:and(lb(m),not(lb(pl(m,1))))]
t14:=ande1(lb(m),not(lb(pl(m,1))),a):lb(m)
t15:=ande2(lb(m),not(lb(pl(m,1))),a):not(lb(pl(m,1)))
[nmp:not(<m>p)][n:nat][np:<n>p]
t16:=mp(<n>p,lessis(m,n),np,<n>t14):lessis(m,n)
t17:=th3"l.imp"(is(m,n),<m>p,nmp,[x:is(m,n)]isp(nat,p,n,m,np,symis(nat,m,n,x))):not(is(m,n))
t18:=ore1(less(m,n),is(m,n),t16,t17):less(m,n)
t19:=satz25b(n,m,t18):lessis(pl(m,1),n)
nmp@t20:=[x:nat][y:<x>p]t19(x,y):lb(pl(m,1))
t21:=mp(lb(pl(m,1)),con,t20,t15):con
a@t22:=et(<m>p,[x:not(<m>p)]t21(x)):<m>p
t23:=andi(lb(m),<m>p,t14,t22):min(m)
-327
s@satz27:=th6"l.some"(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))),[x:nat]min(x),t13".327",[x:nat][y:and(lb(x),not(lb(pl(x,1))))]t23".327"(x,y)):some([x:nat]min(p,x))
+*327
p@[n:non(nat,[x:nat]min(x))][u:nat]
t24:=[x:<u>p]satz24a(u):lbprop(1,u)
n@t25:=[x:nat]t24(x):lb(1)
u@[l:lb(u)]
t26:=<u>n:not(min(u))
t27:=th3"l.and"(lb(u),<u>p,t26,l):not(<u>p)
[v:nat][vp:<v>p]
t28:=th3"l.imp"(is(u,v),<u>p,t27,[x:is(u,v)]isp1(nat,p,v,u,vp,x)):nis(u,v)
t29:=mp(<v>p,lessis(u,v),vp,<v>l):lessis(u,v)
t30:=ore1(less(u,v),is(u,v),t29,t28):less(u,v)
t31:=satz25c(v,u,t30):lessis(<u>suc,v)
v@t32:=[x:<v>p]t31(x):lbprop(<u>suc,v)
l@t33:=[x:nat]t32(x):lb(<u>suc)
u@t34:=induction([x:nat]lb(x),t25,[x:nat][y:lb(x)]t33(x,y),u):lb(u)
p@[s:some(p)][u:nat][up:<u>p]
t35:=satz10g(<u>suc,u,satz18b(u)):not(lessis(<u>suc,u))
t36:=th4"l.imp"(<u>p,lessis(<u>suc,u),up,t35):not(lbprop(<u>suc,u))
t37:=th1"l.all"(nat,[x:nat]lbprop(<u>suc,x),u,t36):not(lb(<u>suc))
t38:=[y:non(nat,[x:nat]min(x))]mp(lb(<u>suc),con,t34(y,<u>suc),t37):some([x:nat]min(x))
s@anders:=someapp(nat,p,s,some([x:nat]min(x)),[x:nat][y:<x>p]t38(x,y)):some([x:nat]min(x))
-327
+*327
p@[n:nat][m:nat][mn:min(p,n)][mm:min(p,m)]
t39:=ande1(lb(n),<n>p,mn):lb(n)
t40:=ande1(lb(m),<m>p,mm):lb(m)
t41:=ande2(lb(n),<n>p,mn):<n>p
t42:=ande2(lb(m),<m>p,mm):<m>p
t43:=<m>t39:lbprop(n,m)
t44:=<n>t40:lbprop(m,n)
t45:=mp(<m>p,lessis(n,m),t42,t43):lessis(n,m)
t46:=mp(<n>p,lessis(m,n),t41,t44):lessis(m,n)
t47:=ore2(more(n,m),is(n,m),satz14(m,n,t46),satz10d(n,m,t45)):is(n,m)
p@t48:=[x:nat][y:nat][u:min(x)][v:min(y)]t47(x,y,u,v):amone(nat,[x:nat]min(p,x))
-327
s@satz27a:=onei(nat,[x:nat]min(p,x),t48".327",satz27):one([x:nat]min(p,x))
+428
x@[f:[y:nat]nat]
prop1:=all([y:nat]is(<<y>suc>f,pl(<y>f,x))):'prop'
prop2:=and(is(<1>f,x),prop1):'prop'
x@[a:[y:nat]nat][b:[y:nat]nat][pa:prop2(a)][pb:prop2(b)][y:nat]
prop3:=is(<y>a,<y>b):'prop'
pb@t1:=ande1(is(<1>a,x),prop1(a),pa):is(<1>a,x)
t2:=ande1(is(<1>b,x),prop1(b),pb):is(<1>b,x)
t3:=tris2(nat,<1>a,<1>b,x,t1,t2):prop3(1)
y@[p:prop3(y)]
t4:=ispl1(<y>a,<y>b,x,p):is(pl(<y>a,x),pl(<y>b,x))
t5:=ande2(is(<1>a,x),prop1(a),pa):prop1(a)
t6:=ande2(is(<1>b,x),prop1(b),pb):prop1(b)
t7:=<y>t5:is(<<y>suc>a,pl(<y>a,x))
t8:=<y>t6:is(<<y>suc>b,pl(<y>b,x))
t9:=tr3is(nat,<<y>suc>a,pl(<y>a,x),pl(<y>b,x),<<y>suc>b,t7,t4,symis(nat,<<y>suc>b,pl(<y>b,x),t8)):prop3(<y>suc)
y@t10:=induction([z:nat]prop3(z),t3,[z:nat][u:prop3(z)]t9(z,u),y):prop3(y)
pb@t11:=fisi(nat,nat,a,b,[y:nat]t10(y)):is"e"([y:nat]nat,a,b)
x@a1:=[z:[y:nat]nat][u:[y:nat]nat][v:prop2(z)][w:prop2(u)]t11(z,u,v,w):amone([y:nat]nat,[z:[y:nat]nat]prop2(z))
prop4:=some"l"([y:nat]nat,[z:[y:nat]nat]prop2(z)):'prop'
@id:=[y:nat]y:[y:nat]nat
t12:=[x:nat]satz4e(x):prop1(1,id)
t13:=andi(is(<1>id,1),prop1(1,id),refis(nat,1),t12):prop2(1,id)
t14:=somei([y:nat]nat,[z:[y:nat]nat]prop2(1,z),id,t13):prop4(1)
x@[p:prop4(x)][f:[y:nat]nat][pf:prop2(f)]
g:=[y:nat]pl(<y>f,y):[y:nat]nat
t15:=ande1(is(<1>f,x),prop1(f),pf):is(<1>f,x)
t16:=tris(nat,<1>g,pl(x,1),<x>suc,ispl1(<1>f,x,1,t15),satz4a(x)):is(<1>g,<x>suc)
[y:nat]
t17:=ande2(is(<1>f,x),prop1(f),pf):prop1(f)
t18:=<y>t17:is(<<y>suc>f,pl(<y>f,x))
t19:=tris(nat,<<y>suc>g,pl(pl(<y>f,x),<y>suc),pl(<y>f,pl(x,<y>suc)),ispl1(<<y>suc>f,pl(<y>f,x),<y>suc,t18),asspl1(<y>f,x,<y>suc)):is(<<y>suc>g,pl(<y>f,pl(x,<y>suc)))
t20:=tr3is(nat,pl(x,<y>suc),<pl(x,y)>suc,pl(<x>suc,y),pl(y,<x>suc),satz4b(x,y),satz4h(x,y),compl(<x>suc,y)):is(pl(x,<y>suc),pl(y,<x>suc))
t21:=tr3is(nat,<<y>suc>g,pl(<y>f,pl(x,<y>suc)),pl(<y>f,pl(y,<x>suc)),pl(<y>g,<x>suc),t19,ispl2(pl(x,<y>suc),pl(y,<x>suc),<y>f,t20),asspl2(<y>f,y,<x>suc)):is(<<y>suc>g,pl(<y>g,<x>suc))
pf@t22:=[y:nat]t21(y):prop1(<x>suc,g)
t23:=andi(is(<1>g,<x>suc),prop1(<x>suc,g),t16,t22):prop2(<x>suc,g)
t24:=somei([y:nat]nat,[z:[y:nat]nat]prop2(<x>suc,z),g,t23):prop4(<x>suc)
p@t25:=someapp([y:nat]nat,[z:[y:nat]nat]prop2(z),p,prop4(<x>suc),[z:[y:nat]nat][u:prop2(z)]t24(z,u)):prop4(<x>suc)
x@b1:=induction([y:nat]prop4(y),t14,[y:nat][u:prop4(y)]t25(y,u),x):prop4(x)
-428
x@satz28:=onei([y:nat]nat,[z:[y:nat]nat]prop2".428"(z),a1".428",b1".428"):one"e"([y:nat]nat,[z:[y:nat]nat]and(is(<1>z,x),all([y:nat]is(<<y>suc>z,pl(<y>z,x)))))
times:=ind([y:nat]nat,[z:[y:nat]nat]prop2".428"(z),satz28):[y:nat]nat
y@ts:=<y>times:nat
+*428
x@t26:=oneax([y:nat]nat,[z:[y:nat]nat]prop2(z),satz28):prop2(times)
-428
x@satz28a:=ande1(is(<1>times,x),prop1".428"(times),t26".428"):is(ts(x,1),x)
+*428
x@t27:=ande2(is(<1>times,x),prop1(times),t26):prop1(times)
-428
y@satz28b:=<y>t27".428":is(ts(x,<y>suc),pl(ts(x,y),x))
+*428
@t28:=t11(1,times(1),id,t26(1),t13):is"e"([y:nat]nat,times(1),id)
-428
x@satz28c:=fise(nat,nat,times(1),id".428",t28".428",x):is(ts(1,x),x)
+*428
x@t29:=t11(<x>suc,times(<x>suc),[y:nat]pl(<y>times,y),t26(<x>suc),t23(b1,times,t26)):is"e"([y:nat]nat,times(<x>suc),[y:nat]pl(<y>times,y))
-428
y@satz28d:=fise(nat,nat,times(<x>suc),[z:nat]pl(<z>times,z),t29".428",y):is(ts(<x>suc,y),pl(ts(x,y),y))
x@satz28e:=symis(nat,ts(x,1),x,satz28a):is(x,ts(x,1))
y@satz28f:=symis(nat,ts(x,<y>suc),pl(ts(x,y),x),satz28b):is(pl(ts(x,y),x),ts(x,<y>suc))
x@satz28g:=symis(nat,ts(1,x),x,satz28c):is(x,ts(1,x))
y@satz28h:=symis(nat,ts(<x>suc,y),pl(ts(x,y),y),satz28d):is(pl(ts(x,y),y),ts(<x>suc,y))
z@[i:is(x,y)]
ists1:=isf(nat,nat,[u:nat]ts(u,z),x,y,i):is(ts(x,z),ts(y,z))
ists2:=isf(nat,nat,[u:nat]ts(z,u),x,y,i):is(ts(z,x),ts(z,y))
z@[u:nat][i:is(x,y)][j:is(z,u)]
ists12:=tris(nat,ts(x,z),ts(y,z),ts(y,u),ists1(i),ists2(z,u,y,j)):is(ts(x,z),ts(y,u))
+429
y@prop1:=is(ts(x,y),ts(y,x)):'prop'
t1:=satz28a(y):is(ts(y,1),y)
t2:=satz28c(y):is(ts(1,y),y)
t3:=tris2(nat,ts(1,y),ts(y,1),y,t2,t1):prop1(1,y)
[p:prop1(x,y)]
t4:=tris(nat,pl(ts(x,y),y),pl(ts(y,x),y),ts(y,<x>suc),ispl1(ts(x,y),ts(y,x),y,p),satz28f(y,x)):is(pl(ts(x,y),y),ts(y,<x>suc))
t5:=satz28d:is(ts(<x>suc,y),pl(ts(x,y),y))
t6:=tris(nat,ts(<x>suc,y),pl(ts(x,y),y),ts(y,<x>suc),t5,t4):prop1(<x>suc,y)
-429
y@satz29:=induction([z:nat]prop1".429"(z,y),t3".429",[z:nat][u:prop1".429"(z,y)]t6".429"(z,y,u),x):is(ts(x,y),ts(y,x))
comts:=satz29:is(ts(x,y),ts(y,x))
+*429
x@t7:=tris(nat,ts(x,1),x,ts(1,x),satz28a,satz28g):prop1(1)
y@[p:prop1(y)]
t8:=tr3is(nat,ts(x,<y>suc),pl(ts(x,y),x),pl(ts(y,x),x),ts(<y>suc,x),satz28b(x,y),ispl1(ts(x,y),ts(y,x),x,p),satz28h(y,x)):prop1(<y>suc)
y@anders:=induction([z:nat]prop1(z),t7,[z:nat][u:prop1(z)]t8(z,u),y):is(ts(x,y),ts(y,x))
-429
+430
z@prop1:=is(ts(x,pl(y,z)),pl(ts(x,y),ts(x,z))):'prop'
y@t1:=tr3is(nat,ts(x,pl(y,1)),ts(x,<y>suc),pl(ts(x,y),x),pl(ts(x,y),ts(x,1)),ists2(pl(y,1),<y>suc,x,satz4a(y)),satz28b,ispl2(x,ts(x,1),ts(x,y),satz28e(x))):prop1(1)
z@[p:prop1(z)]
t2:=tr3is(nat,ts(x,pl(y,<z>suc)),ts(x,<pl(y,z)>suc),pl(ts(x,pl(y,z)),x),pl(pl(ts(x,y),ts(x,z)),x),ists2(pl(y,<z>suc),<pl(y,z)>suc,x,satz4b(y,z)),satz28b(x,pl(y,z)),ispl1(ts(x,pl(y,z)),pl(ts(x,y),ts(x,z)),x,p)):is(ts(x,pl(y,<z>suc)),pl(pl(ts(x,y),ts(x,z)),x))
t3:=tr3is(nat,ts(x,pl(y,<z>suc)),pl(pl(ts(x,y),ts(x,z)),x),pl(ts(x,y),pl(ts(x,z),x)),pl(ts(x,y),ts(x,<z>suc)),t2,asspl1(ts(x,y),ts(x,z),x),ispl2(pl(ts(x,z),x),ts(x,<z>suc),ts(x,y),satz28f(x,z))):prop1(<z>suc)
-430
z@satz30:=induction([u:nat]prop1".430"(u),t1".430",[u:nat][v:prop1".430"(u)]t3".430"(u,v),z):is(ts(x,pl(y,z)),pl(ts(x,y),ts(x,z)))
disttp1:=tr3is(nat,ts(pl(x,y),z),ts(z,pl(x,y)),pl(ts(z,x),ts(z,y)),pl(ts(x,z),ts(y,z)),comts(pl(x,y),z),satz30(z,x,y),ispl12(ts(z,x),ts(x,z),ts(z,y),ts(y,z),comts(z,x),comts(z,y))):is(ts(pl(x,y),z),pl(ts(x,z),ts(y,z)))
disttp2:=satz30:is(ts(x,pl(y,z)),pl(ts(x,y),ts(x,z)))
distpt1:=symis(nat,ts(pl(x,y),z),pl(ts(x,z),ts(y,z)),disttp1):is(pl(ts(x,z),ts(y,z)),ts(pl(x,y),z))
distpt2:=symis(nat,ts(x,pl(y,z)),pl(ts(x,y),ts(x,z)),disttp2):is(pl(ts(x,y),ts(x,z)),ts(x,pl(y,z)))
+431
prop1:=is(ts(ts(x,y),z),ts(x,ts(y,z))):'prop'
y@t1:=tris(nat,ts(ts(x,y),1),ts(x,y),ts(x,ts(y,1)),satz28a(ts(x,y)),ists2(y,ts(y,1),x,satz28e(y))):prop1(1)
z@[p:prop1(z)]
t2:=tr4is(nat,ts(ts(x,y),<z>suc),pl(ts(ts(x,y),z),ts(x,y)),pl(ts(x,ts(y,z)),ts(x,y)),ts(x,pl(ts(y,z),y)),ts(x,ts(y,<z>suc)),satz28b(ts(x,y),z),ispl1(ts(ts(x,y),z),ts(x,ts(y,z)),ts(x,y),p),distpt2(x,ts(y,z),y),ists2(pl(ts(y,z),y),ts(y,<z>suc),x,satz28f(y,z))):prop1(<z>suc)
-431
satz31:=induction([u:nat]prop1".431"(u),t1".431",[u:nat][v:prop1".431"(u)]t2".431"(u,v),z):is(ts(ts(x,y),z),ts(x,ts(y,z)))
assts1:=satz31:is(ts(ts(x,y),z),ts(x,ts(y,z)))
assts2:=symis(nat,ts(ts(x,y),z),ts(x,ts(y,z)),assts1):is(ts(x,ts(y,z)),ts(ts(x,y),z))
[m:more(x,y)]
+432
[u:nat][du:diffprop(u)]
t1:=tris(nat,ts(x,z),ts(pl(y,u),z),pl(ts(y,z),ts(u,z)),ists1(x,pl(y,u),z,du),disttp1(y,u,z)):is(ts(x,z),pl(ts(y,z),ts(u,z)))
t2:=somei(nat,[v:nat]diffprop(ts(x,z),ts(y,z),v),ts(u,z),t1):more(ts(x,z),ts(y,z))
-432
satz32a:=someapp(nat,[u:nat]diffprop(u),m,more(ts(x,z),ts(y,z)),[u:nat][v:diffprop(u)]t2".432"(u,v)):more(ts(x,z),ts(y,z))
z@[i:is(x,y)]
satz32b:=ists1(x,y,z,i):is(ts(x,z),ts(y,z))
z@[l:less(x,y)]
satz32c:=satz11(ts(y,z),ts(x,z),satz32a(y,x,z,satz12(x,y,l))):less(ts(x,z),ts(y,z))
+*432
l@anders1:=satz32a(y,x,z,l):less(ts(x,z),ts(y,z))
-432
m@satz32d:=ismore12(ts(x,z),ts(z,x),ts(y,z),ts(z,y),comts(x,z),comts(y,z),satz32a):more(ts(z,x),ts(z,y))
i@satz32e:=ists2(x,y,z,i):is(ts(z,x),ts(z,y))
l@satz32f:=isless12(ts(x,z),ts(z,x),ts(y,z),ts(z,y),comts(x,z),comts(y,z),satz32c):less(ts(z,x),ts(z,y))
+*432
l@anders2:=satz32d(y,x,z,l):less(ts(z,x),ts(z,y))
-432
z@[u:nat][i:is(x,y)][m:more(z,u)]
satz32g:=ismore2(ts(x,u),ts(y,u),ts(x,z),ists1(x,y,u,i),satz32d(z,u,x,m)):more(ts(x,z),ts(y,u))
satz32h:=ismore12(ts(x,z),ts(z,x),ts(y,u),ts(u,y),comts(x,z),comts(y,u),satz32g):more(ts(z,x),ts(u,y))
i@[l:less(z,u)]
satz32j:=isless2(ts(x,u),ts(y,u),ts(x,z),ists1(x,y,u,i),satz32f(z,u,x,l)):less(ts(x,z),ts(y,u))
satz32k:=isless12(ts(x,z),ts(z,x),ts(y,u),ts(u,y),comts(x,z),comts(y,u),satz32j):less(ts(z,x),ts(u,y))
z@[m:moreis(x,y)]
+*432
m@[n:more(x,y)]
t3:=moreisi1(ts(x,z),ts(y,z),satz32a(n)):moreis(ts(x,z),ts(y,z))
m@[i:is(x,y)]
t4:=moreisi2(ts(x,z),ts(y,z),ists1(x,y,z,i)):moreis(ts(x,z),ts(y,z))
-432
m@satz32l:=orapp(more(x,y),is(x,y),moreis(ts(x,z),ts(y,z)),m,[u:more(x,y)]t3".432"(u),[u:is(x,y)]t4".432"(u)):moreis(ts(x,z),ts(y,z))
satz32m:=ismoreis12(ts(x,z),ts(z,x),ts(y,z),ts(z,y),comts(x,z),comts(y,z),satz32l):moreis(ts(z,x),ts(z,y))
z@[l:lessis(x,y)]
satz32n:=satz13(ts(y,z),ts(x,z),satz32l(y,x,z,satz14(l))):lessis(ts(x,z),ts(y,z))
satz32o:=satz13(ts(z,y),ts(z,x),satz32m(y,x,z,satz14(l))):lessis(ts(z,x),ts(z,y))
+433
z@t1:=satz10a(x,y):or3(is(x,y),more(x,y),less(x,y))
t2:=satz10b(ts(x,z),ts(y,z)):ec3(is(ts(x,z),ts(y,z)),more(ts(x,z),ts(y,z)),less(ts(x,z),ts(y,z)))
-433
z@[m:more(ts(x,z),ts(y,z))]
satz33a:=th11"l.ec3"(is(x,y),more(x,y),less(x,y),is(ts(x,z),ts(y,z)),more(ts(x,z),ts(y,z)),less(ts(x,z),ts(y,z)),t1".433",t2".433",[u:is(x,y)]satz32b(x,y,z,u),[u:more(x,y)]satz32a(x,y,z,u),[u:less(x,y)]satz32c(x,y,z,u),m):more(x,y)
z@[i:is(ts(x,z),ts(y,z))]
satz33b:=th10"l.ec3"(is(x,y),more(x,y),less(x,y),is(ts(x,z),ts(y,z)),more(ts(x,z),ts(y,z)),less(ts(x,z),ts(y,z)),t1".433",t2".433",[u:is(x,y)]satz32b(x,y,z,u),[u:more(x,y)]satz32a(x,y,z,u),[u:less(x,y)]satz32c(x,y,z,u),i):is(x,y)
z@[l:less(ts(x,z),ts(y,z))]
satz33c:=th12"l.ec3"(is(x,y),more(x,y),less(x,y),is(ts(x,z),ts(y,z)),more(ts(x,z),ts(y,z)),less(ts(x,z),ts(y,z)),t1".433",t2".433",[u:is(x,y)]satz32b(x,y,z,u),[u:more(x,y)]satz32a(x,y,z,u),[u:less(x,y)]satz32c(x,y,z,u),l):less(x,y)
+*433
l@anders:=satz33a(y,x,z,l):less(x,y)
-433
u@[m:more(x,y)][n:more(z,u)]
+434
t1:=satz32a(x,y,z,m):more(ts(x,z),ts(y,z))
t2:=ismore12(ts(z,y),ts(y,z),ts(u,y),ts(y,u),comts(z,y),comts(u,y),satz32a(z,u,y,n)):more(ts(y,z),ts(y,u))
-434
satz34:=trmore(ts(x,z),ts(y,z),ts(y,u),t1".434",t2".434"):more(ts(x,z),ts(y,u))
+*434
n@anders:=trmore(ts(x,z),ts(y,z),ts(y,u),satz32a(x,y,z,m),satz32d(z,u,y,n)):more(ts(x,z),ts(y,u))
-434
u@[l:less(x,y)][k:less(z,u)]
satz34a:=satz34(y,x,u,z,l,k):less(ts(x,z),ts(y,u))
+*434
k@andersa:=satz11(ts(y,u),ts(x,z),satz34(y,x,u,z,satz12(x,y,l),satz12(z,u,k))):less(ts(x,z),ts(y,u))
-434
u@[m:moreis(x,y)][n:more(z,u)]
satz35a:=orapp(more(x,y),is(x,y),more(ts(x,z),ts(y,u)),m,[v:more(x,y)]satz34(v,n),[v:is(x,y)]satz32g(u,v,n)):more(ts(x,z),ts(y,u))
u@[m:more(x,y)][n:moreis(z,u)]
satz35b:=orapp(more(z,u),is(z,u),more(ts(x,z),ts(y,u)),n,[v:more(z,u)]satz34(m,v),[v:is(z,u)]satz32h(z,u,x,y,v,m)):more(ts(x,z),ts(y,u))
u@[l:lessis(x,y)][k:less(z,u)]
satz35c:=satz35a(y,x,u,z,satz14(x,y,l),k):less(ts(x,z),ts(y,u))
u@[l:less(x,y)][k:lessis(z,u)]
satz35d:=satz35b(y,x,u,z,l,satz14(z,u,k)):less(ts(x,z),ts(y,u))
u@[m:moreis(x,y)][n:moreis(z,u)]
+436
[i:is(x,y)][j:is(z,u)]
t1:=moreisi2(ts(x,z),ts(y,u),tris(nat,ts(x,z),ts(y,z),ts(y,u),ists1(x,y,z,i),ists2(z,u,y,j))):moreis(ts(x,z),ts(y,u))
i@[o:more(z,u)]
t2:=moreisi1(ts(x,z),ts(y,u),satz35a(m,o)):moreis(ts(x,z),ts(y,u))
i@t3:=orapp(more(z,u),is(z,u),moreis(ts(x,z),ts(y,u)),n,[v:more(z,u)]t2(v),[v:is(z,u)]t1(v)):moreis(ts(x,z),ts(y,u))
n@[o:more(x,y)]
t4:=moreisi1(ts(x,z),ts(y,u),satz35b(o,n)):moreis(ts(x,z),ts(y,u))
-436
satz36:=orapp(more(x,y),is(x,y),moreis(ts(x,z),ts(y,u)),m,[v:more(x,y)]t4".436"(v),[v:is(x,y)]t3".436"(v)):moreis(ts(x,z),ts(y,u))
+*436
n@[o:more(x,y)]
t5:=moreisi1(ts(x,z),ts(y,u),satz35b(o,n)):moreis(ts(x,z),ts(y,u))
n@[i:is(x,y)]
t6:=ismoreis2(ts(x,u),ts(y,u),ts(x,z),ists1(u,i),satz32m(z,u,x,n)):moreis(ts(x,z),ts(y,u))
n@anders:=orapp(more(x,y),is(x,y),moreis(ts(x,z),ts(y,u)),m,[v:more(x,y)]t5(v),[v:is(x,y)]t6(v)):moreis(ts(x,z),ts(y,u))
-436
u@[l:lessis(x,y)][k:lessis(z,u)]
satz36a:=satz13(ts(y,u),ts(x,z),satz36(y,x,u,z,satz14(l),satz14(z,u,k))):lessis(ts(x,z),ts(y,u))
y@[m:more(x,y)]
+mn
t1:=onei(nat,[z:nat]diffprop(x,y,z),satz8b(x,y),m):one([z:nat]diffprop(x,y,z))
-mn
mn:=ind(nat,[z:nat]diffprop(x,y,z),t1".mn"):nat
+*mn
m@th1a:=oneax(nat,[z:nat]diffprop(x,y,z),t1):is(x,pl(y,mn(x,y,m)))
th1b:=symis(nat,x,pl(y,mn(x,y,m)),th1a):is(pl(y,mn(x,y,m)),x)
th1c:=tris(nat,x,pl(y,mn(x,y,m)),pl(mn(x,y,m),y),th1a,compl(y,mn(x,y,m))):is(x,pl(mn(x,y,m),y))
th1d:=symis(nat,x,pl(mn(x,y,m),y),th1c):is(pl(mn(x,y,m),y),x)
y@[z:nat][m:more(x,y)][i:is(pl(y,z),x)]
th1e:=<th1a(m)><symis(nat,pl(y,z),x,i)><mn(x,y,m)><z>satz8b(x,y):is(z,mn(x,y,m))
-mn
z@[u:nat][m:more(x,z)][n:more(y,u)][i:is(x,y)][j:is(z,u)]
+*mn
j@t2:=tr3is(nat,pl(u,mn(x,z,m)),pl(z,mn(x,z,m)),x,y,ispl1(u,z,mn(x,z,m),symis(nat,z,u,j)),th1b(x,z,m),i):is(pl(u,mn(x,z,m)),y)
-mn
j@ismn12:=th1e".mn"(y,u,mn(x,z,m),n,t2".mn"):is(mn(x,z,m),mn(y,u,n))
@[n:nat]
1to:=ot(nat,[x:nat]lessis(x,n)):'type'
[x:nat][l:lessis(x,n)]
outn:=out(nat,[y:nat]lessis(y,n),x,l):1to(n)
n@[xn:1to(n)]
inn:=in"e"(nat,[y:nat]lessis(y,n),xn):nat
1top:=inp(nat,[y:nat]lessis(y,n),xn):lessis(inn,n)
l@[y:nat][k:lessis(y,n)][i:is(x,y)]
isoutni:=isouti(nat,[z:nat]lessis(z,n),x,l,y,k,i):is"e"(1to(n),outn(x,l),outn(y,k))
k@[i:is"e"(1to(n),outn(x,l),outn(y,k))]
isoutne:=isoute(nat,[z:nat]lessis(z,n),x,l,y,k,i):is(x,y)
xn@[yn:1to(n)][i:is"e"(1to(n),xn,yn)]
isinni:=isini(nat,[z:nat]lessis(z,n),xn,yn,i):is(inn(xn),inn(yn))
yn@[i:is(inn(xn),inn(yn))]
isinne:=isine(nat,[z:nat]lessis(z,n),xn,yn,i):is"e"(1to(n),xn,yn)
xn@isoutinn:=isoutin(nat,[y:nat]lessis(y,n),xn):is"e"(1to(n),xn,outn(inn(xn),1top(xn)))
l@isinoutn:=isinout(nat,[y:nat]lessis(y,n),x,l):is(x,inn(outn(x,l)))
@1o:=outn(1,1,lessisi2(1,1,refis(nat,1))):1to(1)
[u:1to(1)]
+singlet
u0:=inn(1,u):nat
t1:=1top(1,u):lessis(u0,1)
t2:=ore2(more(u0,1),is(u0,1),satz24(u0),satz10d(u0,1,t1)):is(u0,1)
th1:=tris(1to(1),u,outn(1,u0,t1),1o,isoutinn(1,u),isoutni(1,u0,t1,1,lessisi2(1,1,refis(nat,1)),t2)):is"e"(1to(1),u,1o)
-singlet
@2:=pl(1,1):nat
[x:nat]
+pair
[l:lessis(x,2)][n:nis(x,2)]
t1:=satz26(1,x,ore1(less(x,2),is(x,2),l,n)):lessis(x,1)
t2:=ore2(more(x,1),is(x,1),satz24(x),satz10d(x,1,t1)):is(x,1)
l@th1:=th2"l.or"(is(x,1),is(x,2),[t:nis(x,2)]t2(t)):or(is(x,1),is(x,2))
@th2:=th1"e.notis"(nat,<1>suc,1,2,<1>ax3,satz4e(1)):nis(2,1)
-pair
@1t:=outn(2,1,satz24a(2)):1to(2)
2t:=outn(2,2,lessisi2(2,2,refis(nat,2))):1to(2)
+*pair
@[u:1to(2)]
u0:=inn(2,u):nat
t3:=1top(2,u):lessis(u0,2)
[i:is(u0,1)]
t4:=isoutni(2,u0,t3,1,satz24a(2),i):is"e"(1to(2),outn(2,u0,t3),1t)
t5:=tris(1to(2),u,outn(2,u0,t3),1t,isoutinn(2,u),t4):is"e"(1to(2),u,1t)
u@[i:is(u0,2)]
t6:=isoutni(2,u0,t3,2,lessisi2(2,2,refis(nat,2)),i):is"e"(1to(2),outn(2,u0,t3),2t)
t7:=tris(1to(2),u,outn(2,u0,t3),2t,isoutinn(2,u),t6):is"e"(1to(2),u,2t)
u@th3:=th9"l.or"(is(u0,1),is(u0,2),is"e"(1to(2),u,1t),is"e"(1to(2),u,2t),th1(u0,t3),[t:is(u0,1)]t5(t),[t:is(u0,2)]t7(t)):or(is"e"(1to(2),u,1t),is"e"(1to(2),u,2t))
@[i:is"e"(1to(2),2t,1t)]
t9:=isini(nat,[x:nat]lessis(x,2),2t,1t,i):is(u0(2t),u0(1t))
t10:=tr3is(nat,2,u0(2t),u0(1t),1,isinoutn(2,2,lessisi2(2,2,refis(nat,2))),t9,symis(nat,1,u0(1t),isinoutn(2,1,satz24a(2)))):is(2,1)
@th4:=th3"l.imp"(is"e"(1to(2),2t,1t),is(2,1),th2,[t:is"e"(1to(2),2t,1t)]t10(t)):not(is"e"(1to(2),2t,1t))
-pair
@[alpha:'type']
pair1type:=[x:1to(2)]alpha:'type'
[a:alpha][b:alpha]
pair1:=[x:1to(2)]ite(is"e"(1to(2),x,1t),alpha,a,b):pair1type
alpha@[p:pair1type]
first1:=<1t>p:alpha
second1:=<2t>p:alpha
b@first1is1:=itet(is"e"(1to(2),1t,1t),alpha,a,b,refis(1to(2),1t)):is"e"(alpha,first1(pair1),a)
first1is2:=symis(alpha,first1(pair1),a,first1is1):is"e"(alpha,a,first1(pair1))
second1is1:=itef(is"e"(1to(2),2t,1t),alpha,a,b,th4".pair"):is"e"(alpha,second1(pair1),b)
second1is2:=symis(alpha,second1(pair1),b,second1is1):is"e"(alpha,b,second1(pair1))
+*pair
p@[q:pair1type][i:is"e"(alpha,first1(p),first1(q))][j:is"e"(alpha,second1(p),second1(q))][u:1to(2)][u1:is"e"(1to(2),u,1t)]
t11:=isf(1to(2),alpha,p,u,1t,u1):is"e"(alpha,<u>p,first1(p))
t12:=symis(alpha,<u>q,first1(q),isf(1to(2),alpha,q,u,1t,u1)):is"e"(alpha,first1(q),<u>q)
t13:=tr3is(alpha,<u>p,first1(p),first1(q),<u>q,t11,i,t12):is"e"(alpha,<u>p,<u>q)
u@[u2:is"e"(1to(2),u,2t)]
t14:=isf(1to(2),alpha,p,u,2t,u2):is"e"(alpha,<u>p,second1(p))
t15:=symis(alpha,<u>q,second1(q),isf(1to(2),alpha,q,u,2t,u2)):is"e"(alpha,second1(q),<u>q)
t16:=tr3is(alpha,<u>p,second1(p),second1(q),<u>q,t14,j,t15):is"e"(alpha,<u>p,<u>q)
u@t17:=orapp(is"e"(1to(2),u,1t),is"e"(1to(2),u,2t),is"e"(alpha,<u>p,<u>q),th3(u),[t:is"e"(1to(2),u,1t)]t13(t),[t:is"e"(1to(2),u,2t)]t16(t)):is"e"(alpha,<u>p,<u>q)
j@th5:=fisi(1to(2),alpha,p,q,[t:1to(2)]t17(t)):is"e"(pair1type,p,q)
p@q0:=pair1(first1,second1):pair1type
t18:=first1is1(first1(p),second1):is"e"(alpha,first1(q0),first1(p))
t19:=second1is1(first1,second1):is"e"(alpha,second1(q0),second1(p))
-pair
p@pair1is1:=th5".pair"(q0".pair",p,t18".pair",t19".pair"):is"e"(pair1type,pair1(first1,second1),p)
pair1is2:=symis(pair1type,pair1(first1,second1),p,pair1is1):is"e"(pair1type,p,pair1(first1,second1))
@[x:nat]
lessisi3:=lessisi2(x,x,refis(nat,x)):lessis(x,x)
1out:=outn(x,1,satz24a(x)):1to(x)
xout:=outn(x,x,lessisi3(x)):1to(x)
[y:nat][l:lessis(y,x)][u:1to(y)]
+left
ui:=inn(y,u):nat
t1:=1top(y,u):lessis(ui,y)
t2:=trlessis(ui,y,x,t1,l):lessis(ui,x)
-left
left1to:=outn(x,ui".left",t2".left"):1to(x)
[v:1to(y)][i:is"e"(1to(x),left1to(u),left1to(v))]
+*left
i@t3:=isoutne(x,ui,t2,ui(v),t2(v),i):is(ui,ui(v))
-left
i@thleft1:=isinne(y,u,v,t3".left"):is"e"(1to(y),u,v)
l@thleft2:=[u:1to(y)][v:1to(y)][t:is"e"(1to(x),left1to(u),left1to(v))]thleft1(u,v,t):injective(1to(y),1to(x),[t:1to(y)]left1to(t))
y@[u:1to(y)]
+right
ui:=inn(y,u):nat
t4:=1top(y,u):lessis(ui,y)
t5:=satz19o(ui,y,x,t4):lessis(pl(x,ui),pl(x,y))
-right
right1to:=outn(pl(x,y),pl(x,ui".right"),t5".right"):1to(pl(x,y))
[v:1to(y)][i:is"e"(1to(pl(x,y)),right1to(u),right1to(v))]
+*right
i@t6:=isoutne(pl(x,y),pl(x,ui(u)),t5(u),pl(x,ui(v)),t5(v),i):is(pl(x,ui(u)),pl(x,ui(v)))
t7:=satz20e(ui(u),ui(v),x,t6):is(ui(u),ui(v))
-right
i@thright1:=isinne(y,u,v,t7".right"):is"e"(1to(y),u,v)
@[alpha:'type'][x:nat][y:nat][l:lessis(y,x)][f:[t:1to(x)]alpha]
left:=[t:1to(y)]<left1to(x,y,l,t)>f:[t:1to(y)]alpha
y@[f:[t:1to(pl(x,y))]alpha]
right:=[t:1to(y)]<right1to(x,y,t)>f:[t:1to(y)]alpha
y@[i:is(y,x)][f:[t:1to(y)]alpha]
+*left
f@t4:=lessisi2(y,x,i):lessis(y,x)
t5:=lessisi2(x,y,symis(nat,y,x,i)):lessis(x,y)
f1:=left(y,x,t5,f):[t:1to(x)]alpha
f2:=left(t4,f1):[t:1to(y)]alpha
[u:1to(y)]
t6:=isinoutn(x,inn(y,u),trlessis(inn(y,u),y,x,1top(y,u),t4)):is(inn(y,u),inn(x,left1to(x,y,t4,u)))
t7:=tris(1to(y),u,outn(y,inn(y,u),1top(y,u)),left1to(y,x,t5,left1to(x,y,t4,u)),isoutinn(y,u),isoutni(y,inn(y,u),1top(y,u),inn(x,left1to(x,y,t4,u)),trlessis(inn(x,left1to(x,y,t4,u)),x,y,1top(x,left1to(x,y,t4,u)),t5),t6)):is"e"(1to(y),u,left1to(y,x,t5,left1to(x,y,t4,u)))
t8:=isf(1to(y),alpha,f,u,left1to(y,x,t5,left1to(x,y,t4,u)),t7):is"e"(alpha,<u>f,<u>f2)
-left
f@thleft:=fisi(1to(y),alpha,f,f2".left",[t:1to(y)]t8".left"(t)):is"e"([t:1to(y)]alpha,f,left(x,y,lessisi2(y,x,i),left(y,x,lessisi2(x,y,symis(nat,y,x,i)),f)))
