% Translating positive formulas to goal and program formulas.  

gl : o -> goal -> type.
pg : o -> prog -> type.
%mode gl +A -G.
%mode pg +A -D.

gl_atom : gl (atom P) (atom' P).

gl_and : gl (A1 and A2) (G1 and' G2)
	  <- gl A1 G1
	  <- gl A2 G2.

gl_imp : gl (A2 imp A1) (D2 imp' G1)
	  <- gl A1 G1
	  <- pg A2 D2.

gl_true : gl (true) (true').

gl_forall : gl (forall A1) (forall' G1)
	     <- {a:i} gl (A1 a) (G1 a).

pg_atom : pg (atom P) (atom^ P).

pg_and : pg (A1 and A2) (G1 and^ G2)
	  <- pg A1 G1
	  <- pg A2 G2.

pg_imp : pg (A2 imp A1) (G2 imp^ D1)
	  <- pg A1 D1
	  <- gl A2 G2.

pg_true: pg (true) (true^).

pg_forall : pg (forall A1) (forall^ D1)
	     <- {a:i} pg (A1 a) (D1 a).