Quelle meng_scaff.pvs Sprache: PVS

meng_scaff[T: TYPE]: THEORY

BEGIN

   IMPORTING meng_scaff_defs[T], sep_set_lems[T], min_lem

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

  P: VAR pred[T]

  ps_ptype(P): TYPE = {ps: prewalk | EXISTS (i: below(length(ps))): P(seq(ps)(i))}

  first(P: pred[T],ps: ps_ptype(P)): below(length(ps)) =
                  min({i: nat | i < length(ps) AND P(seq(ps)(i))})

  first_lem: LEMMA FORALL (ps: ps_ptype(P)): P(seq(ps)(first(P,ps)))

  first_not: LEMMA FORALL (ps: ps_ptype(P)): i < first(P,ps) IMPLIES
        NOT  P(seq(ps)(i))


  z: VAR T

  meng_to_G_sep: LEMMA walk_from?(G, p, s, t) AND
                        in?(G, s, t, w1, w2) AND disjoint?(s, t, w1, w2) AND
                        separates(meng(G, s, t, w1, w2), singleton(z), s, t) AND
                        separable?(G, s, t) AND
                        separates(G, dbl(w1, w2), s, t) AND
                        NOT verts_of(p)(z)
                     IMPLIES sep_num(G, s, t) <= 1

  prep_14: LEMMA  vert(G)(s) AND vert(G)(t) AND
              vert(G)(w1) AND vert(G)(w2) AND
                   disjoint?(s, t, w1, w2) AND
                   sep_num(meng(G, s, t, w1, w2),s,t) <= 1 AND
                   separates(meng(G, s, t, w1, w2), dbl(w1, w2), s, t) AND
              separable?(G, s, t) AND
              separates(G, dbl(w1, w2), s, t) AND
                   sep_num(G, s, t) = 2
                  IMPLIES sep_num(G,s,t) <= 1

   line14: LEMMA separable?(G, s, t) AND
                   in?(G, s, t, w1, w2) AND
                   sep_num(G, s, t) = 2 AND
                   separates(G, dbl(w1, w2), s, t) AND
                   disjoint?(s, t, w1, w2)
                   IMPLIES
                        sep_num(meng(G, s, t, w1, w2), s, t) = 2

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

   prep_16: LEMMA separates(G, dbl(w1, w2), s, t) AND
                     disjoint?(s, t, w1, w2) AND
                     (FORALL p: path_from?(G,p,t,w1) IMPLIES verts_of(p)(w2))
                     AND vert(G)(s) AND vert(G)(t)
                     IMPLIES  sep_num(G,s,t) <= 1

   line16: LEMMA NOT edge?(G)(w1, t) AND
                        disjoint?(s,t,w1,w2) AND
                        separates(G, dbl(w1, w2), s, t) AND
                        sep_num(G,s,t) = 2 AND vert(G)(s) AND vert(G)(t)
                   IMPLIES EXISTS (yt: T): vert(H(G,t,w1,w2))(yt) AND yt /= t

   line19: LEMMA      separable?(G,s,t) AND in?(G,s,t,w1,w2)
                      AND disjoint?(s,t,w1,w2)
                      AND MM = meng(G, s, t, w1, w2)
                      AND separates(G, dbl(w1, w2), s, t)
                      AND path_from?(MM, p, s, t)
                          IMPLIES length(p) > 2 AND (  seq(p)(length(p)-2) = w1
                                               OR seq(p)(length(p)-2) = w2)

   yt: VAR T

   line17_prep: LEMMA vert(G)(s) AND vert(G)(t) AND disjoint?(s,t,w1,w2) AND
                      vert(H(G, t, w1, w2))(yt) AND
                      separates(G, dbl(w1, w2), s, t) IMPLIES
                          NOT vert(H(G, s, w1, w2))(yt)

   line17: LEMMA  vert(H(G,t,w1,w2))(yt) AND
                  in?(G, s, t, w1, w2) AND
                  disjoint?(s, t, w1, w2) AND
                  yt /= t AND
                  separates(G, dbl(w1, w2), s, t)
                       IMPLIES size(meng(G, s, t, w1, w2)) < size(G)

   pre20: LEMMA separable?(G, s, t) AND
                in?(G, s, t, w1, w2) AND
                sep_num(G, s, t) = 2 AND
                separates(G, dbl(w1, w2), s, t) AND
                disjoint?(s, t, w1, w2)
                IMPLIES
               ( separable?(meng(G, s, t, w1, w2),s,t) AND
                     sep_num(meng(G, s, t, w1, w2), s, t) = 2 AND
                     vert(meng(G, s, t, w1, w2))(s) AND
                     vert(meng(G, s, t, w1, w2))(t)                 )

END meng_scaff

quality95%

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