# Landau's "Grundlagen der Analysis", formal specification in AUTOMATH
# Copyright (C) 1977, L.S. van Benthem Jutting
#               1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)

+l
[a:PROP][b:PROP]
imp:=[x,a]b:PROP
@con:=PRIM:PROP
a@not:=imp(con):PROP
wel:=not(not(a)):PROP
[w:wel(a)]
et:=PRIM:a
b@ec:=imp(a,not(b)):PROP
and:=not(ec(a,b)):PROP
@[sigma:TYPE][p:[x,sigma]PROP]
all:=p:PROP
non:=[x,sigma]not(<x>p):[x,sigma]PROP
some:=not(non(p)):PROP
+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
p@amone:=[x,sigma][y,sigma][u,<x>p][v,<y>p]is(x,y):PROP
one:=and(amone(sigma,p),some(sigma,p)):PROP
[o1:one(sigma,p)]
ind:=PRIM:sigma
oneax:=PRIM:<ind>p
sigma@[tau:TYPE][f:[x,sigma]tau]
injective:=all([x,sigma]all([y,sigma]imp(is(tau,<x>f,<y>f),is(x,y)))):PROP
[t0:tau]
image:=some([x,sigma]is(tau,t0,<x>f)):PROP
tau@[f:[x,sigma]tau][g:[x,sigma]tau][i:[x,sigma]is(tau,<x>f,<x>g)]
fisi:=PRIM:is([x,sigma]tau,f,g)
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)
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)
t@firstis1:=PRIM:is(sigma,first(pair),s)
secondis1:=PRIM:is(tau,second(pair),t)
+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][t0:set]
incl:=all([x,sigma]imp(esti(x,s0),esti(x,t0))):PROP
[i:incl(s0,t0)][j:incl(t0,s0)]
isseti:=PRIM:is(set,s0,t0)
+eq
+landau
+n
@nat:=PRIM:TYPE
[x:nat][y:nat]
is:=is(nat,x,y):PROP
nis:=not(is(x,y)):PROP
x@[s:set(nat)]
in:=esti(nat,x,s):PROP
@[p:[x,nat]PROP]
all:=all(nat,p):PROP
@1:=PRIM:nat
suc:=PRIM:[x,nat]nat
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)
-n
-landau
-eq
-st
-e
-l