equal
deleted
inserted
replaced
113 s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> |
113 s2 -e2\<succ>v2-max (max n1 n2) n3\<rightarrow> t2 \<and> |
114 s3 -c -max (max n1 n2) n3\<rightarrow> t3" |
114 s3 -c -max (max n1 n2) n3\<rightarrow> t3" |
115 apply (drule (1) eval_eval_max, erule thin_rl) |
115 apply (drule (1) eval_eval_max, erule thin_rl) |
116 by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2) |
116 by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2) |
117 |
117 |
118 lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body M-n\<rightarrow> t)" |
118 lemma Impl_body_eq: "(\<lambda>t. \<exists>n. Z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. Z -body M-n\<rightarrow> t)" |
119 apply (rule ext) |
119 apply (rule ext) |
120 apply (fast elim: exec_elim_cases intro: exec_eval.Impl) |
120 apply (fast elim: exec_elim_cases intro: exec_eval.Impl) |
121 done |
121 done |
122 |
122 |
123 end |
123 end |