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: old_menger.prf   Sprache: Lisp

Original von: PVS©
(old_menger
 (easy_menger 0
  (easy_menger-1 nil 3507100603
   ("" (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]" old_menger nil)
    (s!1 skolem-const-decl "T" old_menger nil)
    (t!1 skolem-const-decl "T" old_menger nil)
    (ips!1 skolem-const-decl "set_of_paths[T](G!1, s!1, t!1)"
     old_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 old_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 3507100603
   ("" (skosimp*)
    (("" (lemma "h_menger")
      (("" (inst?)
        (("" (assert)
          (("" (skosimp*)
            ((""
              (inst +
               "add(p1!1,singleton[Path_from(G!1,s!1,t!1)](p2!1))")
              (("1" (rewrite "card_add[Path_from(G!1, s!1, t!1)]")
                (("1"
                  (rewrite "card_singleton[Path_from(G!1, s!1, t!1)]")
                  (("1" (assert)
                    (("1" (split +)
                      (("1" (lift-if)
                        (("1" (ground)
                          (("1" (expand "singleton")
                            (("1" (replace -1)
                              (("1"
                                (hide -1)
                                (("1"
                                  (case "length(p2!1) = 2")
                                  (("1"
                                    (expand "path_from?")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (hide -4 -5)
                                        (("1"
                                          (expand "path?")
                                          (("1"
                                            (expand "walk?")
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (hide -2 -4)
                                                (("1"
                                                  (inst - "0")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (expand
                                                       "finseq_appl")
                                                      (("1"
                                                        (expand
                                                         "separable?")
                                                        (("1"
                                                          (flatten)
                                                          (("1"
                                                            (expand
                                                             "from?")
                                                            (("1"
                                                              (flatten)
                                                              (("1"
                                                                (assert)
                                                                nil)))))))))))))))))))))))))))))
                                   ("2"
                                    (expand "independent?")
                                    (("2"
                                      (expand "path_from?")
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (inst -5 "1" "1")
                                          (("2"
                                            (assert)
                                            (("2"
                                              (case "length(p2!1) = 1")
                                              (("1"
                                                (expand "from?")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (expand
                                                       "separable?")
                                                      (("1"
                                                        (propax)
                                                        nil)))))))))
                                               ("2"
                                                (assert)
                                                nil)))))))))))))))))))))))))
                       ("2" (expand "ind_path_set?")
                        (("2" (skosimp*)
                          (("2" (expand "add")
                            (("2" (expand "member")
                              (("2"
                                (expand "singleton")
                                (("2"
                                  (lemma "independent?_comm")
                                  (("2"
                                    (inst -1 "p1!1" "p2!1")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (ground)
                                        nil)))))))))))))))))))))))
                 ("2" (hide 2)
                  (("2"
                    (rewrite
                     "finite_singleton[Path_from(G!1, s!1, t!1)]")
                    nil)))))
               ("2" (rewrite "finite_add[Path_from(G!1, s!1, t!1)]")
                (("2"
                  (rewrite
                   "finite_singleton[Path_from(G!1, s!1, t!1)]")
                  nil))))))))))))))
    nil)
   ((T formal-type-decl nil old_menger nil)
    (h_menger formula-decl nil h_menger nil)
    (nonempty_add_finite application-judgement "non_empty_finite_set"
     finite_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (t!1 skolem-const-decl "T" old_menger nil)
    (s!1 skolem-const-decl "T" old_menger nil)
    (p1!1 skolem-const-decl "prewalk[T]" old_menger nil)
    (G!1 skolem-const-decl "graph[T]" old_menger nil)
    (path_from? const-decl "bool" paths nil)
    (prewalk type-eq-decl nil walks nil)
    (> const-decl "bool" reals 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)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (p2!1 skolem-const-decl "prewalk[T]" old_menger nil)
    (Path_from type-eq-decl nil paths nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set_of_paths type-eq-decl nil ind_paths nil)
    (nonempty? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (card_singleton formula-decl nil finite_sets nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (path? const-decl "bool" paths 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)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (from? const-decl "bool" walks nil)
    (separable? const-decl "bool" sep_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (walk? const-decl "bool" walks nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (independent? const-decl "bool" ind_paths nil)
    (member const-decl "bool" sets nil)
    (independent?_comm formula-decl nil ind_paths nil)
    (ind_path_set? const-decl "bool" ind_paths nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (card_add formula-decl nil finite_sets 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))
 (easy_meng_1 0
  (easy_meng_1-1 nil 3507100603
   ("" (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]" old_menger nil)
    (s!1 skolem-const-decl "T" old_menger nil)
    (t!1 skolem-const-decl "T" old_menger nil)
    (ips!1 skolem-const-decl "set_of_paths[T](G!1, s!1, t!1)"
     old_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 old_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)))


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