equal
deleted
inserted
replaced
7 refl: "star r x x" | |
7 refl: "star r x x" | |
8 step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
8 step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
9 |
9 |
10 lemma star_trans: |
10 lemma star_trans: |
11 "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
11 "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
12 proof(induct rule: star.induct) |
12 proof(induction rule: star.induct) |
13 case refl thus ?case . |
13 case refl thus ?case . |
14 next |
14 next |
15 case step thus ?case by (metis star.step) |
15 case step thus ?case by (metis star.step) |
16 qed |
16 qed |
17 |
17 |