| changeset 12815 | 1f073030b97a |
| parent 11494 | 23a118849801 |
| child 17914 | 99ead7a7eb42 |
| 12814:2f5edb146f7e | 12815:1f073030b97a |
|---|---|
165 *} |
165 *} |
166 (*<*) |
166 (*<*) |
167 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*" |
167 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*" |
168 apply(erule rtc.induct); |
168 apply(erule rtc.induct); |
169 apply blast; |
169 apply blast; |
170 apply(blast intro:rtc_step) |
170 apply(blast intro: rtc_step) |
171 done |
171 done |
172 |
172 |
173 end |
173 end |
174 (*>*) |
174 (*>*) |