<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

{ ----------------------------- the types --------------------------------3-- }

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

{ ----------------------------- first order logic ------------------------5-- }

* 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 * or : prop := imp(not(a),b)
b * iff : prop := and(imp(a,b),imp(b,a))
p * ex : prop := not(for([z,set]not(<z>p)))
p * unique : prop :=
  for([z,set]imp(<z>p,for([z',set]imp(<z'>p,eq(z,z')))))
p * ex_unique : prop := and(ex,unique)

{ ----------------------------- natural deduction ------------------------7-- }

# a * [_:proof(a)][_':proof(a)][h:[_,proof(a)]prop][_1:proof(<_>h)]
#     irrelevance : proof(<_'>h) := PRIM

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

{ ----------------------------- definition by cases ----------------------2-- }

y * [c:prop] cases : set := PRIM
c * cases_axiom :
  proof(and(imp(c,eq(cases(x,y,c),x)),imp(not(c),eq(cases(x,y,c),y)))) := PRIM

{ ----------------------------- set theory -------------------------------6-- }

* empty : set := PRIM
y * double : set := PRIM # {x,y}
x * unions : set := PRIM
x * powerset : set := PRIM
x * [f:[z,set]set] replace : set := PRIM
* omega : set := PRIM

x * single : set := double(x,x)
x * [q:[z,set]prop] restrict : set :=
  unions(replace(x,[z,set]cases(single(z),empty,<z>q)))
y * inter : set := restrict(x,[z,set]in(z,y))
y * union : set := unions(double(x,y))
x * succ : set := union(x,single(x))
y * subset : prop := for([z,set]imp(in(z,x),in(z,y)))
y * disjoint : prop := eq(inter(x,y),empty)
x * omega_closed : prop :=
  and(in(empty,x),for([n,set]imp(in(n,x),in(succ(n),x))))

{ ----------------------------- the axioms -------------------------------8-- }

y * extensionality :
  proof(iff(eq(x,y),for([z,set]iff(in(z,x),in(z,y))))) := PRIM
x * foundation :
  proof(imp(not(eq(x,empty)),ex([z,set]and(in(z,x),disjoint(z,x))))) := PRIM

* empty_axiom : proof(for([z,set]not(in(z,empty)))) := PRIM
y * double_axiom :
  proof(for([z,set]iff(in(z,double(x,y)),or(eq(z,x),eq(z,y))))) := PRIM
x * unions_axiom :
  proof(for([z,set]iff(in(z,unions(x)),ex([y,set]and(in(z,y),in(y,x))))))
  := PRIM
x * powerset_axiom :
  proof(for([z,set]iff(in(z,powerset(x)),subset(z,x)))) := PRIM
f * replace_axiom :
  proof(for([z,set]iff(in(z,replace(x,f)),ex([y,set]and(in(y,x),eq(z,<y>f))))))
  := PRIM
* omega_axiom :
  proof(and(omega_closed(omega),
    for([o,set]imp(omega_closed(o),subset(omega,o))))) := PRIM

{ ----------------------------- choice -----------------------------------1-- }

* AC :
  proof(for([x,set]imp(
   and(for([y,set]imp(in(y,x),not(eq(y,empty)))),
     for([y1,set]imp(in(y1,x),for([y2,set]imp(in(y2,x),
       or(eq(y1,y2),disjoint(y1,y2))))))),
   ex([x',set]for([y,set]imp(in(y,x),ex_unique([y',set]
     and(in(y',x'),in(y',y))))))))) := PRIM