172   tm_wf :: "tprog \<Rightarrow> bool"

   172   tm_wf :: "tprog \<Rightarrow> bool"

   173 where

   173 where

   174   "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> 

   174   "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> 

   175                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"

   175                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"

   176 

   176 

   177 lemma halt_lemma: 

   181 lemma halt_lemma: 

   178   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"

   182   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"

   179 by (metis wf_iff_no_infinite_down_chain)

   183 by (metis wf_iff_no_infinite_down_chain)

   180 

   184 

   181 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)

   185 abbreviation exponent :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" ("_ \<up> _" [100, 99] 100)