--- a/Tests/Rec_def2.thy	Wed Mar 27 09:47:02 2013 +0000
+++ b/Tests/Rec_def2.thy	Wed Mar 27 13:16:37 2013 +0000
@@ -9,6 +9,10 @@
               |  Pr nat recf recf
               |  Mn nat recf 
 
+definition pred_of_nl :: "nat list \<Rightarrow> nat list"
+  where
+  "pred_of_nl xs = butlast xs @ [last xs - 1]"
+
 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
   where
   "rec_exec z xs = 0" |
@@ -17,13 +21,13 @@
   "rec_exec (Cn n f gs) xs = 
      rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | 
   "rec_exec (Pr n f g) xs = 
-     (if hd xs = 0 then rec_exec f (tl xs)
-      else rec_exec g ((hd xs - 1) # (rec_exec (Pr n f g) ((hd xs - 1) # tl xs)) # tl xs))" |
-  "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (x # xs) = 0)"
+     (if last xs = 0 then rec_exec f (butlast xs)
+      else rec_exec g (butlast xs @ (last xs - 1) # [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" |
+  "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"
 by pat_completeness auto
 
 termination
-apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). hd xs)]")
+apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]")
 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
 done
 
@@ -34,11 +38,11 @@
 | termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs"
 | termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); 
               \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs"
-| termi_pr_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)"
-| termi_pr_suc: "\<lbrakk>terminate (Pr n f gs) (x # xs); length xs = n;
-                  terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> 
-                  \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)"
-| termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0;
-              \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
+| termi_pr: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
+              terminate f xs;
+              length xs = n\<rbrakk> 
+              \<Longrightarrow> terminate (Pr n f g) (xs @ [x])"
+| termi_mn: "\<lbrakk>length xs = n; rec_exec f (xs @ [r]) = 0;
+              \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
 
 end
\ No newline at end of file