%%% Proof of Value Soundness
%%% Author: Frank Pfenning, based on [Michaylov & Pfenning 92]

vs : eval E V -> value V -> type.
%mode vs +D -P.

% Natural Numbers


vs_z      : vs (ev_z) (val_z).
vs_s      : vs (ev_s D1) (val_s P1)
	     <- vs D1 P1.


vs_case_z : vs (ev_case_z D2 D1) P2
	     <- vs D2 P2.
vs_case_s : vs (ev_case_s D3 D1) P3
	     <- vs D3 P3.

% Pairs
vs_pair : vs (ev_pair D2 D1) (val_pair P2 P1)
	    <- vs D1 P1
	    <- vs D2 P2.
vs_fst  : vs (ev_fst D') P1
	    <- vs D' (val_pair P2 P1).
vs_snd  : vs (ev_snd D') P2
	    <- vs D' (val_pair P2 P1).

% Functions
vs_lam  : vs (ev_lam) (val_lam).

vs_app  : vs (ev_app D3 D2 D1) P3
	   <- vs D3 P3.

% Definitions
vs_letv : vs (ev_letv D2 D1) P2
	   <- vs D2 P2.
vs_letn : vs (ev_letn D2) P2
	   <- vs D2 P2.

% Recursion
vs_fix : vs (ev_fix D1) P1
	  <- vs D1 P1.

%worlds () (vs D P).
%terminates D (vs D _).
%covers vs +D -P.
%total D (vs D _).