Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


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  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik