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 🍋‹names too generic›
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
lemma star_step1[simp, intro]: "r x y ==> star r x y" by(metis star.refl star.step)
code_pred star .
end
Messung V0.5 in Prozent
¤ 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.0.10Bemerkung:
(vorverarbeitet am 2026-04-26)
¤
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 und die Messung sind noch experimentell.
