% Enumerate the solution for complete computations
%query 4 *
st (emptys ;; empty) (ev (s' z') & done) (empty) >=>* st Ks P S.

% Below are complete computations
%query 1 *
>ceval empty (s' z') W.

%query 1 *
>ceval empty (app' (lam' 1) z') W.

% Doubling 1.
%query 1 1
>ceval empty
  (app' (fix' (lam' (case' 1 z'
		       (s' (s' (app' (1 ^ ^) 1))))))
     (s' z'))
  W.


%{
trans empty F
    (let (fix [plus] lam [x] lam [y] case x y [x'] s (app (app plus x') y))
       [plus] app (app plus (s z)) (s (s z))).
}%

% Addition 1 + 2 = 3.
%query 1 1
>ceval empty
  (letn'
      (fix'
          (lam'
              (lam'
                  (case' (1 ^) 1
                      (s' (app'
                              (app' (1 ^ ^ ^)
                                  1)
                              (1 ^)))))))
      (app' (app' 1 (s' z')) (s' (s' z'))))
W.

%{
trans empty F
    (letn (fix [plus] lam [x] lam [y] case x y [x'] s (app (app plus x') y))
       [plus]
       (letn (fix [mult] lam [x] lam [y] case x z [x']
	       app (app plus (app (app mult x') y)) y)
	  [mult] app (app mult (s (s z))) (s (s (s z))))).
}%


% Multiplication: 2 * 3 = 6.
%query 1 1
>ceval empty
    (letn'
      (fix' (lam' (lam' (case' (1 ^) 1 (s' (app' (app' (1 ^ ^ ^) 1) (1 ^)))))))
      (letn'
          (fix'
              (lam'
                  (lam'
                      (case' (1 ^) z'
                          (app'
                              (app' (1 ^ ^ ^ ^)
                                  (app' (app' (1 ^ ^ ^) 1) (1 ^))) (1 ^))))))
          (app' (app' 1 (s' (s' z'))) (s' (s' (s' z'))))))
      W.

%%% Mapping from evaluations to computations.

% Doubling 1
%query 1 1
feval empty (app' (fix' (lam' (case' 1 z'
				 (s' (s' (app' (1 ^ ^) 1))))))
	       (s' z')) W.

%query 1 *
cev_complete
   (fev_app
      (fev_case_s
          (fev_s
              (fev_s
                  (fev_app (fev_case_z fev_z fev_1) fev_1
                      (fev_^ (fev_^ (fev_1+ (fev_fix fev_lam))))))) fev_1)
      (fev_s fev_z) (fev_fix fev_lam))
C.

% Multiplication: 2 * 3 = 6
%query 1 1
feval empty
    (letn'
      (fix' (lam' (lam' (case' (1 ^) 1 (s' (app' (app' (1 ^ ^ ^) 1) (1 ^)))))))
      (letn'
          (fix'
              (lam'
                  (lam'
                      (case' (1 ^) z'
                          (app'
                              (app' (1 ^ ^ ^ ^)
                                  (app' (app' (1 ^ ^ ^) 1) (1 ^))) (1 ^))))))
          (app' (app' 1 (s' (s' z'))) (s' (s' (s' z'))))))
      W.