<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
#!/usr/local/bin/aut

{ ----------------------------- first order logic -----------------------15-- }

* prop : TYPE := PRIM
* [a:prop] proof : TYPE := PRIM
* set : TYPE := PRIM

* false : prop := PRIM
a * [b:prop] imp : prop := PRIM
* [p:[z,set]prop] for : prop := PRIM
* [x:set][y:set] eq : prop := PRIM
y * in : prop := PRIM

a * not : prop := imp(a,false)
b * and : prop := not(imp(a,not(b)))
b * iff : prop := and(imp(a,b),imp(b,a))
p * ex : prop := not(for([z,set]not(<z>p)))

b * [_:[_1,proof(a)]proof(b)] imp_intro : proof(imp(a,b)) := PRIM
b * [_:proof(imp(a,b))][_1:proof(a)] imp_elim : proof(b) := PRIM
p * [_:[z,set]proof(<z>p)] for_intro : proof(for(p)) := PRIM
p * [_:proof(for(p))][z:set] for_elim : proof(<z>p) := PRIM
a * [_:proof(not(not(a)))] classical : proof(a) := PRIM

x * eq_intro : proof(eq(x,x)) := PRIM
y * [_:proof(eq(x,y))][q:[z,set]prop][_1:proof(<x>q)]
  eq_elim : proof(<y>q) := PRIM

{ ----------------------------- stratification levels --------------------3-- }

* nat : TYPE := PRIM
* 0 : nat := PRIM
* [n:nat] S : nat := PRIM

{ ----------------------------- stratified formulas ---------------------14-- }

* prop' : TYPE := PRIM
n * set' : TYPE := PRIM

* false' : prop' := PRIM
* [a':prop'][b':prop'] imp' : prop' := PRIM
n * [p':[z',set'(n)]prop'] for' : prop' := PRIM
n * [x':set'(n)][y':set'(n)] eq' : prop' := PRIM
n * [x':set'(n)][y':set'(S(n))] in' : prop' := PRIM

a * [a':prop'] same_prop : TYPE := PRIM
n * [x:set][x':set'(n)] same_set : TYPE := PRIM

* same_false : same_prop(false,false') := PRIM
a' * [_1:same_prop(a,a')][b:prop][b':prop'][_2:same_prop(b,b')]
  same_imp : same_prop(imp(a,b),imp'(a',b')) := PRIM
n * [p:[z,set]prop][p':[z',set'(n)]prop']
  [_1:[z,set][z',set'(n)][_:same_set(n,z,z')]same_prop(<z>p,<z'>p')]
  same_for : same_prop(for(p),for'(n,p')) := PRIM
n * [x:set][x':set'(n)][_1:same_set(n,x,x')][y:set]
  [y':set'(n)][_2:same_set(n,y,y')]
  same_eq : same_prop(eq(x,y),eq'(n,x',y')) := PRIM
y * [y':set'(S(n))][_2:same_set(S(n),y,y')]
  same_in : same_prop(in(x,y),in'(n,x',y')) := PRIM

{ ----------------------------- new foundations --------------------------5-- }

* [y:set][z:set]
  axiom_1 : proof(imp(for([x,set]iff(in(x,y),in(x,z))),eq(y,z))) := PRIM

# n * [phi:[x,set]prop][phi':[x',set'(n)]prop']
#   [_1:[x,set][x',set'(n)][_,same_set(n,x,x')]same_prop(<x>phi,<x'>phi')]
#   axiom_2 : proof(ex([A,set]for([x,set]iff(in(x,A),<x>phi)))) := PRIM

a * axiom_scheme : TYPE := PRIM

* [phi:[x,set]prop]
  axiom_base : axiom_scheme(ex([A,set]for([x,set]iff(in(x,A),<x>phi)))) := PRIM
* [p:[z,set]prop][_1:[z,set]axiom_scheme(<z>p)]
  axiom_for : axiom_scheme(for(p)) := PRIM

a' * [_1:axiom_scheme(a)][_2:same_prop(a,a')] axiom_2 : proof(a) := PRIM