Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: metric_space_real_fun.pvs   Sprache: Lisp

Untersuchung 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.65 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik