products/sources/formale Sprachen/PVS/graphs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: min_walk_reduced.pvs   Sprache: PVS

Original von: PVS©
min_walk_reduced[T: TYPE]: THEORY

BEGIN

   IMPORTING min_walks[T], path_ops[T]

   reduced?(G: graph[T], w: Seq(G)): bool = 
          (FORALL (k: nat): k > 0 AND k < length(w) - 1 IMPLIES w(k-1) /= w(k+1))

   x,y: VAR T
   i: VAR nat
   min_walk_vert: LEMMA FORALL (Gw: gr_walk(x,y)): i < length(min_walk_from(x,y,Gw))
                               IMPLIES vert(Gw)(min_walk_from(x,y,Gw)(i))

   min_walk_is_reduced: LEMMA FORALL (Gw: gr_walk(x,y)):
                                     reduced?(Gw,min_walk_from(x,y,Gw))

END min_walk_reduced


¤ Dauer der Verarbeitung: 0.3 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff