diff -r 1bad3ec5bcd5 -r 9510e5131e06 thys/Recursive.thy
--- a/thys/Recursive.thy	Thu Feb 14 12:11:40 2013 +0000
+++ b/thys/Recursive.thy	Fri Feb 15 07:42:47 2013 +0000
@@ -1146,8 +1146,8 @@
          [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @ 
          [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
 apply(simp add: rec_ci.simps)
-apply(rule_tac x = "Recursive.mv_box n (max (Suc (Suc (Suc n)))
-    (max bc ba)) [+] ab [+] Recursive.mv_box n (Suc n)" in exI,
+apply(rule_tac x = "mv_box n (max (Suc (Suc (Suc n)))
+    (max bc ba)) [+] ab [+] mv_box n (Suc n)" in exI,
      simp)
 apply(auto simp add: abc_append_commute numeral_3_eq_3)
 done
@@ -1357,20 +1357,20 @@
       rule_tac x = "initlm ! n" in exI, simp)
 done
 
-lemma [simp]: "abc_fetch 0 (Recursive.mv_box m n) = Some (Dec m 3)"
+lemma [simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
 apply(simp add: mv_box.simps abc_fetch.simps)
 done
 
-lemma [simp]: "abc_fetch (Suc 0) (Recursive.mv_box m n) =
+lemma [simp]: "abc_fetch (Suc 0) (mv_box m n) =
                Some (Inc n)"
 apply(simp add: mv_box.simps abc_fetch.simps)
 done
 
-lemma [simp]: "abc_fetch 2 (Recursive.mv_box m n) = Some (Goto 0)"
+lemma [simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
 apply(simp add: mv_box.simps abc_fetch.simps)
 done
 
-lemma [simp]: "abc_fetch 3 (Recursive.mv_box m n) = None"
+lemma [simp]: "abc_fetch 3 (mv_box m n) = None"
 apply(simp add: mv_box.simps abc_fetch.simps)
 done
 
@@ -1405,15 +1405,15 @@
 lemma [simp]: 
   "\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> 
    \<forall>na. \<not> (\<lambda>(as, lm) m. as = 3) 
-    (abc_steps_l (0, initlm) (Recursive.mv_box m n) na) m \<and> 
+    (abc_steps_l (0, initlm) (mv_box m n) na) m \<and> 
   mv_box_inv (abc_steps_l (0, initlm) 
-           (Recursive.mv_box m n) na) m n initlm \<longrightarrow>
+           (mv_box m n) na) m n initlm \<longrightarrow>
   mv_box_inv (abc_steps_l (0, initlm) 
-           (Recursive.mv_box m n) (Suc na)) m n initlm \<and>
-  ((abc_steps_l (0, initlm) (Recursive.mv_box m n) (Suc na), m),
-   abc_steps_l (0, initlm) (Recursive.mv_box m n) na, m) \<in> mv_box_LE"
+           (mv_box m n) (Suc na)) m n initlm \<and>
+  ((abc_steps_l (0, initlm) (mv_box m n) (Suc na), m),
+   abc_steps_l (0, initlm) (mv_box m n) na, m) \<in> mv_box_LE"
 apply(rule allI, rule impI, simp add: abc_steps_ind)
