equal
deleted
inserted
replaced
86 with inst |
86 with inst |
87 have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti) |
87 have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti) |
88 also |
88 also |
89 from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp |
89 from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp |
90 with cert_in_A step_in_A |
90 with cert_in_A step_in_A |
91 have "?merge = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++_f (c!(pc+1)))" |
91 have "?merge = (map snd [(p',t') \<leftarrow> ?step pc. p'=pc+1] ++_f (c!(pc+1)))" |
92 by (rule merge_not_top_s) |
92 by (rule merge_not_top_s) |
93 finally |
93 finally |
94 have "s' <=_r ?s2" using step_in_A cert_in_A True step |
94 have "s' <=_r ?s2" using step_in_A cert_in_A True step |
95 by (auto intro: pp_ub1') |
95 by (auto intro: pp_ub1') |
96 also |
96 also |