<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

{ ----------------------------- meta logic -------------------------------8-- }

* typ : TYPE := PRIM
* [tau:typ] term : TYPE := PRIM

tau * [tau':typ] fun : typ := PRIM
* prop : typ := PRIM

tau' * [t:[x,term(tau)]term(tau')]
  lambda {Abs} : term(fun(tau,tau')) := PRIM
tau' * [t:term(fun(tau,tau'))][t':term(tau)]
  app {$} : term(tau') := PRIM

* [alpha:typ] all : term(fun(fun(alpha,prop),prop)) := PRIM
* imp {==>} : term(fun(prop,fun(prop,prop))) := PRIM

alpha * [P:term(fun(alpha,prop))] all' : term(prop) :=
  app(fun(alpha,prop),prop,all,P)
* [phi:term(prop)][psi:term(prop)] imp' : term(prop) :=
  app(prop,prop,app(prop,fun(prop,prop),imp,phi),psi)

{ ----------------------------- proof terms ------------------------------5-- }

phi * proof : TYPE := PRIM

psi * [p:[h,proof(phi)]proof(psi)]
  imp_intro {AbsP} : proof(imp'(phi,psi)) := PRIM
psi * [p:proof(imp'(phi,psi))][q:proof(phi)]
  imp_elim {%%} : proof(psi) := PRIM
tau * [phi:[x,term(tau)]term(prop)][p:[x,term(tau)]proof(<x>phi)]
  all_intro {Abst} : proof(all'(tau,lambda(tau,prop,phi))) := PRIM
phi * [p:proof(all'(tau,lambda(tau,prop,phi)))][t:term(tau)]
  all_elim {%} : proof(<t>phi) := PRIM

{ ----------------------------- equality --------------------------------10-- }

tau * eq {==} : term(fun(tau,fun(tau,prop))) := PRIM
tau * [a:term(tau)][b:term(tau)] eq' : term(prop) :=
  app(tau,prop,app(tau,fun(tau,prop),eq,a),b)

* [phi:term(prop)][psi:term(prop)]
  [_1:proof(imp'(phi,psi))][_2:proof(imp'(psi,phi))]
  eq_intro : proof(eq'(prop,phi,psi)) := PRIM
psi * [_1:proof(eq'(prop,phi,psi))][_2:proof(phi)] eq_elim : proof(psi) := PRIM

a * refl : proof(eq'(a,a)) := PRIM
b * [_1:proof(eq'(a,b))] sym : proof(eq'(b,a)) := PRIM
b * [c:term(tau)][_1:proof(eq'(a,b))][_2:proof(eq'(b,c))]
  trans : proof(eq'(a,c)) := PRIM

tau' * [a:[x,term(tau)]term(tau')][b:term(tau)]
  beta : proof(eq'(tau',app(lambda(a),b),<b>a)) := PRIM
tau' * [f:term(fun(tau,tau'))][g:term(fun(tau,tau'))]
  [_1:[x:term(tau)]proof(eq'(tau',app(f,x),app(g,x)))]
  ext : proof(eq'(fun(tau,tau'),f,g)) := PRIM
a * [b:[x,term(tau)]term(tau')][_1:[x,term(tau)]proof(eq'(tau',<x>a,<x>b))]
  abs : proof(eq'(fun(tau,tau'),lambda(a),lambda(b))) := PRIM
g * [a:term(tau)][b:term(tau)]
  [_1:proof(eq'(fun(tau,tau'),f,g))][_2:proof(eq'(a,b))]
  comb : proof(eq'(tau',app(f,a),app(g,b))) := PRIM