equal
deleted
inserted
replaced
694 where |
694 where |
695 "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)" |
695 "inv_end1 x (l, r) = (x > 0 \<and> l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x)" |
696 |
696 |
697 fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
697 fun inv_end2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
698 where |
698 where |
699 "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>)" |
699 "inv_end2 x (l, r) = (\<exists> i j. i + j = Suc x \<and> x > 0 \<and> l = Oc\<up>i @ [Bk] \<and> r = Bk\<up>j @ Oc\<up>x)" |
700 |
700 |
701 fun inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
701 fun inv_end3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" |
702 where |
702 where |
703 "inv_end3 x (l, r) = |
703 "inv_end3 x (l, r) = |
704 (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x )" |
704 (\<exists> i j. x > 0 \<and> i + j = x \<and> l = Oc\<up>i @ [Bk] \<and> r = Oc # Bk\<up>j@ Oc\<up>x )" |