Quelle reduce_walks.pvs Sprache: PVS

reduce_walks[T: TYPE]: THEORY

BEGIN

   IMPORTING paths[T]

   G: VAR digraph[T]

   Long_walk(G): TYPE = {w: Walk(G) | length(w) > 3}

   reduce(G: digraph[T], w: Long_walk(G),
          k: {n: nat | n > 0 AND n < length(w)-1}): Walk(G) =
                      IF w(k-1) = w(k+1) THEN
                          (# length := length(w) - 2,
                          seq := (LAMBDA (i: below(length(w)-2)):
                                     IF i < k THEN w(i)
                                     ELSE w(i+2)
                                     ENDIF) #)
                      ELSE
                          w
                      ENDIF

   reduce_lem: LEMMA FORALL (w: Walk(G),
                            k: {n: nat | n > 0 AND n < length(w)-1}):
       w(k-1) = w(k+1) AND length(w) > 3 IMPLIES
          reduce(G,w,k) = w^(0,k-1) o w^(k+2,length(w)-1)


END reduce_walks

quality96%

¤ 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.