|
walk_inductions[T: TYPE]: THEORY
BEGIN
IMPORTING walks[T]
P: VAR pred[prewalk]
n: VAR nat
w,ww: VAR prewalk
walk_prep : LEMMA (FORALL w: P(w)) IFF
(FORALL n, w : length(w) = n IMPLIES P(w))
graph_induction_walk : THEOREM (FORALL w:
(FORALL ww: length(ww) < length(w) IMPLIES P(ww))
IMPLIES P(w))
IMPLIES (FORALL w: P(w))
END walk_inductions
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
