Quelle  circuit_deg.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