products/sources/formale sprachen/PVS/analysis/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: sort_fseq.prf   Sprache: Lisp

Original von: PVS©
(cross_metric_real_fun
 (IMP_cross_metric_uniform_continuity_TCC1 0
  (IMP_cross_metric_uniform_continuity_TCC1-1 nil 3460386756
   ("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil)
   ((fullset_metric_space1 formula-decl nil cross_metric_real_fun nil))
   nil))
 (IMP_cross_metric_uniform_continuity_TCC2 0
  (IMP_cross_metric_uniform_continuity_TCC2-1 nil 3460386756
   ("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil)
   ((fullset_metric_space2 formula-decl nil cross_metric_real_fun nil))
   nil))
 (IMP_cross_metric_uniform_continuity_TCC3 0
  (IMP_cross_metric_uniform_continuity_TCC3-1 nil 3460386756
   ("" (expand "metric_space?")
    (("" (expand "space_zero?")
      (("" (expand "space_symmetric?")
        (("" (expand "space_triangle?") (("" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((space_zero? const-decl "bool" metric_spaces_def nil)
    (space_triangle? const-decl "bool" metric_spaces_def nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (space_symmetric? const-decl "bool" metric_spaces_def nil)
    (metric_space? const-decl "bool" metric_spaces_def nil))
   nil))
 (curried_min_exists 0
  (curried_min_exists-1 nil 3461589573
   ("" (skosimp*)
    (("" (label "nonempty" -1)
      (("" (label "cont" -2)
        (("" (label "compact" -3)
          (("" (label "t1in" -4)
            (("" (label "final" 1)
              (("" (lemma "cont_on_compact_min")
                (("" (inst - "X!1" "(LAMBDA (x: T1): f!1(x,t!1))")
                  (("" (lemma "curried_is_uniform")
                    (("" (inst - "X!1" "Y!1" "f!1")
                      (("" (lemma "multiary_Heine")
                        (("" (inst - "X!1" "Y!1" "f!1")
                          (("" (lemma "unif_cont_implies_cont")
                            ((""
                              (inst - "X!1"
                               "(LAMBDA (x: T1): f!1(x,t!1))")
                              ((""
                                (assert)
                                ((""
                                  (inst - "t!1")
                                  ((""
                                    (assert)
                                    ((""
                                      (expand "nonempty?")
                                      ((""
                                        (assert)
                                        ((""
                                          (label "contLam" -1)
                                          ((""
                                            (label "ucif" -2)
                                            ((""
                                              (label "uclam" -3)
                                              ((""
                                                (label "min_exists" -4)
                                                ((""
                                                  (prop)
                                                  (("1"
                                                    (expand "empty?")
                                                    (("1"
                                                      (expand "member")
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst
                                                           "final"
                                                           "f!1(x!1,t!1)")
                                                          (("1"
                                                            (inst
                                                             +
                                                             "x!1")
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (expand
                                                     "below_bounded")
                                                    (("2"
                                                      (lemma
                                                       "axiom_of_archimedes")
                                                      (("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (inst
                                                           -1
                                                           "-f!1(s!1,t!1)")
                                                          (("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (inst
                                                               +
                                                               "-i!1-2")
                                                              (("2"
                                                                (expand
                                                                 "lower_bound")
                                                                (("2"
                                                                  (skosimp*)
                                                                  (("2"
                                                                    (typepred
                                                                     "z!1")
                                                                    (("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (inst
                                                                         "min_exists"
                                                                         "x!1")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("3"
                                                    (expand "ext")
                                                    (("3"
                                                      (skosimp*)
                                                      (("3"
                                                        (inst + "s!1")
                                                        (("3"
                                                          (lemma
                                                           "inf_def")
                                                          (("3"
                                                            (inst
                                                             -1
                                                             "{r: real | EXISTS (x: (X!1)): r = f!1(x, t!1)}"
                                                             "f!1(s!1,t!1)")
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (expand
                                                                 "greatest_lower_bound")
                                                                (("1"
                                                                  (expand
                                                                   "lower_bound")
                                                                  (("1"
                                                                    (split)
                                                                    (("1"
                                                                      (skosimp*)
                                                                      (("1"
                                                                        (typepred
                                                                         "z!1")
                                                                        (("1"
                                                                          (skosimp*)
                                                                          (("1"
                                                                            (inst
                                                                             "min_exists"
                                                                             "x!1")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (inst
                                                                         -
                                                                         "f!1(s!1,t!1)")
                                                                        (("2"
                                                                          (inst
                                                                           +
                                                                           "s!1")
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "nonempty?")
                                                              (("2"
                                                                (split)
                                                                (("1"
                                                                  (expand
                                                                   "empty?")
                                                                  (("1"
                                                                    (expand
                                                                     "member")
                                                                    (("1"
                                                                      (skosimp*)
                                                                      (("1"
                                                                        (inst
                                                                         -
                                                                         "f!1(x!1,t!1)")
                                                                        (("1"
                                                                          (inst
                                                                           +
                                                                           "x!1")
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "below_bounded")
                                                                  (("2"
                                                                    (lemma
                                                                     "axiom_of_archimedes")
                                                                    (("2"
                                                                      (inst
                                                                       -
                                                                       "-f!1(s!1,t!1)")
                                                                      (("2"
                                                                        (skosimp*)
                                                                        (("2"
                                                                          (inst
                                                                           +
                                                                           "-i!1-2")
                                                                          (("2"
                                                                            (expand
                                                                             "lower_bound")
                                                                            (("2"
                                                                              (skosimp*)
                                                                              (("2"
                                                                                (typepred
                                                                                 "z!1")
                                                                                (("2"
                                                                                  (skosimp*)
                                                                                  (("2"
                                                                                    (inst
                                                                                     "min_exists"
                                                                                     "x!1")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("4"
                                                    (skosimp*)
                                                    (("4"
                                                      (inst + "s!1")
                                                      (("4"
                                                        (skosimp*)
                                                        (("4"
                                                          (inst
                                                           -
                                                           "y!1")
                                                          (("4"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-nonempty-type-decl nil cross_metric_real_fun nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (x!1 skolem-const-decl "T1" cross_metric_real_fun nil)
    (X!1 skolem-const-decl "set[T1]" cross_metric_real_fun nil)
    (empty? const-decl "bool" sets nil)
    (axiom_of_archimedes formula-decl nil real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (lower_bound const-decl "bool" bound_defs "reals/")
    (minus_int_is_int application-judgement "int" integers nil)
    (below_bounded const-decl "bool" bounded_reals "reals/")
    (inf_def formula-decl nil bounded_reals "reals/")
    (x!1 skolem-const-decl "T1" cross_metric_real_fun nil)
    (s!1 skolem-const-decl "(X!1)" cross_metric_real_fun nil)
    (greatest_lower_bound const-decl "bool" bound_defs "reals/")
    (inf_set type-eq-decl nil bounded_reals "reals/")
    (setof type-eq-decl nil defined_types nil)
    (t!1 skolem-const-decl "T2" cross_metric_real_fun nil)
    (f!1 skolem-const-decl "[[T1, T2] -> real]" cross_metric_real_fun
     nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (ext const-decl "set[real]" bounded_reals "reals/")
    (unif_cont_implies_cont formula-decl nil uniform_continuity nil)
    (multiary_Heine formula-decl nil cross_metric_uniform_continuity
     nil)
    (curried_is_uniform formula-decl nil cross_metric_cont nil)
    (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_real_fun
     nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (cont_on_compact_min formula-decl nil real_fun_on_compact_sets nil)
    (T1 formal-nonempty-type-decl nil cross_metric_real_fun 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)
    (nnreal type-eq-decl nil real_types nil)
    (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_real_fun
     nil))
   nil))
 (curried_min_is_cont_TCC1 0
  (curried_min_is_cont_TCC1-1 nil 3460892462
   ("" (skosimp*)
    (("" (label "nonempty" -1)
      (("" (label "cont" -2)
        (("" (label "compact" -3)
          (("" (label "t1in" -4)
            (("" (label "final" 1)
              (("" (lemma "cont_on_compact_min")
                (("" (inst - "X!1" "(LAMBDA (x: T1): f!1(x,t!1))")
                  (("" (lemma "curried_is_uniform")
                    (("" (inst - "X!1" "Y!1" "f!1")
                      (("" (lemma "multiary_Heine")
                        (("" (inst - "X!1" "Y!1" "f!1")
                          (("" (lemma "unif_cont_implies_cont")
                            ((""
                              (inst - "X!1"
                               "(LAMBDA (x: T1): f!1(x,t!1))")
                              ((""
                                (assert)
                                ((""
                                  (inst - "t!1")
                                  ((""
                                    (assert)
                                    ((""
                                      (expand "nonempty?")
                                      ((""
                                        (assert)
                                        ((""
                                          (label "contLam" -1)
                                          ((""
                                            (label "ucif" -2)
                                            ((""
                                              (label "uclam" -3)
                                              ((""
                                                (label "min_exists" -4)
                                                ((""
                                                  (prop)
                                                  (("1"
                                                    (expand "empty?")
                                                    (("1"
                                                      (expand "member")
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst
                                                           "final"
                                                           "f!1(x!1,t!1)")
                                                          (("1"
                                                            (inst
                                                             +
                                                             "x!1")
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (expand
                                                     "below_bounded")
                                                    (("2"
                                                      (lemma
                                                       "axiom_of_archimedes")
                                                      (("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (inst
                                                           -1
                                                           "-f!1(s!1,t!1)")
                                                          (("2"
                                                            (skosimp*)
                                                            (("2"
                                                              (inst
                                                               +
                                                               "-i!1-2")
                                                              (("2"
                                                                (expand
                                                                 "lower_bound")
                                                                (("2"
                                                                  (skosimp*)
                                                                  (("2"
                                                                    (typepred
                                                                     "z!1")
                                                                    (("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (inst
                                                                         "min_exists"
                                                                         "x!1")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("3"
                                                    (expand "ext")
                                                    (("3"
                                                      (skosimp*)
                                                      (("3"
                                                        (inst + "s!1")
                                                        (("3"
                                                          (lemma
                                                           "inf_def")
                                                          (("3"
                                                            (inst
                                                             -1
                                                             "{r: real | EXISTS (x: (X!1)): r = f!1(x, t!1)}"
                                                             "f!1(s!1,t!1)")
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (expand
                                                                 "greatest_lower_bound")
                                                                (("1"
                                                                  (expand
                                                                   "lower_bound")
                                                                  (("1"
                                                                    (split)
                                                                    (("1"
                                                                      (skosimp*)
                                                                      (("1"
                                                                        (typepred
                                                                         "z!1")
                                                                        (("1"
                                                                          (skosimp*)
                                                                          (("1"
                                                                            (inst
                                                                             "min_exists"
                                                                             "x!1")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (skosimp*)
                                                                      (("2"
                                                                        (inst
                                                                         -
                                                                         "f!1(s!1,t!1)")
                                                                        (("2"
                                                                          (inst
                                                                           +
                                                                           "s!1")
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "nonempty?")
                                                              (("2"
                                                                (split)
                                                                (("1"
                                                                  (expand
                                                                   "empty?")
                                                                  (("1"
                                                                    (expand
                                                                     "member")
                                                                    (("1"
                                                                      (skosimp*)
                                                                      (("1"
                                                                        (inst
                                                                         -
                                                                         "f!1(x!1,t!1)")
                                                                        (("1"
                                                                          (inst
                                                                           +
                                                                           "x!1")
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "below_bounded")
                                                                  (("2"
                                                                    (lemma
                                                                     "axiom_of_archimedes")
                                                                    (("2"
                                                                      (inst
                                                                       -
                                                                       "-f!1(s!1,t!1)")
                                                                      (("2"
                                                                        (skosimp*)
                                                                        (("2"
                                                                          (inst
                                                                           +
                                                                           "-i!1-2")
                                                                          (("2"
                                                                            (expand
                                                                             "lower_bound")
                                                                            (("2"
                                                                              (skosimp*)
                                                                              (("2"
                                                                                (typepred
                                                                                 "z!1")
                                                                                (("2"
                                                                                  (skosimp*)
                                                                                  (("2"
                                                                                    (inst
                                                                                     "min_exists"
                                                                                     "x!1")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-nonempty-type-decl nil cross_metric_real_fun nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (x!1 skolem-const-decl "T1" cross_metric_real_fun nil)
    (X!1 skolem-const-decl "set[T1]" cross_metric_real_fun nil)
    (empty? const-decl "bool" sets nil)
    (axiom_of_archimedes formula-decl nil real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (lower_bound const-decl "bool" bound_defs "reals/")
    (minus_int_is_int application-judgement "int" integers nil)
    (below_bounded const-decl "bool" bounded_reals "reals/")
    (inf_def formula-decl nil bounded_reals "reals/")
    (x!1 skolem-const-decl "T1" cross_metric_real_fun nil)
    (s!1 skolem-const-decl "(X!1)" cross_metric_real_fun nil)
    (greatest_lower_bound const-decl "bool" bound_defs "reals/")
    (inf_set type-eq-decl nil bounded_reals "reals/")
    (setof type-eq-decl nil defined_types nil)
    (t!1 skolem-const-decl "T2" cross_metric_real_fun nil)
    (f!1 skolem-const-decl "[[T1, T2] -> real]" cross_metric_real_fun
     nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (ext const-decl "set[real]" bounded_reals "reals/")
    (unif_cont_implies_cont formula-decl nil uniform_continuity nil)
    (multiary_Heine formula-decl nil cross_metric_uniform_continuity
     nil)
    (curried_is_uniform formula-decl nil cross_metric_cont nil)
    (d2 formal-const-decl "[T2, T2 -> nnreal]" cross_metric_real_fun
     nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (cont_on_compact_min formula-decl nil real_fun_on_compact_sets nil)
    (T1 formal-nonempty-type-decl nil cross_metric_real_fun 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)
    (nnreal type-eq-decl nil real_types nil)
    (d1 formal-const-decl "[T1, T1 -> nnreal]" cross_metric_real_fun
     nil))
   nil))
 (curried_min_is_cont 0
  (curried_min_is_cont-1 nil 3460390218
   ("" (skosimp*)
    (("" (label "compact" -1)
      (("" (label "continuous" -2)
        (("" (label "nonempty" -3)
          (("" (label "final" 1)
            (("" (assert)
              (("" (lemma "multi_Heine_Corollary1")
                (("" (inst?)
                  (("" (assert)
                    (("" (lemma "cont_on_compact_min")
                      (("" (label "cocm" -1)
                        (("" (label "mhc1" -2)
                          (("" (lemma "curried_is_uniform")
                            (("" (label "cmic" -1)
                              ((""
                                (lemma "multiary_Heine")
                                ((""
                                  (inst?)
                                  ((""
                                    (assert)
                                    ((""
                                      (label "ucif" -1)
                                      ((""
                                        (inst "cmic" "X!1" "Y!1" "f!1")
                                        ((""
                                          (assert)
                                          ((""
                                            (expand
                                             "continuous?"
                                             "final")
                                            ((""
                                              (skosimp*)
                                              ((""
                                                (typepred "x!1")
                                                ((""
                                                  (label "tpx!1" -1)
                                                  ((""
                                                    (expand
                                                     "continuous_at?")
                                                    ((""
                                                      (expand "member")
                                                      ((""
                                                        (expand "ball")
                                                        ((""
                                                          (expand
                                                           "real_dist")
                                                          ((""
                                                            (skosimp*)
                                                            ((""
                                                              (inst
                                                               "mhc1"
                                                               "x!1"
                                                               "epsilon!1")
                                                              ((""
                                                                (skosimp*)
                                                                ((""
                                                                  (inst
                                                                   "final"
                                                                   "delta!1")
                                                                  ((""
                                                                    (skosimp*)
                                                                    ((""
                                                                      (typepred
                                                                       "y!1")
                                                                      ((""
                                                                        (label
                                                                         "tpy!1"
                                                                         -1)
                                                                        ((""
                                                                          (name
                                                                           "main_min"
                                                                           "min({r: real | EXISTS (x: (X!1)): r = f!1(x, x!1)})")
                                                                          (("1"
                                                                            (label
                                                                             "main_min"
                                                                             -1)
                                                                            (("1"
                                                                              (name
                                                                               "sec_min"
                                                                               "min({r: real | EXISTS (x: (X!1)): r = f!1(x, y!1)})")
                                                                              (("1"
                                                                                (label
                                                                                 "sec_min"
                                                                                 -1)
                                                                                (("1"
                                                                                  (replace
                                                                                   "main_min")
                                                                                  (("1"
                                                                                    (replace
                                                                                     "sec_min")
                                                                                    (("1"
                                                                                      (name
                                                                                       "main_slice"
                                                                                       "{r: real | EXISTS (x: (X!1)): r = f!1(x, x!1)}")
                                                                                      (("1"
                                                                                        (label
                                                                                         "main_slice"
                                                                                         -1)
                                                                                        (("1"
                                                                                          (name
                                                                                           "sec_slice"
                                                                                           "{r: real | EXISTS (x: (X!1)): r = f!1(x, y!1)}")
                                                                                          (("1"
                                                                                            (label
                                                                                             "sec_slice"
                                                                                             -1)
                                                                                            (("1"
                                                                                              (replace
                                                                                               "main_slice")
                                                                                              (("1"
                                                                                                (replace
                                                                                                 "sec_slice")
                                                                                                (("1"
                                                                                                  (inst-cp
                                                                                                   "cmic"
                                                                                                   "x!1")
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     "cmic"
                                                                                                     "y!1")
                                                                                                    (("1"
                                                                                                      (lemma
                                                                                                       "unif_cont_implies_cont")
                                                                                                      (("1"
                                                                                                        (inst-cp
                                                                                                         -1
                                                                                                         "X!1"
                                                                                                         "LAMBDA (t: T1): f!1(t, y!1)")
                                                                                                        (("1"
                                                                                                          (inst-cp
                                                                                                           -1
                                                                                                           "X!1"
                                                                                                           "LAMBDA (t: T1): f!1(t, x!1)")
                                                                                                          (("1"
                                                                                                            (hide
                                                                                                             -1)
                                                                                                            (("1"
                                                                                                              (label
                                                                                                               "cmicx"
                                                                                                               -1)
                                                                                                              (("1"
                                                                                                                (label
                                                                                                                 "cmicy"
                                                                                                                 -2)
                                                                                                                (("1"
                                                                                                                  (hide
                                                                                                                   "cmic")
                                                                                                                  (("1"
                                                                                                                    (copy
                                                                                                                     "cocm")
                                                                                                                    (("1"
                                                                                                                      (hide
                                                                                                                       "cocm")
                                                                                                                      (("1"
                                                                                                                        (inst-cp
                                                                                                                         -1
                                                                                                                         "X!1"
                                                                                                                         "LAMBDA (t: T1): f!1(t, x!1)")
                                                                                                                        (("1"
                                                                                                                          (label
                                                                                                                           "cocmx"
                                                                                                                           -2)
                                                                                                                          (("1"
                                                                                                                            (inst
                                                                                                                             -1
                                                                                                                             "X!1"
                                                                                                                             "LAMBDA (t: T1): f!1(t, y!1)")
                                                                                                                            (("1"
                                                                                                                              (label
                                                                                                                               "comcy"
                                                                                                                               -1)
                                                                                                                              (("1"
                                                                                                                                (hide
                                                                                                                                 ("tpy!1"
                                                                                                                                  "tpx!1"))
                                                                                                                                (("1"
                                                                                                                                  (lemma
                                                                                                                                   "curried_is_uniform")
                                                                                                                                  (("1"
                                                                                                                                    (inst?)
                                                                                                                                    (("1"
                                                                                                                                      (assert)
                                                                                                                                      (("1"
                                                                                                                                        (expand
                                                                                                                                         "nonempty?")
                                                                                                                                        (("1"
                                                                                                                                          (prop)
                                                                                                                                          (("1"
                                                                                                                                            (skosimp*)
                                                                                                                                            (("1"
                                                                                                                                              (expand
                                                                                                                                               "min")
                                                                                                                                              (("1"
                                                                                                                                                (lemma
                                                                                                                                                 "inf_def")
                                                                                                                                                (("1"
                                                                                                                                                  (inst-cp
                                                                                                                                                   -1
                                                                                                                                                   "main_slice"
                                                                                                                                                   "f!1(s!1,x!1)")
                                                                                                                                                  (("1"
                                                                                                                                                    (inst
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.109 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




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