equal
deleted
inserted
replaced
289 fun Std :: "nat \<Rightarrow> bool" |
289 fun Std :: "nat \<Rightarrow> bool" |
290 where |
290 where |
291 "Std cf = (left_std (Left cf) \<and> right_std (Right cf))" |
291 "Std cf = (left_std (Left cf) \<and> right_std (Right cf))" |
292 |
292 |
293 text{* |
293 text{* |
294 @{text "Nostop m cf k"} means that afer @{text k} steps of |
294 @{text "Stop m cf k"} means that afer @{text k} steps of |
295 execution the TM coded by @{text m} and started in configuration |
295 execution the TM coded by @{text m} and started in configuration |
296 @{text cf} is not at a stardard final configuration. *} |
296 @{text cf} is in a stardard final configuration. *} |
297 |
297 |
298 fun Final :: "nat \<Rightarrow> bool" |
298 fun Final :: "nat \<Rightarrow> bool" |
299 where |
299 where |
300 "Final cf = (State cf = 0)" |
300 "Final cf = (State cf = 0)" |
301 |
301 |