Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Makefile.in   Sprache: Unknown

Original von: 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



¤ Dauer der Verarbeitung: 0.26 Sekunden  (vorverarbeitet)  ¤





vermutete Sprache:
Sekunden
vermutete Sprache:
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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik