%%% Completeness of resolution without unification

% Lemma: totality of resolution

r_total : {D:prog} resolve D P G -> type.
% this was mode incorrect without the explicit
% P, since P was inferred to be an output argument.
% %mode r_total +D -R.
%mode +{D:prog} +{P:p} -{G:goal} -{R:resolve D P G} r_total D R.

rt_and : r_total (D1 and^ D2) (r_and R2 R1)
	   <- r_total D1 R1
	   <- r_total D2 R2.

rt_imp : r_total (G2 imp^ D1) (r_imp R1)
	   <- r_total D1 R1.

rt_true : r_total (true^) (r_true).

rt_forall : r_total (forall^ D1) (r_forall R1)
	      <- {a:i} r_total (D1 a) (R1 a).

rt_atom : r_total (atom^ Q) (r_atom).

%worlds (l_i) (r_total D R).
%total (D) (r_total D R).

% Completeness of resolution

s'_comp : solve A -> gl A G -> solve' G -> type.
h'_comp : assume A -> pg A D -> assume' D -> type.
r_comp : A >> P -> pg A D -> resolve D P G -> solve' G -> type.
%mode s'_comp +S +GL -S'.
%mode h'_comp +H -PG -H'.
%mode r_comp +I +PG +R -S'.

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

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

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

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

s's_atom : s'_comp (s_atom (I2 : A >> P) H1) (gl_atom) (s'_atom S'3 R2 H'1)
	    <- h'_comp H1 (PG1 : pg A D) H'1
	    <- r_total D R2
	    <- r_comp I2 PG1 R2 S'3.

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

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

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

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

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

%block l_h'_comp :
  some {A:o} {D:prog} {PG:pg A D}
  block {h:assume A} {h':assume' D}
        {hc:h'_comp h PG h'}.
%worlds (l_i | l_h'_comp)
  (s'_comp S GL S')
  (h'_comp H PG H')
  (r_comp I PG R S'').
%total (S H I)
  (s'_comp S GL _)
  (h'_comp H _ _)
  (r_comp I PG R _).