| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle min_walks.pvs Sprache: PVS |
|||||||||
|
min_walks[T: TYPE]: THEORY
BEGIN IMPORTING digraphs[T] IMPORTING walks[T], abstract_min v1,v2,x,y: VAR T G: VAR digraph[T] gr_walk(v1,v2): TYPE = {G: digraph[T] | vert(G)(v1) AND vert(G)(v2) AND (EXISTS (w: Seq(G)): walk_from?(G,w,v1,v2))} min_walk_from(x,y,(Gw:gr_walk(x,y))): Walk(Gw) = min[Seq(Gw),(LAMBDA (w: Seq(Gw)): length(w)), (LAMBDA (w: Seq(Gw)): walk_from?(Gw,w,x,y))] is_min(G,(w: Seq(G)),x,y): bool = walk?(G,w) AND (FORALL (ww: Seq(G)): walk_from?(G,ww,x,y) IMPLIES length(w) <= length(ww)) min_walk_def: LEMMA FORALL (Gw: gr_walk(x,y)): walk_from?(Gw,min_walk_from(x,y,Gw),x,y) AND is_min(Gw, min_walk_from(x,y,Gw),x,y) min_walk_in : LEMMA FORALL (Gw: gr_walk(x,y)): walk_from?(Gw,min_walk_from(x,y,Gw),x,y) min_walk_is_min: LEMMA FORALL (Gw: gr_walk(x,y), ww: Seq(Gw)): walk_from?(Gw,ww,x,y) IMPLIES length(min_walk_from(x,y,Gw)) <= length(ww) END min_walks ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28