diff -r 89ed51d72e4a -r aea02b5a58d2 thys/Recursive.thy
--- a/thys/Recursive.thy	Thu May 02 12:49:15 2013 +0100
+++ b/thys/Recursive.thy	Thu May 02 12:49:33 2013 +0100
@@ -6,7 +6,6 @@
   where
   "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
 
-(* moves register m to register n *)
 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where
   "mv_box m n = [Dec m 3, Inc n, Goto 0]"
@@ -19,7 +18,7 @@
 text {* The compilation of @{text "s"}-operator. *}
 definition rec_ci_s :: "abc_inst list"
   where
-  "rec_ci_s \<equiv> addition 0 1 2 [+] [Inc 1]"
+  "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"
 
 
 text {* The compilation of @{text "id i j"}-operator *}
@@ -37,7 +36,8 @@
   "empty_boxes 0 = []" |
   "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]"
 
-fun cn_merge_gs :: "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
+fun cn_merge_gs ::
+  "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
   where
   "cn_merge_gs [] p = []" |
   "cn_merge_gs (g # gs) p = 
@@ -91,7 +91,20 @@
 declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] 
         abc_step_l.simps[simp del] 
 
-fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
+inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs"
+
+inductive_cases terminate_z_reverse[elim!]: "terminate z xs"
+
+inductive_cases terminate_s_reverse[elim!]: "terminate s xs"
+
+inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs"
+
+inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs"
+
+inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs"
+
+fun addition_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>     
+                     nat list \<Rightarrow> bool"
   where
   "addition_inv (as, lm') m n p lm = 
         (let sn = lm ! n in
@@ -140,18 +153,21 @@
               else if as = 4 then 0 
               else 0)"
 
-fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
+fun addition_measure :: "((nat \<times> nat list) \<times> nat \<times> nat) \<Rightarrow> 
+                                                 (nat \<times> nat \<times> nat)"
   where
   "addition_measure ((as, lm), m, p) =
      (addition_stage1 (as, lm) m p, 
       addition_stage2 (as, lm) m p,
       addition_stage3 (as, lm) m p)"
 
-definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> ((nat \<times> nat list) \<times> nat \<times> nat)) set"
+definition addition_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> 
+                          ((nat \<times> nat list) \<times> nat \<times> nat)) set"
   where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"
 
 lemma [simp]: "wf addition_LE"
-by(auto simp: wf_inv_image addition_LE_def lex_triple_def lex_pair_def)
+by(auto simp: wf_inv_image addition_LE_def lex_triple_def
+             lex_pair_def)
 
 declare addition_inv.simps[simp del]
 
@@ -313,23 +329,17 @@
 qed
 
 lemma compile_s_correct':
