equal
deleted
inserted
replaced
13 "update2 p a \<equiv> update a p" |
13 "update2 p a \<equiv> update a p" |
14 |
14 |
15 consts DUMMY::'a |
15 consts DUMMY::'a |
16 |
16 |
17 notation (latex output) |
17 notation (latex output) |
18 Cons ("_::_" [78,77] 73) and |
18 Cons ("_::_" [48,47] 48) and |
19 set ("") and |
19 set ("") and |
20 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
20 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
21 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
21 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
22 update2 ("update") and |
22 update2 ("update") and |
23 tm_wf0 ("wf") and |
23 tm_wf0 ("wf") and |
897 @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\ |
897 @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\ |
898 & & @{thm (rhs) inv_begin02} \\ |
898 & & @{thm (rhs) inv_begin02} \\ |
899 @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ |
899 @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ |
900 @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\ |
900 @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\ |
901 @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\ |
901 @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\ |
902 @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps} |
902 @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\ |
|
903 @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\ |
|
904 & & @{thm (rhs) inv_loop1_exit.simps}\\ |
|
905 @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}\\ |
903 \end{tabular} |
906 \end{tabular} |
904 \end{center} |
907 \end{center} |
905 \caption{The invariants for each state of @{term tcopy_begin}. They depend on |
908 \caption{The invariants for each state of @{term tcopy_begin}. They depend on |
906 the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin} |
909 the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin} |
907 \end{figure} |
910 \end{figure} |