%query 10 *
init # (ev (app (lam [x] x) z)) =>* S.

%query 1 *
C* : init # (ev (app (lam [x] x) z)) =>* answer V.

%solve c0 : init # (ev (app (lam [x] x) z)) =>* answer V.

%query 1 *
csd c0 D C'.

%query 1 *
(init) # (ev (app (lam [x] x) z)) =>* (answer V).

%query 1 *
ceval (app (lam [x] x) z) V.

% Doubling 3
%query 1 *
C : ceval (app (fix [double] lam [x]
		  case x z
		  [x'] s (s (app double x'))) (s (s (s z))))
    V.

% Computing 2 * 3
%query 1 *
ceval (letv (lam [x] fix [add] lam [y]
	       case y x [y'] s (app add y')) [add]
	 (letv (lam [x] fix [mult] lam [y]
		  case y z ([y'] (app (app add x)
					 (app mult y')))) [mult]
	    (app (app mult (s (s z))) (s (s (s z))))))
V.

% Applying soundness to computation of doubling 3
%query 1 *
cpm_sound
(cev
   (stop << st_init << st_return << st_return << st_return << st_return
      << st_return << st_return << st_z << st_case1_z << st_return << st_z
      << st_case << st_app2 << st_return << st_z << st_app1 << st_return
      << st_lam << st_fix << st_app << st_s << st_s << st_case1_s
      << st_return << st_return << st_z << st_s << st_case << st_app2
      << st_return << st_return << st_z << st_s << st_app1 << st_return
      << st_lam << st_fix << st_app << st_s << st_s << st_case1_s
      << st_return << st_return << st_return << st_z << st_s << st_s
      << st_case << st_app2 << st_return << st_return << st_return << st_z
      << st_s << st_s << st_app1 << st_return << st_lam << st_fix << st_app
      << st_s << st_s << st_case1_s << st_return << st_return << st_return
      << st_return << st_z << st_s << st_s << st_s << st_case << st_app2
      << st_return << st_return << st_return << st_return << st_z << st_s
      << st_s << st_s << st_app1 << st_return << st_lam << st_fix << st_app)
: ceval (app (fix [double] lam [x]
		  case x z
		  [x'] s (s (app double x'))) (s (s (s z))))
        (s (s (s (s (s (s z)))))))
D.

% Natural evaluation of 2 * 3
%query 1 1
eval (letv (lam [x] fix [add] lam [y]
		   case y x [y'] s (app add y')) [add]
	     (letv (lam [x] fix [mult] lam [y]
		      case y z ([y'] (app (app add x)
					    (app mult y')))) [mult]
		(app (app mult (s (s z))) (s (s (s z))))))
V.


% Counterexample to the conjecture that
% If K # (ev E) =>* K # (return V) then eval E V.
e0 : exp = (app (fix [f] lam [x] case x z [x'] app f x') (s (s z))).

%query 1 *
eval e0 V.

%query 50 *
(init # ev e0) =>* K # I.

k1 : cont =
(init ; ([x2:exp] app2 
	   (lam [x:exp] case x z
	      ([x':exp] app (fix [x7:exp] lam [x8:exp]
			       case x8 z ([x'4:exp] app x7 x'4)) x')) x2)).

%query 3 *
(k1 # ev (s (s z))) =>* (k1 # (return V)).