Quelle sep_set_lems.pvs Sprache: 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

quality98%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.