9 b@ec:=imp(a,not(b)):PROP
10 and:=not(ec(a,b)):PROP
11 @[sigma:TYPE][p:[x,sigma]PROP]
13 non:=[x,sigma]not(<x>p):[x,sigma]PROP
14 some:=not(non(p)):PROP
16 sigma@[s:sigma][t:sigma]
19 p@[s:sigma][t:sigma][sp:<s>p][i:is(s,t)]
21 p@amone:=[x,sigma][y,sigma][u,<x>p][v,<y>p]is(x,y):PROP
22 one:=and(amone(sigma,p),some(sigma,p)):PROP
26 sigma@[tau:TYPE][f:[x,sigma]tau]
27 injective:=all([x,sigma]all([y,sigma]imp(is(tau,<x>f,<y>f),is(x,y)))):PROP
29 image:=some([x,sigma]is(tau,t0,<x>f)):PROP
30 tau@[f:[x,sigma]tau][g:[x,sigma]tau][i:[x,sigma]is(tau,<x>f,<x>g)]
31 fisi:=PRIM:is([x,sigma]tau,f,g)
36 p@otax1:=PRIM:injective(ot,sigma,[x,ot]in(x))
38 otax2:=PRIM:image(ot,sigma,[x,ot]in(x),s)
39 tau@pairtype:=PRIM:TYPE
45 pairis1:=PRIM:is(pairtype,pair(first,second),p1)
46 t@firstis1:=PRIM:is(sigma,first(pair),s)
47 secondis1:=PRIM:is(tau,second(pair),t)
54 estii:=PRIM:esti(s,setof(p))
55 s@[e:esti(s,setof(p))]
57 sigma@[s0:set][t0:set]
58 incl:=all([x,sigma]imp(esti(x,s0),esti(x,t0))):PROP
59 [i:incl(s0,t0)][j:incl(t0,s0)]
60 isseti:=PRIM:is(set,s0,t0)
67 nis:=not(is(x,y)):PROP
69 in:=esti(nat,x,s):PROP
74 ax3:=PRIM:[x,nat]nis(<x>suc,1)
75 ax4:=PRIM:[x,nat][y,nat][u,is(<x>suc,<y>suc)]is(x,y)
78 cond2:=all([x,nat]imp(in(x,s),in(<x>suc,s))):PROP
79 @ax5:=PRIM:[s,set(nat)][u,cond1(s)][v,cond2(s)][x,nat]in(x,s)