SSL circuit_deg.pvs Sprache: PVS

circuit_deg[T: TYPE]: THEORY

BEGIN

   IMPORTING graph_deg[T], circuits[T], subgraphs_from_walk[T]

   G: VAR graph[T]

   e_duo(e1,e2: doubleton[T]): finite_set[doubleton[T]] =
                   add[doubleton[T]](e1,singleton[doubleton[T]](e2))

   z: VAR T
   cir_deg_G: LEMMA (EXISTS (a,b: (vert(G))): vert(G)(z) AND
                          a /= b AND edge?(G)(a,z) AND edge?(G)(b,z) ) IMPLIES
                              deg(z,G) >= 2

   circuit_deg: LEMMA FORALL (w: Walk(G),i: below(length(w))): circuit?(G,w)
                            IMPLIES deg(w(i),G_from(G,w)) >= 2

   circuit_subgraph_len_1: LEMMA FORALL (w: Walk(G)): circuit?(G,w)
                                IMPLIES card(vert(G_from(G,w))) > 1

END circuit_deg

quality96%

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