Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: coqchk.ml Sprache: PVS

Original von: PVS^©

h_menger[T: TYPE]: THEORY

BEGIN

   IMPORTING meng_scaff_prelude[T], graph_inductions[T], graph_ops[T], path_ops[T]

   G,MM: VAR graph[T]
   v,s,t,w1,w2,av,ajm,z,x: VAR T
   W: VAR finite_set[T]
   p,p1,p2: VAR prewalk
   e: VAR doubleton[T]

   path_not_thru: LEMMA separable?(G,s,t) AND
                        sep_num(G,s,t) = 2 AND
                        vert(G)(s) AND vert(G)(t)
                    IMPLIES
                      (FORALL (z: T): z /= s AND z /= t IMPLIES
                        (EXISTS (pn: prewalk): path_from?(del_vert(G,z),pn,s,t)))

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

  sep_num_del: LEMMA separable?(G,s,t) AND vert(G)(s) AND vert(G)(t)
                     AND v /= t AND v /= s IMPLIES
                     sep_num(del_vert(G, v), s, t) <= sep_num(G, s, t)

  separates_del: LEMMA separates(del_vert(G,ajm), singleton(z), s,t) AND
                         vert(G)(ajm) AND vert(G)(s) AND vert(G)(t) AND
                         ajm /= s AND ajm /= t
                       IMPLIES
                           separates(G, dbl(ajm,z), s,t)

  induction_step_comm: LEMMA induction_step(G,s,t) IMPLIES induction_step(G,t,s)

  separable?_del: LEMMA separable?(G,s,t) AND vert(G)(s) AND vert(G)(t)
                        AND v /= s AND v /= t
                        IMPLIES separable?(del_vert(G, v), s, t) AND
                                vert(del_vert(G, v))(s) AND
                                vert(del_vert(G, v))(t)

  seq_j: LEMMA (length(p) > 3 AND edge?(G)(seq(p)(length(p)-2),t) AND
               NOT edge?(G)(seq(p)(0),t)) IMPLIES
                 (EXISTS (j: nat): j > 0 AND j < length(p) AND
                                   NOT edge?(G)(seq(p)(j - 1), t)
                                   AND edge?(G)(seq(p)(j), t))

  short_path_case: LEMMA vert(G)(x) AND vert(G)(s) AND vert(G)(t) AND
                         edge?(G)(s, x) AND edge?(G)(x, t) AND
                         separable?(G, s, t) AND
                         sep_num(G, s, t) = 2
                     IMPLIES
                  (EXISTS (p1, p2: prewalk):
                    path_from?(G, p1, s, t)
                        AND path_from?(G, p2, s, t) AND independent?(p1, p2))

  finale: LEMMA  separable?(G,s,t) AND sep_num(G,s,t) = 2 AND
                 vert(G)(s) AND vert(G)(t) AND
                 induction_step(G,s,t)
                IMPLIES
                      (EXISTS (p1,p2: prewalk): path_from?(G,p1,s,t) AND
                                               path_from?(G,p2,s,t) AND
                                               independent?(p1,p2))

  h_menger: LEMMA  separable?(G,s,t) AND sep_num(G,s,t) = 2 AND
                      vert(G)(s) AND vert(G)(t)
                IMPLIES
                      (EXISTS (p1,p2: prewalk): path_from?(G,p1,s,t) AND
                                               path_from?(G,p2,s,t) AND
                                               independent?(p1,p2))

  hard_menger: LEMMA  separable?(G,s,t) AND sep_num(G,s,t) = 2 AND
                      vert(G)(s) AND vert(G)(t)
                IMPLIES
                        (EXISTS (ips: set_of_paths(G,s,t)):
                                 card(ips) = 2 AND ind_path_set?(G,s,t,ips))

END h_menger

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