--- a/Paper.thy	Sat Jan 12 01:05:01 2013 +0000
+++ b/Paper.thy	Sat Jan 12 01:33:20 2013 +0000
@@ -71,6 +71,14 @@
 apply(auto simp add: tshift.simps)
 done
 
+lemma change_termi_state_def2:
+ "change_termi_state p  == 
+  (map (\<lambda> (a, s). (a, if s = 0 then Suc ((length s) div 2)) else s) t)"
+apply(rule eq_reflection)
+apply(auto simp add: change_termi_state.simps)
+done
+
+
 
 consts DUMMY::'a
 
@@ -85,7 +93,7 @@
   abc_lm_v ("lookup") and
   abc_lm_s ("set") and
   haltP ("stdhalt") and 
-  change-termi-state ("adjust") and
+  change_termi_state ("adjust") and
   tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 
   DUMMY  ("\<^raw:\mbox{$\_$}>")