Quellcode-Bibliothek meng_scaff_defs.pvs Sprache: PVS

meng_scaff_defs[T: TYPE]: THEORY
BEGIN

   IMPORTING paths[T], subgraphs[T], sep_sets[T],
             path_ops[T], subgraph_paths[T]

   G,HH: VAR graph[T]
   w1,w2,v,s,t,z: VAR T
   e: VAR doubleton[T]
   V: VAR finite_set[T]
   p: VAR prewalk

   IMPORTING ind_paths[T]

   path_comp(G,(x:T)): Subgraph(G) = subgraph(G,path_verts(G,x))

   IMPORTING graph_deg[T]

   H(G,(x,w1,w2:T)): Subgraph(G) = path_comp(del_vert(del_vert(G,w1),w2),x)


   incident(v,G,(x,w1,w2:T)): finite_set[doubleton[T]]
              = {e: doubleton[T] | (EXISTS z: edges(G)(e) AND e = dbl(v,z)
                                              AND vert(H(G,x,w1,w2))(z))}

   meng(G,(x,y: (vert(G))),(w1,w2: {t | vert(G)(t) AND t /= y})): graph[T] =
                   (# vert  := add(y,add(w1,add(w2,vert(H(G,x,w1,w2))))),
                      edges := add(dbl(w1,y), add(dbl(w2,y),
                                 union(edges(H(G,x,w1,w2)),
                                       union(incident(w1,G,x,w1,w2),
                                             incident(w2,G,x,w1,w2)))))
                   #)

   in?(G,s,t,w1,w2): bool = vert(G)(s) AND vert(G)(t) AND vert(G)(w1)
                                AND vert(G)(w2)

   disjoint?(s,t,w1,w2): bool = (s /= t AND w1 /= w2 AND w1 /= s AND w2 /= s
                                     AND w1 /= t AND w2 /= t)

   vert_H_s: LEMMA vert(G)(s) AND s /= w1 AND s /= w2
                     IMPLIES vert(H(G, s, w1, w2))(s)

   path_H_W        : LEMMA path?(H(G,s,w1,w2),p) IMPLIES
                              NOT verts_of(p)(w1) AND NOT verts_of(p)(w2)

%  MOVED TO theory subgraph_paths
%
%  walk?_subgraph  : LEMMA subgraph?(HH,G) AND walk?(HH, p)
%                               IMPLIES walk?(G, p)
%
%  path?_subgraph  : LEMMA subgraph?(HH,G) AND path?(HH, p)
%                                  IMPLIES path?(G, p)

   path_comp_in    : LEMMA path?(H(G,s,w1,w2),p) IMPLIES path?(G,p)

   walk?_H         : LEMMA walk?(G, p) AND seq(p)(0) = s AND
                           NOT verts_of(p)(w1) AND NOT verts_of(p)(w2)
                         IMPLIES walk?(H(G, s, w1, w2), p)

   vert_meng_sub   : LEMMA in?(G, s, t, w1, w2) AND disjoint?(s, t, w1, w2)
                           IMPLIES subset?(vert(meng(G, s, t, w1, w2)), vert(G))

   del_vert_comm   : LEMMA del_vert(del_vert(G,w2),w1) =
                                    del_vert(del_vert(G,w1),w2)

   H_comm          : LEMMA H(G, t, w2, w1) = H(G, t, w1, w2)

   incident_comm   : LEMMA incident(v, G, t, w2, w1) = incident(v, G, t, w1, w2)

   meng_comm       : LEMMA vert(G)(s)  AND vert(G)(t) AND
                              vert(G)(w1) AND w1 /= s    AND
                              vert(G)(w2) AND w2 /= s
                            IMPLIES meng(G, t, s, w1, w2) = meng(G, t, s, w2, w1)

END meng_scaff_defs

quality100%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.