4948 "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" |
4948 "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')" |
4949 using h |
4949 using h |
4950 by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto) |
4950 by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto) |
4951 |
4951 |
4952 then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)" |
4952 then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)" |
4953 by(auto intro: is_final_steps) |
4953 by(auto intro: after_is_final) |
4954 then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)" |
4954 then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)" |
4955 using e |
4955 using e |
4956 by(simp add: steps_add f) |
4956 by(simp add: steps_add f) |
4957 from this and c d show "False" by simp |
4957 from this and c d show "False" by simp |
4958 qed |
4958 qed |