Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
walk_inductions.pvs
Sprache: PVS
|
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
[ zur Elbe Produktseite wechseln0.18Quellennavigators
Analyse erneut starten
]
|
|
