<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

{ ----------------------------- pseudoterms ------------------------------4-- }

* pterm : TYPE := PRIM

* [a:pterm][b:pterm] app : pterm := PRIM
a * [h:[x,pterm]pterm] lambda : pterm := PRIM
h * Pi : pterm := PRIM

{ ----------------------------- specifications ---------------------------3-- }

* [s:pterm] sort : TYPE := PRIM
* [c:pterm][s:pterm] axiom : TYPE := PRIM
* [s1:pterm][s2:pterm][s3:pterm] rule : TYPE := PRIM

{ ----------------------------- judgments --------------------------------2-- }

a * [A:pterm] in : TYPE := PRIM
b * eq : TYPE := PRIM

{ ----------------------------- equality ---------------------------------7-- }

a * refl : eq(a,a) := PRIM
b * [_1:eq(a,b)] sym : eq(b,a) := PRIM
b * [c:pterm][_1:eq(a,b)][_2:eq(b,c)] trans : eq(a,c) := PRIM
b * [c:[x,pterm]pterm][_1:eq(a,b)] cong : eq(<a>c,<b>c) := PRIM
a * [b:[x,pterm]pterm][c:[x,pterm]pterm][_1:[x,pterm]eq(<x>b,<x>c)]
  cong_lambda : eq(lambda(a,b),lambda(a,c)) := PRIM
  cong_Pi : eq(Pi(a,b),Pi(a,c)) := PRIM

h * [x:pterm] beta : eq(app(lambda(a,h),x),<x>h) := PRIM

{ ----------------------------- pure type system -------------------------5-- }

* [s:pterm][c:pterm][_1:axiom(c,s)]
  axiom_in : in(c,s) := PRIM
* [F:pterm][a:pterm][A:pterm][B:[x,pterm]pterm][_1:in(F,Pi(A,B))][_2:in(a,A)]
  application : in(app(F,a),<a>B) := PRIM
s3 * [A:pterm][B:[x,pterm]pterm]
  [_1:in(A,s1)][_2:[x,pterm][_,in(x,A)]in(<x>B,s2)][_3:rule(s1,s2,s3)]
  product : in(Pi(A,B),s3) := PRIM
s * [A:pterm][B:[x,pterm]pterm][C:[x,pterm]pterm]
  [_1:[x,pterm][_,in(x,A)]in(<x>B,<x>C)][_2:in(Pi(A,C),s)][_3:sort(s)]
  abstraction : in(lambda(A,B),Pi(A,C)) := PRIM
s * [A:pterm][B:pterm][B':pterm][_1:in(A,B)][_2:in(B',s)]
  [_3:eq(B,B')][_4:sort(s)]
  conversion : in(A,B') := PRIM

{ ----------------------------- CC sorts ---------------------------------4-- }

* star : pterm := PRIM
* box : pterm := PRIM

* sort_star : sort(star) := PRIM
* sort_box : sort(box) := PRIM

{ ----------------------------- CC axioms --------------------------------1-- }

* axiom_star_box : axiom(star,box) := PRIM

{ ----------------------------- CC rules ---------------------------------4-- }

* rule_arrow : rule(star,star,star) := PRIM
* rule_2 : rule(box,star,star) := PRIM
* rule_P : rule(star,box,box) := PRIM
* rule_omega : rule(box,box,box) := PRIM