%%% Soundness of resolution without unification

s'_sound : solve' G -> gl A G -> solve A -> type.
h'_sound : assume' D -> pg A D -> assume A -> type.
r_sound : resolve D P G -> solve' G -> pg A D -> A >> P -> type.
%mode s'_sound +S' +GL -S.
% following is incorrect
% %mode h'_sound +H' +PG -H.
%mode h'_sound +H' -PG -H.
%mode r_sound +R +S' +PG -I.

s's_and : s'_sound (s'_and S'2 S'1) (gl_and GL2 GL1) (s_and S2 S1)
	   <- s'_sound S'1 GL1 S1
	   <- s'_sound S'2 GL2 S2.

s's_imp : s'_sound (s'_imp S'1) (gl_imp PG2 GL1) (s_imp S1)
	   <- {h' : assume' D2} {h : assume A2}
	      h'_sound h' PG2 h -> s'_sound (S'1 h') GL1 (S1 h).

s's_true : s'_sound (s'_true) (gl_true) (s_true).

s's_forall : s'_sound (s'_forall S'1) (gl_forall GL1) (s_forall S1)
	      <- {a:i} s'_sound (S'1 a) (GL1 a) (S1 a).

s's_atom : s'_sound (s'_atom S'3 R2 H'1) (gl_atom) (s_atom I2 PR1)
	    <- h'_sound H'1 PG1 PR1
	    <- r_sound R2 S'3 PG1 I2.

rs'_andl : r_sound (r_and R2 R1) (s'_orl S'1) (pg_and PG2 PG1) (i_andl I1)
	    <- r_sound R1 S'1 PG1 I1.

rs'_andr : r_sound (r_and R2 R1) (s'_orr S'2) (pg_and PG2 PG1) (i_andr I2)
	    <- r_sound R2 S'2 PG2 I2.

rs'_imp  : r_sound (r_imp R1) (s'_and S'2 S'1) (pg_imp GL2 PG1) (i_imp S2 I1)
	    <- r_sound R1 S'1 PG1 I1
	    <- s'_sound S'2 GL2 S2.

% rs'_true:  no case since by inversion there is no proof of false.

rs'_forall : r_sound (r_forall R1) (s'_exists T S'1) (pg_forall PG1)
	      (i_forall T I1)
	      <- r_sound (R1 T) S'1 (PG1 T) I1.

rs'_atom : r_sound (r_atom) (s'_eqp) (pg_atom) (i_atom).

%{
%block l5 :some {D2: prog}{A2:o}{PG2:pg A2 D2} 
  block {h' : assume' D2}{h : assume A2}{hs':h'_sound h' PG2 h}.
%worlds (l2 | l5) (s'_sound _ _ _)
                  (h'_sound _ _ _)
                  (r_sound _ _ _ _).
%covers (s'_sound +S' +GL -S)
        (h'_sound +H' -PG -H)
        (r_sound +R +S' +PG -I).
}%