<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

{ ----------------------------- universe levels --------------------------3-- }

* omega : TYPE := PRIM
* 0 : omega := PRIM
* [i:omega] S : omega := PRIM

{ ----------------------------- terms -----------------------------------10-- }

* term : TYPE := PRIM

* Prop : term := PRIM
i * Type : term := PRIM
* [A:term][B:[x,term]term] Pi : term := PRIM
A * [M:[x,term]term] lambda : term := PRIM
* [M:term][N:term] app : term := PRIM
A * [B:[x,term]term] Sigma : term := PRIM
B * [M:term][N:term] pair : term := PRIM
* [M:term] pi_1 : term := PRIM
  pi_2 : term := PRIM

{ ----------------------------- conversion ------------------------------12-- }

* [A:term][B:term] eq : TYPE := PRIM

A * refl_eq : eq(A,A) := PRIM
B * [_1:eq(A,B)] sym_eq : eq(B,A) := PRIM
B * [C:term][_1:eq(A,B)][_2:eq(B,C)] trans_eq : eq(A,C) := PRIM
B * [C:[x,term]term][_1:eq(A,B)] cong : eq(<A>C,<B>C) := PRIM
A * [B:[x,term]term][B':[x,term]term][_1:[x,term]eq(<x>B,<x>B')]
  cong_lambda : eq(lambda(A,B),lambda(A,B')) := PRIM
  cong_Pi : eq(Pi(A,B),Pi(A,B')) := PRIM
  cong_Sigma : eq(Sigma(A,B),Sigma(A,B')) := PRIM
[M:term][N:term]
  cong_pair : eq(pair(A,B,M,N),pair(A,B',M,N)) := PRIM

A * [M:[x,term]term][N:term] beta : eq(app(lambda(A,M),N),<N>M) := PRIM
A * [B:[x,term]term][M_1:term][M_2:term]
  beta_pi_1 : eq(pi_1(pair(A,B,M_1,M_2)),M_1) := PRIM
  beta_pi_2 : eq(pi_2(pair(A,B,M_1,M_2)),M_2) := PRIM

{ ----------------------------- type cumulativity ------------------------8-- }

* [A:term][B:term] sub : TYPE := PRIM

B * [_1:eq(A,B)] refl_sub : sub(A,B) := PRIM
B * [C:term][_1:sub(A,B)][_2:sub(B,C)] trans_sub : sub(A,C) := PRIM
B * [_1:sub(A,B)][_2:sub(B,A)] antisym_sub : eq(A,B) := PRIM

* sub_Prop_Type : sub(Prop,Type(0)) := PRIM
i * sub_Type_Type : sub(Type(i),Type(S(i))) := PRIM

* [A:term][A':term][B:[x,term]term][B':[x,term]term]
  [_1:sub(A,A')][_2:[x,term]sub(<x>B,<x>B')]
  Pi_sub : sub(Pi(A,B),Pi(A',B')) := PRIM
  Sigma_sub : sub(Sigma(A,B),Sigma(A',B')) := PRIM

{ ----------------------------- inference rules -------------------------13-- }

* [A:term][B:term] in : TYPE := PRIM

* _K1_ : in(Prop,Type(0)) := PRIM
i * _K2_ : in(Type(i),Type(S(i))) := PRIM
A * [P:[x,term]term][_1:[x,term][_,in(x,A)]in(<x>P,Prop)]
  _Pi1_ : in(Pi(A,P),Prop) := PRIM
i * [A:term][B:[x,term]term]
  [_1:in(A,Type(i))][_2:[x,term][_,in(x,A)]in(<x>B,Type(i))]
  _Pi2_ : in(Pi(A,B),Type(i)) := PRIM
* [A:term][M:[x,term]term][B:[x,term]term]
  [_1:[x,term][_,in(x,A)]in(<x>M,<x>B)]
  _lambda_ : in(lambda(A,M),Pi(A,B)) := PRIM
A * [B:[x,term]term][M:term][N:term][_1:in(M,Pi(A,B))][_2:in(N,A)]
  _app_ : in(app(M,N),<N>B) := PRIM
i * [A:term][B:[x,term]term]
  [_1:in(A,Type(i))][_2:[x,term][_,in(x,A)]in(<x>B,Type(i))]
  _Sigma_ : in(Sigma(A,B),Type(i)) := PRIM
i * [A:term][B:[x,term]term][M:term][N:term]
  [_1:in(M,A)][_2:in(N,<M>B)][_3:[x,term][_,in(x,A)]in(<x>B,Type(i))]
  _pair_ : in(pair(A,B,M,N),Sigma(A,B)) := PRIM
* [A:term][B:[x,term]term][M:term][_1:in(M,Sigma(A,B))]
  _pi1_ : in(pi_1(M),A) := PRIM
  _pi2_ : in(pi_2(M),<pi_1(M)>B) := PRIM
i * [A:term][A':term][M:term][_1:in(M,A)][_2:in(A',Type(i))][_3:eq(A,A')]
  _conv_ : in(M,A') := PRIM
_2 * [_3:sub(A,A')]
  _cum_ : in(M,A') := PRIM