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.12Bemerkung: (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.