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

% Below are complete computations
Ev : >ceval empty (s' z') W.

Ev : >ceval empty (app' (lam' 1) z') W.

% Doubling 1.
Ev : >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.
>ceval empty
  (let'
      (fix'
          (lam'
              (lam'
                  (case' (1 ^) 1
                      (s' (app'
                              (app' (1 ^ ^ ^)
                                  1)
                              (1 ^)))))))
      (app' (app' 1 (s' z')) (s' (s' z'))))
W.

%{

trans empty F
    (let (fix [plus] lam [x] lam [y] case x y [x'] s (app (app plus x') y))
       [plus]
       (let (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.
Ev : >ceval empty
    (let'
      (fix' (lam' (lam' (case' (1 ^) 1 (s' (app' (app' (1 ^ ^ ^) 1) (1 ^)))))))
      (let'
          (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.

sigma [D:feval empty (s' z') W]
cev_complete D C.

sigma [D:feval empty (app' (lam' 1) z') W]
cev_complete D C.

% Doubling 1
sigma [D:feval empty (app' (fix' (lam' (case' 1 z'
			    (s' (s' (app' (1 ^ ^) 1))))))
		           (s' z')) W]
cev_complete D C.

%{
% This is VERY slow
% Multiplication: 2 * 3 = 6.
sigma [D:feval empty
    (let'
      (fix' (lam' (lam' (case' (1 ^) 1 (s' (app' (app' (1 ^ ^ ^) 1) (1 ^)))))))
      (let'
          (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]
cev_complete D C.
}%