products/Sources/formale Sprachen/Java/openjdk-20-36_src/test/jdk/java/lang/AssertionError/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: tan_quad.pvs   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.22 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff