Quelle ind_paths.pvs Sprache: PVS

ind_paths[T: TYPE]: THEORY

BEGIN

   IMPORTING paths[T]

   G: VAR graph[T]
   u,v,s,t: VAR T
   e: VAR doubleton[T]
   V: VAR finite_set[T]
   n: VAR nat

   independent?(w1,w2: prewalk): bool =
                       (FORALL (i,j: nat): i > 0 AND i < length(w1) - 1 AND
                                           j > 0 AND j < length(w2) - 1 IMPLIES
                                    seq(w1)(i) /= seq(w2)(j))

   p1,p2: VAR prewalk
   independent?_comm: LEMMA independent?(p1,p2) IMPLIES
                                    independent?(p2,p1)

   independent_ne: LEMMA length(p1) > 2 AND independent?(p1,p2) IMPLIES p1 /= p2

   ps: VAR prewalk

%   IMPORTING finite_sets

   set_of_paths(G,s,t): TYPE = finite_set[Path_from(G,s,t)]

   ind_path_set?(G,s,t,(pset: set_of_paths(G,s,t))): bool =
                   (FORALL (p1,p2: Path_from(G,s,t)):
                             pset(p1) AND pset(p2) AND  p1 /= p2
                                         IMPLIES independent?(p1,p2))

   ind_path_set_2: LEMMA FORALL (ips: set_of_paths(G,s,t)):
                                    card(ips) = 2 AND
                                    ind_path_set?(G, s, t, ips)
                              IMPLIES
                         (EXISTS (P_1,P_2: prewalk): path_from?(G, P_1, s, t) AND
                                                    path_from?(G, P_2, s, t) AND
                                                      independent?(P_1,P_2) )

   internal_verts(w: prewalk): finite_set[T] =
               {t: T | (EXISTS (i: nat): i > 0 AND i < length(w) - 1 AND w(i) = t)}

   indep?(w1,w2: prewalk): bool = empty?(intersection(internal_verts(w1),
                                                      internal_verts(w2)))

   w1,w2: VAR prewalk
   indep?_lem: LEMMA indep?(w1,w2) IFF independent?(w1,w2)

END ind_paths

quality85%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.