<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

{ ----------------------------- type.ml ----------------------------------3-- }

* type : TYPE := PRIM
* bool : type := PRIM
* [A:type][B:type] fun : type := PRIM

{ ----------------------------- term.ml ----------------------------------4-- }

A * term : TYPE := PRIM
B * [t:term(fun(A,B))][u:term(A)] comb : term(B) := PRIM
B * [t:[x,term(A)]term(B)] lambda : term(fun(A,B)) := PRIM
    # "abs" is used in the type definitions
A * eq : term(fun(A,fun(A,bool))) := PRIM
A * [t:term(A)][u:term(A)] eq' : term(bool) :=
  comb(A,bool,comb(A,fun(A,bool),eq(A),t),u)

{ ----------------------------- thm.ml ----------------------------------13-- }

* [t:term(bool)] thm : TYPE := PRIM
A * [t:term(A)]
  REFL : thm(eq'(A,t,t)) := PRIM
B * [s:term(fun(A,B))][t:term(fun(A,B))][u:term(A)][v:term(A)]
  [_st:thm(eq'(fun(A,B),s,t))][_uv:thm(eq'(A,u,v))]
  MK_COMB : thm(eq'(B,comb(s,u),comb(t,v))) := PRIM
B * [s:[x,term(A)]term(B)][t:[x,term(A)]term(B)]
  [_st:[x,term(A)]thm(eq'(B,<x>s,<x>t))]
  ABS : thm(eq'(fun(A,B),lambda(s),lambda(t))) := PRIM
B * [t:[x,term(A)]term(B)][x:term(A)]
  BETA : thm(eq'(B,comb(A,B,lambda(t),x),<x>t)) := PRIM
  # ASSUME
* [p:term(bool)][q:term(bool)][_pq:thm(eq'(bool,p,q))][_p:thm(p)]
  EQ_MP : thm(q) := PRIM
q * [_p:[_q,thm(q)]thm(p)][_q:[_p,thm(p)]thm(q)]
  DEDUCT_ANTISYM_RULE : thm(eq'(bool,p,q)) := PRIM
  # INST
  # INST_TYPE
{
A * [s:term(A)][t:term(A)][u:term(A)][_st:thm(eq'(A,s,t))][_tu:thm(eq'(A,t,u))]
  TRANS : thm(eq'(A,s,u)) := EQ_MP(eq'(A,s,t),eq'(A,s,u),
    MK_COMB(A,bool,comb(A,fun(A,bool),eq(A),s),comb(A,fun(A,bool),eq(A),s),
      t,u,REFL(fun(A,bool),comb(A,fun(A,bool),eq(A),s)),_tu),_st)
}

  # new_definition
A * [P:term(fun(A,bool))][t:term(A)][_Pt:thm(comb(A,bool,P,t))]
  new_type : type := PRIM
_Pt * abs : term(fun(A,new_type)) := PRIM
_Pt * rep : term(fun(new_type,A)) := PRIM
_Pt * [a:term(new_type)]
  _absrep : thm(eq'(new_type,comb(A,new_type,abs,comb(new_type,A,rep,a)),a))
  := PRIM
_Pt * [r:term(A)]
  _repabs : thm(eq'(bool,comb(A,bool,P,r),
    eq'(A,comb(new_type,A,rep,comb(A,new_type,abs,r)),r))) := PRIM

{ ----------------------------- bool.ml ----------------------------------0-- }

* T : term(bool) :=
  eq'(fun(bool,bool),lambda(bool,bool,[x,term(bool)]x),
    lambda(bool,bool,[x,term(bool)]x))
* and : term(fun(bool,fun(bool,bool))) :=
  lambda(bool,fun(bool,bool),[t1,term(bool)]lambda(bool,bool,[t2,term(bool)]
    eq'(fun(fun(bool,fun(bool,bool)),bool),
      lambda(fun(bool,fun(bool,bool)),bool,[f,term(fun(bool,fun(bool,bool)))]
        comb(bool,bool,comb(bool,fun(bool,bool),f,t1),t2)),
      lambda(fun(bool,fun(bool,bool)),bool,[f,term(fun(bool,fun(bool,bool)))]
        comb(bool,bool,comb(bool,fun(bool,bool),f,T),T)))))
* [p:term(bool)][q:term(bool)]
  and' : term(bool) := comb(bool,bool,comb(bool,fun(bool,bool),and,p),q)
* imp : term(fun(bool,fun(bool,bool))) :=
  lambda(bool,fun(bool,bool),[t1,term(bool)]lambda(bool,bool,[t2,term(bool)]
    eq'(bool,and'(t1,t2),t1)))
q * imp' : term(bool) := comb(bool,bool,comb(bool,fun(bool,bool),imp,p),q)
A * forall : term(fun(fun(A,bool),bool)) :=
  lambda(fun(A,bool),bool,[P,term(fun(A,bool))]
    eq'(fun(A,bool),P,lambda(A,bool,[x,term(A)]T)))
A * [P:[x,term(A)]term(bool)]
  forall' : term(bool) := comb(fun(A,bool),bool,forall,lambda(A,bool,P))
A * exists : term(fun(fun(A,bool),bool)) :=
  lambda(fun(A,bool),bool,[P,term(fun(A,bool))]
    forall'(bool,[Q,term(bool)]
      imp'(forall'(A,[x,term(A)]imp'(comb(A,bool,P,x),Q)),Q)))
P * exists' : term(bool) := comb(fun(A,bool),bool,exists,lambda(A,bool,P))
* F : term(bool) := forall'(bool,[t,term(bool)]t)
* not : term(fun(bool,bool)) := lambda(bool,bool,[t,term(bool)]imp'(t,F))
p * not' : term(bool) := comb(bool,bool,not,p)

{ ----------------------------- num.ml -----------------------------------2-- }

* ind : type := PRIM
B * ONE_ONE : term(fun(fun(A,B),bool)) :=
  lambda(fun(A,B),bool,[f,term(fun(A,B))]
    forall'(A,[x1,term(A)]forall'(A,[x2,term(A)]
      imp'(eq'(B,comb(A,B,f,x1),comb(A,B,f,x2)),eq'(A,x1,x2)))))
B * ONTO : term(fun(fun(A,B),bool)) :=
  lambda(fun(A,B),bool,[f,term(fun(A,B))]
    forall'(B,[y,term(B)]exists'(A,[x,term(A)]eq'(B,y,comb(A,B,f,x)))))
* INFINITY_AX :
  thm(exists'(fun(ind,ind),[f,term(fun(ind,ind))]
    and'(comb(fun(ind,ind),bool,ONE_ONE(ind,ind),f),
      not'(comb(fun(ind,ind),bool,ONTO(ind,ind),f))))) := PRIM

{ ----------------------------- class.ml ---------------------------------3-- }

B * ETA_AX :
    thm(forall'(fun(A,B),[t,term(fun(A,B))]
      eq'(fun(A,B),lambda(A,B,[x,term(A)]comb(A,B,t,x)),t))) := PRIM

A * select : term(fun(fun(A,bool),A)) := PRIM
A * SELECT_AX :
    thm(forall'(fun(A,bool),[P,term(fun(A,bool))]forall'(A,[x,term(A)]
      imp'(comb(A,bool,P,x),comb(A,bool,P,comb(fun(A,bool),A,select,P))))))
    := PRIM