#!/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(c,c) := PRIM a * [b:[x,pterm]pterm][c:[x,pterm]pterm][_1:[x,pterm]eq(b,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),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),B) := PRIM s3 * [A:pterm][B:[x,pterm]pterm] [_1:in(A,s1)][_2:[x,pterm][_,in(x,A)]in(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(B,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