%%% Representation of the Proof of Type Preservation
%%% Author: Frank Pfenning, based on [Michaylov & Pfenning 92]

tps : eval E V -> of E T -> of V T -> type.
%mode tps +D +P -Q.

% Natural Numbers
tps_z     : tps (ev_z) (tp_z) (tp_z).
tps_s     : tps (ev_s D1) (tp_s P1) (tp_s Q1)
	     <- tps D1 P1 Q1.

tps_case_z: tps (ev_case_z D2 D1) (tp_case P3 P2 P1) Q2
	     <- tps D2 P2 Q2.

tps_case_s: tps (ev_case_s D3 D1) (tp_case P3 P2 P1) Q3
	     <- tps D1 P1 (tp_s Q1')
	     <- tps D3 (P3 V1 Q1') Q3.

% Pairs
tps_pair : tps (ev_pair D2 D1) (tp_pair P2 P1) (tp_pair Q2 Q1)
	      <- tps D1 P1 Q1
	      <- tps D2 P2 Q2.
tps_fst  : tps (ev_fst D1) (tp_fst P1) Q1
	      <- tps D1 P1 (tp_pair Q2 Q1).
tps_snd  : tps (ev_snd D1) (tp_snd P1) Q2
	      <- tps D1 P1 (tp_pair Q2 Q1).

% Functions
tps_lam  : tps (ev_lam) (tp_lam P) (tp_lam P).

tps_app  : tps (ev_app D3 D2 D1) (tp_app P2 P1) Q3
	    <- tps D1 P1 (tp_lam Q1')
	    <- tps D2 P2 Q2
	    <- tps D3 (Q1' V2 Q2) Q3.

% Definitions
tps_letv : tps (ev_letv D2 D1) (tp_letv P2 P1) Q2
	    <- tps D1 P1 Q1
	    <- tps D2 (P2 V1 Q1) Q2.


tps_letn : tps (ev_letn D2) (tp_letn P2 P1) Q2
	    <- tps D2 P2 Q2.



% Recursion
tps_fix : tps (ev_fix D1) (tp_fix P1) Q1
	    <- tps D1 (P1 _ (tp_fix P1)) Q1.


%%% Termination of type preservation judgment
%worlds () (tps D _ _).
%terminates D (tps D _ _).
%covers tps +D +P -Q.
%total D (tps D P _).