helm/software/lambda-delta/automath/grundlagen_pn.aut

   1 +l
   2 [a:PROP][b:PROP]
   3 imp:=[x,a]b:PROP
   4 @con:=PRIM:PROP
   5 a@not:=imp(con):PROP
   6 wel:=not(not(a)):PROP
   7 [w:wel(a)]
   8 et:=PRIM:a
   9 b@ec:=imp(a,not(b)):PROP
  10 and:=not(ec(a,b)):PROP
  11 @[sigma:TYPE][p:[x,sigma]PROP]
  12 all:=p:PROP
  13 non:=[x,sigma]not(<x>p):[x,sigma]PROP
  14 some:=not(non(p)):PROP
  15 +e
  16 sigma@[s:sigma][t:sigma]
  17 is:=PRIM:PROP
  18 s@refis:=PRIM:is(s,s)
  19 p@[s:sigma][t:sigma][sp:<s>p][i:is(s,t)]
  20 isp:=PRIM:<t>p
  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
  23 [o1:one(sigma,p)]
  24 ind:=PRIM:sigma
  25 oneax:=PRIM:<ind>p
  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
  28 [t0:tau]
  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)
  32 p@ot:=PRIM:TYPE
  33 [o1:ot]
  34 in:=PRIM:sigma
  35 inp:=PRIM:<in>p
  36 p@otax1:=PRIM:injective(ot,sigma,[x,ot]in(x))
  37 [s:sigma][sp:<s>p]
  38 otax2:=PRIM:image(ot,sigma,[x,ot]in(x),s)
  39 tau@pairtype:=PRIM:TYPE
  40 [s:sigma][t:tau]
  41 pair:=PRIM:pairtype
  42 tau@[p1:pairtype]
  43 first:=PRIM:sigma
  44 second:=PRIM:tau
  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)
  48 +st
  49 sigma@set:=PRIM:TYPE
  50 [s:sigma][s0:set]
  51 esti:=PRIM:PROP
  52 p@setof:=PRIM:set
  53 [s:sigma][sp:<s>p]
  54 estii:=PRIM:esti(s,setof(p))
  55 s@[e:esti(s,setof(p))]
  56 estie:=PRIM:<s>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)
  61 +eq
  62 +landau
  63 +n
  64 @nat:=PRIM:TYPE
  65 [x:nat][y:nat]
  66 is:=is(nat,x,y):PROP
  67 nis:=not(is(x,y)):PROP
  68 x@[s:set(nat)]
  69 in:=esti(nat,x,s):PROP
  70 @[p:[x,nat]PROP]
  71 all:=all(nat,p):PROP
  72 @1:=PRIM:nat
  73 suc:=PRIM:[x,nat]nat
  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)
  76 [s:set(nat)]
  77 cond1:=in(1,s):PROP
  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)
  80 -n
  81 -landau
  82 -eq
  83 -st
  84 -e
  85 -l