Landau in Automath

0.aut

+l
@[a:'prop'][b:'prop']
imp:=[x:a]b:'prop'
[a1:a][i:imp(a,b)]
mp:=<a1>i:b
a@refimp:=[x:a]x:imp(a,a)
b@[c:'prop'][i:imp(a,b)][j:imp(b,c)]
trimp:=[x:a]<<x>i>j:imp(a,c)
@con:='prim':'prop'
a@not:=imp(con):'prop'
wel:=not(not(a)):'prop'
[a1:a]
weli:=[x:not(a)]<a1>x:wel(a)
a@[w:wel(a)]
et:='prim':a
a@[c1:con]
cone:=et([x:not(a)]c1):a
+imp
b@[i:imp(a,b)][j:imp(not(a),b)]
th1:=et(b,[x:not(b)]<<trimp(con,i,x)>j>x):b
b@[n:not(a)]
th2:=trimp(con,b,n,[x:con]cone(b,x)):imp(a,b)
b@[n:not(b)][i:imp(a,b)]
th3:=trimp(con,i,n):not(a)
b@[a1:a][n:not(b)]
th4:=[x:imp(a,b)]<a1>th3(n,x):not(imp(a,b))
b@[n:not(imp(a,b))]
th5:=et([x:not(a)]<th2(x)>n):a
th6:=[x:b]<[y:a]x>n:not(b)
b@[n:not(b)][i:imp(not(a),b)]
th7:=et(a,th3(not(a),b,n,i)):a
-imp
b@[i:imp(not(b),not(a))]
cp:=[x:a]th7".imp"(b,not(a),weli(x),i):imp(a,b)
@obvious:=imp(con,con):'prop'
obviousi:=refimp(con):obvious
b@ec:=imp(a,not(b)):'prop'
[n:not(a)]
eci1:=th2".imp"(not(b),n):ec(a,b)
b@[n:not(b)]
eci2:=[x:a]n:ec(a,b)
+ec
b@[i:imp(a,not(b))]
th1:=i:ec(a,b)
b@[i:imp(b,not(a))]
th2:=[x:a][y:b]<x><y>i:ec(a,b)
-ec
b@[e:ec(a,b)]
comec:=th2".ec"(b,a,e):ec(b,a)
[a1:a]
ece1:=<a1>e:not(b)
e@[b1:b]
ece2:=th3".imp"(not(b),weli(b,b1),e):not(a)
+*ec
c@[e:ec(a,b)][i:imp(c,a)]
th3:=trimp(c,a,not(b),i,e):ec(c,b)
e@[i:imp(c,b)]
th4:=comec(c,a,th3(b,a,c,comec(e),i)):ec(a,c)
-ec
b@and:=not(ec(a,b)):'prop'
[a1:a][b1:b]
andi:=th4".imp"(not(b),a1,weli(b,b1)):and(a,b)
b@[a1:and(a,b)]
ande1:=th5".imp"(not(b),a1):a
ande2:=et(b,th6".imp"(not(b),a1)):b
comand:=andi(b,a,ande2,ande1):and(b,a)
+and
b@[n:not(a)]
th1:=weli(ec,eci1(n)):not(and)
b@[n:not(b)]
th2:=weli(ec,eci2(n)):not(and)
b@[n:not(and)][a1:a]
th3:=ece1(et(ec,n),a1):not(b)
n@[b1:b]
th4:=ece2(et(ec,n),b1):not(a)
n@th5:=th3"l.imp"(and(b,a),and(a,b),n,[x:and(b,a)]comand(b,a,x)):not(and(b,a))
c@[a1:and(a,b)][i:imp(a,c)]
th6:=andi(c,b,<ande1(a1)>i,ande2(a1)):and(c,b)
a1@[i:imp(b,c)]
th7:=andi(a,c,ande1(a1),<ande2(a1)>i):and(a,c)
-and
b@or:=imp(not(a),b):'prop'
[a1:a]
ori1:=th2".imp"(not(a),b,weli(a1)):or(a,b)
b@[b1:b]
ori2:=[x:not(a)]b1:or(a,b)
+or
b@[i:imp(not(a),b)]
th1:=i:or(a,b)
b@[i:imp(not(b),a)]
th2:=[x:not]et(b,th3"l.imp"(not(b),a,x,i)):or(a,b)
-or
b@[o:or(a,b)][n:not(a)]
ore2:=<n>o:b
o@[n:not(b)]
ore1:=et(th3".imp"(not(a),b,n,o)):a
o@comor:=[x:not(b)]ore1(x):or(b,a)
+*or
b@[n:not(a)][m:not(b)]
th3:=th4"l.imp"(not(a),b,n,m):not(or(a,b))
b@[n:not(or(a,b))]
th4:=th5"l.imp"(not(a),b,n):not(a)
th5:=th6"l.imp"(not(a),b,n):not(b)
a@th6:=refimp(not(a)):or(a,not(a))
-or
c@[o:or(a,b)][i:imp(a,c)][j:imp(b,c)]
orapp:=th1".imp"(c,i,trimp(not,b,c,o,j)):c
c@[d:'prop']
+*or
o@[i:imp(a,c)]
th7:=trimp(not(c),not,b,[x:not(c)]th3"l.imp"(a,c,x,i),o):or(c,b)
o@[i:imp(b,c)]
th8:=trimp(not(a),b,c,o,i):or(a,c)
d@[o:or(a,b)][i:imp(a,c)][j:imp(b,d)]
th9:=th7(a,d,c,th8(a,b,d,o,j),i):or(c,d)
b@[o:or(a,b)]
th10:=o:imp(not(a),b)
th11:=comor(o):imp(not(b),a)
b@[o:or(not(a),b)]
th12:=trimp(a,wel(a),b,[x:a]weli(x),o):imp(a,b)
b@[i:imp(a,b)]
th13:=trimp(wel(a),a,b,[x:wel(a)]et(x),i):or(not(a),b)
b@[o:or(not(a),not(b))]
th14:=weli(ec,th12(not(b),o)):not(and)
b@[n:not(and)]
th15:=th13(not(b),et(ec,n)):or(not(a),not(b))
b@[a1:and(not(a),not(b))]
th16:=th3(ande1(not(a),not(b),a1),ande2(not(a),not(b),a1)):not(or(a,b))
b@[n:not(or(a,b))]
th17:=andi(not(a),not(b),th4(n),th5(n)):and(not(a),not(b))
-or
b@orec:=and(or(a,b),ec(a,b)):'prop'
[o:or(a,b)][e:ec(a,b)]
oreci:=andi(or(a,b),ec(a,b),o,e):orec(a,b)
+orec
b@[a1:a][n:not(b)]
th1:=oreci(ori1(a1),eci2(n)):orec(a,b)
b@[n:not(a)][b1:b]
th2:=oreci(ori2(b1),eci1(n)):orec(a,b)
-orec
b@[o:orec(a,b)]
orece1:=ande1(or(a,b),ec,o):or(a,b)
orece2:=ande2(or(a,b),ec,o):ec(a,b)
comorec:=oreci(b,a,comor(orece1),comec(orece2)):orec(b,a)
+*orec
o@[a1:a]
th3:=ece1(orece2,a1):not(b)
o@[b1:b]
th4:=ece2(orece2,b1):not(a)
o@[n:not(a)]
th5:=ore2(orece1,n):b
o@[n:not(b)]
th6:=ore1(orece1,n):a
-orec
b@iff:=and(imp(a,b),imp(b,a)):'prop'
[i:imp(a,b)][j:imp(b,a)]
iffi:=andi(imp(a,b),imp(b,a),i,j):iff(a,b)
+iff
b@[a1:a][b1:b]
th1:=iffi([x:a]b1,[x:b]a1):iff(a,b)
b@[n:not(a)][m:not(b)]
th2:=iffi(th2"l.imp"(n),th2"l.imp"(b,a,m)):iff(a,b)
-iff
b@[i:iff(a,b)]
iffe1:=ande1(imp(a,b),imp(b,a),i):imp(a,b)
iffe2:=ande2(imp(a,b),imp(b,a),i):imp(b,a)
comiff:=iffi(b,a,iffe2,iffe1):iff(b,a)
+*iff
i@[a1:a]
th3:=<a1>iffe1:b
i@[b1:b]
th4:=<b1>iffe2:a
i@[n:not(a)]
th5:=th3"l.imp"(b,a,n,iffe2):not(b)
i@[n:not(b)]
th6:=th3"l.imp"(n,iffe1):not(a)
b@[a1:a][n:not(b)]
th7:=th1"l.and"(imp(a,b),imp(b,a),th4"l.imp"(a1,n)):not(iff(a,b))
b@[n:not(a)][b1:b]
th8:=th2"l.and"(imp(a,b),imp(b,a),th4"l.imp"(b,a,b1,n)):not(iff(a,b))
-iff
a@refiff:=iffi(a,refimp,refimp):iff(a,a)
b@[i:iff(a,b)]
symiff:=comiff(i):iff(b,a)
c@[i:iff(a,b)][j:iff(b,c)]
triff:=iffi(a,c,trimp(iffe1(i),iffe1(b,c,j)),trimp(c,b,a,iffe2(b,c,j),iffe2(i))):iff(a,c)
+*iff
b@[i:iff(a,b)]
th9:=[x:not(a)]th5(i,x):imp(not(a),not(b))
th10:=[x:not(b)]th6(i,x):imp(not(b),not(a))
th11:=iffi(not(a),not(b),th9,th10):iff(not(a),not(b))
b@[i:imp(not(a),not(b))][j:imp(not(b),not(a))]
th12:=iffi(cp(j),cp(b,a,i)):iff(a,b)
b@[o:orec(a,b)]
th13:=iffi(not(b),orece2(o),comor(orece1(o))):iff(a,not(b))
th14:=th13(b,a,comorec(o)):iff(b,not(a))
b@[i:iff(a,not(b))]
th15:=oreci(comor(b,a,iffe2(not(b),i)),iffe1(not(b),i)):orec(a,b)
b@[i:iff(b,not(a))]
th16:=comorec(b,a,th15(b,a,i)):orec(a,b)
c@[i:iff(a,b)][j:imp(a,c)]
thimp1:=trimp(b,a,c,iffe2(i),j):imp(b,c)
i@[j:imp(c,a)]
thimp2:=trimp(c,a,b,j,iffe1(i)):imp(c,b)
i@[e:ec(a,c)]
thec1:=th3"l.ec"(c,b,e,iffe2(i)):ec(b,c)
i@[e:ec(c,a)]
thec2:=th4"l.ec"(c,a,b,e,iffe2(i)):ec(c,b)
i@[a1:and(a,c)]
thand1:=th6"l.and"(c,b,a1,iffe1(i)):and(b,c)
i@[a1:and(c,a)]
thand2:=th7"l.and"(c,a,b,a1,iffe1(i)):and(c,b)
i@[o:or(a,c)]
thor1:=th7"l.or"(c,b,o,iffe1(i)):or(b,c)
i@[o:or(c,a)]
thor2:=th8"l.or"(c,a,b,o,iffe1(i)):or(c,b)
i@[o:orec(a,c)]
thorec1:=oreci(b,c,thor1(orece1(a,c,o)),thec1(orece2(a,c,o))):orec(b,c)
i@[o:orec(c,a)]
thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b)
-iff
@[sigma:'type'][p:[x:sigma]'prop']
all:=p:'prop'
[a1:all(sigma,p)][s:sigma]
alle:=<s>a1:<s>p
+all
p@[s:sigma][n:not(<s>p)]
th1:=[x:all(sigma,p)]<<s>x>n:not(all(sigma,p))
-all
p@non:=[x:sigma]not(<x>p):[x:sigma]'prop'
some:=not(non(p)):'prop'
[s:sigma][sp:<s>p]
somei:=th1".all"(non(p),s,weli(<s>p,sp)):some(sigma,p)
+some
p@[n:not(all(sigma,p))][m:non(non(p))][s:sigma]
t1:=et(<s>p,<s>m):<s>p
%set etared
m@t2:=<[x:sigma]t1(x)>n:con
%reset etared
n@th1:=[x:non(non(p))]t2(x):some(non(p))
p@[s:some(non(p))][a1:all(sigma,p)][t:sigma]
t3:=weli(<t>p,<t>a1):not(not(<t>p))
a1@t4:=<[x:sigma]t3(x)>s:con
s@th2:=[x:all(sigma,p)]t4(x):not(all(sigma,p))
p@[n:not(some(sigma,p))]
th3:=et(non(p),n):non(p)
[s:sigma]
th4:=<s>th3:not(<s>p)
p@[n:non(p)]
th5:=weli(non(p),n):not(some(sigma,p))
-some
p@[s:some(sigma,p)][x:'prop'][i:[y:sigma]imp(<y>p,x)]
+*some
i@[n:not(x)][t:sigma]
t5:=th3"l.imp"(<t>p,x,n,<t>i):not(<t>p)
n@t6:=mp(some(sigma,p),con,s,th5([y:sigma]t5(y))):con
-some
i@someapp:=et(x,[y:not(x)]t6".some"(y)):x
+*some
p@[q:[x:sigma]'prop'][s:some(sigma,p)][i:[x:sigma]imp(<x>p,<x>q)]
th6:=someapp(s,some(q),[x:sigma][y:<x>p]somei(q,x,mp(<x>p,<x>q,y,<x>i))):some(q)
-some
c@or3:=or(a,or(b,c)):'prop'
[o:or3(a,b,c)][n:not(a)]
+or3
th1:=ore2(or(b,c),o,n):or(b,c)
-or3
[m:not(b)]
or3e3:=ore2(b,c,th1".or3",m):c
o@[n:not(b)]
+*or3
n@th2:=th2"l.or"(c,a,[x:not(a)]or3e3(x,n)):or(c,a)
-or3
n@[m:not(c)]
or3e1:=ore2(c,a,th2".or3",m):a
o@[n:not(c)]
+*or3
n@th3:=th2"l.or"([x:not(b)]or3e1(x,n)):or(a,b)
-or3
n@[m:not(a)]
or3e2:=ore2(th3".or3",m):b
+*or3
o@th4:=th1"l.or"(b,or(c,a),[x:not(b)]th2(x)):or3(b,c,a)
th5:=th4(b,c,a,th4):or3(c,a,b)
-or3
c@[a1:a]
or3i1:=ori1(a,or(b,c),a1):or3(a,b,c)
c@[b1:b]
or3i2:=ori2(a,or(b,c),ori1(b,c,b1)):or3(a,b,c)
c@[c1:c]
or3i3:=ori2(a,or(b,c),ori2(b,c,c1)):or3(a,b,c)
+*or3
c@[o:or(a,b)]
th6:=th4"or3"(c,a,b,ori2(c,or(a,b),o)):or3(a,b,c)
c@[o:or(b,c)]
th7:=ori2(or(b,c),o):or3(a,b,c)
c@[o:or(c,a)]
th8:=th4"or3"(c,a,b,th6(c,a,b,o)):or3(a,b,c)
-or3
d@[o:or3(a,b,c)][i:imp(a,d)][j:imp(b,d)][k:imp(c,d)]
or3app:=orapp(or(b,c),d,o,i,[x:or(b,c)]orapp(b,c,d,x,j,k)):d
c@and3:=and(a,and(b,c)):'prop'
[a1:and3(a,b,c)]
and3e1:=ande1(and(b,c),a1):a
and3e2:=ande1(b,c,ande2(and(b,c),a1)):b
and3e3:=ande2(b,c,ande2(and(b,c),a1)):c
c@[a1:a][b1:b][c1:c]
and3i:=andi(a,and(b,c),a1,andi(b,c,b1,c1)):and3(a,b,c)
+and3
c@[a1:and3(a,b,c)]
th1:=and3i(b,c,a,and3e2(a1),and3e3(a1),and3e1(a1)):and3(b,c,a)
th2:=th1(b,c,a,th1):and3(c,a,b)
th3:=andi(and3e1(a1),and3e2(a1)):and(a,b)
th4:=ande2(and(b,c),a1):and(b,c)
th5:=th3(c,a,b,th2):and(c,a)
th6:=and3i(c,b,a,and3e3(a1),and3e2(a1),and3e1(a1)):and3(c,b,a)
-and3
c@ec3:=and3(ec,ec(b,c),ec(c,a)):'prop'
[e:ec3(a,b,c)]
+ec3
th1:=and3e1(ec,ec(b,c),ec(c,a),e):ec(a,b)
th2:=and3e2(ec,ec(b,c),ec(c,a),e):ec(b,c)
th3:=and3e3(ec,ec(b,c),ec(c,a),e):ec(c,a)
th4:=th1"l.and3"(ec,ec(b,c),ec(c,a),e):ec3(b,c,a)
th5:=th4(b,c,a,th4):ec3(c,a,b)
th5a:=and3i(ec(c,b),ec(b,a),ec(a,c),comec(b,c,th2(e)),comec(a,b,th1(e)),comec(c,a,th3(e))):ec3(c,b,a)
-ec3
[a1:a]
ec3e12:=ece1(th1".ec3",a1):not(b)
ec3e13:=ece2(c,a,th3".ec3",a1):not(c)
e@[b1:b]
ec3e23:=ec3e12(b,c,a,th4".ec3",b1):not(c)
ec3e21:=ec3e13(b,c,a,th4".ec3",b1):not(a)
e@[c1:c]
ec3e31:=ec3e12(c,a,b,th5".ec3",c1):not(a)
ec3e32:=ec3e13(c,a,b,th5".ec3",c1):not(b)
+*ec3
c@[e:ec(a,b)][f:ec(b,c)][g:ec(c,a)]
th6:=and3i(ec,ec(b,c),ec(c,a),e,f,g):ec3(a,b,c)
c@[e:ec3(a,b,c)][o:or(a,b)]
th7:=orapp(not(c),o,[x:a]ece2(c,a,th3"ec3"(e),x),[x:b]ece1(b,c,th2"ec3"(e),x)):not(c)
e@[o:or(b,c)]
th8:=th7(b,c,a,th4"ec3"(e),o):not(a)
e@[o:or(c,a)]
th9:=th7(c,a,b,th5"ec3"(e),o):not(b)
-ec3
c@[n:not(a)][m:not(b)]
ec3i1:=th6".ec3"(eci1(n),eci1(b,c,m),eci2(c,a,n)):ec3(a,b,c)
c@[n:not(b)][m:not(c)]
ec3i2:=th6".ec3"(eci2(n),eci1(b,c,n),eci1(c,a,m)):ec3(a,b,c)
c@[n:not(c)][m:not(a)]
ec3i3:=th6".ec3"(eci1(m),eci2(b,c,n),eci1(c,a,n)):ec3(a,b,c)
+*ec3
d@[e:'prop'][f:'prop'][o1:or3(a,b,c)][p1:ec3(d,e,f)][i:imp(a,d)][j:imp(b,e)][k:imp(c,f)][d1:d]
t1:=[x:b]mp(e,con,<x>j,ec3e12(d,e,f,p1,d1)):not(b)
t2:=[x:c]mp(f,con,<x>k,ec3e13(d,e,f,p1,d1)):not(c)
th10:=or3e1(o1,t1,t2):a
k@[e1:e]
th11:=th10(b,c,a,e,f,d,th4"l.or3"(o1),th4"ec3"(d,e,f,p1),j,k,i,e1):b
k@[f1:f]
th12:=th10(c,a,b,f,d,e,th5"l.or3"(o1),th5"ec3"(d,e,f,p1),k,i,j,f1):c
-ec3
c@orec3:=and(or3(a,b,c),ec3(a,b,c)):'prop'
[o:orec3(a,b,c)]
orec3e1:=ande1(or3(a,b,c),ec3(a,b,c),o):or3(a,b,c)
orec3e2:=ande2(or3(a,b,c),ec3(a,b,c),o):ec3(a,b,c)
c@[o:or3(a,b,c)][e:ec3(a,b,c)]
orec3i:=andi(or3(a,b,c),ec3(a,b,c),o,e):orec3(a,b,c)
+orec3
c@[o:orec3(a,b,c)]
th1:=orec3i(b,c,a,th4"l.or3"(orec3e1(o)),th4"l.ec3"(orec3e2(o))):orec3(b,c,a)
th2:=orec3i(c,a,b,th5"l.or3"(orec3e1(o)),th5"l.ec3"(orec3e2(o))):orec3(c,a,b)
-orec3
+e
sigma@[s:sigma][t:sigma]
is:='prim':'prop'
s@refis:='prim':is(s,s)
p@[s:sigma][t:sigma][sp:<s>p][i:is(s,t)]
isp:='prim':<t>p
sigma@[s:sigma][t:sigma][i:is(s,t)]
symis:=isp([x:sigma]is(x,s),s,t,refis(s),i):is(t,s)
t@[u:sigma][i:is(s,t)][j:is(t,u)]
tris:=isp([x:sigma]is(x,u),t,s,j,symis(i)):is(s,u)
u@[i:is(u,s)][j:is(u,t)]
tris1:=tris(s,u,t,symis(u,s,i),j):is(s,t)
u@[i:is(s,u)][j:is(t,u)]
tris2:=tris(s,u,t,i,symis(t,u,j)):is(s,t)
sp@[i:is(t,s)]
isp1:=isp(symis(t,s,i)):<t>p
t@[n:not(is(s,t))]
symnotis:=th3"l.imp"(is(t,s),is(s,t),n,[x:is(t,s)]symis(t,s,x)):not(is(t,s))
+notis
u@[n:not(is(s,t))][i:is(s,u)]
th1:=isp([x:sigma]not(is(x,t)),s,u,n,i):not(is(u,t))
n@[i:is(u,s)]
th2:=th1(symis(u,s,i)):not(is(u,t))
n@[i:is(t,u)]
th3:=isp([x:sigma]not(is(s,x)),t,u,n,i):not(is(s,u))
n@[i:is(u,t)]
th4:=th3(symis(u,t,i)):not(is(s,u))
u@[v:sigma][n:not(is(s,t))][i:is(s,u)][j:is(t,v)]
th5:=th3(u,t,v,th1(n,i),j):not(is(u,v))
-notis
u@[v:sigma][i:is(s,t)][j:is(t,u)][k:is(u,v)]
tr3is:=tris(s,u,v,tris(i,j),k):is(s,v)
v@[w:sigma][i:is(s,t)][j:is(t,u)][k:is(u,v)][l:is(v,w)]
tr4is:=tris(s,v,w,tr3is(i,j,k),l):is(s,w)
p@amone:=[x:sigma][y:sigma][u:<x>p][v:<y>p]is(x,y):'prop'
[a1:amone(sigma,p)][s:sigma][t:sigma][sp:<s>p][tp:<t>p]
amonee:=<tp><sp><t><s>a1:is(s,t)
p@one:=and(amone(sigma,p),some(sigma,p)):'prop'
[a1:amone(sigma,p)][s:some(sigma,p)]
onei:=andi(amone(sigma,p),some(sigma,p),a1,s):one(sigma,p)
p@[o1:one(sigma,p)]
onee1:=ande1(amone(sigma,p),some(sigma,p),o1):amone(sigma,p)
onee2:=ande2(amone(sigma,p),some(sigma,p),o1):some(sigma,p)
ind:='prim':sigma
oneax:='prim':<ind>p
+one
[s:sigma][sp:<s>p]
th1:=amonee(onee1,ind,s,oneax,sp):is(ind,s)
-one
sigma@[tau:'type'][f:[x:sigma]tau][s:sigma][t:sigma][i:is(s,t)]
isf:=isp(sigma,[x:sigma]is(tau,<s>f,<x>f),s,t,refis(tau,<s>f),i):is(tau,<s>f,<t>f)
f@injective:=all([x:sigma]all([y:sigma]imp(is(tau,<x>f,<y>f),is(x,y)))):'prop'
[i:injective(f)][s:sigma][t:sigma][j:is(tau,<s>f,<t>f)]
isfe:=<j><t><s>i:is(s,t)
f@[t0:tau]
image:=some([x:sigma]is(tau,t0,<x>f)):'prop'
f@[s:sigma]
tofs:=<s>f:tau
imagei:=somei([x:sigma]is(tau,tofs,<x>f),s,refis(tau,tofs)):image(tofs)
+inj
i@[ta:tau][tb:tau][j:is(tau,ta,tb)][sa:sigma][sb:sigma][ja:is(tau,ta,tofs(sa))][jb:is(tau,tb,tofs(sb))]
t1:=tr3is(tau,tofs(sa),ta,tb,tofs(sb),symis(tau,ta,tofs(sa),ja),j,jb):is(tau,tofs(sa),tofs(sb))
th1:=isfe(sa,sb,t1):is(sa,sb)
i@[t0:tau]
th2:=[x:sigma][y:sigma][u:is(tau,t0,<x>f)][v:is(tau,t0,<y>f)]th1(t0,t0,refis(tau,t0),x,y,u,v):amone([x:sigma]is(tau,t0,<x>f))
[j:image(f,t0)]
th3:=onei([x:sigma]is(tau,t0,<x>f),th2,j):one([x:sigma]is(tau,t0,<x>f))
-inj
i@[t0:tau][j:image(f,t0)]
soft:=ind([x:sigma]is(tau,t0,<x>f),th3".inj"(t0,j)):sigma
i@inverse:=[x:tau][u:image(f,x)]soft(x,u):[x:tau][u:image(f,x)]sigma
j@ists1:=oneax([x:sigma]is(tau,t0,<x>f),th3".inj"(t0,j)):is(tau,t0,tofs(soft(t0,j)))
ists2:=symis(tau,t0,tofs(soft(t0,j)),ists1):is(tau,tofs(soft(t0,j)),t0)
i@[ta:tau][ja:image(ta)][tb:tau][jb:image(tb)][j:is(tau,ta,tb)]
isinv:=th1".inj"(ta,tb,j,soft(ta,ja),soft(tb,jb),ists1(ta,ja),ists1(tb,jb)):is(soft(ta,ja),soft(tb,jb))
jb@[j:is(soft(ta,ja),soft(tb,jb))]
isinve:=tr3is(tau,ta,tofs(soft(ta,ja)),tofs(soft(tb,jb)),tb,ists1(ta,ja),isf(soft(ta,ja),soft(tb,jb),j),ists2(tb,jb)):is(tau,ta,tb)
i@[s:sigma]
isst1:=isfe(s,soft(tofs(s),imagei(s)),ists1(tofs(s),imagei(s))):is(s,soft(tofs(s),imagei(s)))
isst2:=symis(s,soft(tofs(s),imagei(s)),isst1):is(soft(tofs(s),imagei(s)),s)
f@surjective:=all(tau,[x:tau]image(x)):'prop'
bijective:=and(injective,surjective):'prop'
[b:bijective(f)]
+*inj
b@t2:=ande1(injective,surjective,b):injective(f)
t3:=ande2(injective,surjective,b):surjective(f)
[t:tau]
so:=soft(t2,t,<t>t3):sigma
-inj
b@invf:=[x:tau]so".inj"(x):[x:tau]sigma
[s:sigma]
thinvf1:=tris(s,soft(t2".inj",tofs(s),imagei(s)),<<s>f>invf,isst1(t2".inj",s),isinv(t2".inj",tofs(s),imagei(s),tofs(s),<tofs(s)>t3".inj",refis(tau,tofs(s)))):is(s,<<s>f>invf)
b@[t:tau]
thinvf2:=ists1(t2".inj",t,<t>t3".inj"):is(tau,t,<<t>invf>f)
tau@[upsilon:'type'][f:[x:sigma]tau][g:[x:tau]upsilon]
+*inj
g@[if:injective(sigma,tau,f)][ig:injective(tau,upsilon,g)]
h:=[x:sigma]<<x>f>g:[x:sigma]upsilon
[s:sigma][t:sigma][i:is(upsilon,<s>h,<t>h)]
t4:=isfe(tau,upsilon,g,ig,<s>f,<t>f,i):is(tau,<s>f,<t>f)
t5:=isfe(f,if,s,t,t4):is(s,t)
ig@th4:=[x:sigma][y:sigma][v:is(upsilon,<x>h,<y>h)]t5(x,y,v):injective(sigma,upsilon,[x:sigma]<<x>f>g)
-inj
+surj
g@[sf:surjective(sigma,tau,f)][sg:surjective(tau,upsilon,g)]
h:=[x:sigma]<<x>f>g:[x:sigma]upsilon
[u:upsilon]
t1:=<u>sg:image(tau,upsilon,g,u)
[t:tau][i:is(upsilon,u,<t>g)]
t2:=<t>sf:image(sigma,tau,f,t)
[s:sigma][j:is(tau,t,<s>f)]
t3:=tris(upsilon,u,<t>g,<s>h,i,isf(tau,upsilon,g,t,<s>f,j)):is(upsilon,u,<s>h)
t4:=somei([x:sigma]is(upsilon,u,<x>h),s,t3):image(sigma,upsilon,h,u)
i@t5:=someapp([x:sigma]is(tau,t,<x>f),t2,image(sigma,upsilon,h,u),[x:sigma][v:is(tau,t,<x>f)]t4(x,v)):image(sigma,upsilon,h,u)
u@t6:=someapp(tau,[x:tau]is(upsilon,u,<x>g),t1,image(sigma,upsilon,h,u),[x:tau][v:is(upsilon,u,<x>g)]t5(x,v)):image(sigma,upsilon,h,u)
sg@th1:=[x:upsilon]t6(x):surjective(sigma,upsilon,[x:sigma]<<x>f>g)
-surj
+bij
g@[bf:bijective(sigma,tau,f)][bg:bijective(tau,upsilon,g)]
h:=[x:sigma]<<x>f>g:[x:sigma]upsilon
t1:=th4"e.inj"(f,g,ande1(injective(f),surjective(f),bf),ande1(injective(tau,upsilon,g),surjective(tau,upsilon,g),bg)):injective(sigma,upsilon,h)
t2:=th1"e.surj"(f,g,ande2(injective(f),surjective(f),bf),ande2(injective(tau,upsilon,g),surjective(tau,upsilon,g),bg)):surjective(sigma,upsilon,h)
th1:=andi(injective(sigma,upsilon,h),surjective(sigma,upsilon,h),t1,t2):bijective(sigma,upsilon,[x:sigma]<<x>f>g)
-bij
tau@[f:[x:sigma]tau][g:[x:sigma]tau][i:is([x:sigma]tau,f,g)][s:sigma]
fise:=isp([x:sigma]tau,[y:[x:sigma]tau]is(tau,<s>f,<s>y),f,g,refis(tau,<s>f),i):is(tau,<s>f,<s>g)
g@[i:[x:sigma]is(tau,<x>f,<x>g)]
fisi:='prim':is([x:sigma]tau,f,g)
+fis
g@[i:is([x:sigma]tau,f,g)][s:sigma][t:sigma][j:is(s,t)]
th1:=tris(tau,<s>f,<t>f,<t>g,isf(f,s,t,j),fise(i,t)):is(tau,<s>f,<t>g)
-fis
p@ot:='prim':'type'
[o1:ot]
in:='prim':sigma
inp:='prim':<in>p
p@otax1:='prim':injective(ot,sigma,[x:ot]in(x))
[s:sigma][sp:<s>p]
otax2:='prim':image(ot,sigma,[x:ot]in(x),s)
o1@[o2:ot][i:is(ot,o1,o2)]
isini:=isf(ot,sigma,[x:ot]in(x),o1,o2,i):is(in(o1),in(o2))
o2@[i:is(in(o1),in(o2))]
isine:=isfe(ot,sigma,[x:ot]in(x),otax1,o1,o2,i):is(ot,o1,o2)
sp@out:=soft(ot,sigma,[x:ot]in(x),otax1,s,otax2):ot
[t:sigma][tp:<t>p][i:is(s,t)]
isouti:=isinv(ot,sigma,[x:ot]in(x),otax1,s,otax2,t,otax2(t,tp),i):is(ot,out(s,sp),out(t,tp))
tp@[i:is(ot,out(s,sp),out(t,tp))]
isoute:=isinve(ot,sigma,[x:ot]in(x),otax1,s,otax2,t,otax2(t,tp),i):is(s,t)
o1@isoutin:=tris(ot,o1,soft(ot,sigma,[x:ot]in(x),otax1,in(o1),imagei(ot,sigma,[x:ot]in(x),o1)),out(in(o1),inp(o1)),isst1(ot,sigma,[x:ot]in(x),otax1,o1),isinv(ot,sigma,[x:ot]in(x),otax1,in(o1),imagei(ot,sigma,[x:ot]in(x),o1),in(o1),otax2(in(o1),inp(o1)),refis(sigma,in(o1)))):is(ot,o1,out(in(o1),inp(o1)))
sp@isinout:=ists1(ot,sigma,[x:ot]in(x),otax1,s,otax2):is(s,in(out(s,sp)))
tau@pairtype:='prim':'type'
[s:sigma][t:tau]
pair:='prim':pairtype
tau@[p1:pairtype]
first:='prim':sigma
second:='prim':tau
pairis1:='prim':is(pairtype,pair(first,second),p1)
pairis2:=symis(pairtype,pair(first,second),p1,pairis1):is(pairtype,p1,pair(first,second))
t@firstis1:='prim':is(sigma,first(pair),s)
firstis2:=symis(sigma,first(pair),s,firstis1):is(sigma,s,first(pair))
secondis1:='prim':is(tau,second(pair),t)
secondis2:=symis(tau,second(pair),t,secondis1):is(tau,t,second(pair))
a@[ksi:'type'][x:ksi][y:ksi]
+ite
[z:ksi]
prop1:=and(imp(a,is(ksi,z,x)),imp(not(a),is(ksi,z,y))):'prop'
y@[a1:a][x1:ksi][y1:ksi][px1:prop1(x1)][py1:prop1(y1)]
t1:=ande1(imp(a,is(ksi,x1,x)),imp(not(a),is(ksi,x1,y)),px1):imp(a,is(ksi,x1,x))
t2:=mp(a,is(ksi,x1,x),a1,t1):is(ksi,x1,x)
t3:=t2(y1,x1,py1,px1):is(ksi,y1,x)
t4:=tris2(ksi,x1,y1,x,t2,t3):is(ksi,x1,y1)
a1@t5:=[s:ksi][t:ksi][ps:prop1(s)][pt:prop1(t)]t4(s,t,ps,pt):amone(ksi,[t:ksi]prop1(t))
t6:=[x1:a]refis(ksi,x):imp(a,is(ksi,x,x))
t7:=th2"l.imp"(not(a),is(ksi,x,y),weli(a,a1)):imp(not(a),is(ksi,x,y))
t8:=andi(imp(a,is(ksi,x,x)),imp(not(a),is(ksi,x,y)),t6,t7):prop1(x)
t9:=somei(ksi,[t:ksi]prop1(t),x,t8):some(ksi,[t:ksi]prop1(t))
t10:=onei(ksi,[t:ksi]prop1(t),t5,t9):one(ksi,[t:ksi]prop1(t))
y@[n:not(a)][x1:ksi][y1:ksi][px1:prop1(x1)][py1:prop1(y1)]
t11:=ande2(imp(a,is(ksi,x1,x)),imp(not(a),is(ksi,x1,y)),px1):imp(not(a),is(ksi,x1,y))
t12:=mp(not(a),is(ksi,x1,y),n,t11):is(ksi,x1,y)
t13:=t12(y1,x1,py1,px1):is(ksi,y1,y)
t14:=tris2(ksi,x1,y1,y,t12,t13):is(ksi,x1,y1)
n@t15:=[s:ksi][t:ksi][ps:prop1(s)][pt:prop1(t)]t14(s,t,ps,pt):amone(ksi,[t:ksi]prop1(t))
t16:=[x1:not(a)]refis(ksi,y):imp(not(a),is(ksi,y,y))
t17:=th2"l.imp"(a,is(ksi,y,x),n):imp(a,is(ksi,y,x))
t18:=andi(imp(a,is(ksi,y,x)),imp(not(a),is(ksi,y,y)),t17,t16):prop1(y)
t19:=somei(ksi,[t:ksi]prop1(t),y,t18):some(ksi,[t:ksi]prop1(t))
t20:=onei(ksi,[t:ksi]prop1(t),t15,t19):one(ksi,[t:ksi]prop1(t))
y@t21:=th1"l.imp"(a,one(ksi,[t:ksi]prop1(t)),[t:a]t10(t),[t:not(a)]t20(t)):one(ksi,[t:ksi]prop1(t))
-ite
ite:=ind(ksi,[t:ksi]prop1".ite"(t),t21".ite"):ksi
+*ite
y@t22:=oneax(ksi,[t:ksi]prop1(t),t21):prop1(ite)
t23:=ande1(imp(a,is(ksi,ite,x)),imp(not(a),is(ksi,ite,y)),t22):imp(a,is(ksi,ite,x))
t24:=ande2(imp(a,is(ksi,ite,x)),imp(not(a),is(ksi,ite,y)),t22):imp(not(a),is(ksi,ite,y))
-ite
y@[a1:a]
itet:=mp(a,is(ksi,ite,x),a1,t23".ite"):is(ksi,ite,x)
y@[n:not(a)]
itef:=mp(not(a),is(ksi,ite,y),n,t24".ite"):is(ksi,ite,y)
sigma@[s0:sigma][t0:sigma]
+wissel
[s:sigma]
wa:=ite(is(s,s0),sigma,t0,s):sigma
[i:is(s,s0)]
t1:=itet(is(s,s0),sigma,t0,s,i):is(wa,t0)
s@[n:not(is(s,s0))]
t2:=itef(is(s,s0),sigma,t0,s,n):is(wa,s)
s@wb:=ite(is(s,t0),sigma,s0,wa):sigma
[i:is(s,t0)]
t3:=itet(is(s,t0),sigma,s0,wa,i):is(wb,s0)
s@[n:not(is(s,t0))]
t4:=itef(is(s,t0),sigma,s0,wa,n):is(wb,wa)
s@[i:is(s,s0)][j:is(s0,t0)]
t5:=tris(wb,s0,t0,t3(tris(s,s0,t0,i,j)),j):is(wb,t0)
i@[n:not(is(s0,t0))]
t6:=tris(wb,wa,t0,t4(th2"e.notis"(s0,t0,s,n,i)),t1(i)):is(wb,t0)
i@t7:=th1"l.imp"(is(s0,t0),is(wb,t0),[t:is(s0,t0)]t5(t),[t:not(is(s0,t0))]t6(t)):is(wb,t0)
s@[n:not(is(s,s0))][o:not(is(s,t0))]
t8:=tris(wb,wa,s,t4(o),t2(n)):is(wb,s)
-wissel
wissel:=[x:sigma]wb".wissel"(x):[x:sigma]sigma
[s:sigma][i:is(s,s0)]
iswissel1:=t7".wissel"(s,i):is(<s>wissel,t0)
s@[i:is(s,t0)]
iswissel2:=t3".wissel"(s,i):is(<s>wissel,s0)
s@[n:not(is(s,s0))][o:not(is(s,t0))]
iswissel3:=t8".wissel"(s,n,o):is(<s>wissel,s)
+*wissel
s@[t:sigma][i:is(wb(s),wb(t))][n:not(is(s,t))][j:is(s,s0)]
t9:=symnotis(s0,t,th1"e.notis"(s,t,s0,n,j)):not(is(t,s0))
[k:is(s0,t0)]
t10:=th3"e.notis"(t,s0,t0,t9,k):not(is(t,t0))
t11:=tris(wb(s),wb(t),t,i,t8(t,t9,t10)):is(wb(s),t)
t12:=<tris1(t,t0,wb(s),t11,t7(j))>t10:con
j@t13:=[v:is(s0,t0)]t12(v):not(is(s0,t0))
[k:is(t,t0)]
t14:=tris(wb(s),wb(t),s0,i,t3(t,k)):is(wb(s),s0)
t15:=t12(tris1(s0,t0,wb(s),t14,t7(j))):con
j@t16:=[v:is(t,t0)]t15(v):not(is(t,t0))
t17:=tris(wb(s),wb(t),t,i,t8(t,t9,t16)):is(wb(s),t)
t18:=t15(tris1(t,t0,wb(s),t17,t7(j))):con
n@t19:=[v:is(s,s0)]t18(v):not(is(s,s0))
t20:=t19(t,s,symis(wb(s),wb(t),i),symnotis(s,t,n)):not(is(t,s0))
[j:is(s,t0)]
t21:=symnotis(t0,t,th1"e.notis"(s,t,t0,n,j)):not(is(t,t0))
t22:=tris(wb(s),wb(t),t,i,t8(t,t20,t21)):is(wb(s),t)
t23:=<tris1(t,s0,wb(s),t22,t3(j))>t20:con
n@t24:=[v:is(s,t0)]t23(v):not(is(s,t0))
t25:=t24(t,s,symis(wb(s),wb(t),i),symnotis(s,t,n)):not(is(t,t0))
t26:=tris(wb(s),wb(t),t,i,t8(t,t20,t25)):is(wb(s),t)
t27:=<tris1(s,t,wb(s),t8(t19,t24),t26)>n:con
i@t28:=et(is(s,t),[v:not(is(s,t))]t27(v)):is(s,t)
t0@th1:=[x:sigma][y:sigma][v:is(wb(x),wb(y))]t28(x,y,v):injective(sigma,sigma,wissel)
s@[i:is(s,s0)]
t29:=tris2(s,wb(t0),s0,i,t3(t0,refis(t0))):is(s,wb(t0))
t30:=somei(sigma,[x:sigma]is(s,wb(x)),t0,t29):image(sigma,sigma,wissel,s)
s@[i:is(s,t0)]
t31:=tris2(s,wb(s0),t0,i,t7(s0,refis(s0))):is(s,wb(s0))
t32:=somei(sigma,[x:sigma]is(s,wb(x)),s0,t31):image(sigma,sigma,wissel,s)
s@[n:not(is(s,s0))][o:not(is(s,t0))]
t33:=symis(wb(s),s,t8(n,o)):is(s,wb(s))
t34:=somei(sigma,[x:sigma]is(s,wb(x)),s,t33):image(sigma,sigma,wissel,s)
n@t35:=th1"l.imp"(is(s,t0),image(sigma,sigma,wissel,s),[v:is(s,t0)]t32(v),[v:not(is(s,t0))]t34(v)):image(sigma,sigma,wissel,s)
s@t36:=th1"l.imp"(is(s,s0),image(sigma,sigma,wissel,s),[v:is(s,s0)]t30(v),[v:not(is(s,s0))]t35(v)):image(sigma,sigma,wissel,s)
t0@th2:=[x:sigma]t36(x):surjective(sigma,sigma,wissel)
th3:=andi(injective(sigma,sigma,wissel),surjective(sigma,sigma,wissel),th1,th2):bijective(sigma,sigma,wissel)
-wissel
tau@[f:[x:sigma]tau][s0:sigma][t0:sigma]
changef:=[x:sigma]<<x>wissel(s0,t0)>f:[x:sigma]tau
[s:sigma][i:is(s,s0)]
changef1:=isf(sigma,tau,f,<s>wissel(s0,t0),t0,iswissel1(s0,t0,s,i)):is(tau,<s>changef,<t0>f)
s@[i:is(s,t0)]
changef2:=isf(sigma,tau,f,<s>wissel(s0,t0),s0,iswissel2(s0,t0,s,i)):is(tau,<s>changef,<s0>f)
s@[n:not(is(s,s0))][o:not(is(s,t0))]
changef3:=isf(sigma,tau,f,<s>wissel(s0,t0),s,iswissel3(s0,t0,s,n,o)):is(tau,<s>changef,<s>f)
+*wissel
t0@[i:injective(f)]
th4:=th4"e.inj"(sigma,sigma,tau,wissel(s0,t0),f,th1(s0,t0),i):injective(changef)
t0@[s:surjective(f)]
th5:=th1"e.surj"(sigma,sigma,tau,wissel(s0,t0),f,th2(s0,t0),s):surjective(changef)
t0@[b:bijective(f)]
th6:=th1"e.bij"(sigma,sigma,tau,wissel(s0,t0),f,th3(s0,t0),b):bijective(changef)
-wissel
-e
+r
a@[b:[x:a]'prop']
imp:=b:'prop'
[a1:a][i:imp(a,b)]
mp:=<a1>i:<a1>b
+imp
b@[n:not(a)]
%set etared
th2:=[x:a]cone(<x>b,mp"l"(a,con,x,n)):imp(a,b)
%reset etared
-imp
b@ec:=[x:a]not(<x>b):'prop'
[n:not(a)]
eci1:=[x:a]cone(not(<x>b),mp"l"(a,con,x,n)):ec(a,b)
b@[a1:and(a,b)]
ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b
a@[ksi:'type']
+ite
[x1:ksi][y1:ksi]
is:=is"l.e"(ksi,x1,y1):'prop'
-ite
[x:[t:a]ksi][y:[t:not(a)]ksi][i:[t:a][u:a]is".ite"(<t>x,<u>x)][j:[t:not(a)][u:not(a)]is".ite"(<t>y,<u>y)]
+*ite
j@[z:ksi]
prop1:=and(imp(a,[t:a]is(z,<t>x)),imp(not(a),[t:not(a)]is(z,<t>y))):'prop'
j@[a1:a][x1:ksi][y1:ksi][px1:prop1(x1)][py1:prop1(y1)]
t1:=ande1"l"(imp(a,[t:a]is(x1,<t>x)),imp(not(a),[t:not(a)]is(x1,<t>y)),px1):imp(a,[t:a]is(x1,<t>x))
t2:=mp(a,[t:a]is(x1,<t>x),a1,t1):is(x1,<a1>x)
t3:=t2(y1,x1,py1,px1):is(y1,<a1>x)
t4:=tris2"l.e"(ksi,x1,y1,<a1>x,t2,t3):is(x1,y1)
a1@t5:=[s:ksi][t:ksi][ps:prop1(s)][pt:prop1(t)]t4(s,t,ps,pt):amone"l.e"(ksi,[t:ksi]prop1(t))
t6:=<a1>i:imp(a,[t:a]is(<a1>x,<t>x))
t7:=th2"r.imp"(not(a),[t:not(a)]is(<a1>x,<t>y),weli(a,a1)):imp(not(a),[t:not(a)]is(<a1>x,<t>y))
t8:=andi(imp(a,[t:a]is(<a1>x,<t>x)),imp(not(a),[t:not(a)]is(<a1>x,<t>y)),t6,t7):prop1(<a1>x)
t9:=somei(ksi,[t:ksi]prop1(t),<a1>x,t8):some(ksi,[t:ksi]prop1(t))
t10:=onei"l.e"(ksi,[t:ksi]prop1(t),t5,t9):one"l.e"(ksi,[t:ksi]prop1(t))
j@[n:not(a)][x1:ksi][y1:ksi][px1:prop1(x1)][py1:prop1(y1)]
t11:=ande2"l"(imp(a,[t:a]is(x1,<t>x)),imp(not(a),[t:not(a)]is(x1,<t>y)),px1):imp(not(a),[t:not(a)]is(x1,<t>y))
t12:=mp(not(a),[t:not(a)]is(x1,<t>y),n,t11):is(x1,<n>y)
t13:=t12(y1,x1,py1,px1):is(y1,<n>y)
t14:=tris2"l.e"(ksi,x1,y1,<n>y,t12,t13):is(x1,y1)
n@t15:=[s:ksi][t:ksi][ps:prop1(s)][pt:prop1(t)]t14(s,t,ps,pt):amone"l.e"(ksi,[t:ksi]prop1(t))
t16:=<n>j:imp(not(a),[t:not(a)]is(<n>y,<t>y))
t17:=th2"r.imp"(a,[t:a]is(<n>y,<t>x),n):imp(a,[t:a]is(<n>y,<t>x))
t18:=andi"l"(imp(a,[t:a]is(<n>y,<t>x)),imp(not(a),[t:not(a)]is(<n>y,<t>y)),t17,t16):prop1(<n>y)
t19:=somei(ksi,[t:ksi]prop1(t),<n>y,t18):some(ksi,[t:ksi]prop1(t))
t20:=onei"l.e"(ksi,[t:ksi]prop1(t),t15,t19):one"l.e"(ksi,[t:ksi]prop1(t))
j@t21:=th1"l.imp"(a,one"l.e"(ksi,[t:ksi]prop1(t)),[t:a]t10(t),[t:not(a)]t20(t)):one"l.e"(ksi,[t:ksi]prop1(t))
-ite
j@ite:=ind"l.e"(ksi,[t:ksi]prop1".ite"(t),t21".ite"):ksi
+*ite
j@t22:=oneax"l.e"(ksi,[t:ksi]prop1(t),t21):prop1(ite)
t23:=ande1"l"(imp(a,[t:a]is(ite,<t>x)),imp(not(a),[t:not(a)]is(ite,<t>y)),t22):imp(a,[t:a]is(ite,<t>x))
t24:=ande2"l"(imp(a,[t:a]is(ite,<t>x)),imp(not(a),[t:not(a)]is(ite,<t>y)),t22):imp(not(a),[t:not(a)]is(ite,<t>y))
-ite
j@[a1:a]
itet:=mp(a,[t:a]is".ite"(ite,<t>x),a1,t23".ite"):is".ite"(ksi,ite,<a1>x)
j@[n:not(a)]
itef:=mp(not(a),[t:not(a)]is".ite"(ite,<t>y),n,t24".ite"):is".ite"(ksi,ite,<n>y)
-r
+*e
+st
sigma@set:='prim':'type'
[s:sigma][s0:set]
esti:='prim':'prop'
p@setof:='prim':set
[s:sigma][sp:<s>p]
estii:='prim':esti(s,setof(p))
s@[e:esti(s,setof(p))]
estie:='prim':<s>p
sigma@[s0:set]
empty:=non([x:sigma]esti(x,s0)):'prop'
nonempty:=some([x:sigma]esti(x,s0)):'prop'
[n:[x:sigma]not(esti(x,s0))]
emptyi:=n:empty(s0)
s0@[e:empty(s0)][s:sigma]
emptye:=<s>e:not(esti(s,s0))
s0@[s:sigma][ses0:esti(s,s0)]
nonemptyi:=somei([x:sigma]esti(x,s0),s,ses0):nonempty(s0)
s0@[n:nonempty(s0)][x:'prop'][x1:[y:sigma][z:esti(y,s0)]x]
nonemptyapp:=someapp([y:sigma]esti(y,s0),n,x,x1):x
s0@[t0:set]
incl:=all([x:sigma]imp(esti(x,s0),esti(x,t0))):'prop'
[e:[x:sigma][y:esti(x,s0)]esti(x,t0)]
incli:=e:incl(s0,t0)
t0@[i:incl(s0,t0)][s:sigma][ses0:esti(s,s0)]
incle:=<ses0><s>i:esti(s,t0)
s0@refincl:=[x:sigma][y:esti(x,s0)]y:incl(s0,s0)
t0@disj:=all([x:sigma]ec(esti(x,s0),esti(x,t0))):'prop'
[n:[x:sigma][y:esti(x,s0)]not(esti(x,t0))]
disji1:=n:disj(s0,t0)
t0@[n:[x:sigma][y:esti(x,t0)]not(esti(x,s0))]
disji2:=[x:sigma]th2"l.ec"(esti(x,s0),esti(x,t0),<x>n):disj(s0,t0)
t0@[d:disj(s0,t0)][s:sigma][ses0:esti(s,s0)]
disje1:=ece1(esti(s,s0),esti(s,t0),<s>d,ses0):not(esti(s,t0))
s@[set0:esti(s,t0)]
disje2:=ece2(esti(s,s0),esti(s,t0),<s>d,set0):not(esti(s,s0))
t0@[d:disj(s0,t0)]
symdisj:=[x:sigma][y:esti(x,t0)]disje2(d,x,y):disj(t0,s0)
+disj
t0@[s:sigma][ses0:esti(s,s0)][set0:esti(s,t0)]
th1:=th1"l.all"([x:sigma]ec(esti(x,s0),esti(x,t0)),s,th4"l.imp"(esti(s,s0),not(esti(s,t0)),ses0,weli(esti(s,t0),set0))):not(disj(s0,t0))
th2:=th1(t0,s0,s,set0,ses0):not(disj(t0,s0))
-disj
t0@[i:is(set,s0,t0)][s:sigma][ses0:esti(s,s0)]
issete1:=isp(set,[x:set]esti(s,x),s0,t0,ses0,i):esti(s,t0)
s@[set0:esti(s,t0)]
issete2:=isp1(set,[x:set]esti(s,x),t0,s0,set0,i):esti(s,s0)
+isset
i@th1:=[x:sigma][y:esti(x,s0)]issete1(x,y):incl(s0,t0)
th2:=[x:sigma][y:esti(x,t0)]issete2(x,y):incl(t0,s0)
-isset
t0@[i:incl(s0,t0)][j:incl(t0,s0)]
isseti:='prim':is(set,s0,t0)
+*isset
t0@[s:sigma][ses0:esti(s,s0)][n:not(esti(s,t0))]
th3:=th3"l.imp"(is(set,s0,t0),esti(s,t0),n,[t:is(set,s0,t0)]issete1(t,s,ses0)):not(is(set,s0,t0))
th4:=symnotis(set,s0,t0,th3):not(is(set,t0,s0))
s@nissetprop:=and(esti(s,s0),not(esti(s,t0))):'prop'
[n:not(nissetprop(s0,t0,s))][e:esti(s,s0)]
t1:=et(esti(s,t0),th3"l.and"(esti(s,s0),not(esti(s,t0)),n,e)):esti(s,t0)
t0@[n:not(is(set,s0,t0))][m:not(some([x:sigma]nissetprop(s0,t0,x)))][l:non([x:sigma]nissetprop(t0,s0,x))][s:sigma]
t2:=th4"l.some"([x:sigma]nissetprop(s0,t0,x),m,s):not(nissetprop(s0,t0,s))
t3:=<s>l:not(nissetprop(t0,s0,s))
l@t4:=isseti(s0,t0,[x:sigma][y:esti(x,s0)]t1(s0,t0,x,t2(x),y),[x:sigma][y:esti(x,t0)]t1(t0,s0,x,t3(x),y)):is(set,s0,t0)
m@t5:=th3"l.imp"(non([x:sigma]nissetprop(t0,s0,x)),is(set,s0,t0),n,[y:non([x:sigma]nissetprop(t0,s0,x))]t4(y)):some([x:sigma]nissetprop(t0,s0,x))
n@th5:=th1"l.or"(some([x:sigma]nissetprop(s0,t0,x)),some([x:sigma]nissetprop(t0,s0,x)),[y:not(some([x:sigma]nissetprop(s0,t0,x)))]t5(y)):or(some([x:sigma]nissetprop(s0,t0,x)),some([x:sigma]nissetprop(t0,s0,x)))
-isset
sigma@[alpha:'type'][sa:[x:alpha]set]
unmore:=setof([x:sigma]some(alpha,[y:alpha]esti(x,<y>sa))):set
[s:sigma][a:alpha][seasa:esti(s,<a>sa)]
eunmore1:=estii([x:sigma]some(alpha,[y:alpha]esti(x,<y>sa)),s,somei(alpha,[y:alpha]esti(s,<y>sa),a,seasa)):esti(s,unmore(sa))
s@[seun:esti(s,unmore(sa))][x:'prop'][x1:[y:alpha][z:esti(s,<y>sa)]x]
unmoreapp:=someapp(alpha,[y:alpha]esti(s,<y>sa),estie([z:sigma]some(alpha,[y:alpha]esti(z,<y>sa)),s,seun),x,x1):x
+eq
sigma@[r:[x:sigma][y:sigma]'prop'][refr1:[x:sigma]<x><x>r][symr1:[x:sigma][y:sigma][t:<y><x>r]<x><y>r][trr1:[x:sigma][y:sigma][z:sigma][t:<y><x>r][u:<z><y>r]<z><x>r][s:sigma]
refr:=<s>refr1:<s><s>r
[t:sigma][tsr:<t><s>r]
symr:=<tsr><t><s>symr1:<s><t>r
t@[u:sigma][tsr:<t><s>r][utr:<u><t>r]
trr:=<utr><tsr><u><t><s>trr1:<u><s>r
u@[sur:<s><u>r][tur:<t><u>r]
tr1r:=trr(s,u,t,symr(u,s,sur),tur):<t><s>r
u@[usr:<u><s>r][utr:<u><t>r]
tr2r:=trr(s,u,t,usr,symr(t,u,utr)):<t><s>r
s@ecelt:=setof(<s>r):set
+1
th1:=estii(<s>r,s,refr):esti(s,ecelt(s))
t@[tsr:<t><s>r]
th2:=estii(<s>r,t,tsr):esti(t,ecelt(s))
t@[e:esti(t,ecelt(s))]
th3:=estie(<s>r,t,e):<t><s>r
tsr@[u:sigma][e:esti(u,ecelt(s))]
t1:=th2(t,u,tr1r(t,u,s,tsr,th3(u,e))):esti(u,ecelt(t))
tsr@th4:=isseti(ecelt(s),ecelt(t),[x:sigma][y:esti(x,ecelt(s))]t1(x,y),[x:sigma][y:esti(x,ecelt(t))]t1(t,s,symr(tsr),x,y)):is(set,ecelt(s),ecelt(t))
t@[n:not(<t><s>r)][u:sigma][e:esti(u,ecelt(s))]
t2:=th3"l.imp"(esti(u,ecelt(t)),<t><s>r,n,[x:esti(u,ecelt(t))]tr2r(s,t,u,th3(u,e),th3(t,u,x))):not(esti(u,ecelt(t)))
n@th5:=[x:sigma][y:esti(x,ecelt(s))]t2(x,y):disj(ecelt(s),ecelt(t))
s@th6:=nonemptyi(ecelt(s),s,th1):nonempty(ecelt(s))
-1
trr1@[s0:set][s:sigma]
ecp:=is(set,s0,ecelt(s)):'prop'
s0@anec:=some([x:sigma]ecp(x)):'prop'
+2
trr1@[s:sigma]
th1:=somei([x:sigma]ecp(ecelt(s),x),s,refis(set,ecelt(s))):anec(ecelt(s))
-2
[ecs0:anec(s0)]
+*2
ecs0@[s:sigma][ses0:esti(s,s0)][t:sigma][e:ecp(s0,t)]
t1:=issete1(s0,ecelt(t),e,s,ses0):esti(s,ecelt(t))
t2:=th4"eq.1"(t,s,th3"eq.1"(t,s,t1)):is(set,ecelt(t),ecelt(s))
t3:=tris(set,s0,ecelt(t),ecelt(s),e,t2):is(set,s0,ecelt(s))
ses0@th2:=someapp([x:sigma]ecp(x),ecs0,is(set,s0,ecelt(s)),[x:sigma][y:ecp(x)]t3(x,y)):is(set,s0,ecelt(s))
[t:sigma][tes0:esti(t,s0)]
th3:=th3"eq.1"(s,t,issete1(s0,ecelt(s),th2,t,tes0)):<t><s>r
t@[tsr:<t><s>r]
th4:=issete2(s0,ecelt(s),th2,t,th2"eq.1"(s,t,tsr)):esti(t,s0)
ecs0@[s:sigma][e:ecp(s0,s)]
t4:=isp(set,[x:set]nonempty(x),ecelt(s),s0,th6"eq.1"(s),symis(set,s0,ecelt(s),e)):nonempty(s0)
ecs0@th5:=someapp([x:sigma]ecp(x),ecs0,nonempty(s0),[x:sigma][y:ecp(x)]t4(x,y)):nonempty(s0)
-2
+3
ecs0@[t0:set][ect0:anec(t0)][s:sigma][ses0:esti(s,s0)][t:sigma][tet0:esti(t,t0)][tsr:<t><s>r]
th1:=tr3is(set,s0,ecelt(s),ecelt(t),t0,th2"eq.2"(s0,ecs0,s,ses0),th4"eq.1"(s,t,tsr),symis(set,t0,ecelt(t),th2"eq.2"(t0,ect0,t,tet0))):is(set,s0,t0)
tet0@[n:not(<t><s>r)]
t1:=isp1(set,[x:set]disj(x,ecelt(t)),ecelt(s),s0,th5"eq.1"(s,t,n),th2"eq.2"(s0,ecs0,s,ses0)):disj(s0,ecelt(t))
th2:=isp1(set,[x:set]disj(s0,x),ecelt(t),t0,t1,th2"eq.2"(t0,ect0,t,tet0)):disj(s0,t0)
t0@[i:is(set,s0,t0)][s:sigma][ses0:esti(s,s0)]
t2:=issete1(s0,t0,i,s,ses0):esti(s,t0)
t3:=th1"st.disj"(s0,t0,s,ses0,t2):not(disj(s0,t0))
i@th3:=nonemptyapp(s0,th5"eq.2"(s0,ecs0),not(disj(s0,t0)),[x:sigma][y:esti(x,s0)]t3(x,y)):not(disj(s0,t0))
-3
trr1@ect:=ot(set,[x:set]anec(x)):'type'
ecs0@ectset:=out(set,[x:set]anec(x),s0,ecs0):ect
trr1@[s:sigma]
ectelt:=ectset(ecelt(s),th1".2"(s)):ect
trr1@[e:ect]
ecect:=in(set,[x:set]anec(x),e):set
+4
th1:=inp(set,[x:set]anec(x),e):anec(ecect(e))
th2:=th5"eq.2"(ecect(e),th1):nonempty(ecect(e))
[x:'prop'][x1:[y:sigma][z:esti(y,ecect(e))]x]
th3:=nonemptyapp(ecect(e),th2,x,x1):x
s@th4:=isinout(set,[x:set]anec(x),ecelt(s),th1"eq.2"(s)):is(set,ecelt(s),ecect(ectelt(s)))
th5:=issete1(ecelt(s),ecect(ectelt(s)),th4,s,th1"eq.1"(s)):esti(s,ecect(ectelt(s)))
th6:=eunmore1(ect,[x:ect]ecect(x),s,ectelt(s),th5):esti(s,unmore(ect,[x:ect]ecect(x)))
e@[s:sigma][see:esti(s,ecect(e))][t:sigma][tee:esti(t,ecect(e))]
th7:=th3"eq.2"(ecect(e),th1,s,see,t,tee):<t><s>r
t@[tsr:<t><s>r]
th8:=th4"eq.2"(ecect(e),th1,s,see,t,tsr):esti(t,ecect(e))
-4
+5
[f:ect][i:is(ect,e,f)]
th1:=isini(set,[x:set]anec(x),e,f,i):is(set,ecect(e),ecect(f))
f@[i:is(set,ecect(e),ecect(f))]
th2:=isine(set,[x:set]anec(x),e,f,i):is(ect,e,f)
f@[s:sigma][see:esti(s,ecect(e))][t:sigma][tef:esti(t,ecect(f))][tsr:<t><s>r]
th3:=th2(th1"eq.3"(ecect(e),th1"eq.4"(e),ecect(f),th1"eq.4"(f),s,see,t,tef,tsr)):is(ect,e,f)
see@[i:is(ect,e,f)]
th4:=issete1(ecect(e),ecect(f),th1(i),s,see):esti(s,ecect(f))
tef@[i:is(ect,e,f)]
th5:=th3"eq.2"(ecect(f),th1"eq.4"(f),s,th4(i),t,tef):<t><s>r
trr1@[s:sigma][t:sigma][tsr:<t><s>r]
th6:=isouti(set,[x:set]anec(x),ecelt(s),th1"eq.2"(s),ecelt(t),th1"eq.2"(t),th4"eq.1"(s,t,tsr)):is(ect,ectelt(s),ectelt(t))
-5
trr1@[alpha:'type'][fu:[x:sigma]alpha]
fixfu:=[x:sigma][y:sigma][z:<y><x>r]is(alpha,<x>fu,<y>fu):'prop'
+10
[ff:fixfu][e:ect][a1:alpha][s:sigma]
prop1:=and(esti(s,ecect(e)),is(alpha,<s>fu,a1)):'prop'
a1@prop2:=some([x:sigma]prop1(x)):'prop'
e@[s:sigma][see:esti(s,ecect(e))]
t1:=andi(esti(s,ecect(e)),is(alpha,<s>fu,<s>fu),see,refis(alpha,<s>fu)):prop1(<s>fu,s)
t2:=somei([x:sigma]prop1(<s>fu,x),s,t1):prop2(<s>fu)
t3:=somei(alpha,[x:alpha]prop2(x),<s>fu,t2):some(alpha,[x:alpha]prop2(x))
e@t4:=th3"eq.4"(e,some(alpha,[x:alpha]prop2(x)),[x:sigma][y:esti(x,ecect(e))]t3(x,y)):some(alpha,[x:alpha]prop2(x))
a1@[b1:alpha][pa1:prop2(a1)][pb1:prop2(b1)][s:sigma][pa1s:prop1(a1,s)][t:sigma][pb1t:prop1(b1,t)]
t5:=ande1(esti(s,ecect(e)),is(alpha,<s>fu,a1),pa1s):esti(s,ecect(e))
t6:=ande1(esti(t,ecect(e)),is(alpha,<t>fu,b1),pb1t):esti(t,ecect(e))
t7:=th7"eq.4"(e,s,t5,t,t6):<t><s>r
t8:=ande2(esti(s,ecect(e)),is(alpha,<s>fu,a1),pa1s):is(alpha,<s>fu,a1)
t9:=ande2(esti(t,ecect(e)),is(alpha,<t>fu,b1),pb1t):is(alpha,<t>fu,b1)
t10:=tr3is(alpha,a1,<s>fu,<t>fu,b1,symis(alpha,<s>fu,a1,t8),<t7><t><s>ff,t9):is(alpha,a1,b1)
pa1s@t11:=someapp([x:sigma]prop1(b1,x),pb1,is(alpha,a1,b1),[x:sigma][y:prop1(b1,x)]t10(x,y)):is(alpha,a1,b1)
pb1@t12:=someapp([x:sigma]prop1(a1,x),pa1,is(alpha,a1,b1),[x:sigma][y:prop1(a1,x)]t11(x,y)):is(alpha,a1,b1)
e@t13:=[x:alpha][y:alpha][u:prop2(x)][v:prop2(y)]t12(x,y,u,v):amone(alpha,[x:alpha]prop2(x))
t14:=onei(alpha,[x:alpha]prop2(x),t13,t4):one(alpha,[x:alpha]prop2(x))
-10
e".10"@indeq:=ind(alpha,[x:alpha]prop2".10"(x),t14".10"):alpha
+*10
e@th1:=oneax(alpha,[x:alpha]prop2(x),t14):some([x:sigma]and(esti(x,ecect(e)),is(alpha,<x>fu,indeq)))
[s:sigma][see:esti(s,ecect(e))]
th2:=t12(<s>fu,indeq,t2(s,see),th1):is(alpha,<s>fu,indeq)
ff@[s:sigma]
th3:=th2(ectelt(s),s,th5"eq.4"(s)):is(alpha,<s>fu,indeq(ectelt(s)))
-10
alpha@[fu2:[x:sigma][y:sigma]alpha]
fixfu2:=[x:sigma][y:sigma][z:sigma][u:sigma][v:<y><x>r][w:<u><z>r]is(alpha,<z><x>fu2,<u><y>fu2):'prop'
+11
[ff2:fixfu2][s:sigma][t:sigma][tsr:<t><s>r][u:sigma]
t1:=<refr(u)><tsr><u><u><t><s>ff2:is(alpha,<u><s>fu2,<u><t>fu2)
tsr@t2:=fisi(sigma,alpha,<s>fu2,<t>fu2,[x:sigma]t1(x)):is([x:sigma]alpha,<s>fu2,<t>fu2)
ff2@[e:ect]
i:=indeq([x:sigma]alpha,fu2,[x:sigma][y:sigma][z:<y><x>r]t2(x,y,z),e):[x:sigma]alpha
[s:sigma][t:sigma][tsr:<t><s>r][u:sigma][uee:esti(u,ecect(e))]
t3:=th2"eq.10"([x:sigma]alpha,fu2,[x:sigma][y:sigma][z:<y><x>r]t2(x,y,z),e,u,uee):is([x:sigma]alpha,<u>fu2,i)
t4:=fise(alpha,<u>fu2,i,t3,s):is(alpha,<s><u>fu2,<s>i)
t5:=fise(alpha,<u>fu2,i,t3,t):is(alpha,<t><u>fu2,<t>i)
t6:=<tsr><refr(u)><t><s><u><u>ff2:is(alpha,<s><u>fu2,<t><u>fu2)
t7:=tr3is(alpha,<s>i,<s><u>fu2,<t><u>fu2,<t>i,symis(alpha,<s><u>fu2,<s>i,t4),t6,t5):is(alpha,<s>i,<t>i)
tsr@t8:=th3"eq.4"(e,is(alpha,<s>i,<t>i),[x:sigma][y:esti(x,ecect(e))]t7(x,y)):is(alpha,<s>i,<t>i)
-11
e".11"@[f:ect]
indeq2:=indeq(i".11",[x:sigma][y:sigma][z:<y><x>r]t8".11"(x,y,z),f):alpha
+*11
f@[s:sigma][see:esti(s,ecect(e))][t:sigma][tef:esti(t,ecect(f))]
t9:=th2"eq.10"(i,[x:sigma][y:sigma][z:<y><x>r]t8(x,y,z),f,t,tef):is(alpha,<t>i,indeq2(e,f))
t10:=th2"eq.10"([x:sigma]alpha,fu2,[x:sigma][y:sigma][z:<y><x>r]t2(x,y,z),e,s,see):is([x:sigma]alpha,<s>fu2,i)
t11:=fise(alpha,<s>fu2,i,t10,t):is(alpha,<t><s>fu2,<t>i)
th1:=tris(alpha,<t><s>fu2,<t>i,indeq2,t11,t9):is(alpha,<t><s>fu2,indeq2(e,f))
ff2@[s:sigma][t:sigma]
th2:=th1(ectelt(s),ectelt(t),s,th5"eq.4"(s),t,th5"eq.4"(t)):is(alpha,<t><s>fu2,indeq2(ectelt(s),ectelt(t)))
-11