-  "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} 
-   addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] 
-   {\<lambda>nl. nl = n # Suc n # 0 # anything}"
+  "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 [+] [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}"
 proof(rule_tac abc_Hoare_plus_halt)
-  show "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} 
-        addition 0 (Suc 0) 2 
-        {\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}"
+  show "{\<lambda>nl. nl = n # 0 \<up> 2 @ anything} addition 0 (Suc 0) 2 {\<lambda> nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)}"
     by(rule_tac addition_correct, auto simp: numeral_2_eq_2)
 next
-  show "{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)} 
-        [Inc (Suc 0)] 
-        {\<lambda>nl. nl = n # Suc n # 0 # anything}"
+  show "{\<lambda>nl. addition_inv (7, nl) 0 (Suc 0) 2 (n # 0 \<up> 2 @ anything)} [Inc (Suc 0)] {\<lambda>nl. nl = n # Suc n # 0 # anything}"
     by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps 
       abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps)
 qed
   
-declare rec_eval.simps[simp del]
+declare rec_exec.simps[simp del]
 
 lemma abc_comp_commute: "(A [+] B) [+] C = A [+] (B [+] C)"
 apply(auto simp: abc_comp.simps abc_shift.simps)
@@ -339,24 +349,24 @@
 
 
 lemma compile_z_correct: 
-  "\<lbrakk>rec_ci z = (ap, arity, fp); rec_eval z [n] = r\<rbrakk> \<Longrightarrow> 
+  "\<lbrakk>rec_ci z = (ap, arity, fp); rec_exec z [n] = r\<rbrakk> \<Longrightarrow> 
   {\<lambda>nl. nl = n # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = n # r # 0 \<up> (fp - Suc arity) @ anything}"
 apply(rule_tac abc_Hoare_haltI)
 apply(rule_tac x = 1 in exI)
 apply(auto simp: abc_steps_l.simps rec_ci.simps rec_ci_z_def 
-                 numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_eval.simps)
+                 numeral_2_eq_2 abc_fetch.simps abc_step_l.simps rec_exec.simps)
 done
 
 lemma compile_s_correct: 
-  "\<lbrakk>rec_ci s = (ap, arity, fp); rec_eval s [n] = r\<rbrakk> \<Longrightarrow> 
+  "\<lbrakk>rec_ci s = (ap, arity, fp); rec_exec s [n] = r\<rbrakk> \<Longrightarrow> 
   {\<lambda>nl. nl = n # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = n # r # 0 \<up> (fp - Suc arity) @ anything}"
-apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_eval.simps)
+apply(auto simp: rec_ci.simps rec_ci_s_def compile_s_correct' rec_exec.simps)
 done
 
 lemma compile_id_correct':
   assumes "n < length args" 
   shows "{\<lambda>nl. nl = args @ 0 \<up> 2 @ anything} addition n (length args) (Suc (length args))
-  {\<lambda>nl. nl = args @ rec_eval (recf.id (length args) n) args # 0 # anything}"
+  {\<lambda>nl. nl = args @ rec_exec (recf.id (length args) n) args # 0 # anything}"
 proof -
   have "{\<lambda>nl. nl = args @ 0 \<up> 2 @ anything} addition n (length args) (Suc (length args))
   {\<lambda>nl. addition_inv (7, nl) n (length args) (Suc (length args)) (args @ 0 \<up> 2 @ anything)}"
@@ -364,12 +374,12 @@
     by(rule_tac addition_correct, auto simp: numeral_2_eq_2 nth_append)
   thus "?thesis"
     using assms
-    by(simp add: addition_inv.simps rec_eval.simps 
+    by(simp add: addition_inv.simps rec_exec.simps 
       nth_append numeral_2_eq_2 list_update_append)
 qed
 
 lemma compile_id_correct: 
-  "\<lbrakk>n < m; length xs = m; rec_ci (recf.id m n) = (ap, arity, fp); rec_eval (recf.id m n) xs = r\<rbrakk>
+  "\<lbrakk>n < m; length xs = m; rec_ci (recf.id m n) = (ap, arity, fp); rec_exec (recf.id m n) xs = r\<rbrakk>
        \<Longrightarrow> {\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ r # 0 \<up> (fp - Suc arity) @ anything}"
 apply(auto simp: rec_ci.simps rec_ci_id.simps compile_id_correct')
 done
@@ -391,8 +401,8 @@
 done
 
 lemma param_pattern: 
-  "\<lbrakk>terminates f xs; rec_ci f = (p, arity, fp)\<rbrakk> \<Longrightarrow> length xs = arity"
-apply(induct arbitrary: p arity fp rule: terminates.induct)
+  "\<lbrakk>terminate f xs; rec_ci f = (p, arity, fp)\<rbrakk> \<Longrightarrow> length xs = arity"
+apply(induct arbitrary: p arity fp rule: terminate.induct)
 apply(auto simp: rec_ci.simps)
 apply(case_tac "rec_ci f", simp)
 apply(case_tac "rec_ci f", case_tac "rec_ci g", simp)
@@ -590,11 +600,11 @@
 
 lemma [simp]:
   "\<lbrakk>length xs < gf; gf \<le> ft; n < length gs\<rbrakk>
-  \<Longrightarrow> (rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
-  [ft + n - length xs := rec_eval (gs ! n) xs, 0 := 0] =
-  0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
-using list_update_append[of "rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs)"
-                             "0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything" "ft + n - length xs" "rec_eval (gs ! n) xs"]
+  \<Longrightarrow> (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
+  [ft + n - length xs := rec_exec (gs ! n) xs, 0 := 0] =
+  0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
+using list_update_append[of "rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs)"
+                             "0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything" "ft + n - length xs" "rec_exec (gs ! n) xs"]
 apply(auto)
 apply(case_tac "length gs - n", simp, simp add: list_update.simps replicate_Suc_iff_anywhere Suc_diff_Suc del: replicate_Suc)
 apply(simp add: list_update.simps)
@@ -602,14 +612,14 @@
 
 lemma compile_cn_gs_correct':
   assumes
-  g_cond: "\<forall>g\<in>set (take n gs). terminates g xs \<and>
-  (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+  g_cond: "\<forall>g\<in>set (take n gs). terminate g xs \<and>
+  (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
   and ft: "ft = max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
   shows 
   "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything}
     cn_merge_gs (map rec_ci (take n gs)) ft
   {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @
-                    map (\<lambda>i. rec_eval i xs) (take n gs) @ 0\<up>(length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+                    map (\<lambda>i. rec_exec i xs) (take n gs) @ 0\<up>(length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
   using g_cond
 proof(induct n)
   case 0
@@ -624,17 +634,17 @@
 next
   case (Suc n)
   have ind': "\<forall>g\<in>set (take n gs).
-     terminates g xs \<and> (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> 
-    (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc})) \<Longrightarrow>
+     terminate g xs \<and> (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> 
+    (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc})) \<Longrightarrow>
     {\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft 
-    {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+    {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
     by fact
   have g_newcond: "\<forall>g\<in>set (take (Suc n) gs).
-     terminates g xs \<and> (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+     terminate g xs \<and> (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
     by fact
   from g_newcond have ind:
     "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft 
-    {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+    {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
     apply(rule_tac ind', rule_tac ballI, erule_tac x = g in ballE, simp_all add: take_Suc)
     by(case_tac "n < length gs", simp add:take_Suc_conv_app_nth, simp)    
   show "?case"
@@ -650,17 +660,17 @@
       moreover have 
         "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything}
         cn_merge_gs (map rec_ci (take n gs)) ft [+] (gp [+] mv_box ga (ft + n))
-        {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 
-        rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+        {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 
+        rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
       proof(rule_tac abc_Hoare_plus_halt)
         show "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything} cn_merge_gs (map rec_ci (take n gs)) ft
-          {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
+          {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything}"
           using ind by simp
       next
         have x: "gs!n \<in> set (take (Suc n) gs)"
           using h
           by(simp add: take_Suc_conv_app_nth)
-        have b: "terminates (gs!n) xs"
+        have b: "terminate (gs!n) xs"
           using a g_newcond h x
           by(erule_tac x = "gs!n" in ballE, simp_all)
         hence c: "length xs = ga"
@@ -672,18 +682,18 @@
             rule_tac f = "(\<lambda>(aprog, p, n). n)" and x = "rec_ci (gs!n)" in image_eqI, simp, 
             rule_tac x = "gs!n" in image_eqI, simp, simp)
         show "{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ 
-          map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp [+] mv_box ga (ft + n)
-          {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) 
-          (take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+          map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp [+] mv_box ga (ft + n)
+          {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) 
+          (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
         proof(rule_tac abc_Hoare_plus_halt)
-          show "{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp 
-                {\<lambda>nl. nl = xs @ (rec_eval (gs!n) xs) # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) 
+          show "{\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} gp 
+                {\<lambda>nl. nl = xs @ (rec_exec (gs!n) xs) # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) 
                               (take n gs) @  0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}"
           proof -
             have 
-              "({\<lambda>nl. nl = xs @ 0 \<up> (gf - ga) @ 0\<up>(ft - gf)@map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} 
-            gp {\<lambda>nl. nl = xs @ (rec_eval (gs!n) xs) # 0 \<up> (gf - Suc ga) @ 
-              0\<up>(ft - gf)@map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything})"
+              "({\<lambda>nl. nl = xs @ 0 \<up> (gf - ga) @ 0\<up>(ft - gf)@map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything} 
+            gp {\<lambda>nl. nl = xs @ (rec_exec (gs!n) xs) # 0 \<up> (gf - Suc ga) @ 
+              0\<up>(ft - gf)@map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 \<up> Suc (length xs) @ anything})"
               using a g_newcond h x
               apply(erule_tac x = "gs!n" in ballE)
               apply(simp, simp)
@@ -694,33 +704,33 @@
           qed
         next
           show 
-            "{\<lambda>nl. nl = xs @ rec_eval (gs ! n) xs #
-            0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}
+            "{\<lambda>nl. nl = xs @ rec_exec (gs ! n) xs #
+            0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}
             mv_box ga (ft + n)
-            {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @
-            rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+            {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @
+            rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
           proof -
-            have "{\<lambda>nl. nl = xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
-              map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}
-              mv_box ga (ft + n) {\<lambda>nl. nl = (xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
-              map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
-              [ft + n := (xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 
+            have "{\<lambda>nl. nl = xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
+              map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything}
+              mv_box ga (ft + n) {\<lambda>nl. nl = (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
+              map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
+              [ft + n := (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 
               0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) ! ga +
-              (xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ 
-              map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) !
+              (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ 
+              map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) !
                       (ft + n),  ga := 0]}"
               using a c d e h
               apply(rule_tac mv_box_correct)
               apply(simp, arith, arith)
               done
-            moreover have "(xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
-              map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
-              [ft + n := (xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ 
+            moreover have "(xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @
+              map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
+              [ft + n := (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 
               0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) ! ga +
-              (xs @ rec_eval (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ 
-              map (\<lambda>i. rec_eval i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) !
+              (xs @ rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ 
+              map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything) !
                       (ft + n),  ga := 0]= 
-              xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
+              xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
               using a c d e h
               by(simp add: list_update_append nth_append length_replicate split: if_splits del: list_update.simps(2), auto)
             ultimately show "?thesis"
@@ -732,7 +742,7 @@
         "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything}
         cn_merge_gs (map rec_ci (take n gs)) ft [+] (case rec_ci (gs ! n) of (gprog, gpara, gn) \<Rightarrow>
         gprog [+] mv_box gpara (ft + min (length gs) n))
-        {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) (take n gs) @ rec_eval (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
+        {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything}"
         by simp
     qed
   next
@@ -740,7 +750,7 @@
     have h: "\<not> n < length gs" by fact
     hence ind': 
       "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything} cn_merge_gs (map rec_ci gs) ft
-        {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
+        {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
       using ind
       by simp
     thus "?thesis"
@@ -751,14 +761,14 @@
     
 lemma compile_cn_gs_correct:
   assumes
-  g_cond: "\<forall>g\<in>set gs. terminates g xs \<and>
-  (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+  g_cond: "\<forall>g\<in>set gs. terminate g xs \<and>
+  (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
   and ft: "ft = max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
   shows 
   "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (ft + length gs) @ anything}
     cn_merge_gs (map rec_ci gs) ft
   {\<lambda>nl. nl = xs @ 0 \<up> (ft - length xs) @
-                    map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
+                    map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}"
 using assms
 using compile_cn_gs_correct'[of "length gs" gs xs ft ffp anything ]
 apply(auto)
@@ -957,14 +967,14 @@
      
 lemma save_paras: 
   "{\<lambda>nl. nl = xs @ 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length xs) @
-  map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> Suc (length xs) @ anything}
+  map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> Suc (length xs) @ anything}
   mv_boxes 0 (Suc (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) (length xs)
-  {\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\<lambda>i. rec_eval i xs) gs @ 0 # xs @ anything}"
+  {\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\<lambda>i. rec_exec i xs) gs @ 0 # xs @ anything}"
 proof -
   let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
-  have "{\<lambda>nl. nl = [] @ xs @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_eval i xs) gs @ [0]) @ 
+  have "{\<lambda>nl. nl = [] @ xs @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_exec i xs) gs @ [0]) @ 
           0 \<up> (length xs) @ anything} mv_boxes 0 (Suc ?ft + length gs) (length xs) 
-        {\<lambda>nl. nl = [] @ 0 \<up> (length xs) @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_eval i xs) gs @ [0]) @ xs @ anything}"
+        {\<lambda>nl. nl = [] @ 0 \<up> (length xs) @ (0\<up>(?ft - length xs) @  map (\<lambda>i. rec_exec i xs) gs @ [0]) @ xs @ anything}"
     by(rule_tac mv_boxes_correct, auto)
   thus "?thesis"
     by(simp add: replicate_merge_anywhere)
@@ -978,15 +988,15 @@
 
 lemma restore_new_paras:
   "ffp \<ge> length gs 
- \<Longrightarrow> {\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\<lambda>i. rec_eval i xs) gs @ 0 # xs @ anything}
+ \<Longrightarrow> {\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ map (\<lambda>i. rec_exec i xs) gs @ 0 # xs @ anything}
     mv_boxes (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) 0 (length gs)
-  {\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ 0 # xs @ anything}"
+  {\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ 0 # xs @ anything}"
 proof -
   let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
   assume j: "ffp \<ge> length gs"
-  hence "{\<lambda> nl. nl = [] @ 0\<up>length gs @ 0\<up>(?ft - length gs) @  map (\<lambda>i. rec_eval i xs) gs @ ((0 # xs) @ anything)}
+  hence "{\<lambda> nl. nl = [] @ 0\<up>length gs @ 0\<up>(?ft - length gs) @  map (\<lambda>i. rec_exec i xs) gs @ ((0 # xs) @ anything)}
        mv_boxes ?ft 0 (length gs)
-        {\<lambda> nl. nl = [] @ map (\<lambda>i. rec_eval i xs) gs @ 0\<up>(?ft - length gs) @ 0\<up>length gs @ ((0 # xs) @ anything)}"
+        {\<lambda> nl. nl = [] @ map (\<lambda>i. rec_exec i xs) gs @ 0\<up>(?ft - length gs) @ 0\<up>length gs @ ((0 # xs) @ anything)}"
     by(rule_tac mv_boxes_correct2, auto)
   moreover have "?ft \<ge> length gs"
     using j
@@ -1007,29 +1017,29 @@
   "\<lbrakk>far = length gs;
   ffp \<le> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)));
   far < ffp\<rbrakk>
-\<Longrightarrow>  {\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
-  rec_eval (Cn (length xs) f gs) xs # 0 \<up> max (Suc (length xs))
+\<Longrightarrow>  {\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @
+  rec_exec (Cn (length xs) f gs) xs # 0 \<up> max (Suc (length xs))
   (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ xs @ anything}
     mv_box far (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))))
-    {\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
+    {\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @
                0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) @
-               rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
+               rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
 proof -
   let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
   thm mv_box_correct
-  let ?lm= " map (\<lambda>i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> ?ft @ xs @ anything"
+  let ?lm= " map (\<lambda>i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> ?ft @ xs @ anything"
   assume h: "far = length gs" "ffp \<le> ?ft" "far < ffp"
   hence "{\<lambda> nl. nl = ?lm} mv_box far ?ft {\<lambda> nl. nl = ?lm[?ft := ?lm!far + ?lm!?ft, far := 0]}"
     apply(rule_tac mv_box_correct)
     by(case_tac "rec_ci a", auto)  
   moreover have "?lm[?ft := ?lm!far + ?lm!?ft, far := 0]
-    = map (\<lambda>i. rec_eval i xs) gs @
+    = map (\<lambda>i. rec_exec i xs) gs @
     0 \<up> (?ft - length gs) @
-    rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+    rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
     using h
     apply(simp add: nth_append)
-    using list_update_length[of "map (\<lambda>i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs #
-       0 \<up> (?ft - Suc (length gs))" 0 "0 \<up> length gs @ xs @ anything" "rec_eval (Cn (length xs) f gs) xs"]
+    using list_update_length[of "map (\<lambda>i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs #
+       0 \<up> (?ft - Suc (length gs))" 0 "0 \<up> length gs @ xs @ anything" "rec_exec (Cn (length xs) f gs) xs"]
     apply(simp add: replicate_merge_anywhere replicate_Suc_iff_anywhere del: replicate_Suc)
     by(simp add: list_update_append list_update.simps replicate_Suc_iff_anywhere del: replicate_Suc)
   ultimately show "?thesis"
@@ -1108,21 +1118,21 @@
 
 lemma clean_paras: 
   "ffp \<ge> length gs \<Longrightarrow>
-  {\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
+  {\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @
   0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length gs) @
-  rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
+  rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
   empty_boxes (length gs)
   {\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ 
-  rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
+  rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}"
 proof-
   let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
   assume h: "length gs \<le> ffp"
-  let ?lm = "map (\<lambda>i. rec_eval i xs) gs @ 0 \<up> (?ft - length gs) @
-    rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+  let ?lm = "map (\<lambda>i. rec_exec i xs) gs @ 0 \<up> (?ft - length gs) @
+    rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
   have "{\<lambda> nl. nl = ?lm} empty_boxes (length gs) {\<lambda> nl. nl = 0\<up>length gs @ drop (length gs) ?lm}"
     by(rule_tac empty_boxes_correct, simp)
   moreover have "0\<up>length gs @ drop (length gs) ?lm 
-           =  0 \<up> ?ft @  rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+           =  0 \<up> ?ft @  rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
     using h
     by(simp add: replicate_merge_anywhere)
   ultimately show "?thesis"
@@ -1132,20 +1142,20 @@
 
 lemma restore_rs:
   "{\<lambda>nl. nl = 0 \<up> max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) @ 
-  rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
+  rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything}
   mv_box (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) (length xs)
   {\<lambda>nl. nl = 0 \<up> length xs @
-  rec_eval (Cn (length xs) f gs) xs #
+  rec_exec (Cn (length xs) f gs) xs #
   0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - (length xs)) @
   0 \<up> length gs @ xs @ anything}"
 proof -
   let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
-  let ?lm = "0\<up>(length xs) @  0\<up>(?ft - (length xs)) @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
+  let ?lm = "0\<up>(length xs) @  0\<up>(?ft - (length xs)) @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> length gs @ xs @ anything"
   thm mv_box_correct
   have "{\<lambda> nl. nl = ?lm} mv_box ?ft (length xs) {\<lambda> nl. nl = ?lm[length xs := ?lm!?ft + ?lm!(length xs), ?ft := 0]}"
     by(rule_tac mv_box_correct, simp, simp)
   moreover have "?lm[length xs := ?lm!?ft + ?lm!(length xs), ?ft := 0]
-               =  0 \<up> length xs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> (?ft - (length xs)) @ 0 \<up> length gs @ xs @ anything"
+               =  0 \<up> length xs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft - (length xs)) @ 0 \<up> length gs @ xs @ anything"
     apply(auto simp: list_update_append nth_append)
     apply(case_tac ?ft, simp_all add: Suc_diff_le list_update.simps)
     apply(simp add: exp_suc replicate_Suc[THEN sym] del: replicate_Suc)
@@ -1156,17 +1166,17 @@
 
 lemma restore_orgin_paras:
   "{\<lambda>nl. nl = 0 \<up> length xs @
-  rec_eval (Cn (length xs) f gs) xs #
+  rec_exec (Cn (length xs) f gs) xs #
   0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) - length xs) @ 0 \<up> length gs @ xs @ anything}
   mv_boxes (Suc (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) 0 (length xs)
-  {\<lambda>nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> 
+  {\<lambda>nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> 
   (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything}"
 proof -
   let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
   thm mv_boxes_correct2
-  have "{\<lambda> nl. nl = [] @ 0\<up>(length xs) @ (rec_eval (Cn (length xs) f gs) xs # 0 \<up> (?ft - length xs) @ 0 \<up> length gs) @ xs @ anything}
+  have "{\<lambda> nl. nl = [] @ 0\<up>(length xs) @ (rec_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft - length xs) @ 0 \<up> length gs) @ xs @ anything}
         mv_boxes (Suc ?ft + length gs) 0 (length xs)
-        {\<lambda> nl. nl = [] @ xs @ (rec_eval (Cn (length xs) f gs) xs # 0 \<up> (?ft - length xs) @ 0 \<up> length gs) @ 0\<up>length xs @ anything}"
+        {\<lambda> nl. nl = [] @ xs @ (rec_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft - length xs) @ 0 \<up> length gs) @ 0\<up>length xs @ anything}"
     by(rule_tac mv_boxes_correct2, auto)
   thus "?thesis"
     by(simp add: replicate_merge_anywhere)
@@ -1174,14 +1184,14 @@
 
 lemma compile_cn_correct':
   assumes f_ind: 
-  "\<And> anything r. rec_eval f (map (\<lambda>g. rec_eval g xs) gs) = rec_eval (Cn (length xs) f gs) xs \<Longrightarrow>
-  {\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
-                {\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> (ffp - Suc far) @ anything}"
+  "\<And> anything r. rec_exec f (map (\<lambda>g. rec_exec g xs) gs) = rec_exec (Cn (length xs) f gs) xs \<Longrightarrow>
+  {\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
+                {\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> (ffp - Suc far) @ anything}"
   and compile: "rec_ci f = (fap, far, ffp)"
-  and term_f: "terminates f (map (\<lambda>g. rec_eval g xs) gs)"
-  and g_cond: "\<forall>g\<in>set gs. terminates g xs \<and>
+  and term_f: "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
+  and g_cond: "\<forall>g\<in>set gs. terminate g xs \<and>
   (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow> 
-  (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+  (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
   shows 
   "{\<lambda>nl. nl = xs @ 0 # 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything}
   cn_merge_gs (map rec_ci gs) (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) [+]
@@ -1191,7 +1201,7 @@
   (empty_boxes (length gs) [+]
   (mv_box (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))) (length xs) [+]
   mv_boxes (Suc (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs)) 0 (length xs)))))))
-  {\<lambda>nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs # 
+  {\<lambda>nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 
 0 \<up> (max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs))) + length gs) @ anything}"
 proof -
   let ?ft = "max (Suc (length xs)) (Max (insert ffp ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
@@ -1204,8 +1214,8 @@
   let ?G = "mv_box ?ft (length xs)"
   let ?H = "mv_boxes (Suc (?ft + length gs)) 0 (length xs)"
   let ?P1 = "\<lambda>nl. nl = xs @ 0 # 0 \<up> (?ft + length gs) @ anything"
-  let ?S = "\<lambda>nl. nl = xs @ rec_eval (Cn (length xs) f gs) xs # 0 \<up> (?ft + length gs) @ anything"
-  let ?Q1 = "\<lambda> nl. nl = xs @ 0\<up>(?ft - length xs) @ map (\<lambda> i. rec_eval i xs) gs @ 0\<up>(Suc (length xs)) @ anything"
+  let ?S = "\<lambda>nl. nl = xs @ rec_exec (Cn (length xs) f gs) xs # 0 \<up> (?ft + length gs) @ anything"
+  let ?Q1 = "\<lambda> nl. nl = xs @ 0\<up>(?ft - length xs) @ map (\<lambda> i. rec_exec i xs) gs @ 0\<up>(Suc (length xs)) @ anything"
   show "{?P1} (?A [+] (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))))) {?S}"
   proof(rule_tac abc_Hoare_plus_halt)
     show "{?P1} ?A {?Q1}"
@@ -1213,13 +1223,13 @@
       by(rule_tac compile_cn_gs_correct, auto)
   next
     let ?Q2 = "\<lambda>nl. nl = 0 \<up> ?ft @
-                    map (\<lambda>i. rec_eval i xs) gs @ 0 # xs @ anything"
+                    map (\<lambda>i. rec_exec i xs) gs @ 0 # xs @ anything"
     show "{?Q1} (?B [+] (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H)))))) {?S}"
     proof(rule_tac abc_Hoare_plus_halt)
       show "{?Q1} ?B {?Q2}"
         by(rule_tac save_paras)
     next
-      let ?Q3 = "\<lambda> nl. nl = map (\<lambda>i. rec_eval i xs) gs @ 0\<up>?ft @ 0 # xs @ anything" 
+      let ?Q3 = "\<lambda> nl. nl = map (\<lambda>i. rec_exec i xs) gs @ 0\<up>?ft @ 0 # xs @ anything" 
       show "{?Q2} (?C [+] (?D [+] (?E [+] (?F [+] (?G [+] ?H))))) {?S}"
       proof(rule_tac abc_Hoare_plus_halt)
         have "ffp \<ge> length gs"
@@ -1230,7 +1240,7 @@
         thus "{?Q2} ?C {?Q3}"
           by(erule_tac restore_new_paras)
       next
-        let ?Q4 = "\<lambda> nl. nl = map (\<lambda>i. rec_eval i xs) gs @ rec_eval (Cn (length xs) f gs) xs # 0\<up>?ft @ xs @ anything"
+        let ?Q4 = "\<lambda> nl. nl = map (\<lambda>i. rec_exec i xs) gs @ rec_exec (Cn (length xs) f gs) xs # 0\<up>?ft @ xs @ anything"
         have a: "far = length gs"
           using compile term_f
           by(drule_tac param_pattern, auto)
@@ -1241,23 +1251,23 @@
           by(erule_tac footprint_ge)
         show "{?Q3} (?D [+] (?E [+] (?F [+] (?G [+] ?H)))) {?S}"
         proof(rule_tac abc_Hoare_plus_halt)
-          have "{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ 0 \<up> (ffp - far) @ 0\<up>(?ft - ffp + far) @ 0 # xs @ anything} fap
-            {\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval (Cn (length xs) f gs) xs # 
+          have "{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ 0 \<up> (ffp - far) @ 0\<up>(?ft - ffp + far) @ 0 # xs @ anything} fap
+            {\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec (Cn (length xs) f gs) xs # 
             0 \<up> (ffp - Suc far) @ 0\<up>(?ft - ffp + far) @ 0 # xs @ anything}"
-            by(rule_tac f_ind, simp add: rec_eval.simps)
+            by(rule_tac f_ind, simp add: rec_exec.simps)
           thus "{?Q3} fap {?Q4}"
             using a b c
             by(simp add: replicate_merge_anywhere,
                case_tac "?ft", simp_all add: exp_suc del: replicate_Suc)
         next
-          let ?Q5 = "\<lambda>nl. nl = map (\<lambda>i. rec_eval i xs) gs @
-               0\<up>(?ft - length gs) @ rec_eval (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
+          let ?Q5 = "\<lambda>nl. nl = map (\<lambda>i. rec_exec i xs) gs @
+               0\<up>(?ft - length gs) @ rec_exec (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
           show "{?Q4} (?E [+] (?F [+] (?G [+] ?H))) {?S}"
           proof(rule_tac abc_Hoare_plus_halt)
             from a b c show "{?Q4} ?E {?Q5}"
               by(erule_tac save_rs, simp_all)
           next
-            let ?Q6 = "\<lambda>nl. nl = 0\<up>?ft @ rec_eval (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
+            let ?Q6 = "\<lambda>nl. nl = 0\<up>?ft @ rec_exec (Cn (length xs) f gs) xs # 0\<up>(length gs)@ xs @ anything"
             show "{?Q5} (?F [+] (?G [+] ?H)) {?S}"
             proof(rule_tac abc_Hoare_plus_halt)
               have "length gs \<le> ffp" using a b c
@@ -1265,7 +1275,7 @@
               thus "{?Q5} ?F {?Q6}"
                 by(erule_tac clean_paras)
             next
-              let ?Q7 = "\<lambda>nl. nl = 0\<up>length xs @ rec_eval (Cn (length xs) f gs) xs # 0\<up>(?ft - (length xs)) @ 0\<up>(length gs)@ xs @ anything"
+              let ?Q7 = "\<lambda>nl. nl = 0\<up>length xs @ rec_exec (Cn (length xs) f gs) xs # 0\<up>(?ft - (length xs)) @ 0\<up>(length gs)@ xs @ anything"
               show "{?Q6} (?G [+] ?H) {?S}"
               proof(rule_tac abc_Hoare_plus_halt)
                 show "{?Q6} ?G {?Q7}"
@@ -1283,24 +1293,24 @@
 qed
 
 lemma compile_cn_correct:
-  assumes termi_f: "terminates f (map (\<lambda>g. rec_eval g xs) gs)"
+  assumes termi_f: "terminate f (map (\<lambda>g. rec_exec g xs) gs)"
   and f_ind: "\<And>ap arity fp anything.
   rec_ci f = (ap, arity, fp)
-  \<Longrightarrow> {\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ 0 \<up> (fp - arity) @ anything} ap
-  {\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval f (map (\<lambda>g. rec_eval g xs) gs) # 0 \<up> (fp - Suc arity) @ anything}"
+  \<Longrightarrow> {\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ 0 \<up> (fp - arity) @ anything} ap
+  {\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec f (map (\<lambda>g. rec_exec g xs) gs) # 0 \<up> (fp - Suc arity) @ anything}"
   and g_cond: 
-  "\<forall>g\<in>set gs. terminates g xs \<and>
-  (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>   (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_eval g xs # 0 \<up> (xb - Suc xa) @ xc}))"
+  "\<forall>g\<in>set gs. terminate g xs \<and>
+  (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>   (\<forall>xc. {\<lambda>nl. nl = xs @ 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ rec_exec g xs # 0 \<up> (xb - Suc xa) @ xc}))"
   and compile: "rec_ci (Cn n f gs) = (ap, arity, fp)"
   and len: "length xs = n"
-  shows "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_eval (Cn n f gs) xs # 0 \<up> (fp - Suc arity) @ anything}"
+  shows "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_exec (Cn n f gs) xs # 0 \<up> (fp - Suc arity) @ anything}"
 proof(case_tac "rec_ci f")
   fix fap far ffp
   assume h: "rec_ci f = (fap, far, ffp)"
-  then have f_newind: "\<And> anything .{\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
-    {\<lambda>nl. nl = map (\<lambda>g. rec_eval g xs) gs @ rec_eval f (map (\<lambda>g. rec_eval g xs) gs) # 0 \<up> (ffp - Suc far) @ anything}"
+  then have f_newind: "\<And> anything .{\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ 0 \<up> (ffp - far) @ anything} fap
+    {\<lambda>nl. nl = map (\<lambda>g. rec_exec g xs) gs @ rec_exec f (map (\<lambda>g. rec_exec g xs) gs) # 0 \<up> (ffp - Suc far) @ anything}"
     by(rule_tac f_ind, simp_all)
-  thus "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_eval (Cn n f gs) xs # 0 \<up> (fp - Suc arity) @ anything}"
+  thus "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_exec (Cn n f gs) xs # 0 \<up> (fp - Suc arity) @ anything}"
     using compile len h termi_f g_cond
     apply(auto simp: rec_ci.simps abc_comp_commute)
     apply(rule_tac compile_cn_correct', simp_all)
@@ -1319,9 +1329,9 @@
 
 lemma save_init_rs: 
   "\<lbrakk>length xs = n; ft = max (n+3) (max fft gft)\<rbrakk> 
-     \<Longrightarrow>  {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (ft - n) @ anything} mv_box n (Suc n) 
-       {\<lambda>nl. nl = xs @ 0 # rec_eval f xs # 0 \<up> (ft - Suc n) @ anything}"
-using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \<up> (ft - n) @ anything"]
+     \<Longrightarrow>  {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (ft - n) @ anything} mv_box n (Suc n) 
+       {\<lambda>nl. nl = xs @ 0 # rec_exec f xs # 0 \<up> (ft - Suc n) @ anything}"
+using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (ft - n) @ anything"]
 apply(auto simp: list_update_append list_update.simps nth_append split: if_splits)
 apply(case_tac "(max (length xs + 3) (max fft gft))", simp_all add: list_update.simps Suc_diff_le)
 done
@@ -1371,9 +1381,9 @@
 
 lemma [simp]:
   "length xs = n
- \<Longrightarrow> {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything} mv_box n (Suc n)
-    {\<lambda>nl. nl = xs @ 0 # rec_eval f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ x # anything}"
-using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
+ \<Longrightarrow> {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything} mv_box n (Suc n)
+    {\<lambda>nl. nl = xs @ 0 # rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ x # anything}"
+using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
 apply(simp add: nth_append list_update_append list_update.simps)
 apply(case_tac "max (n + 3) (max fft gft)", simp_all)
 apply(case_tac nat, simp_all add: Suc_diff_le list_update.simps)
@@ -1457,14 +1467,14 @@
 by arith
 
 lemma [simp]: "\<lbrakk>ft = max (n + 3) (max fft gft); length xs = n\<rbrakk> \<Longrightarrow>
-     {\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
+     {\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
      [Dec ft (length gap + 7)] 
-     {\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
+     {\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
 apply(simp add: abc_Hoare_halt_def)
 apply(rule_tac x = 1 in exI)
 apply(auto simp: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps list_update_append)
 using list_update_length
-[of "(x - Suc y) # rec_eval (Pr (length xs) f g) (xs @ [x - Suc y]) #
+[of "(x - Suc y) # rec_exec (Pr (length xs) f g) (xs @ [x - Suc y]) #
           0 \<up> (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" "Suc y" anything y]
 apply(simp)
 done
@@ -1516,7 +1526,7 @@
 using adjust_paras'[of xs n x y anything]
 by(simp add: abc_comp.simps abc_shift.simps numeral_2_eq_2 numeral_3_eq_3)
 
-lemma [simp]: "\<lbrakk>rec_ci g = (gap, gar, gft); \<forall>y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]);
+lemma [simp]: "\<lbrakk>rec_ci g = (gap, gar, gft); \<forall>y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]);
         length xs = n; Suc y\<le>x\<rbrakk> \<Longrightarrow> gar = Suc (Suc n)"
   apply(erule_tac x = y in allE, simp)
   apply(drule_tac param_pattern, auto)
@@ -1563,14 +1573,14 @@
 apply(simp add: abc_steps_l.simps abc_step_l.simps abc_fetch.simps nth_append abc_lm_v.simps abc_lm_s.simps)
 done
 
-lemma rec_eval_pr_0_simps: "rec_eval (Pr n f g) (xs @ [0]) = rec_eval f xs"
- by(simp add: rec_eval.simps)
+lemma rec_exec_pr_0_simps: "rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
+ by(simp add: rec_exec.simps)
 
-lemma rec_eval_pr_Suc_simps: "rec_eval (Pr n f g) (xs @ [Suc y])
-          = rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+lemma rec_exec_pr_Suc_simps: "rec_exec (Pr n f g) (xs @ [Suc y])
+          = rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
 apply(induct y)
-apply(simp add: rec_eval.simps)
-apply(simp add: rec_eval.simps)
+apply(simp add: rec_exec.simps)
+apply(simp add: rec_exec.simps)
 done
 
 lemma [simp]: "Suc (max (n + 3) (max fft gft) - Suc (Suc (Suc n))) = max (n + 3) (max fft gft) - Suc (Suc n)"
@@ -1580,44 +1590,44 @@
   assumes code: "code = ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @
     [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
   and len: "length xs = n"
-  and g_ind: "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-  {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
+  and g_ind: "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+  {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
   and compile_g: "rec_ci g = (gap, gar, gft)"
-  and termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+  and termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
   and ft: "ft = max (n + 3) (max fft gft)"
   and less: "Suc y \<le> x"
   shows 
-  "\<exists>stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
-  code stp = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything)"
+  "\<exists>stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
+  code stp = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything)"
 proof -
   let ?A = "[Dec  ft (length gap + 7)]"
   let ?B = "gap"
   let ?C = "[Inc n, Dec (Suc n) 3, Goto (Suc 0)]"
   let ?D = "[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
-  have "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
+  have "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
             ((?A [+] (?B [+] ?C)) @ ?D) stp = (length (?A [+] (?B [+] ?C)), 
-          xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])])
+          xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])])
                   # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
   proof -
-    have "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
+    have "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
       ((?A [+] (?B [+] ?C))) stp = (length (?A [+] (?B [+] ?C)),  xs @ (x - y) # 0 # 
-      rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
+      rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
     proof -
-      have "{\<lambda> nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
+      have "{\<lambda> nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
         (?A [+] (?B [+] ?C)) 
         {\<lambda> nl. nl = xs @ (x - y) # 0 # 
-        rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
+        rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
       proof(rule_tac abc_Hoare_plus_halt)
-        show "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
+        show "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything}
           [Dec ft (length gap + 7)] 
-          {\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
+          {\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything}"
           using ft len
           by(simp)
       next
         show 
-          "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything} 
+          "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything} 
           ?B [+] ?C
-          {\<lambda>nl. nl = xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
+          {\<lambda>nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
         proof(rule_tac abc_Hoare_plus_halt)
           have a: "gar = Suc (Suc n)" 
             using compile_g termi_g len less
@@ -1625,14 +1635,14 @@
           have b: "gft > gar"
             using compile_g
             by(erule_tac footprint_ge)
-          show "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything} gap 
-                {\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 
-                      rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
+          show "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ y # anything} gap 
+                {\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 
+                      rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
           proof -
             have 
-              "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (gft - gar) @ 0\<up>(ft - gft) @ y # anything} gap
-              {\<lambda>nl. nl = xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 
-              rec_eval g (xs @ [(x - Suc y), rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (gft - Suc gar) @ 0\<up>(ft - gft) @ y # anything}"
+              "{\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (gft - gar) @ 0\<up>(ft - gft) @ y # anything} gap
+              {\<lambda>nl. nl = xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 
+              rec_exec g (xs @ [(x - Suc y), rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (gft - Suc gar) @ 0\<up>(ft - gft) @ y # anything}"
               using g_ind less by simp
             thus "?thesis"
               using a b ft
@@ -1640,41 +1650,41 @@
           qed
         next
           show "{\<lambda>nl. nl = xs @ (x - Suc y) #
-                    rec_eval (Pr n f g) (xs @ [x - Suc y]) #
-            rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}
+                    rec_exec (Pr n f g) (xs @ [x - Suc y]) #
+            rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}
             [Inc n, Dec (Suc n) 3, Goto (Suc 0)]
-            {\<lambda>nl. nl = xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) 
+            {\<lambda>nl. nl = xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) 
                     (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything}"
             using len less
-            using adjust_paras[of xs n "x - Suc y" " rec_eval (Pr n f g) (xs @ [x - Suc y])"
-              " rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 
+            using adjust_paras[of xs n "x - Suc y" " rec_exec (Pr n f g) (xs @ [x - Suc y])"
+              " rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 
               0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything"]
             by(simp add: Suc_diff_Suc)
         qed
       qed
       thus "?thesis"
-        by(simp add: abc_Hoare_halt_def, auto, rule_tac x = na in exI, case_tac "abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 
+        by(simp add: abc_Hoare_halt_def, auto, rule_tac x = na in exI, case_tac "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 
           0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
              ([Dec ft (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) na", simp)
     qed
-    then obtain stpa where "abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
+    then obtain stpa where "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (ft - Suc (Suc n)) @ Suc y # anything)
             ((?A [+] (?B [+] ?C))) stpa = (length (?A [+] (?B [+] ?C)), 
-          xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])])
+          xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])])
                   # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)" ..
     thus "?thesis"
       by(erule_tac abc_append_frist_steps_halt_eq)
   qed
   moreover have 
     "\<exists> stp. abc_steps_l (length (?A [+] (?B [+] ?C)),
-    xs @ (x - y) # 0 # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)
-    ((?A [+] (?B [+] ?C)) @ ?D) stp  = (0, xs @ (x - y) # rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) # 
+    xs @ (x - y) # 0 # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)
+    ((?A [+] (?B [+] ?C)) @ ?D) stp  = (0, xs @ (x - y) # rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) # 
     0 # 0 \<up> (ft - Suc (Suc (Suc n))) @ y # anything)"
     using len
     by(rule_tac loop_back, simp_all)
-  moreover have "rec_eval g (xs @ [x - Suc y, rec_eval (Pr n f g) (xs @ [x - Suc y])]) = rec_eval (Pr n f g) (xs @ [x - y])"
+  moreover have "rec_exec g (xs @ [x - Suc y, rec_exec (Pr n f g) (xs @ [x - Suc y])]) = rec_exec (Pr n f g) (xs @ [x - y])"
     using less
-    thm rec_eval.simps
-    apply(case_tac "x - y", simp_all add: rec_eval_pr_Suc_simps)
+    thm rec_exec.simps
+    apply(case_tac "x - y", simp_all add: rec_exec_pr_Suc_simps)
     by(subgoal_tac "nat = x - Suc y", simp, arith)    
   ultimately show "?thesis"
     using code ft
@@ -1682,21 +1692,21 @@
 qed
 
 lemma [simp]: 
-  "length xs = n \<Longrightarrow> abc_lm_s (xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) 
+  "length xs = n \<Longrightarrow> abc_lm_s (xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) 
   (max fft gft) - Suc (Suc n)) @ 0 # anything) (max (n + 3) (max fft gft)) 0 =
-    xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything"
+    xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything"
 apply(simp add: abc_lm_s.simps)
-using list_update_length[of "xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n))"
+using list_update_length[of "xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n))"
                         0 anything 0]
 apply(auto simp: Suc_diff_Suc)
 apply(simp add: exp_suc[THEN sym] Suc_diff_Suc  del: replicate_Suc)
 done
 
 lemma [simp]:
-  "(xs @ x # rec_eval (Pr (length xs) f g) (xs @ [x]) # 0 \<up> (max (length xs + 3)
+  "(xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) # 0 \<up> (max (length xs + 3)
   (max fft gft) - Suc (Suc (length xs))) @ 0 # anything) !
     max (length xs + 3) (max fft gft) = 0"
-using nth_append_length[of "xs @ x # rec_eval (Pr (length xs) f g) (xs @ [x]) #
+using nth_append_length[of "xs @ x # rec_exec (Pr (length xs) f g) (xs @ [x]) #
   0 \<up> (max (length xs + 3) (max fft gft) - Suc (Suc (length xs)))" 0  anything]
 by(simp)
 
@@ -1704,12 +1714,12 @@
   assumes less: "y \<le> x" 
   and len: "length xs = n"
   and compile_g: "rec_ci g = (gap, gar, gft)"
-  and termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
-  and g_ind: "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-  {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
-  shows "{\<lambda>nl. nl = xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ y # anything}
+  and termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
+  and g_ind: "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+  {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
+  shows "{\<lambda>nl. nl = xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (max (n + 3) (max fft gft) - Suc (Suc n)) @ y # anything}
    ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]
-   {\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}" 
+   {\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}" 
   using less
 proof(induct y)
   case 0
@@ -1725,37 +1735,37 @@
   let ?C = "[Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] 
     [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
   have ind: "y \<le> x \<Longrightarrow>
-         {\<lambda>nl. nl = xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything}
-         ?C {\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything}" by fact 
+         {\<lambda>nl. nl = xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything}
+         ?C {\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything}" by fact 
   have less: "Suc y \<le> x" by fact
   have stp1: 
-    "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (?ft - Suc (Suc n)) @ Suc y # anything)
-    ?C stp  = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)"
+    "\<exists> stp. abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (?ft - Suc (Suc n)) @ Suc y # anything)
+    ?C stp  = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)"
     using assms less
     by(rule_tac  pr_loop, auto)
   then obtain stp1 where a:
-    "abc_steps_l (0, xs @ (x - Suc y) # rec_eval (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (?ft - Suc (Suc n)) @ Suc y # anything)
-   ?C stp1 = (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)" ..
+    "abc_steps_l (0, xs @ (x - Suc y) # rec_exec (Pr n f g) (xs @ [x - Suc y]) # 0 \<up> (?ft - Suc (Suc n)) @ Suc y # anything)
+   ?C stp1 = (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)" ..
   moreover have 
-    "\<exists> stp. abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
-    ?C stp = (length ?C, xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)"
+    "\<exists> stp. abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
+    ?C stp = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)"
     using ind less
-    by(auto simp: abc_Hoare_halt_def, case_tac "abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g) 
+    by(auto simp: abc_Hoare_halt_def, case_tac "abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) 
       (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything) ?C na", rule_tac x = na in exI, simp)
   then obtain stp2 where b:
-    "abc_steps_l (0, xs @ (x - y) # rec_eval (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
-    ?C stp2 = (length ?C, xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)" ..
+    "abc_steps_l (0, xs @ (x - y) # rec_exec (Pr n f g) (xs @ [x - y]) # 0 \<up> (?ft - Suc (Suc n)) @ y # anything)
+    ?C stp2 = (length ?C, xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything)" ..
   from a b show "?case"
     by(simp add: abc_Hoare_halt_def, rule_tac x = "stp1 + stp2" in exI, simp add: abc_steps_add)
 qed
 
 lemma compile_pr_correct':
-  assumes termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+  assumes termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
   and g_ind: 
-  "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-  {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
-  and termi_f: "terminates f xs"
-  and f_ind: "\<And> anything. {\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ anything} fap {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (fft - Suc far) @ anything}"
+  "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+  {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
+  and termi_f: "terminate f xs"
+  and f_ind: "\<And> anything. {\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ anything} fap {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (fft - Suc far) @ anything}"
   and len: "length xs = n"
   and compile1: "rec_ci f = (fap, far, fft)"
   and compile2: "rec_ci g = (gap, gar, gft)"
@@ -1765,7 +1775,7 @@
   (fap [+] (mv_box n (Suc n) [+]
   ([Dec (max (n + 3) (max fft gft)) (length gap + 7)] [+] (gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]) @
   [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)])))
-  {\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}"
+  {\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ anything}"
 proof -
   let ?ft = "max (n+3) (max fft gft)"
   let ?A = "mv_box n ?ft"
@@ -1775,14 +1785,14 @@
   let ?E = "gap [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]"
   let ?F = "[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gap + 4)]"
   let ?P = "\<lambda>nl. nl = xs @ x # 0 \<up> (?ft - n) @ anything"
-  let ?S = "\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything"
+  let ?S = "\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (?ft - Suc n) @ anything"
   let ?Q1 = "\<lambda>nl. nl = xs @ 0 \<up> (?ft - n) @  x # anything"
   show "{?P} (?A [+] (?B [+] (?C [+] (?D [+] ?E @ ?F)))) {?S}"
   proof(rule_tac abc_Hoare_plus_halt)
     show "{?P} ?A {?Q1}"
       using len by simp
   next
-    let ?Q2 = "\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (?ft - Suc n) @  x # anything"
+    let ?Q2 = "\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (?ft - Suc n) @  x # anything"
     have a: "?ft \<ge> fft"
       by arith
     have b: "far = n"
@@ -1794,7 +1804,7 @@
     show "{?Q1} (?B [+] (?C [+] (?D [+] ?E @ ?F))) {?S}"
     proof(rule_tac abc_Hoare_plus_halt)
       have "{\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ 0\<up>(?ft - fft) @ x # anything} fap 
-            {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (fft - Suc far) @ 0\<up>(?ft - fft) @ x # anything}"
+            {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (fft - Suc far) @ 0\<up>(?ft - fft) @ x # anything}"
         by(rule_tac f_ind)
       moreover have "fft - far + ?ft - fft = ?ft - far"
         using a b c by arith
@@ -1804,50 +1814,50 @@
         using b
         by(simp add: replicate_merge_anywhere)
     next
-      let ?Q3 = "\<lambda> nl. nl = xs @ 0 # rec_eval f xs # 0\<up>(?ft - Suc (Suc n)) @ x # anything"
+      let ?Q3 = "\<lambda> nl. nl = xs @ 0 # rec_exec f xs # 0\<up>(?ft - Suc (Suc n)) @ x # anything"
       show "{?Q2} (?C [+] (?D [+] ?E @ ?F)) {?S}"
       proof(rule_tac abc_Hoare_plus_halt)
         show "{?Q2} (?C) {?Q3}"
-          using mv_box_correct[of n "Suc n" "xs @ rec_eval f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
+          using mv_box_correct[of n "Suc n" "xs @ rec_exec f xs # 0 \<up> (max (n + 3) (max fft gft) - Suc n) @ x # anything"]
           using len
           by(auto)
       next
         show "{?Q3} (?D [+] ?E @ ?F) {?S}"
           using pr_loop_correct[of x x xs n g  gap gar gft f fft anything] assms
-          by(simp add: rec_eval_pr_0_simps)
+          by(simp add: rec_exec_pr_0_simps)
       qed
     qed
   qed
 qed 
 
 lemma compile_pr_correct:
-  assumes g_ind: "\<forall>y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) \<and>
+  assumes g_ind: "\<forall>y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) \<and>
   (\<forall>x xa xb. rec_ci g = (x, xa, xb) \<longrightarrow>
-  (\<forall>xc. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (xb - xa) @ xc} x
-  {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (xb - Suc xa) @ xc}))"
-  and termi_f: "terminates f xs"
+  (\<forall>xc. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (xb - xa) @ xc} x
+  {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (xb - Suc xa) @ xc}))"
+  and termi_f: "terminate f xs"
   and f_ind:
   "\<And>ap arity fp anything.
-  rec_ci f = (ap, arity, fp) \<Longrightarrow> {\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (fp - Suc arity) @ anything}"
+  rec_ci f = (ap, arity, fp) \<Longrightarrow> {\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (fp - Suc arity) @ anything}"
   and len: "length xs = n"
   and compile: "rec_ci (Pr n f g) = (ap, arity, fp)"
-  shows "{\<lambda>nl. nl = xs @ x # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ x # rec_eval (Pr n f g) (xs @ [x]) # 0 \<up> (fp - Suc arity) @ anything}"
+  shows "{\<lambda>nl. nl = xs @ x # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ x # rec_exec (Pr n f g) (xs @ [x]) # 0 \<up> (fp - Suc arity) @ anything}"
 proof(case_tac "rec_ci f", case_tac "rec_ci g")
   fix fap far fft gap gar gft
   assume h: "rec_ci f = (fap, far, fft)" "rec_ci g = (gap, gar, gft)"
   have g: 
-    "\<forall>y<x. (terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) \<and>
-     (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-    {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything}))"
+    "\<forall>y<x. (terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) \<and>
+     (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+    {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything}))"
     using g_ind h
     by(auto)
-  hence termi_g: "\<forall> y<x. terminates g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])])"
+  hence termi_g: "\<forall> y<x. terminate g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])])"
     by simp
   from g have g_newind: 
-    "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
-    {\<lambda>nl. nl = xs @ y # rec_eval (Pr n f g) (xs @ [y]) # rec_eval g (xs @ [y, rec_eval (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
+    "\<forall> y<x. (\<forall>anything. {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # 0 \<up> (gft - gar) @ anything} gap
+    {\<lambda>nl. nl = xs @ y # rec_exec (Pr n f g) (xs @ [y]) # rec_exec g (xs @ [y, rec_exec (Pr n f g) (xs @ [y])]) # 0 \<up> (gft - Suc gar) @ anything})"
     by auto
-  have f_newind: "\<And> anything. {\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ anything} fap {\<lambda>nl. nl = xs @ rec_eval f xs # 0 \<up> (fft - Suc far) @ anything}"
+  have f_newind: "\<And> anything. {\<lambda>nl. nl = xs @ 0 \<up> (fft - far) @ anything} fap {\<lambda>nl. nl = xs @ rec_exec f xs # 0 \<up> (fft - Suc far) @ anything}"
     using h
     by(rule_tac f_ind, simp)
   show "?thesis"
@@ -1984,20 +1994,20 @@
   and len: "length xs = arity"
   and far: "far = Suc arity"
   and ind: " (\<forall>xc. ({\<lambda>nl. nl = xs @ x # 0 \<up> (fft - far) @ xc} fap
-    {\<lambda>nl. nl = xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (fft - Suc far) @ xc}))"
-  and exec_less: "rec_eval f (xs @ [x]) > 0"
+    {\<lambda>nl. nl = xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (fft - Suc far) @ xc}))"
+  and exec_less: "rec_exec f (xs @ [x]) > 0"
   and compile: "rec_ci f = (fap, far, fft)"
   shows "\<exists> stp > 0. abc_steps_l (0, xs @ x # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
     (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything)"
 proof -
   have "\<exists> stp. abc_steps_l (0, xs @ x # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
-    (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+    (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
   proof -
     have "\<exists> stp. abc_steps_l (0, xs @ x # 0 \<up> (ft - Suc arity) @ anything) fap stp =
-      (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+      (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
     proof -
       have "{\<lambda>nl. nl = xs @ x # 0 \<up> (fft - far) @ 0\<up>(ft - fft) @ anything} fap 
-            {\<lambda>nl. nl = xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
+            {\<lambda>nl. nl = xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
         using ind by simp
       moreover have "fft > far"
         using compile
@@ -2008,17 +2018,17 @@
         by(simp add: replicate_merge_anywhere max_absorb2)
     qed
     then obtain stp where "abc_steps_l (0, xs @ x # 0 \<up> (ft - Suc arity) @ anything) fap stp =
-      (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
+      (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
     thus "?thesis"
       by(erule_tac abc_append_frist_steps_halt_eq)
   qed
   moreover have 
-    "\<exists> stp > 0. abc_steps_l (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp =
+    "\<exists> stp > 0. abc_steps_l (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp =
     (0, xs @ Suc x # 0 # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
-    using mn_correct[of f fap far fft "rec_eval f (xs @ [x])" xs arity B
-      "(\<lambda>stp. (abc_steps_l (length fap, xs @ x # rec_eval f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp, length fap, arity))"     
+    using mn_correct[of f fap far fft "rec_exec f (xs @ [x])" xs arity B
+      "(\<lambda>stp. (abc_steps_l (length fap, xs @ x # rec_exec f (xs @ [x]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp, length fap, arity))"     
       x "0 \<up> (ft - Suc (Suc arity)) @ anything" "(\<lambda>((as, lm), ss, arity). as = 0)" 
-      "(\<lambda>((as, lm), ss, aritya). mn_ind_inv (as, lm) (length fap) x (rec_eval f (xs @ [x])) (0 \<up> (ft - Suc (Suc arity)) @ anything) xs) "]  
+      "(\<lambda>((as, lm), ss, aritya). mn_ind_inv (as, lm) (length fap) x (rec_exec f (xs @ [x])) (0 \<up> (ft - Suc (Suc arity)) @ anything) xs) "]  
       B compile  exec_less len
     apply(subgoal_tac "fap \<noteq> []", auto)
     apply(rule_tac x = stp in exI, auto simp: mn_ind_inv.simps)
@@ -2038,8 +2048,8 @@
   and ft: "ft = max (Suc arity) fft"
   and len: "length xs = arity"
   and ind_all: "\<forall>i\<le>x. (\<forall>xc. ({\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-  and exec_ge: "\<forall> i\<le>x. rec_eval f (xs @ [i]) > 0"
+    {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+  and exec_ge: "\<forall> i\<le>x. rec_exec f (xs @ [i]) > 0"
   and compile: "rec_ci f = (fap, far, fft)"
   and far: "far = Suc arity"
   shows "\<exists> stp > x. abc_steps_l (0, xs @ 0 # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp = 
@@ -2052,12 +2062,12 @@
     by(rule_tac mn_loop, simp_all)
 next
   case (Suc x)
-  have ind': "\<lbrakk>\<forall>i\<le>x. \<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc};
-               \<forall>i\<le>x. 0 < rec_eval f (xs @ [i])\<rbrakk> \<Longrightarrow> 
+  have ind': "\<lbrakk>\<forall>i\<le>x. \<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc};
+               \<forall>i\<le>x. 0 < rec_exec f (xs @ [i])\<rbrakk> \<Longrightarrow> 
             \<exists>stp > x. abc_steps_l (0, xs @ 0 # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp = (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything)" by fact
-  have exec_ge: "\<forall>i\<le>Suc x. 0 < rec_eval f (xs @ [i])" by fact
+  have exec_ge: "\<forall>i\<le>Suc x. 0 < rec_exec f (xs @ [i])" by fact
   have ind_all: "\<forall>i\<le>Suc x. \<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap 
-    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}" by fact
+    {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}" by fact
   have ind: "\<exists>stp > x. abc_steps_l (0, xs @ 0 # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
     (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything)" using ind' exec_ge ind_all by simp
   have stp: "\<exists> stp > 0. abc_steps_l (0, xs @ Suc x # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp =
@@ -2074,8 +2084,8 @@
   and ft: "ft = max (Suc arity) fft"
   and len: "length xs = arity"
   and ind_all: "\<forall>i\<le>x. (\<forall>xc. ({\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-  and exec_ge: "\<forall> i\<le>x. rec_eval f (xs @ [i]) > 0"
+    {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+  and exec_ge: "\<forall> i\<le>x. rec_exec f (xs @ [i]) > 0"
   and compile: "rec_ci f = (fap, far, fft)"
   and far: "far = Suc arity"
   shows "\<exists> stp. abc_steps_l (0, xs @ 0 # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp = 
@@ -2092,17 +2102,17 @@
   assumes B:  "B = [Dec (Suc arity) (length fap + 5), Dec (Suc arity) (length fap + 3), Goto (Suc (length fap)), Inc arity, Goto 0]"
   and ft: "ft = max (Suc arity) fft"
   and len: "length xs = arity"
-  and termi_f: "terminates f (xs @ [r])"
+  and termi_f: "terminate f (xs @ [r])"
   and f_ind: "\<And>anything. {\<lambda>nl. nl = xs @ r # 0 \<up> (fft - far) @ anything} fap 
         {\<lambda>nl. nl = xs @ r # 0 # 0 \<up> (fft - Suc far) @ anything}"
   and ind_all: "\<forall>i < r. (\<forall>xc. ({\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
-  and exec_less: "\<forall> i<r. rec_eval f (xs @ [i]) > 0"
-  and exec: "rec_eval f (xs @ [r]) = 0"
+    {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+  and exec_less: "\<forall> i<r. rec_exec f (xs @ [i]) > 0"
+  and exec: "rec_exec f (xs @ [r]) = 0"
   and compile: "rec_ci f = (fap, far, fft)"
   shows "{\<lambda>nl. nl = xs @ 0 \<up> (max (Suc arity) fft - arity) @ anything}
     fap @ B
-    {\<lambda>nl. nl = xs @ rec_eval (Mn arity f) xs # 0 \<up> (max (Suc arity) fft - Suc arity) @ anything}"
+    {\<lambda>nl. nl = xs @ rec_exec (Mn arity f) xs # 0 \<up> (max (Suc arity) fft - Suc arity) @ anything}"
 proof -
   have a: "far = Suc arity"
     using len compile termi_f
@@ -2117,13 +2127,13 @@
     by(rule_tac mn_loop_correct, auto)  
   moreover have 
     "\<exists> stp. abc_steps_l (0, xs @ r # 0 \<up> (ft - Suc arity) @ anything) (fap @ B) stp = 
-    (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+    (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
   proof -
     have "\<exists> stp. abc_steps_l (0, xs @ r # 0 \<up> (ft - Suc arity) @ anything) fap stp =
-      (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+      (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
     proof -
       have "{\<lambda>nl. nl = xs @ r # 0 \<up> (fft - far) @ 0\<up>(ft - fft) @ anything} fap 
-            {\<lambda>nl. nl = xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
+            {\<lambda>nl. nl = xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (fft - Suc far) @ 0\<up>(ft - fft) @ anything}"
         using f_ind exec by simp
       thus "?thesis"
         using ft a b
@@ -2131,20 +2141,20 @@
         by(simp add: replicate_merge_anywhere max_absorb2)
     qed
     then obtain stp where "abc_steps_l (0, xs @ r # 0 \<up> (ft - Suc arity) @ anything) fap stp =
-      (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
+      (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)" ..
     thus "?thesis"
       by(erule_tac abc_append_frist_steps_halt_eq)
   qed
   moreover have 
-    "\<exists> stp. abc_steps_l (length fap, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = 
-             (length fap + 5, xs @ r # rec_eval f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
+    "\<exists> stp. abc_steps_l (length fap, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything) (fap @ B) stp = 
+             (length fap + 5, xs @ r # rec_exec f (xs @ [r]) # 0 \<up> (ft - Suc (Suc arity)) @ anything)"
     using ft a b len B exec
     apply(rule_tac x = 1 in exI, auto)
     by(auto simp: abc_steps_l.simps B abc_step_l.simps 
       abc_fetch.simps nth_append max_absorb2 abc_lm_v.simps abc_lm_s.simps)
-  moreover have "rec_eval (Mn (length xs) f) xs = r"
+  moreover have "rec_exec (Mn (length xs) f) xs = r"
     using exec exec_less
-    apply(auto simp: rec_eval.simps Least_def)
+    apply(auto simp: rec_exec.simps Least_def)
     thm the_equality
     apply(rule_tac the_equality, auto)
     apply(metis exec_less less_not_refl3 linorder_not_less)
@@ -2158,18 +2168,18 @@
 
 lemma compile_mn_correct:
   assumes len: "length xs = n"
-  and termi_f: "terminates f (xs @ [r])"
+  and termi_f: "terminate f (xs @ [r])"
   and f_ind: "\<And>ap arity fp anything. rec_ci f = (ap, arity, fp) \<Longrightarrow> 
   {\<lambda>nl. nl = xs @ r # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ r # 0 # 0 \<up> (fp - Suc arity) @ anything}"
-  and exec: "rec_eval f (xs @ [r]) = 0"
+  and exec: "rec_exec f (xs @ [r]) = 0"
   and ind_all: 
-  "\<forall>i<r. terminates f (xs @ [i]) \<and>
+  "\<forall>i<r. terminate f (xs @ [i]) \<and>
   (\<forall>x xa xb. rec_ci f = (x, xa, xb) \<longrightarrow> 
-  (\<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (xb - Suc xa) @ xc})) \<and>
-  0 < rec_eval f (xs @ [i])"
+  (\<forall>xc. {\<lambda>nl. nl = xs @ i # 0 \<up> (xb - xa) @ xc} x {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (xb - Suc xa) @ xc})) \<and>
+  0 < rec_exec f (xs @ [i])"
   and compile: "rec_ci (Mn n f) = (ap, arity, fp)"
   shows "{\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap 
-  {\<lambda>nl. nl = xs @ rec_eval (Mn n f) xs # 0 \<up> (fp - Suc arity) @ anything}"
+  {\<lambda>nl. nl = xs @ rec_exec (Mn n f) xs # 0 \<up> (fp - Suc arity) @ anything}"
 proof(case_tac "rec_ci f")
   fix fap far fft
   assume h: "rec_ci f = (fap, far, fft)"
@@ -2179,10 +2189,10 @@
     by(rule_tac f_ind, simp)
   have newind_all: 
     "\<forall>i < r. (\<forall>xc. ({\<lambda>nl. nl = xs @ i # 0 \<up> (fft - far) @ xc} fap
-    {\<lambda>nl. nl = xs @ i # rec_eval f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
+    {\<lambda>nl. nl = xs @ i # rec_exec f (xs @ [i]) # 0 \<up> (fft - Suc far) @ xc}))"
     using ind_all h
     by(auto)
-  have all_less: "\<forall> i<r. rec_eval f (xs @ [i]) > 0"
+  have all_less: "\<forall> i<r. rec_exec f (xs @ [i]) > 0"
     using ind_all by auto
   show "?thesis"
     using h compile f_newind newind_all all_less len termi_f exec
@@ -2191,10 +2201,10 @@
 qed
     
 lemma recursive_compile_correct:
-   "\<lbrakk>terminates recf args; rec_ci recf = (ap, arity, fp)\<rbrakk>
+   "\<lbrakk>terminate recf args; rec_ci recf = (ap, arity, fp)\<rbrakk>
   \<Longrightarrow> {\<lambda> nl. nl = args @ 0\<up>(fp - arity) @ anything} ap 
-         {\<lambda> nl. nl = args@ rec_eval recf args # 0\<up>(fp - Suc arity) @ anything}"
-apply(induct arbitrary: ap arity fp anything r rule: terminates.induct)
+         {\<lambda> nl. nl = args@ rec_exec recf args # 0\<up>(fp - Suc arity) @ anything}"
+apply(induct arbitrary: ap arity fp anything r rule: terminate.induct)
 apply(simp_all add: compile_s_correct compile_z_correct compile_id_correct 
                     compile_cn_correct compile_pr_correct compile_mn_correct)
 done
@@ -2323,8 +2333,8 @@
 
 lemma recursive_compile_correct_norm': 
   "\<lbrakk>rec_ci f = (ap, arity, ft);  
-    terminates f args\<rbrakk>
-  \<Longrightarrow> \<exists> stp rl. (abc_steps_l (0, args) ap stp) = (length ap, rl) \<and> abc_list_crsp (args @ [rec_eval f args]) rl"
+    terminate f args\<rbrakk>
+  \<Longrightarrow> \<exists> stp rl. (abc_steps_l (0, args) ap stp) = (length ap, rl) \<and> abc_list_crsp (args @ [rec_exec f args]) rl"
   using recursive_compile_correct[of f args ap arity ft "[]"]
 apply(auto simp: abc_Hoare_halt_def)
 apply(rule_tac x = n in exI)
@@ -2334,9 +2344,9 @@
 done
 
 lemma [simp]:
-  assumes a: "args @ [rec_eval f args] = lm @ 0 \<up> n"
+  assumes a: "args @ [rec_exec f args] = lm @ 0 \<up> n"
   and b: "length args < length lm"
-  shows "\<exists>m. lm = args @ rec_eval f args # 0 \<up> m"
+  shows "\<exists>m. lm = args @ rec_exec f args # 0 \<up> m"
 using assms
 apply(case_tac n, simp)
 apply(rule_tac x = 0 in exI, simp)
@@ -2344,9 +2354,9 @@
 done
 
 lemma [simp]: 
-"\<lbrakk>args @ [rec_eval f args] = lm @ 0 \<up> n; \<not> length args < length lm\<rbrakk>
+"\<lbrakk>args @ [rec_exec f args] = lm @ 0 \<up> n; \<not> length args < length lm\<rbrakk>
   \<Longrightarrow> \<exists>m. (lm @ 0 \<up> (length args - length lm) @ [Suc 0])[length args := 0] =
-  args @ rec_eval f args # 0 \<up> m"
+  args @ rec_exec f args # 0 \<up> m"
 apply(case_tac n, simp_all add: exp_suc list_update_append list_update.simps del: replicate_Suc)
 apply(subgoal_tac "length args = Suc (length lm)", simp)
 apply(rule_tac x = "Suc (Suc 0)" in exI, simp)
@@ -2355,16 +2365,16 @@
 
 lemma compile_append_dummy_correct: 
   assumes compile: "rec_ci f = (ap, ary, fp)"
-  and termi: "terminates f args"
-  shows "{\<lambda> nl. nl = args} (ap [+] dummy_abc (length args)) {\<lambda> nl. (\<exists> m. nl = args @ rec_eval f args # 0\<up>m)}"
+  and termi: "terminate f args"
+  shows "{\<lambda> nl. nl = args} (ap [+] dummy_abc (length args)) {\<lambda> nl. (\<exists> m. nl = args @ rec_exec f args # 0\<up>m)}"
 proof(rule_tac abc_Hoare_plus_halt)
-  show "{\<lambda>nl. nl = args} ap {\<lambda> nl. abc_list_crsp (args @ [rec_eval f args]) nl}"
+  show "{\<lambda>nl. nl = args} ap {\<lambda> nl. abc_list_crsp (args @ [rec_exec f args]) nl}"
     using compile termi recursive_compile_correct_norm'[of f ap ary fp args]
     apply(auto simp: abc_Hoare_halt_def)
     by(rule_tac x = stp in exI, simp)
 next
-  show "{abc_list_crsp (args @ [rec_eval f args])} dummy_abc (length args) 
-    {\<lambda>nl. \<exists>m. nl = args @ rec_eval f args # 0 \<up> m}"
+  show "{abc_list_crsp (args @ [rec_exec f args])} dummy_abc (length args) 
+    {\<lambda>nl. \<exists>m. nl = args @ rec_exec f args # 0 \<up> m}"
     apply(auto simp: dummy_abc_def abc_Hoare_halt_def)
     apply(rule_tac x = 3 in exI)
     by(auto simp: abc_steps_l.simps abc_list_crsp_def abc_step_l.simps numeral_3_eq_3 abc_fetch.simps
@@ -2386,15 +2396,15 @@
   and compile2: "rec_ci (gs!i) = (gap, gar, gft) \<and> gar = length args"
   and g_unhalt: "\<And> anything. {\<lambda> nl. nl = args @ 0\<up>(gft - gar) @ anything} gap \<up>"
   and g_ind: "\<And> apj arj ftj j anything. \<lbrakk>j < i; rec_ci (gs!j) = (apj, arj, ftj)\<rbrakk> 
-  \<Longrightarrow> {\<lambda> nl. nl = args @ 0\<up>(ftj - arj) @ anything} apj {\<lambda> nl. nl = args @ rec_eval (gs!j) args # 0\<up>(ftj - Suc arj) @ anything}"
-  and all_termi: "\<forall> j<i. terminates (gs!j) args"
+  \<Longrightarrow> {\<lambda> nl. nl = args @ 0\<up>(ftj - arj) @ anything} apj {\<lambda> nl. nl = args @ rec_exec (gs!j) args # 0\<up>(ftj - Suc arj) @ anything}"
+  and all_termi: "\<forall> j<i. terminate (gs!j) args"
   shows "{\<lambda> nl. nl = args @ 0\<up>(ft - ar) @ anything} ap \<up>"
 using compile1
 apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_comp_commute)
 proof(rule_tac abc_Hoare_plus_unhalt1)
   fix fap far fft
   let ?ft = "max (Suc (length args)) (Max (insert fft ((\<lambda>(aprog, p, n). n) ` rec_ci ` set gs)))"
-  let ?Q = "\<lambda>nl. nl = args @ 0\<up> (?ft - length args) @ map (\<lambda>i. rec_eval i args) (take i gs) @ 
+  let ?Q = "\<lambda>nl. nl = args @ 0\<up> (?ft - length args) @ map (\<lambda>i. rec_exec i args) (take i gs) @ 
     0\<up>(length gs - i) @ 0\<up> Suc (length args) @ anything"
   have "cn_merge_gs (map rec_ci gs) ?ft = 
     cn_merge_gs (map rec_ci (take i gs)) ?ft [+] (gap [+] 
@@ -2403,11 +2413,11 @@
   thus "{\<lambda>nl. nl = args @ 0 # 0 \<up> (?ft + length gs) @ anything} (cn_merge_gs (map rec_ci gs) ?ft) \<up>"
   proof(simp, rule_tac abc_Hoare_plus_unhalt1, rule_tac abc_Hoare_plus_unhalt2, 
               rule_tac abc_Hoare_plus_unhalt1)
-    let ?Q_tmp = "\<lambda>nl. nl = args @ 0\<up> (gft - gar) @ 0\<up>(?ft - (length args) - (gft -gar)) @ map (\<lambda>i. rec_eval i args) (take i gs) @ 
+    let ?Q_tmp = "\<lambda>nl. nl = args @ 0\<up> (gft - gar) @ 0\<up>(?ft - (length args) - (gft -gar)) @ map (\<lambda>i. rec_exec i args) (take i gs) @ 
       0\<up>(length gs - i) @ 0\<up> Suc (length args) @ anything"
     have a: "{?Q_tmp} gap \<up>"
       using g_unhalt[of "0 \<up> (?ft - (length args) - (gft - gar)) @
-        map (\<lambda>i. rec_eval i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything"]
+        map (\<lambda>i. rec_exec i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything"]
       by simp
     moreover have "?ft \<ge> gft"
       using g compile2
@@ -2424,7 +2434,7 @@
     show "{\<lambda>nl. nl = args @ 0 # 0 \<up> (?ft + length gs) @ anything} 
       cn_merge_gs (map rec_ci (take i gs)) ?ft
        {\<lambda>nl. nl = args @ 0 \<up> (?ft - length args) @
-      map (\<lambda>i. rec_eval i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything}"
+      map (\<lambda>i. rec_exec i args) (take i gs) @ 0 \<up> (length gs - i) @ 0 \<up> Suc (length args) @ anything}"
       using all_termi
       apply(rule_tac compile_cn_gs_correct', auto simp: set_conv_nth)
       by(drule_tac apj = x and arj = xa and  ftj = xb and j = ia and anything = xc in g_ind, auto)
@@ -2435,7 +2445,7 @@
 
 lemma mn_unhalt_case':
   assumes compile: "rec_ci f = (a, b, c)"
-  and all_termi: "\<forall>i. terminates f (args @ [i]) \<and> 0 < rec_eval f (args @ [i])"
+  and all_termi: "\<forall>i. terminate f (args @ [i]) \<and> 0 < rec_exec f (args @ [i])"
   and B: "B = [Dec (Suc (length args)) (length a + 5), Dec (Suc (length args)) (length a + 3), 
   Goto (Suc (length a)), Inc (length args), Goto 0]"
   shows "{\<lambda>nl. nl = args @ 0 \<up> (max (Suc (length args)) c - length args) @ anything}
@@ -2455,7 +2465,7 @@
   proof(rule_tac mn_loop_correct', auto)
     fix i xc
     show "{\<lambda>nl. nl = args @ i # 0 \<up> (c - Suc (length args)) @ xc} a 
-      {\<lambda>nl. nl = args @ i # rec_eval f (args @ [i]) # 0 \<up> (c - Suc (Suc (length args))) @ xc}"
+      {\<lambda>nl. nl = args @ i # rec_exec f (args @ [i]) # 0 \<up> (c - Suc (Suc (length args))) @ xc}"
       using all_termi recursive_compile_correct[of f "args @ [i]" a b c xc] compile a
       by(simp)
   qed
@@ -2477,7 +2487,7 @@
     
 lemma mn_unhalt_case: 
   assumes compile: "rec_ci (Mn n f) = (ap, ar, ft) \<and> length args = ar"
-  and all_term: "\<forall> i. terminates f (args @ [i]) \<and> rec_eval f (args @ [i]) > 0"
+  and all_term: "\<forall> i. terminate f (args @ [i]) \<and> rec_exec f (args @ [i]) > 0"
   shows "{\<lambda> nl. nl = args @ 0\<up>(ft - ar) @ anything} ap \<up> "
   using assms
 apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_comp_commute)
@@ -2490,34 +2500,34 @@
 
 lemma recursive_compile_to_tm_correct1: 
   assumes  compile: "rec_ci recf = (ap, ary, fp)"
-  and termi: " terminates recf args"
+  and termi: " terminate recf args"
   and tp: "tp = tm_of (ap [+] dummy_abc (length args))"
   shows "\<exists> stp m l. steps0 (Suc 0, Bk # Bk # ires, <args> @ Bk\<up>rn)
-  (tp @ shift (mopup (length args)) (length tp div 2)) stp = (0, Bk\<up>m @ Bk # Bk # ires, Oc\<up>Suc (rec_eval recf args) @ Bk\<up>l)"
+  (tp @ shift (mopup (length args)) (length tp div 2)) stp = (0, Bk\<up>m @ Bk # Bk # ires, Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)"
 proof -
-  have "{\<lambda>nl. nl = args} ap [+] dummy_abc (length args) {\<lambda>nl. \<exists>m. nl = args @ rec_eval recf args # 0 \<up> m}"
+  have "{\<lambda>nl. nl = args} ap [+] dummy_abc (length args) {\<lambda>nl. \<exists>m. nl = args @ rec_exec recf args # 0 \<up> m}"
     using compile termi compile
     by(rule_tac compile_append_dummy_correct, auto)
   then obtain stp m where h: "abc_steps_l (0, args) (ap [+] dummy_abc (length args)) stp = 
-    (length (ap [+] dummy_abc (length args)), args @ rec_eval recf args # 0\<up>m) "
+    (length (ap [+] dummy_abc (length args)), args @ rec_exec recf args # 0\<up>m) "
     apply(simp add: abc_Hoare_halt_def, auto)
     by(case_tac "abc_steps_l (0, args) (ap [+] dummy_abc (length args)) n", auto)
   thus "?thesis"
     using assms tp
-    by(rule_tac  lm = args and stp = stp and am = "args @ rec_eval recf args # 0 \<up> m"
+    by(rule_tac  lm = args and stp = stp and am = "args @ rec_exec recf args # 0 \<up> m"
       in compile_correct_halt, auto simp: crsp.simps start_of.simps length_abc_comp abc_lm_v.simps)
 qed
 
 lemma recursive_compile_to_tm_correct2: 
-  assumes termi: " terminates recf args"
+  assumes termi: " terminate recf args"
   shows "\<exists> stp m l. steps0 (Suc 0, [Bk, Bk], <args>) (tm_of_rec recf) stp = 
-                     (0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_eval recf args) @ Bk\<up>l)"
+                     (0, Bk\<up>Suc (Suc m), Oc\<up>Suc (rec_exec recf args) @ Bk\<up>l)"
 proof(case_tac "rec_ci recf", simp add: tm_of_rec.simps)
   fix ap ar fp
   assume "rec_ci recf = (ap, ar, fp)"
   thus "\<exists>stp m l. steps0 (Suc 0, [Bk, Bk], <args>) 
     (tm_of (ap [+] dummy_abc ar) @ shift (mopup ar) (listsum (layout_of (ap [+] dummy_abc ar)))) stp =
-    (0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_eval recf args @ Bk \<up> l)"
+    (0, Bk # Bk # Bk \<up> m, Oc # Oc \<up> rec_exec recf args @ Bk \<up> l)"
     using recursive_compile_to_tm_correct1[of recf ap ar fp args "tm_of (ap [+] dummy_abc (length args))" "[]" 0]
       assms param_pattern[of recf args ap ar fp]
     by(simp add: replicate_Suc[THEN sym] replicate_Suc_iff_anywhere del: replicate_Suc tm_of_rec_def, 
@@ -2525,9 +2535,9 @@
 qed
 
 lemma recursive_compile_to_tm_correct3: 
-  assumes termi: "terminates recf args"
+  assumes termi: "terminate recf args"
   shows "{\<lambda> tp. tp =([Bk, Bk], <args>)} (tm_of_rec recf) 
-         {\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_eval recf args> @ Bk \<up> l)}"
+         {\<lambda> tp. \<exists> k l. tp = (Bk\<up> k, <rec_exec recf args> @ Bk \<up> l)}"
 using recursive_compile_to_tm_correct2[OF assms]
 apply(auto simp add: Hoare_halt_def)
 apply(rule_tac x = stp in exI)