equal
deleted
inserted
replaced
52 qed |
52 qed |
53 qed |
53 qed |
54 |
54 |
55 text {* The other direction! *} |
55 text {* The other direction! *} |
56 |
56 |
57 inductive_cases [elim!]: "(([],p,s),next) : stepa1" |
57 inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1" |
58 |
58 |
59 lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)" |
59 lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)" |
60 apply(rule iffI) |
60 apply(rule iffI) |
61 apply(erule converse_rel_powE, simp, fast) |
61 apply(erule converse_rel_powE, simp, fast) |
62 apply simp |
62 apply simp |