Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: graph_complected.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.