Quellcode-Bibliothek graph_complected.pvs Sprache: PVS

graph_complected[T: TYPE]: THEORY

BEGIN

   IMPORTING graph_conn_defs[T], graph_ops[T], graph_deg[T],
             graph_inductions[T]

   G,G1,G2: VAR graph[T]

   v,v1,v2: VAR T
   e: VAR doubleton[T]

%Consider moving below to graphs module.

   two_vertices: LEMMA FORALL (v1,v2: T): edges(G)(e) AND e(v2) AND
                            vert(G) = dbl(v1, v2) IMPLIES e(v1)

   sub_T: LEMMA FORALL (v: (vert(G))):
                          NOT empty?(vert(del_vert(G,v))) AND deg(v,G) = 0
                             IMPLIES NOT connected?(G)

   rev_lem2  : LEMMA FORALL (v: (vert(G))):
                     connected?(G) AND
                     deg(v, G) = 1 IMPLIES
                             connected?(del_vert(G, v))

   conn_lem2 : LEMMA FORALL (v: (vert(G))):
                     connected?(G) AND NOT isolated?(G) AND
                     deg(v, G) = 1 IMPLIES
                         (EXISTS (x: (vert(G))): deg(x, G) = 1
                                     AND connected?(del_vert(G, x)))

   del_rem_lem: LEMMA edges(G)(e) AND e(v)
                      IMPLIES del_vert(del_edge(G, e), v) = del_vert(G, v)

   conn_lem3 : LEMMA connected?(G) AND NOT isolated?(G) AND
                     NOT (EXISTS (v: (vert(G))): deg(v, G) = 1)
                     IMPLIES
                        (EXISTS (e: (edges(G))): connected?(del_edge(G, e)))

   BIG       : LEMMA connected?(del_edge(G, e)) IMPLIES connected?(G)

   conn_lem6 : LEMMA  edges(G)(e) AND connected?(del_edge(G, e))
                      AND NOT isolated?(G) AND
                      NOT (EXISTS (v: (vert(G))): deg(v, G) = 1)
                      IMPLIES
                         connected?(G )

   conn_eq_compl: LEMMA connected?(G) IFF
                        (IF isolated?(G) THEN singleton?(G)
                        ELSIF (EXISTS (v: (vert(G))): deg(v,G) = 1) THEN
                           (EXISTS (x: (vert(G))): deg(x,G) = 1 AND
                              connected?(del_vert(G,x)))
                        ELSE
                           (EXISTS (e: (edges(G))):
                              connected?(del_edge(G,e)))
                        ENDIF)

    conn_del_vert: LEMMA  (EXISTS (v: (vert(G))): deg(v,G) = 1 AND                                             connected?(del_vert(G,v)))
                          IMPLIES connected?(G)

    connected_not_empty: LEMMA connected?(G) IMPLIES NOT empty?(G)

connect_deg_0: LEMMA connected?(G) and vert(G)(v) and deg(v,G)= 0 IMPLIES G=singleton_graph(v)

END graph_complected

quality94%

¤ 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

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders