%query 1 * (init) # (ev (app (lam [x] (vl x)) z)) =>* (answer V). %query 1 * ceval (app (lam [x] (vl x)) z) V. % Doubling 3 %query 1 * ceval (app (fix [double] lam [x] case (vl x) z [x'] s (s (app double (vl x')))) (s (s (s z)))) V. % Computing 2 * 3 %query 1 * ceval (letv (lam [x] fix [add] lam [y] case (vl y) (vl x) [y'] s (app add (vl y'))) [add] (letv (lam [x] fix [mult] lam [y] case (vl y) z ([y'] (app (app (vl add) (vl x)) (app mult (vl y'))))) [mult] (app (app (vl mult) (s (s z))) (s (s (s z)))))) V. % Applying soundness to computation of doubling 3 %query 1 * ceval_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_vl << st_case << st_app2 << st_return << st_vl << st_app1 << st_return << st_lam << st_fix << st_app << st_s << st_s << st_case1_s << st_return << st_vl << st_case << st_app2 << st_return << st_vl << st_app1 << st_return << st_lam << st_fix << st_app << st_s << st_s << st_case1_s << st_return << st_vl << st_case << st_app2 << st_return << st_vl << st_app1 << st_return << st_lam << st_fix << st_app << st_s << st_s << st_case1_s << st_return << st_vl << 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)) D. % Natural evaluation of 2 * 3 %query 1 1 eval (letv (lam [x] fix [add] lam [y] case (vl y) (vl x) [y'] s (app add (vl y'))) [add] (letv (lam [x] fix [mult] lam [y] case (vl y) z ([y'] (app (app (vl add) (vl x)) (app mult (vl y'))))) [mult] (app (app (vl mult) (s (s z))) (s (s (s z)))))) V. % Currently kills SML %{ % Applying completeness proof to obtain a computation of 2 * 3 %query 1 1 ceval_complete (ev_letv (ev_letv (ev_app (ev_case_s (ev_app (ev_case_s (ev_s (ev_app (ev_case_s (ev_s (ev_app (ev_case_s (ev_s (ev_app (ev_case_s (ev_s (ev_app (ev_case_z ev_vl ev_vl) ev_vl (ev_fix ev_lam))) ev_vl) ev_vl (ev_fix ev_lam))) ev_vl) ev_vl (ev_fix ev_lam))) ev_vl) ev_vl (ev_fix ev_lam))) ev_vl) (ev_app (ev_case_s (ev_app (ev_case_s (ev_s (ev_app (ev_case_s (ev_s (ev_app (ev_case_z ev_vl ev_vl) ev_vl (ev_fix ev_lam))) ev_vl) ev_vl (ev_fix ev_lam))) ev_vl) (ev_app (ev_case_s (ev_app (ev_case_z ev_vl ev_vl) (ev_app (ev_case_z ev_z ev_vl) ev_vl (ev_fix ev_lam)) (ev_app (ev_fix ev_lam) ev_vl ev_vl)) ev_vl) ev_vl (ev_fix ev_lam)) (ev_app (ev_fix ev_lam) ev_vl ev_vl)) ev_vl) ev_vl (ev_fix ev_lam)) (ev_app (ev_fix ev_lam) ev_vl ev_vl)) ev_vl) (ev_s (ev_s (ev_s ev_z))) (ev_app (ev_fix ev_lam) (ev_s (ev_s ev_z)) ev_vl)) ev_lam) ev_lam) CE. }%