products/Sources/formale Sprachen/PVS/graphs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: isar_cmd.ML   Sprache: Lisp

Original von: PVS©
(cycle_deg
 (reachable_TCC1 0
  (reachable_TCC1-2 nil 3312297543
   ("" (skosimp*)
    (("" (typepred "vert(G!1)")
      (("" (lemma "finite_subset[T]")
        ((""
          (inst -1 "vert(G!1)" "{y: T |
                  vert(G!1)(y) AND
                   (EXISTS (w: Seq[T](G!1)): walk_from?[T](G!1, w, x!1, y))}")
          (("" (bddsimp)
            (("" (hide 2)
              (("" (expand "subset?")
                (("" (expand "member") (("" (skosimp*) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil cycle_deg nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (verts_in? const-decl "bool" walks nil)
    (Seq type-eq-decl nil walks nil)
    (walk_from? const-decl "bool" walks nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (finite_subset formula-decl nil finite_sets nil))
   nil)
  (reachable_TCC1-1 nil 3312285093 ("" (subtype-tcc) nil nil) nil nil))
 (reachable_subset 0
  (reachable_subset-1 nil 3312297501 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil cycle_deg nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (graph type-eq-decl nil graphs nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (/= const-decl "boolean" notequal nil)
    (edge? const-decl "bool" graphs nil)
    (walk? const-decl "bool" walks nil)
    (walk_from? const-decl "bool" walks nil)
    (reachable const-decl "finite_set[T]" cycle_deg nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (nil application-judgement "finite_set[T]" cycle_deg nil))
   shostak))
 (reachable_conn 0
  (reachable_conn-5 nil 3559571065
   ("" (skosimp*)
    (("" (lemma "conn_eq_path")
      (("" (inst -1 "subgraph(G!1, reachable(G!1, x!1))")
        (("" (iff -1)
          (("" (bddsimp)
            (("" (hide 1)
              (("" (expand "path_connected?")
                (("" (bddsimp)
                  (("1" (install-rewrites "subgraphs")
                    (("1" (assert)
                      (("1" (inst -1 "x!1")
                        (("1" (bddsimp)
                          (("1"
                            (inst 1
                             "(#length := 1, seq :=(LAMBDA (i:below(1)): x!1)#)")
                            (("1" (assert) nil nil)) nil)
                           ("2" (typepred "x!1")
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp*)
                    (("2" (typepred "x!2")
                      (("2" (typepred "y!1")
                        (("2" (expand "subgraph" -)
                          (("2" (flatten)
                            (("2" (expand "reachable" -)
                              (("2"
                                (bddsimp)
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (lemma "walk?_reverse")
                                    (("2"
                                      (inst-cp
                                       -1
                                       "G!1"
                                       "x!1"
                                       "y!1"
                                       "w!1")
                                      (("2"
                                        (inst
                                         -1
                                         "G!1"
                                         "x!1"
                                         "x!2"
                                         "w!2")
                                        (("2"
                                          (bddsimp)
                                          (("2"
                                            (skosimp*)
                                            (("2"
                                              (lemma "walk_merge")
                                              (("2"
                                                (inst
                                                 -1
                                                 "G!1"
                                                 "w!4"
                                                 "w!3"
                                                 "x!2"
                                                 "y!1"
                                                 "x!1")
                                                (("2"
                                                  (bddsimp)
                                                  (("2"
                                                    (skosimp*)
                                                    (("2"
                                                      (inst 1 "p!1")
                                                      (("1"
                                                        (install-rewrites
                                                         "walks")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (bddsimp)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        (("2"
                                                          (install-rewrites
                                                           "walks")
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (skosimp*)
                                                              (("2"
                                                                (bddsimp)
                                                                (("1"
                                                                  (skosimp*)
                                                                  (("1"
                                                                    (bddsimp)
                                                                    (("1"
                                                                      (typepred
                                                                       "p!1")
                                                                      (("1"
                                                                        (inst
                                                                         -11
                                                                         "n!1")
                                                                        (("1"
                                                                          (bddsimp)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (inst-cp
                                                                         -9
                                                                         "n!1")
                                                                        (("1"
                                                                          (inst
                                                                           -9
                                                                           "1+n!1")
                                                                          (("1"
                                                                            (hide
                                                                             -3
                                                                             -4
                                                                             -5
                                                                             -6)
                                                                            (("1"
                                                                              (bddsimp
                                                                               (-2
                                                                                -5
                                                                                -6
                                                                                1))
                                                                              (("1"
                                                                                (hide
                                                                                 -8
                                                                                 -9
                                                                                 -11
                                                                                 -12)
                                                                                (("1"
                                                                                  (reveal
                                                                                   -10
                                                                                   -11)
                                                                                  (("1"
                                                                                    (reveal
                                                                                     (-1
                                                                                      -2
                                                                                      -7
                                                                                      -8))
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "walk?_caret")
                                                                                      (("1"
                                                                                        (inst
                                                                                         -1
                                                                                         "G!1"
                                                                                         "0"
                                                                                         "n!1"
                                                                                         "p!1")
                                                                                        (("1"
                                                                                          (stop-rewrite)
                                                                                          (("1"
                                                                                            (assert)
                                                                                            (("1"
                                                                                              (case
                                                                                               "walk?(G!1,p!1)")
                                                                                              (("1"
                                                                                                (bddsimp)
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   -8
                                                                                                   "G!1"
                                                                                                   "x!2"
                                                                                                   "x!3"
                                                                                                   "p!1 ^ (0, n!1)")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "walk_from?"
                                                                                                     -8)
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "^"
                                                                                                       -8
                                                                                                       (1
                                                                                                        2
                                                                                                        3))
                                                                                                      (("1"
                                                                                                        (bddsimp
                                                                                                         (-2
                                                                                                          -8))
                                                                                                        (("1"
                                                                                                          (skosimp*)
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -9
                                                                                                             "G!1"
                                                                                                             "w!5"
                                                                                                             "w!2"
                                                                                                             "x!1"
                                                                                                             "x!3"
                                                                                                             "x!2")
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "walk_from?"
                                                                                                               -9
                                                                                                               (1
                                                                                                                2))
                                                                                                              (("1"
                                                                                                                (typepred
                                                                                                                 "w!2")
                                                                                                                (("1"
                                                                                                                  (case
                                                                                                                   "walk?(G!1,w!2)")
                                                                                                                  (("1"
                                                                                                                    (bddsimp)
                                                                                                                    (("1"
                                                                                                                      (skosimp*)
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         1
                                                                                                                         "p!2")
                                                                                                                        (("1"
                                                                                                                          (expand
                                                                                                                           "walk_from?"
                                                                                                                           -12)
                                                                                                                          (("1"
                                                                                                                            (flatten)
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "walk?"
                                                                                                                               -14)
                                                                                                                              (("1"
                                                                                                                                (flatten)
                                                                                                                                (("1"
                                                                                                                                  (hide-all-but
                                                                                                                                   (-4
                                                                                                                                    -7
                                                                                                                                    -12
                                                                                                                                    -13
                                                                                                                                    -14
                                                                                                                                    -15
                                                                                                                                    -25
                                                                                                                                    -26)
                                                                                                                                   -)
                                                                                                                                  (("1"
                                                                                                                                    (grind)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil)
                                                                                                                         ("2"
                                                                                                                          (hide-all-but
                                                                                                                           -12
                                                                                                                           -)
                                                                                                                          (("2"
                                                                                                                            (grind)
                                                                                                                            nil
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (hide-all-but
                                                                                                                     (-2
                                                                                                                      -7
                                                                                                                      -8
                                                                                                                      -19)
                                                                                                                     -)
                                                                                                                    (("2"
                                                                                                                      (hide
                                                                                                                       2)
                                                                                                                      (("2"
                                                                                                                        (install-rewrites
                                                                                                                         "walks")
                                                                                                                        (("2"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (expand
                                                                                                           min)
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (reveal
                                                                                                 -10)
                                                                                                (("2"
                                                                                                  (hide
                                                                                                   (-16
                                                                                                    -17))
                                                                                                  (("2"
                                                                                                    (hide-all-but
                                                                                                     (-1
                                                                                                      -9
                                                                                                      -12
                                                                                                      -13
                                                                                                      -14
                                                                                                      -15)
                                                                                                     -)
                                                                                                    (("2"
                                                                                                      (hide
                                                                                                       2)
                                                                                                      (("2"
                                                                                                        (assert)
                                                                                                        (("2"
                                                                                                          (grind)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (hide-all-but
                                                                                 (-1
                                                                                  -3)
                                                                                 -)
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil)
                                                                               ("3"
                                                                                (reveal
                                                                                 -6
                                                                                 -7)
                                                                                (("3"
                                                                                  (lemma
                                                                                   "walk?_caret")
                                                                                  (("3"
                                                                                    (inst
                                                                                     -1
                                                                                     "G!1"
                                                                                     "0"
                                                                                     "1+n!1"
                                                                                     "p!1")
                                                                                    (("3"
                                                                                      (inst
                                                                                       -3
                                                                                       "G!1"
                                                                                       "x!2"
                                                                                       "x!3"
                                                                                       "p!1 ^ (0, 1 + n!1)")
                                                                                      (("1"
                                                                                        (typepred
                                                                                         "n!1")
                                                                                        (("1"
                                                                                          (bddsimp
                                                                                           (-1
                                                                                            -2
                                                                                            -4
                                                                                            -5
                                                                                            -8))
                                                                                          (("1"
                                                                                            (skosimp*)
                                                                                            (("1"
                                                                                              (inst
                                                                                               -6
                                                                                               "G!1"
                                                                                               "w!5"
                                                                                               "w!2"
                                                                                               "x!1"
                                                                                               "x!3"
                                                                                               "x!2")
                                                                                              (("1"
                                                                                                (hide-all-but
                                                                                                 (-3
                                                                                                  -6
                                                                                                  -12
                                                                                                  -13
                                                                                                  -14)
                                                                                                 -)
                                                                                                (("1"
                                                                                                  (typepred
                                                                                                   "w!2")
                                                                                                  (("1"
                                                                                                    (case
                                                                                                     "walk_from?(G!1, w!2, x!1, x!2)")
                                                                                                    (("1"
                                                                                                      (bddsimp
                                                                                                       (-1
                                                                                                        -4
                                                                                                        -5))
                                                                                                      (("1"
                                                                                                        (skosimp*)
                                                                                                        (("1"
                                                                                                          (inst
                                                                                                           1
                                                                                                           "p!2")
                                                                                                          (("1"
                                                                                                            (hide-all-but
                                                                                                             -3
                                                                                                             -)
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              (("1"
                                                                                                                (grind)
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil)
                                                                                                           ("2"
                                                                                                            (hide-all-but
                                                                                                             -3
                                                                                                             -)
                                                                                                            (("2"
                                                                                                              (grind)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (hide-all-but
                                                                                                       (-1
                                                                                                        -2
                                                                                                        -5
                                                                                                        -6
                                                                                                        -7)
                                                                                                       -)
                                                                                                      (("2"
                                                                                                        (hide
                                                                                                         2)
                                                                                                        (("2"
                                                                                                          (assert)
                                                                                                          (("2"
                                                                                                            (grind)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide
                                                                                             2)
                                                                                            (("2"
                                                                                              (hide
                                                                                               (-5
                                                                                                -11
                                                                                                -12
                                                                                                -13
                                                                                                -14
                                                                                                -15
                                                                                                -16
                                                                                                -17
                                                                                                -18))
                                                                                              (("2"
                                                                                                (assert)
                                                                                                (("2"
                                                                                                  (bddsimp)
                                                                                                  (("1"
                                                                                                    (grind)
                                                                                                    nil
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (grind)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("3"
                                                                                            (hide
                                                                                             2)
                                                                                            (("3"
                                                                                              (hide
                                                                                               -2
                                                                                               -5
                                                                                               -11
                                                                                               -12
                                                                                               -13
                                                                                               -14
                                                                                               -15
                                                                                               -16)
                                                                                              (("3"
                                                                                                (assert)
                                                                                                (("3"
                                                                                                  (bddsimp)
                                                                                                  (("3"
                                                                                                    (typepred
                                                                                                     "p!1")
                                                                                                    (("3"
                                                                                                      (reveal
                                                                                                       -13)
                                                                                                      (("3"
                                                                                                        (propax)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("4"
                                                                                            (hide
                                                                                             -4
                                                                                             -12
                                                                                             -15
                                                                                             3)
                                                                                            (("4"
                                                                                              (reveal
                                                                                               -8)
                                                                                              (("4"
                                                                                                (hide
                                                                                                 2)
                                                                                                (("4"
                                                                                                  (assert)
                                                                                                  (("4"
                                                                                                    (bddsimp)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("5"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("6"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("7"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("8"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (hide
                                                                                         -2
                                                                                         -9
                                                                                         -12
                                                                                         -15
                                                                                         2)
                                                                                        (("2"
                                                                                          (hide
                                                                                           -1)
                                                                                          (("2"
                                                                                            (grind)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("4"
                                                                                (assert
                                                                                 (-1
                                                                                  -2
                                                                                  1))
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (assert
                                                                             (-1
                                                                              1))
                                                                            nil
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (assert
                                                                           (-1
                                                                            1))
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("3"
                                                                      (inst
                                                                       -9
                                                                       "n!1")
                                                                      (("3"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (skosimp*)
                                                                  (("2"
                                                                    (inst
                                                                     -7
                                                                     "i!1")
                                                                    (("2"
                                                                      (bddsimp)
                                                                      (("2"
                                                                        (lemma
                                                                         "walk?_caret")
                                                                        (("2"
                                                                          (inst
                                                                           -1
                                                                           "G!1"
                                                                           "0"
                                                                           "i!1"
                                                                           "p!1")
                                                                          (("2"
                                                                            (typepred
                                                                             "i!1")
                                                                            (("2"
                                                                              (reveal
                                                                               -4)
                                                                              (("2"
                                                                                (inst
                                                                                 -1
                                                                                 "G!1"
                                                                                 "x!2"
                                                                                 "seq(p!1)(i!1)"
                                                                                 "p!1 ^ (0, i!1)")
                                                                                (("1"
                                                                                  (case
--> --------------------

--> maximum size reached

--> --------------------

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


Bot Zugriff