inductive
star :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" for r where
refl: "star r x x" |
step: "r x y \ star r y z \ star r x z"
hide_fact (open) refl step \<comment> \<open>names too generic\<close>
lemma star_trans: "star r x y \ star r y z \ star r x z" proof(induction rule: star.induct) case refl thus ?case . next case step thus ?caseby (metis star.step) qed
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
