6316 (t_steps (Suc 0, b, c) |
6316 (t_steps (Suc 0, b, c) |
6317 (mop_bef n @ tshift mp_up (2 * n), 0) stp)" |
6317 (mop_bef n @ tshift mp_up (2 * n), 0) stp)" |
6318 apply(rule_tac mopup_halt_bef, auto) |
6318 apply(rule_tac mopup_halt_bef, auto) |
6319 done |
6319 done |
6320 from h1 and h2 and h3 show |
6320 from h1 and h2 and h3 show |
6321 "\<exists>stp. case t_steps tc (tm_of aprog @ abacus.tshift (mop_bef n @ abacus.tshift mp_up (2 * n)) |
6321 "\<exists>stp. case t_steps tc (tm_of aprog @ tshift (mop_bef n @ tshift mp_up (2 * n)) |
6322 (start_of (layout_of aprog) (length aprog) - Suc 0), 0) stp of (s, ab) |
6322 (start_of (layout_of aprog) (length aprog) - Suc 0), 0) stp of (s, ab) |
6323 \<Rightarrow> s = 0 \<and> mopup_inv (0, ab) am n ires" |
6323 \<Rightarrow> s = 0 \<and> mopup_inv (0, ab) am n ires" |
6324 proof(erule_tac exE, |
6324 proof(erule_tac exE, |
6325 case_tac "(t_steps (Suc 0, b, c) |
6325 case_tac "(t_steps (Suc 0, b, c) |
6326 (mop_bef n @ tshift mp_up (2 * n), 0) stpa)", simp, |
6326 (mop_bef n @ tshift mp_up (2 * n), 0) stpa)", simp, |