Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: sep_set_lems.pvs Sprache: PVS

Original von: PVS^©

sep_set_lems[T: TYPE]: THEORY
BEGIN

   IMPORTING paths[T], sep_sets[T], path_ops[T]

   G,MM: VAR graph[T]
   v,s,t,w1,w2: VAR T
   e: VAR doubleton[T]
   W: VAR finite_set[T]
   p: VAR prewalk

   sep_num_0: LEMMA separable?(G,s,t) AND sep_num(G, s, t) = 0 IMPLIES
                          separates(G, emptyset[T], s, t)

   sep_num_gt_0: LEMMA vert(G)(s) AND vert(G)(t) AND separable?(G,s,t)
                       AND sep_num(G,s,t) > 0 IMPLIES
                              (EXISTS (w: prewalk): walk_from?(G,w,s,t))


   sep_num_is_1: LEMMA vert(G)(s) AND vert(G)(t) AND v /= s AND v /= t AND
                          (FORALL (p: prewalk): walk_from?(G,p,s,t) IMPLIES
                                  (EXISTS (i: below(length(p))): seq(p)(i) = v))
                             IMPLIES sep_num(G,s,t) <= 1

   av: VAR T
   sep_num_le1: LEMMA vert(G)(s) AND vert(G)(t) AND vert(G)(av) AND
                          av /= s AND av /= t AND
                          separable?(G, s, t) AND
                          sep_num(G,s,t) <= 1 IMPLIES
                             (EXISTS (z: T): vert(G)(z) AND z /= s AND z /= t AND
                                               separates(G,singleton(z),s,t))

   separable?_comm: LEMMA separable?(G,s,t) IMPLIES separable?(G,t,s)

   separates_comm:  LEMMA separates(G, W, s, t) = separates(G, W, t, s)

   sep_num_comm:    LEMMA vert(G)(s) AND vert(G)(t) IMPLIES
                            sep_num(G,s,t) = sep_num(G,t,s)

   v_not_in: LEMMA  walk_from?(del_verts(G, remove(v, W)), p,s,t)
               AND W(v) AND NOT verts_of(p)(v)
               IMPLIES walk_from?(del_verts(G, W), p, s, t)

   k: VAR nat
   path_thru_each: LEMMA     sep_num(G,s,t) = k
                         AND separates(G, W, s, t)
                         AND card(W) = k AND W(v)
                         AND vert(G)(s) AND vert(G)(t)
              IMPLIES
                 (EXISTS (pv: prewalk): verts_of(pv)(v) AND path_from?(G,pv,s,t))


   one_to_each: LEMMA     sep_num(G,s,t) = 2
                      AND separates(G, dbl(w1, w2), s, t)
                      AND vert(G)(s) AND vert(G)(t)
              IMPLIES
             ( (EXISTS (Psw1: prewalk): path_from?(G, Psw1, s, w1)) AND
        (EXISTS (Psw2: prewalk): path_from?(G, Psw2, s, w2)))

   walk?_del_verts  : LEMMA walk?(del_verts(G, W), p) IMPLIES walk?[T](G, p)

   del_verts_eq: LEMMA del_vert(del_vert(G, w1), w2) = del_verts(G, dbl(w1, w2))

END sep_set_lems

¤ Dauer der Verarbeitung: 0.1 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.