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


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Dedekind_Real.thy   Sprache: Lisp

Original von: PVS©

(vect2_cont_dot
 (dot_cont_vr 0
  (dot_cont_vr-2 nil 3445266811
   ("" (skeep)
    (("" (typepred "vv1")
      (("" (typepred "vv2")
        (("" (expand "continuous_vv")
          (("" (expand "continuous_vr")
            (("" (expand "continuous_vr?")
              (("" (expand "continuous_vv?")
                (("" (skeep)
                  (("" (expand "continuous_vr?")
                    (("" (expand "continuous_vv?")
                      (("" (skosimp*)
                        (("" (inst - "x0")
                          (("" (inst -2 "x0")
                            (("" (inst-cp -2 "1")
                              ((""
                                (skosimp*)
                                ((""
                                  (case
                                   "FORALL (x: Vect2): norm(x - x0) < delta!1 IMPLIES norm(vv1(x)) < 1 + norm(vv1(x0))")
                                  (("1"
                                    (hide -4)
                                    (("1"
                                      (name "r" "1 + norm(vv1(x0))")
                                      (("1"
                                        (inst -3 "epsilon!1/(2*r)")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (case "norm(vv2(x0)) = 0")
                                            (("1"
                                              (lemma "norm_eq_0")
                                              (("1"
                                                (inst?)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (replace -1 * lr)
                                                    (("1"
                                                      (hide -1)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (hide -5)
                                                          (("1"
                                                            (inst
                                                             +
                                                             "min(delta!1,delta!2)")
                                                            (("1"
                                                              (skosimp*)
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "x!1")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "x!1")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (lemma
                                                                       "schwarz")
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (replace
                                                                           -3)
                                                                          (("1"
                                                                            (mult-ineq
                                                                             -3
                                                                             -4)
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (case-replace
                                                                                 "r * (epsilon!1 / (2 * r)) = epsilon!1/2")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide-all-but
                                                                                   1)
                                                                                  (("2"
                                                                                    (cross-mult
                                                                                     1)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (inst
                                               -4
                                               "epsilon!1/(2*norm(vv2(x0)))")
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (inst
                                                   +
                                                   "min(min(delta!1,delta!2),delta!3)")
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (inst - "x!1")
                                                      (("1"
                                                        (inst - "x!1")
                                                        (("1"
                                                          (inst
                                                           -
                                                           "x!1")
                                                          (("1"
                                                            (case
                                                             "abs(vv1(x!1) * vv2(x!1) - vv1(x0) * vv2(x0)) <= norm(vv2(x0)) * norm((vv1(x!1) - vv1(x0))) + norm(vv1(x!1)) * norm((vv2(x!1) - vv2(x0)))")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (case
                                                                 "norm(vv1(x!1)) * norm((vv2(x!1) - vv2(x0))) )
                                                                (("1"
                                                                  (case
                                                                   "norm(vv2(x0)) * norm((vv1(x!1) - vv1(x0))) < epsilon!1/2")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (hide
                                                                       -1
                                                                       -2
                                                                       -3
                                                                       -5
                                                                       2)
                                                                      (("2"
                                                                        (cross-mult
                                                                         -2)
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   -1
                                                                   3)
                                                                  (("2"
                                                                    (replace
                                                                     -1)
                                                                    (("2"
                                                                      (mult-ineq
                                                                       -2
                                                                       -3)
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (case
                                                                           "r * (epsilon!1 / (2 * r)) = epsilon!1/2")
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
                                                                             1)
                                                                            (("2"
                                                                              (cross-mult
                                                                               1)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (hide 3)
                                                              (("2"
                                                                (lemma
                                                                 "triangle")
                                                                (("2"
                                                                  (inst
                                                                   -1
                                                                   "vv1(x!1) * (vv2(x!1) - vv2(x0))"
                                                                   "vv2(x0)*(vv1(x!1) - vv1(x0))")
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (lemma
                                                                       "schwarz")
                                                                      (("2"
                                                                        (inst-cp
                                                                         -1
                                                                         "vv1(x!1)"
                                                                         "(vv2(x!1) - vv2(x0))")
                                                                        (("2"
                                                                          (inst
                                                                           -
                                                                           "vv2(x0)"
                                                                           "(vv1(x!1) - vv1(x0))")
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (hide
                                                                               -4
                                                                               -5
                                                                               -6
                                                                               -7
                                                                               -8)
                                                                              (("2"
                                                                                (grind
                                                                                 :exclude
                                                                                 ("norm"
                                                                                  "abs"))
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide -2 -3 3)
                                                (("2"
                                                  (case
                                                   "epsilon!1 / (2 * norm(vv2(x0))) > 0")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (hide 2)
                                                    (("2"
                                                      (cross-mult 1)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("3"
                                                    (flatten)
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (flatten)
                                                (("3"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (hide -1 -2)
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (inst?)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (hide -1)
                                              (("2"
                                                (lemma "norm_sub_ge")
                                                (("2"
                                                  (inst?)
                                                  (("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)
   ((continuous_vv? const-decl "bool" cont_vect2_vect2 nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (continuous_vr? const-decl "bool" cont_vect2_real nil)
    (continuous_vv? const-decl "bool" cont_vect2_vect2 nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (< const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (vv2 skolem-const-decl "{f: [Vect2 -> Vect2] | continuous_vv?(f)}"
     vect2_cont_dot nil)
    (x0 skolem-const-decl "Vect2" vect2_cont_dot nil)
    (epsilon!1 skolem-const-decl "posreal" vect2_cont_dot nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (triangle formula-decl nil real_props nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (* const-decl "real" vectors_2D "vectors/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (norm_eq_0 formula-decl nil vectors_2D "vectors/")
    (schwarz formula-decl nil vectors_2D "vectors/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (times_div1 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (lt_times_lt_any1 formula-decl nil extra_real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (dot_zero_right formula-decl nil vectors_2D "vectors/")
    (sub_zero_right formula-decl nil vectors_2D "vectors/")
    (norm_zero formula-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (norm_sub_ge formula-decl nil vectors_2D "vectors/")
    (continuous_vr? const-decl "bool" cont_vect2_real nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)
  (dot_cont_vr-1 nil 3445172424
   ("" (skeep) (("" (postpone) nil nil)) nilnil shostak))
 (dot_cont_rr 0
  (dot_cont_rr-3 nil 3445259881
   ("" (skeep)
    (("" (typepred "rv1")
      (("" (typepred "rv2")
        (("" (expand "continuous?")
          (("" (skeep)
            (("" (rewrite "continuous_functions[T].continuity_def")
              (("" (expand "continuous_rv?")
                (("" (expand "convergence")
                  (("" (expand "convergence")
                    (("" (split +)
                      (("1" (hide -)
                        (("1" (expand "fullset")
                          (("1" (expand "adh")
                            (("1" (skosimp*)
                              (("1"
                                (inst?)
                                (("1" (assertnil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (expand "fullset")
                          (("2" (inst - "x0")
                            (("2" (inst -2 "x0")
                              (("2"
                                (expand "continuous_rv?")
                                (("2"
                                  (inst-cp -2 "1")
                                  (("2"
                                    (skosimp*)
                                    (("2"
                                      (case
                                       "FORALL x: abs(x - x0) < delta!1 IMPLIES norm(rv1(x)) < 1 + norm(rv1(x0))")
                                      (("1"
                                        (hide -4)
                                        (("1"
                                          (name
                                           "r"
                                           "1 + norm(rv1(x0))")
                                          (("1"
                                            (inst -3 "epsilon!1/(2*r)")
                                            (("1"
                                              (skosimp*)
                                              (("1"
                                                (case
                                                 "norm(rv2(x0)) = 0")
                                                (("1"
                                                  (lemma "norm_eq_0")
                                                  (("1"
                                                    (inst?)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (replace
                                                         -1
                                                         *
                                                         lr)
                                                        (("1"
                                                          (hide -1)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (hide -5)
                                                              (("1"
                                                                (inst
                                                                 +
                                                                 "min(delta!1,delta!2)")
                                                                (("1"
                                                                  (skosimp*)
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "x!1")
                                                                    (("1"
                                                                      (inst
                                                                       -
                                                                       "x!1")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (lemma
                                                                           "schwarz")
                                                                          (("1"
                                                                            (inst?)
                                                                            (("1"
                                                                              (replace
                                                                               -3)
                                                                              (("1"
                                                                                (mult-ineq
                                                                                 -3
                                                                                 -5)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (case-replace
                                                                                     "r * (epsilon!1 / (2 * r)) = epsilon!1/2")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil)
                                                                                     ("2"
                                                                                      (hide-all-but
                                                                                       1)
                                                                                      (("2"
                                                                                        (cross-mult
                                                                                         1)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (inst
                                                   -4
                                                   "epsilon!1/(2*norm(rv2(x0)))")
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (inst
                                                       +
                                                       "min(min(delta!1,delta!2),delta!3)")
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst
                                                           -
                                                           "x!1")
                                                          (("1"
                                                            (inst
                                                             -
                                                             "x!1")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "x!1")
                                                              (("1"
                                                                (case
                                                                 "abs(rv1(x!1) * rv2(x!1) - rv1(x0) * rv2(x0)) <= norm(rv2(x0)) * norm((rv1(x!1) - rv1(x0))) + norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0)))")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (case
                                                                     "norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0))) )
                                                                    (("1"
                                                                      (case
                                                                       "norm(rv2(x0)) * norm((rv1(x!1) - rv1(x0))) < epsilon!1/2")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (hide
                                                                         -1
                                                                         -2
                                                                         -6
                                                                         2)
                                                                        (("2"
                                                                          (cross-mult
                                                                           -4)
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       -1
                                                                       -6
                                                                       3)
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (replace
                                                                           -1)
                                                                          (("2"
                                                                            (mult-ineq
                                                                             -2
                                                                             -4)
                                                                            (("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (case
                                                                                 "r * (epsilon!1 / (2 * r)) = epsilon!1/2")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide-all-but
                                                                                   1)
                                                                                  (("2"
                                                                                    (cross-mult
                                                                                     1)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   3)
                                                                  (("2"
                                                                    (lemma
                                                                     "triangle")
                                                                    (("2"
                                                                      (inst
                                                                       -1
                                                                       "rv1(x!1) * (rv2(x!1) - rv2(x0))"
                                                                       "rv2(x0)*(rv1(x!1) - rv1(x0))")
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (lemma
                                                                           "schwarz")
                                                                          (("2"
                                                                            (inst-cp
                                                                             -1
                                                                             "rv1(x!1)"
                                                                             "(rv2(x!1) - rv2(x0))")
                                                                            (("2"
                                                                              (inst
                                                                               -
                                                                               "rv2(x0)"
                                                                               "(rv1(x!1) - rv1(x0))")
                                                                              (("2"
                                                                                (assert)
                                                                                (("2"
                                                                                  (hide
                                                                                   -4
                                                                                   -5
                                                                                   -6
                                                                                   -7
                                                                                   -8)
                                                                                  (("2"
                                                                                    (grind
                                                                                     :exclude
                                                                                     ("norm"
                                                                                      "abs"))
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide -2 -3 3)
                                                    (("2"
                                                      (case
                                                       "epsilon!1 / (2 * norm(rv2(x0))) > 0")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil)
                                                       ("2"
                                                        (hide 2)
                                                        (("2"
                                                          (cross-mult
                                                           1)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (flatten)
                                                        (("3"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("3"
                                                    (flatten)
                                                    (("3"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (hide -1 -2)
                                          (("2"
                                            (skosimp*)
                                            (("2"
                                              (inst?)
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (hide -1)
                                                  (("2"
                                                    (lemma
                                                     "norm_sub_ge")
                                                    (("2"
                                                      (inst?)
                                                      (("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)
   ((continuous_rv? const-decl "bool" cont_real_vect2 nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (T formal-subtype-decl nil vect2_cont_dot nil)
    (T_pred const-decl "[real -> boolean]" vect2_cont_dot 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)
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (continuity_def formula-decl nil continuous_functions "analysis/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (convergence const-decl "bool" lim_of_functions "analysis/")
    (fullset const-decl "set" sets nil)
    (abs_0 formula-decl nil abs_lems "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (adh const-decl "setof[real]" convergence_functions "analysis/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (rv2 skolem-const-decl "{f: [T -> Vect2] | continuous_rv?(f)}"
     vect2_cont_dot nil)
    (x0 skolem-const-decl "T" vect2_cont_dot nil)
    (epsilon!1 skolem-const-decl "posreal" vect2_cont_dot nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (triangle formula-decl nil real_props nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (norm_eq_0 formula-decl nil vectors_2D "vectors/")
    (schwarz formula-decl nil vectors_2D "vectors/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (times_div1 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (lt_times_lt_any1 formula-decl nil extra_real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (sub_zero_right formula-decl nil vectors_2D "vectors/")
    (dot_zero_right formula-decl nil vectors_2D "vectors/")
    (norm_zero formula-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (norm_sub_ge formula-decl nil vectors_2D "vectors/")
    (continuous_rv? const-decl "bool" cont_real_vect2 nil)
    (convergence const-decl "bool" convergence_functions "analysis/")
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)
  (dot_cont_rr-2 nil 3445259024
   ("" (skeep)
    (("" (typepred "rv1")
      (("" (typepred "rv2")
        (("" (expand "continuous_rv")
          (("" (expand "continuous?")
            (("" (expand "continuous")
              (("" (skosimp*)
                (("" (expand "continuous")
                  (("" (expand "continuous?")
                    (("" (expand "convergence")
                      (("" (expand "convergence")
                        (("" (split +)
                          (("1" (hide -)
                            (("1" (expand "fullset")
                              (("1"
                                (expand "adh")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (inst?)
                                    (("1" (assertnil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skosimp*)
                            (("2" (expand "fullset")
                              (("2"
                                (inst - "x0!1")
                                (("2"
                                  (inst -2 "x0!1")
                                  (("2"
                                    (inst-cp -2 "1")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (case
                                         "FORALL x: abs(x - x0!1) < delta!1 IMPLIES norm(rv1(x)) < 1 + norm(rv1(x0!1))")
                                        (("1"
                                          (hide -4)
                                          (("1"
                                            (name
                                             "r"
                                             "1 + norm(rv1(x0!1))")
                                            (("1"
                                              (inst
                                               -3
                                               "epsilon!1/(2*r)")
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (inst
                                                   -4
                                                   "epsilon!1/(2*norm(rv2(x0!1)))")
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (inst
                                                       +
                                                       "min(min(delta!1,delta!2),delta!3)")
                                                      (("1"
                                                        (skosimp*)
                                                        (("1"
                                                          (inst
                                                           -
                                                           "x!1")
                                                          (("1"
                                                            (inst
                                                             -
                                                             "x!1")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "x!1")
                                                              (("1"
                                                                (case-replace
                                                                 "abs(rv1(x!1) * rv2(x!1) - rv1(x0!1) * rv2(x0!1)) < norm(rv2(x0!1)) * norm((rv1(x!1) - rv1(x0!1))) + norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0!1)))")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (case
                                                                     "norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0!1))) )
                                                                    (("1"
                                                                      (case
                                                                       "norm(rv2(x0!1)) * norm((rv1(x!1) - rv1(x0!1))) < epsilon!1/2")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (hide
                                                                         2)
                                                                        (("2"
                                                                          (hide
                                                                           -1
                                                                           -2
                                                                           -6)
                                                                          (("2"
                                                                            (cross-mult
                                                                             -4)
                                                                            (("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       -1
                                                                       -6
                                                                       2)
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (replace
                                                                           -1)
                                                                          (("2"
                                                                            (mult-ineq
                                                                             -2
                                                                             -4)
                                                                            (("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (case
                                                                                 "r * (epsilon!1 / (2 * r)) = epsilon!1/2")
--> --------------------

--> maximum size reached

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

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