Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: meng_scaff_prelude.pvs Sprache: PVS

Original von: PVS^©

meng_scaff_prelude[T: TYPE]: THEORY

BEGIN

   IMPORTING meng_scaff[T], sep_set_lems[T], meng_scaff_defs[T]

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

   induction_step(G,s,t): bool = FORALL (GG: graph[T]): size(GG) < size(G)
                               IMPLIES FORALL (s: T, t: T):
                                          separable?(GG,s,t) AND
                                          sep_num(GG, s, t) = 2 AND
                                          vert(GG)(s) AND vert(GG)(t)
                                   IMPLIES (EXISTS (p1,p2: prewalk):
                                                  path_from?(GG,p1,s,t) AND
                                                  path_from?(GG,p2,s,t) AND
                                                  independent?(p1,p2))


   line20: 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)
                   AND MM = meng(G,s,t,w1,w2)
                   AND induction_step(G,s,t)
                   AND NOT (edge?(G)(w1,t) AND edge?(G)(w2,t))
              IMPLIES
                  (EXISTS (P1,P2: prewalk):
                              path_from?(MM,P1,s,t) AND length(P1) > 2 AND
                              path_from?(MM,P2,s,t) AND length(P2) > 2 AND
                              seq(P1)(length(P1)-2) = w1 AND NOT verts_of(P1)(w2) AND
                              seq(P2)(length(P2)-2) = w2 AND NOT verts_of(P2)(w1) AND
                              independent?(P1,P2))

   Long_walk_from(G,s,v): TYPE = {w: Walk_from(G,s,v) | length(w) > 1}

   join2(G,s,t,v,(p1: Long_walk_from(G,s,v)),(p2: Walk_from(G,t,v))):
                                 Walk_from(G,s,t) = p1^(0,length(p1)-2) o rev(p2)

   path_meng_t  : LEMMA path_from?(G, p, s, t) AND length(p) > 0
                           IMPLIES (i < length(p) AND seq(p)(i) = t
                                      IMPLIES i = length(p) - 1)

   path_H_def   : LEMMA path?(H(G,s,w1,w2),p) AND j < length(p) IMPLIES
                           walk?(del_verts[T](G, dbl[T](w1, w2)), p^(0,j))

   path_H_ind   : LEMMA length(p1) > 1 AND length(p2) > 1 AND
                        path?(H(G,s,w1,w2),trunc1(p1)) AND
                        path?(H(G,t,w1,w2),trunc1(p2)) AND
                        separates(G, dbl(w1, w2), s, t) AND
                        seq(p1)(0) = s AND seq(p2)(0) = t
                      IMPLIES independent?(p1,p2)

   path_comps_ind3: LEMMA length(p1) > 2 AND length(p2) > 2 AND
                             path?(H(G,s,w1,w2),trunc1(trunc1(p1))) AND
                             path?(H(G,t,w1,w2),trunc1(trunc1(p2))) AND
                             separates(G, dbl(w1, w2), s, t) AND
                             seq(p1)(0) = s AND seq(p2)(0) = t
                           IMPLIES independent?(trunc1(p1),trunc1(p2))

   path_H_trunc: LEMMA length(p) >= 2 AND
                    path?(H(G, s, w1, w2), trunc1(p)) AND
                    from?(p, s, w1) AND
                    edge?(G)(p(length(p)-2),p(length(p)-1)) AND
                    vert(G)(s)  AND w1 /= s AND
                    vert(G)(t)  AND w2 /= s AND
                    vert(G)(w1) AND vert(G)(w2)
                 IMPLIES
                    path_from?[T](G, p, s, w1)

   meng_last: LEMMA length(p) > 2 AND
                    vert(G)(s)  AND w1 /= s AND w1 /= t AND
                    vert(G)(t)  AND w2 /= s AND w2 /= t AND
                    vert(G)(w1) AND vert(G)(w2) AND
                    path_from?(meng(G, s, t, w1, w2), p, s, t)
                  IMPLIES edge?(G)(seq(p)(length(p) - 3), seq(p)(length(p) - 2))

   ind_verts_W: LEMMA path_from?(G,p1,s,t) AND
                      path_from?(G,p2,t,s) AND
                      length(p1) > 2 AND seq(p1)(length(p1) - 2) = w1 AND
                      length(p2) > 2 AND seq(p2)(length(p2) - 2) = w2 AND
                      independent?(p1,p2) AND
                      w1 /= s AND w1 /= t AND
                      w2 /= s AND w2 /= t
               IMPLIES NOT verts_of(p1)(w2) AND NOT verts_of(p2)(w1)

  ind_verts_w: LEMMA path_from?(G,p1,s,t) AND
                         path_from?(G,p2,s,t) AND
                         length(p1) > 2 AND seq(p1)(length(p1) - 2) = w1 AND
                         length(p2) > 2 AND seq(p2)(length(p2) - 2) = w2 AND
                         independent?(p1,p2) AND
                         w1 /= s AND w1 /= t AND
                         w2 /= s AND w2 /= t
                  IMPLIES NOT verts_of(p1)(w2) AND NOT verts_of(p2)(w1)

   path_meng_in: LEMMA length(p) > 2 AND
                       vert(G)(s) AND w1 /= s AND w1 /= t AND
                       vert(G)(t) AND w2 /= s AND w2 /= t AND
                       vert(G)(w1) AND vert(G)(w2) AND
                       path?(meng(G, s, t, w1, w2), p) AND
                       from?(p,s,t) AND
                       ((seq(p)(length(p) - 2) = w1 AND NOT verts_of(p)(w2)) OR
                        (seq(p)(length(p) - 2) = w2 AND NOT verts_of(p)(w1))    )
                   IMPLIES
                      path?(H(G, s, w1, w2), trunc1(trunc1(p)))

   disjoint?(w1,w2: prewalk): bool = (FORALL (i,j: nat):
                                     i < length(w1)  AND j < length(w2) IMPLIES
                                          seq(w1)(i) /= seq(w2)(j))

   join2_lem: LEMMA path_from?(G,p1,s,v) AND path_from?(G,p2,t,v) AND
                    s /= v AND t /= v AND s /= t AND
                    disjoint?(trunc1(p1),trunc1(p2))
                       IMPLIES path_from?(G,join2(G,s,t,v,p1,p2),s,t)

   path_from_to_walk_from: LEMMA path_from?(G,p,s,t) IMPLIES
                                     walk_from?(G,p,s,t)

   paths_H_disj: LEMMA path?(H(G, t, w1, w2), p2) AND
                            path?(H(G, s, w1, w2), p1) AND
                            separates(G, dbl(w1, w2), s, t) AND
                            seq(p1)(0) = s AND seq(p2)(0) = t AND s /= t
                       IMPLIES disjoint?(p1,p2)


   prelude: LEMMA separates(G, dbl(w1, w2), s, t) AND
                     separable?(G,s,t) AND
                     sep_num(G,s,t) = 2 AND
                     induction_step(G,s,t) AND
                     in?(G,s,t,w1,w2) AND
                     disjoint?(s,t,w1,w2) AND
                     NOT (edge?(G)(w1,s) AND edge?(G)(w2,s)) AND
                     NOT (edge?(G)(w1,t) AND edge?(G)(w2,t))
                   IMPLIES
                         (EXISTS (p1,p2: prewalk): path_from?(G,p1,s,t) AND
                                                  path_from?(G,p2,s,t) AND
                                                  independent?(p1,p2))

END meng_scaff_prelude

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