-apply(case_tac "(abc_steps_l (0, initlm) (Recursive.mv_box m n) na)",
+apply(case_tac "(abc_steps_l (0, initlm) (mv_box m n) na)",
       simp)
 apply(auto split:if_splits simp add:abc_steps_l.simps mv_box_inv.simps)
 apply(auto simp add: mv_box_LE_def lex_triple_def lex_pair_def 
@@ -1430,14 +1430,14 @@
              (abc_steps_l (0::nat, initlm) (mv_box m n) stp)"
 apply(insert halt_lemma2[of mv_box_LE
     "\<lambda> ((as, lm), m). mv_box_inv (as, lm) m n initlm"
-    "\<lambda> stp. (abc_steps_l (0, initlm) (Recursive.mv_box m n) stp, m)"
+    "\<lambda> stp. (abc_steps_l (0, initlm) (mv_box m n) stp, m)"
     "\<lambda> ((as, lm), m). as = (3::nat)"
     ])
 apply(insert wf_mv_box_le)
 apply(simp add: mv_box_inv_init abc_steps_zero)
 apply(erule_tac exE)
 apply(rule_tac x = na in exI)
-apply(case_tac "(abc_steps_l (0, initlm) (Recursive.mv_box m n) na)",
+apply(case_tac "(abc_steps_l (0, initlm) (mv_box m n) na)",
       simp, auto)
 done
 
@@ -1454,7 +1454,7 @@
   = (3, (lm[n := (lm ! m + lm ! n)])[m := 0::nat])"
 apply(drule mv_box_inv_halt, simp, erule_tac exE)
 apply(rule_tac x = stp in exI)
-apply(case_tac "abc_steps_l (0, lm) (Recursive.mv_box m n) stp",
+apply(case_tac "abc_steps_l (0, lm) (mv_box m n) stp",
       simp)
 apply(erule_tac mv_box_halt_cond, auto)
 done
@@ -1510,7 +1510,7 @@
   \<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and> 
          ap = mv_box n (max (Suc (Suc (Suc n))) (max bc ba))"
 apply(simp add: rec_ci.simps)
-apply(rule_tac x = "(ab [+] (Recursive.mv_box n (Suc n) [+]
+apply(rule_tac x = "(ab [+] (mv_box n (Suc n) [+]
               ([Dec (max (n + 3) (max bc ba)) (length a + 7)] 
       [+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @ 
       [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI, auto)
@@ -1615,10 +1615,10 @@
 
 lemma pr_prog_ex[simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 
       rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>
-    \<Longrightarrow> \<exists>cp. aprog = Recursive.mv_box n (max (n + 3) 
+    \<Longrightarrow> \<exists>cp. aprog = mv_box n (max (n + 3) 
                     (max bc ba)) [+] cp"
 apply(simp add: rec_ci.simps)
-apply(rule_tac x = "(ab [+] (Recursive.mv_box n (Suc n) [+]
+apply(rule_tac x = "(ab [+] (mv_box n (Suc n) [+]
               ([Dec (max (n + 3) (max bc ba)) (length a + 7)] 
              [+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]))
              @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI)
@@ -1639,7 +1639,7 @@
 apply(case_tac "rec_ci g", simp add: rec_ci.simps)
 apply(rule_tac x = "mv_box n 
               (max (n + 3) (max bc c))" in exI, simp)
-apply(rule_tac x = "Recursive.mv_box n (Suc n) [+]
+apply(rule_tac x = "mv_box n (Suc n) [+]
                  ([Dec (max (n + 3) (max bc c)) (length a + 7)]
                  [+] a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])
                @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI, 
@@ -1651,10 +1651,10 @@
   "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
     rec_ci g = (a, aa, ba); 
     rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> 
-    \<exists>ap. (\<exists>cp. aprog = ap [+] Recursive.mv_box n (Suc n) [+] cp)
+    \<exists>ap. (\<exists>cp. aprog = ap [+] mv_box n (Suc n) [+] cp)
       \<and> length ap = 3 + length ab"
 apply(simp add: rec_ci.simps)
-apply(rule_tac x = "Recursive.mv_box n (max (n + 3)
+apply(rule_tac x = "mv_box n (max (n + 3)
                                 (max bc ba)) [+] ab" in exI, simp)
 apply(rule_tac x = "([Dec (max (n + 3) (max bc ba))
   (length a + 7)] [+] a [+] 
@@ -1673,9 +1673,9 @@
              Goto (length a + 4)] [+] cp) \<and>
              length ap = 6 + length ab"
 apply(simp add: rec_ci.simps)
-apply(rule_tac x = "Recursive.mv_box n
+apply(rule_tac x = "mv_box n
     (max (n + 3) (max bc ba)) [+] ab [+] 
-     Recursive.mv_box n (Suc n)" in exI, simp)
+     mv_box n (Suc n)" in exI, simp)
 apply(rule_tac x = "[]" in exI, auto)
 apply(simp add: abc_append_commute)
 done
@@ -1751,7 +1751,7 @@
       apply(erule_tac exE, erule_tac exE, simp)
       apply(subgoal_tac 
            "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm)
-              ([] [+] Recursive.mv_box n
+              ([] [+] mv_box n
                   (max (n + 3) (max bc ba)) [+] cp) stp =
              (0 + 3, butlast lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ 
                                         last lm # suf_lm)", simp)
@@ -1817,21 +1817,21 @@
                        0\<up>(a_md - rs_pos - 2) @ last lm # suf_lm)"
       proof -	     
 	from h have "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
-          length ap = 3 + length ab \<and> bp = Recursive.mv_box n (Suc n)"
+          length ap = 3 + length ab \<and> bp = mv_box n (Suc n)"
 	  by auto
 	thus "?thesis"
 	proof(erule_tac exE, erule_tac exE, erule_tac exE, 
               erule_tac exE)
 	  fix ap cp bp apa
 	  assume "aprog = ap [+] bp [+] cp \<and> length ap = 3 + 
-                    length ab \<and> bp = Recursive.mv_box n (Suc n)"
+                    length ab \<and> bp = mv_box n (Suc n)"
 	  thus "?thesis"
 	    apply(simp del: abc_append_commute)
 	    apply(subgoal_tac 
               "\<exists>stp. abc_steps_l (3 + length ab, 
                butlast lm @ rsa # 0\<up>(a_md - Suc rs_pos) @
                  last lm # suf_lm) (ap [+] 
-                   Recursive.mv_box n (Suc n) [+] cp) stp =
+                   mv_box n (Suc n) [+] cp) stp =
               ((3 + length ab) + 3, butlast lm @ 0 # rsa # 
                   0\<up>(a_md - Suc (Suc rs_pos)) @ last lm # suf_lm)", simp)
 	    apply(rule_tac abc_append_exc1, simp_all)
@@ -2811,7 +2811,7 @@
     from h show 
       "\<exists>bstp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ butlast ys @ 
                                   0\<up>(a_md - (pstr + length list)) @ suf_lm) 
-              ((\<lambda>(gprog, gpara, gn). gprog [+] Recursive.mv_box gpara 
+              ((\<lambda>(gprog, gpara, gn). gprog [+] mv_box gpara 
               (pstr + length list)) (rec_ci a)) bstp =
               ((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3, 
              lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
@@ -2850,7 +2850,7 @@
       from h and this show     
       "\<exists>bstp. abc_steps_l (0, lm @ ys ! length list #
           0\<up>(pstr - Suc n) @ butlast ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm)
-                 (Recursive.mv_box b (pstr + length list)) bstp =
+                 (mv_box b (pstr + length list)) bstp =
        (3, lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
 	apply(insert mv_box_ex [of b "pstr + length list" 
          "lm @ ys ! length list # 0\<up>(pstr - Suc n) @ butlast ys @ 
@@ -2862,7 +2862,7 @@
 	done
     next
       fix aa b c
-      show "3 = length (Recursive.mv_box b (pstr + length list))" 
+      show "3 = length (mv_box b (pstr + length list))" 
         by simp
     next
       fix aa b aaa ba
@@ -2875,7 +2875,7 @@
   next
     show "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3 = 
         length ((\<lambda>(gprog, gpara, gn). gprog [+]
-           Recursive.mv_box gpara (pstr + length list)) (rec_ci a))"
+           mv_box gpara (pstr + length list)) (rec_ci a))"
       by(case_tac "rec_ci a", simp)
   next
     show "listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
@@ -2884,7 +2884,7 @@
                 ((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3)" by simp
   next
     show "(\<lambda>(gprog, gpara, gn). gprog [+] 
-      Recursive.mv_box gpara (pstr + length list)) (rec_ci a) \<noteq> []"
+      mv_box gpara (pstr + length list)) (rec_ci a) \<noteq> []"
       by(case_tac "rec_ci a", 
          simp add: abc_append.simps abc_shift.simps)
   qed
@@ -2983,7 +2983,7 @@
             "length (lm3::nat list) = ba - Suc (aa + n)"
   thus " \<exists>bstp. abc_steps_l (0, lm1 @ 0\<up>n @ last lm2 # lm3 @
                        butlast lm2 @ 0 # lm4) 
-                         (Recursive.mv_box (aa + n) (ba + n)) bstp
+                         (mv_box (aa + n) (ba + n)) bstp
                = (3, lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4)"
     apply(insert mv_box_ex[of "aa + n" "ba + n" 
        "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp)
@@ -3065,7 +3065,7 @@
   thus
     "\<exists>bstp. abc_steps_l (0, lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ 
                                last lm3 # lm4) 
-           (Recursive.mv_box (aa + n) (ba + n)) bstp =
+           (mv_box (aa + n) (ba + n)) bstp =
                  (3, lm1 @ lm3 @ lm2 @ 0 # 0\<up>n @ lm4)"
     apply(insert mv_box_ex[of "aa + n" "ba + n" "lm1 @ butlast lm3 @ 
                           0 # lm2 @ 0\<up>n @ last lm3 # lm4"], simp)
@@ -3133,9 +3133,9 @@
       simp add: cn_merge_gs_len)
 apply(rule_tac x = 
   "mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
-   0 (length gs) [+] a [+]Recursive.mv_box aa (max (Suc n) 
+   0 (length gs) [+] a [+]mv_box aa (max (Suc n) 
    (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
-   empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n) 
+   empty_boxes (length gs) [+] mv_box (max (Suc n) 
   (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
    mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) 
    ` set gs))) + length gs)) 0 n" in exI, auto)
@@ -3218,9 +3218,9 @@
    (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+]
    mv_boxes (max (Suc n) (Max (insert ba 
   (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
-   a [+] Recursive.mv_box aa (max (Suc n)
+   a [+] mv_box aa (max (Suc n)
     (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
-   empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n)
+   empty_boxes (length gs) [+] mv_box (max (Suc n)
     (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
     mv_boxes (Suc (max (Suc n) (Max 
     (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n"
@@ -3332,9 +3332,9 @@
            (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n" in exI, 
        simp add: cn_merge_gs_len)
 apply(rule_tac x = "a [+]
-     Recursive.mv_box aa (max (Suc n) (Max (insert ba 
+     mv_box aa (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
-     empty_boxes (length gs) [+] Recursive.mv_box 
+     empty_boxes (length gs) [+] mv_box 
      (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n
       [+] mv_boxes (Suc (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
@@ -3423,9 +3423,9 @@
      mv_boxes (max (Suc n) (Max (insert ba 
       (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs)" in exI,
      simp add: cn_merge_gs_len)
-apply(rule_tac x = "Recursive.mv_box aa (max (Suc n) (Max (insert ba 
+apply(rule_tac x = "mv_box aa (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
-     empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n) (
+     empty_boxes (length gs) [+] mv_box (max (Suc n) (
      Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
      mv_boxes (Suc (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
@@ -3523,7 +3523,7 @@
   "\<lbrakk>pstr > length ys\<rbrakk>
   \<Longrightarrow> \<exists>stp. abc_steps_l (0, ys @ rs # 0\<up>pstr @ lm @ 
   0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) 
-  (Recursive.mv_box (length ys) pstr) stp =
+  (mv_box (length ys) pstr) stp =
   (3, ys @ 0\<up>(pstr - (length ys)) @ rs # 
   0\<up>length ys  @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
 apply(insert mv_box_ex[of "length ys" pstr 
@@ -3552,7 +3552,7 @@
   in exI, simp add: cn_merge_gs_len)
 apply(rule_tac x = 
   "empty_boxes (length gs) [+]
-   Recursive.mv_box (max (Suc n) (Max (insert ba 
+   mv_box (max (Suc n) (Max (insert ba 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
    mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))
     + length gs)) 0 n" in exI, 
@@ -3599,7 +3599,7 @@
     fix ap bp apa cp
     assume "aprog = ap [+] bp [+] cp \<and> length ap = 
       (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 
-      3 * n + length a \<and> bp = Recursive.mv_box (length ys) pstr"
+      3 * n + length a \<and> bp = mv_box (length ys) pstr"
     thus"?thesis"
       apply(simp, rule_tac abc_append_exc1, simp_all)
       apply(rule_tac save_rs', insert h)
@@ -3674,10 +3674,10 @@
      (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n
     [+] mv_boxes (max (Suc n) (Max (insert ba 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
-     a [+] Recursive.mv_box aa (max (Suc n) 
+     a [+] mv_box aa (max (Suc n) 
    (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))" 
     in exI, simp add: cn_merge_gs_len)
-apply(rule_tac x = " Recursive.mv_box (max (Suc n) (Max (insert ba
+apply(rule_tac x = " mv_box (max (Suc n) (Max (insert ba
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
      mv_boxes (Suc (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, 
@@ -3755,7 +3755,7 @@
         \<circ> rec_ci) ` set gs))) + length gs)) n [+]
      mv_boxes (max (Suc n) (Max (insert ba 
       (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
-     a [+] Recursive.mv_box aa (max (Suc n)
+     a [+] mv_box aa (max (Suc n)
        (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
      empty_boxes (length gs)" in exI, simp add: cn_merge_gs_len)
 apply(rule_tac x = "mv_boxes (Suc (max (Suc n) 
@@ -3798,7 +3798,7 @@
  proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
    fix ap bp apa cp
    assume "aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> 
-                                 bp = Recursive.mv_box pstr n"
+                                 bp = mv_box pstr n"
    thus"?thesis"
      apply(simp, rule_tac abc_append_exc1, simp_all add: starts h)
      apply(insert mv_box_ex[of pstr n "0\<up>pstr @ rs # 0\<up>length gs @
@@ -3834,10 +3834,10 @@
        (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) 
      + length gs)) n [+] mv_boxes (max (Suc n) 
     (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
-     a [+] Recursive.mv_box aa (max (Suc n) 
+     a [+] mv_box aa (max (Suc n) 
       (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
      empty_boxes (length gs) [+]
-     Recursive.mv_box (max (Suc n) (Max (insert ba 
+     mv_box (max (Suc n) (Max (insert ba 
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n" in exI, simp add: cn_merge_gs_len)
 apply(rule_tac x = "[]" in exI, auto simp: abc_append_commute)
 done
@@ -4383,9 +4383,9 @@
      (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) +
       length gs)) n [+] mv_boxes (max (Suc n) (Max (insert c 
       (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
-      a [+] Recursive.mv_box b (max (Suc n) 
+      a [+] mv_box b (max (Suc n) 
       (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
-     empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n) 
+     empty_boxes (length gs) [+] mv_box (max (Suc n) 
       (Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
       mv_boxes (Suc (max (Suc n) (Max (insert c 
     (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI)