| products/sources/formale sprachen/PVS/digraphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: exponentiation_aux.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
ind_paths[T: TYPE]: THEORY
BEGIN IMPORTING paths[T] G: VAR digraph[T] u,v,s,t: VAR T e: VAR edgetype[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 ¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
