|
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
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
