Quelle path_circ.pvs Sprache: PVS

path_circ[T: TYPE]: THEORY

BEGIN

IMPORTING walks[T],circuits[T],paths[T]

  x,y,s,t,ss,tt: VAR T
  i: VAR nat
  G,GG: VAR graph[T]
  u,w,p,q: VAR prewalk

  path_reduc       : LEMMA FORALL (p: Path(G)) : reduced?(G,p)

  trunc_long       : LEMMA length(u)>= 2 AND length(w) >= 2 IMPLIES length(trunc1(u) o w) >= 1

  trunc_walk       : LEMMA length(u)>=2 AND walk?(G,u) IMPLIES walk?(G,trunc1(u))

  walks_concat_red : LEMMA walk?(G,u) AND walk?(G,w) AND
                           length(u) >=2 AND length(w) >=2 AND reduced?(G,u) AND
                           reduced?(G,w) AND u(length(u)-1) = w(0) AND
                           u(length(u)-2) /= w(1) IMPLIES reduced?(G,trunc1(u) o w)

  index_rev        : LEMMA length(q)>=2 IMPLIES length(rev(q)) = length(q) AND
                                           rev(q)(0) = q(length(q)-1) AND
                                           rev(q)(1) = q(length(q)-2)

  rev_rev          : LEMMA rev(rev(q))=q

  ind_rev_rev      : LEMMA length(q)>=2  IMPLIES rev(q)(length(q)-1) = q(0) AND
                                            rev(q)(length(q)-2) = q(1)

  second_in_cat    : LEMMA s /= t AND from?(p,s,t) AND from?(q,s,t) IMPLIES
                               p(1) = (trunc1(p) o rev(q))(1)

  sec_from_last    : LEMMA s /= t AND from?(p,s,t) AND from?(q,s,t) IMPLIES
                           q(1) = (trunc1(p) o rev(q))(length(trunc1(p) o rev(q))-2)

  prewalk_same     : LEMMA s=t AND length(p)=1 AND length(q)=1 AND from?(p,s,t) AND
                           from?(q,s,t) IMPLIES p=q

  compose_long     : LEMMA s /= t AND from?(p,s,t) AND from?(q,s,t) AND
                           p(length(p)-2) /= q(length(q)-2) IMPLIES length(trunc1(p) o rev(q)) > 2

  red_compos       : LEMMA s /= t AND path_from?(G,p,s,t) AND
                           path_from?(G,q,s,t) AND p(length(p)-2) /= q(length(q)-2)
                              IMPLIES reduced?(G,trunc1(p) o rev(q))

  cycl_red_compos  : LEMMA s /= t AND path_from?(G,p,s,t) AND
                           path_from?(G,q,s,t) AND p(length(p)-2) /= q(length(q)-2) AND
                           p(1) /= q(1)
                              IMPLIES cyclically_reduced?(G,trunc1(p) o rev(q))

  walkers          : LEMMA finseq_appl(p)(0)=finseq_appl(q)(0) AND
                           finseq_appl(p)(length(p)-1)=finseq_appl(q)(length(q)-1)
                         IMPLIES
                           from?(p,finseq_appl(p)(0),finseq_appl(p)(length(p)-1)) AND
                           from?(q,finseq_appl(p)(0),finseq_appl(p)(length(p)-1))

  path_one         : LEMMA s=t and path_from?(G,p,s,t) IMPLIES length(p)=1 OR circuit?(G,p)

  rev_eq           : LEMMA rev(p)=rev(q) IMPLIES p=q

  front_back       : LEMMA from?(p,s,t) AND from?(q,s,t)
                            IMPLIES p(0)=q(0) AND  p(length(p)-1)=q(length(q)-1)

  walk_from_l      : LEMMA from?(p,s,t) AND s /= t IMPLIES length(p) >= 2

  plus_up          : LEMMA s /= t AND from?(p,s,t) AND from?(q,s,t)  IMPLIES
                (trunc1(p) = trunc1(q) IMPLIES  p=q)

  two_walks        : LEMMA s /=t AND walk?(G,p) AND walk?(G,q) AND
                           from?(p,s,t) AND from?(q,s,t) IMPLIES
                                     pre_circuit?(G,trunc1(p) o rev(q))

  back_short       : LEMMA s /= t AND path_from?(G,p,s,t) AND
                           path_from?(G,q,s,t)
                        IMPLIES
                           ( p(length(p)-2)=q(length(q)-2) AND p /= q IMPLIES
                             (EXISTS (pp,qq: prewalk) : pp /= qq AND
                                 path_from?(G,pp,s,p(length(p)-2)) AND
                                 path_from?(G,qq,s,p(length(p)-2)) AND
                                 length(pp)= length(p)-1 AND length(qq)=length(q)-1)
                           )

  from_rev         : LEMMA from?(p,s,t) IMPLIES from?(rev(p),t,s)

  front_short: LEMMA s /= t AND path_from?(G,p,s,t) AND path_from?(G,q,s,t)
                      IMPLIES
                        ( p(1)=q(1) AND p /= q  IMPLIES
                          (EXISTS (pp,qq: prewalk) :
                            pp /= qq AND path_from?(G,pp,t,p(1))
                            AND path_from?(G,qq,t,p(1))
                            AND length(pp)= length(p)-1 AND length(qq)=length(q)-1)
                        )

  add1_rev: LEMMA FORALL (w:Seq(G),x:(vert(G))):
                   length(w)>1 AND x /= seq(w)(length(w)-1)
                   IMPLIES add1(w,x)=trunc1(w) o rev(gen_seq2(G,x,seq(w)(length(w)-1)))

END path_circ

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.