# 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/)
-# 2008, revised by F. Guidi to remove the eta-reductions
+# 2008, revised by F. Guidi to remove eta-reductions
+# 2014, revised by F. Guidi to remove sort inclusions on binders of degree 1
# 2014, revised by F. Guidi to suggest @-typing removal
+l
thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b)
-iff
@[sigma:'type'][p:[x:sigma]'prop']
-%suggestion by van Daalen to remove the first eta-reduction
+%suggestion by van Daalen to remove eta-reduction
%all:=p:'prop' %original line
all:=[x:sigma]<x>p:'prop'
%end of suggestion
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'
-{ to validate }
+%suggestion by Guidi to remove sort inclusion of degree 1 by adding all-introduction
+none:=all(sigma,non(p)):'prop'
+%end of suggestion ("non" replaced by "none" where needed)
+some:=not(none(p)):'prop' %none
[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]
+p@[n:not(all(sigma,p))][m:none(non(p))][s:sigma] %none
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))
+n@th1:=[x:none(non(p))]t2(x):some(non(p)) %none
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)
+th3:=et(none(p),n):none(p) %none x 2
[s:sigma]
th4:=<s>th3:not(<s>p)
-p@[n:non(p)]
-th5:=weli(non(p),n):not(some(sigma,p))
+p@[n:none(p)] %none
+th5:=weli(none(p),n):not(some(sigma,p)) %none
-some
p@[s:some(sigma,p)][x:'prop'][i:[y:sigma]imp(<y>p,x)]
+*some
-e
+r
a@[b:[x:a]'prop']
-%suggestion by van Daalen to remove the second eta-reduction
+%suggestion by van Daalen to remove eta-reduction
%imp:=b:'prop' %original line
imp:=[x:a]<x>b:'prop'
%end of suggestion
[n:not(a)]
eci1:=[x:a]cone(not(<x>b),mp"l"(a,con,x,n)):ec(a,b)
%suggestion by Guidi to remove @-typing by adding imp-introduction
-b@[a1:and(a,b)] %original line
-ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b %original line
-%b@[a1:and(a,imp(a,b))]
-%ande2:=<ande1(a,imp(a,b),a1)>ande2"l"(a,imp(a,b),a1):<ande1(a,imp(a,b),a1)>b
+%b@[a1:and(a,b)] %original line
+%ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b %original line
+b@[a1:and(a,imp(a,b))]
+ande2:=<ande1(a,imp(a,b),a1)>ande2"l"(a,imp(a,b),a1):<ande1(a,imp(a,b),a1)>b
%end of suggestion
a@[ksi:'type']
+ite
s@[e:esti(s,setof(p))]
estie:='prim':<s>p
sigma@[s0:set]
-empty:=non([x:sigma]esti(x,s0)):'prop'
+empty:=none([x:sigma]esti(x,s0)):'prop' %none
nonempty:=some([x:sigma]esti(x,s0)):'prop'
[n:[x:sigma]not(esti(x,s0))]
emptyi:=n:empty(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]
+t0@[n:not(is(set,s0,t0))][m:not(some([x:sigma]nissetprop(s0,t0,x)))][l:none([x:sigma]nissetprop(t0,s0,x))][s:sigma] %none
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))
+m@t5:=th3"l.imp"(none([x:sigma]nissetprop(t0,s0,x)),is(set,s0,t0),n,[y:none([x:sigma]nissetprop(t0,s0,x))]t4(y)):some([x:sigma]nissetprop(t0,s0,x)) %none x 2
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]
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)]
+s@[n:none(nat,[x:nat]and(lb(x),not(lb(pl(x,1)))))][m:nat][l:lb(m)] %none
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)))))
+s@t13:=[x:none(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))))) %none
[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)))
-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]
+p@[n:none(nat,[x:nat]min(x))][u:nat] %none
t24:=[x:<u>p]satz24a(u):lbprop(1,u)
n@t25:=[x:nat]t24(x):lb(1)
u@[l:lb(u)]
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))
+t38:=[y:none(nat,[x:nat]min(x))]mp(lb(<u>suc),con,t34(y,<u>suc),t37):some([x:nat]min(x)) %none
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
-eq
-st
-e
-{}
-l