Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: menger.prf Sprache: Lisp

Original von: PVS^©

(menger
(easy_menger 0
  (easy_menger-1 nil 3393145124
   ("" (skosimp*)
    (("" (expand "sep_num")
      (("" (lemma "injection_and_cardinal[Path_from(G!1,s!1,t!1),T]")
        (("" (inst?)
          (("" (assert)
            (("" (hide 2)
              ((""
                (case "FORALL (p: (ips!1)):
         nonempty?(intersection(min_sep_set(G!1, s!1, t!1),internal_verts(p)))")
                (("1" (expand "intersection")
                  (("1" (expand "member")
                    (("1"
                      (inst 1
                       "(LAMBDA (p: (ips!1)): choose({x: T | min_sep_set[T](G!1, s!1, t!1)(x) AND internal_verts(p)(x)}))")
                      (("1" (expand "injective?")
                        (("1" (skosimp*)
                          (("1" (typepred "x1!1")
                            (("1" (typepred "x2!1")
                              (("1"
                                (expand "path_from?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (expand "ind_path_set?")
                                    (("1"
                                      (inst -12 "x1!1" "x2!1")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand "independent?")
                                          (("1"
                                            (hide
                                             -1
                                             -2
                                             -3
                                             -4
                                             -5
                                             -6
                                             -7
                                             -8)
                                            (("1"
                                              (typepred
                                               "choose({x: T |
             min_sep_set[T](G!1, s!1, t!1)(x) AND internal_verts(x1!1)(x)})")
                                              (("1"
                                                (expand
                                                 "internal_verts")
                                                (("1"
                                                  (skosimp*)
                                                  (("1"
                                                    (hide -1)
                                                    (("1"
                                                      (replace -3 * rl)
                                                      (("1"
                                                        (hide -3)
                                                        (("1"
                                                          (typepred
                                                           "choose({x: T |
             min_sep_set[T](G!1, s!1, t!1)(x) AND internal_verts(x2!1)(x)})")
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (expand
                                                               "internal_verts")
                                                              (("1"
                                                                (skosimp*)
                                                                (("1"
                                                                  (replace
                                                                   -3
                                                                   *
                                                                   rl)
                                                                  (("1"
                                                                    (hide
                                                                     -3)
                                                                    (("1"
                                                                      (expand
                                                                       "finseq_appl")
                                                                      (("1"
                                                                        (inst
                                                                         -8
                                                                         "i!1"
                                                                         "i!2")
                                                                        (("1"
                                                                          (assert)
                                                                          nil)))))))))))))))
                                                           ("2"
                                                            (expand
                                                             "nonempty?")
                                                            (("2"
                                                              (expand
                                                               "empty?")
                                                              (("2"
                                                                (expand
                                                                 "member")
                                                                (("2"
                                                                  (inst
                                                                   -4
                                                                   "x2!1")
                                                                  (("2"
                                                                    (skosimp*)
                                                                    (("2"
                                                                      (inst?)
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (expand
                                                                           "internal_verts")
                                                                          (("2"
                                                                            (expand
                                                                             "finseq_appl")
                                                                            (("2"
                                                                              (inst
                                                                               +
                                                                               "i!2")
                                                                              (("2"
                                                                                (assert)
                                                                                nil)))))))))))))))))))))))))))))))))
                                               ("2"
                                                (inst -1 "x1!1")
                                                nil)))))))))))))))))))))))))
                       ("2" (skosimp*) (("2" (assert) nil)))))))))
                 ("2" (skosimp*)
                  (("2" (expand "nonempty?")
                    (("2" (lemma "min_sep_set_seps")
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (hide -4 1)
                            (("2" (expand "separates")
                              (("2"
                                (flatten)
                                (("2"
                                  (inst 3 "p!1")
                                  (("2"
                                    (hide -2 1 2)
                                    (("2"
                                      (typepred "p!1")
                                      (("2"
                                        (expand "path_from?")
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (expand "walk_from?")
                                            (("2"
                                              (expand "from?")
                                              (("2"
                                                (flatten)
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (lemma
                                                     "walk?_del_verts_not")
                                                    (("2"
                                                      (inst?)
                                                      (("2"
                                                        (expand
                                                         "path?")
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (hide
                                                               -1
                                                               -2
                                                               -3
                                                               -4
                                                               -5
                                                               -6
                                                               2)
                                                              (("2"
                                                                (reveal
                                                                 2
                                                                 3)
                                                                (("2"
                                                                  (name-replace
                                                                   "MSS"
                                                                   "min_sep_set(G!1, s!1, t!1)")
                                                                  (("2"
                                                                    (expand
                                                                     "intersection")
                                                                    (("2"
                                                                      (expand
                                                                       "empty?")
                                                                      (("2"
                                                                        (expand
                                                                         "member")
                                                                        (("2"
                                                                          (expand
                                                                           "verts_of")
                                                                          (("2"
                                                                            (expand
                                                                             "internal_verts")
                                                                            (("2"
                                                                              (expand
                                                                               "finseq_appl")
                                                                              (("2"
                                                                                (skosimp*)
                                                                                (("2"
                                                                                  (inst
                                                                                   -3
                                                                                   "x!1")
                                                                                  (("2"
                                                                                    (assert)
                                                                                    (("2"
                                                                                      (inst?)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    nil)
   ((sep_num const-decl "nat" sep_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set_of_paths type-eq-decl nil ind_paths nil)
    (min_sep_set const-decl "finite_set[T]" sep_sets nil)
    (min_sep_set_seps formula-decl nil sep_sets nil)
    (separates const-decl "bool" sep_sets nil)
    (from? const-decl "bool" walks nil)
    (verts_of const-decl "finite_set[T]" walks nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil) (path? const-decl "bool" paths nil)
    (walk?_del_verts_not formula-decl nil sep_sets nil)
    (walk_from? const-decl "bool" walks nil)
    (G!1 skolem-const-decl "graph[T]" menger nil)
    (s!1 skolem-const-decl "T" menger nil)
    (t!1 skolem-const-decl "T" menger nil)
    (ips!1 skolem-const-decl "set_of_paths[T](G!1, s!1, t!1)" menger
     nil)
    (choose const-decl "(p)" sets nil)
    (independent? const-decl "bool" ind_paths nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (empty? const-decl "bool" sets nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ind_path_set? const-decl "bool" ind_paths nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (injective? const-decl "bool" functions nil)
    (member const-decl "bool" sets nil)
    (internal_verts const-decl "finite_set[T]" ind_paths nil)
    (intersection const-decl "set" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (injection_and_cardinal formula-decl nil finite_sets_card_eq
     "finite_sets/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil menger nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (path_from? const-decl "bool" paths nil)
    (Path_from type-eq-decl nil paths nil))
   nil))
(hard_menger 0
  (hard_menger-1 nil 3393145124
   ("" (skosimp*)
    (("" (lemma "hard_menger_trad")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((T formal-type-decl nil menger nil)
    (hard_menger_trad formula-decl nil k_menger nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers 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)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)))

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