|
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.21 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
