Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: vect_trig_2D.prf Sprache: Lisp

Original von: PVS^©

(cont_if_fun
(discont_pts_lem 0
  (discont_pts_lem-1 nil 3440865406
   ("" (skeep)
    (("" (expand "discont_pts")
      (("" (expand "continuous?")
        (("" (inst - "1")
          (("" (skosimp*)
            (("" (expand "b2n")
              (("" (lift-if)
                (("" (case "P(a)")
                  (("1" (assert)
                    (("1" (inst + "delta!1")
                      (("1" (flatten)
                        (("1" (skosimp*)
                          (("1" (assert)
                            (("1" (inst - "x!1")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "abs")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert)
                    (("2" (inst + "delta!1")
                      (("2" (skosimp*)
                        (("2" (assert)
                          (("2" (inst - "x!2") (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((discont_pts const-decl "set[T]" cont_if_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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (b2n const-decl "nbit" bit nil)
    (abs_nat formula-decl nil abs_lems "reals/")
    (abs_0 formula-decl nil abs_lems "reals/")
    (real_ge_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)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (T formal-subtype-decl nil cont_if_fun nil)
    (T_pred const-decl "[real -> boolean]" cont_if_fun nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(if_fun_cont 0
  (if_fun_cont-2 nil 3440865362
   ("" (skeep)
    (("" (expand "continuous?")
      (("" (skeep)
        (("" (rewrite continuity_def)
          (("" (expand "if_fun")
            (("" (expand "continuous?")
              (("" (expand "convergence")
                (("" (expand "convergence")
                  (("" (expand "fullset")
                    (("" (prop)
                      (("1" (hide -)
                        (("1" (expand "adh")
                          (("1" (skosimp*)
                            (("1" (inst + x0) (("1" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (inst - "x0")
                          (("2" (inst -2 "x0")
                            (("2" (inst - "epsilon!1/2")
                              (("2"
                                (inst - "epsilon!1/2")
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (inst -3 "x0")
                                    (("2"
                                      (case "discont_pts(P)(x0)")
                                      (("1"
                                        (inst + "min(delta!1,delta!2)")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (case "P(x0)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (case "P(x!1)")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (inst -5 "x!1")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (inst -5 "x!1")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (case "P(x!1)")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (inst -4 "x!1")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (assert)
                                                (("2"
                                                  (inst -4 "x!1")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide -3)
                                        (("2"
                                          (lemma "discont_pts_lem")
                                          (("2"
                                            (inst?)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (skosimp*)
                                                (("2"
                                                  (split -1)
                                                  (("1"
                                                    (case "P(x0)")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (inst
                                                         +
                                                         "min(delta!1,delta!3)")
                                                        (("1"
                                                          (hide -4)
                                                          (("1"
                                                            (skosimp*)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "x!1")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "x!1")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (inst
                                                     +
                                                     "min(delta!2,delta!3)")
                                                    (("2"
                                                      (skosimp*)
                                                      (("2"
                                                        (inst - "x!1")
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (case
                                                             "P(x0)")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (reveal
                                                                 -1)
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "x0")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (assert)
                                                              (("2"
                                                                (inst
                                                                 -3
                                                                 "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)
   ((continuous? const-decl "bool" continuous_functions nil)
    (continuity_def formula-decl nil continuous_functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (if_fun const-decl "[T -> real]" cont_if_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)
    (T_pred const-decl "[real -> boolean]" cont_if_fun nil)
    (T formal-subtype-decl nil cont_if_fun nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (convergence const-decl "bool" convergence_functions nil)
    (adh const-decl "setof[real]" convergence_functions nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs_0 formula-decl nil abs_lems "reals/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (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) (set type-eq-decl nil sets nil)
    (discont_pts const-decl "set[T]" cont_if_fun 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)
    (discont_pts_lem formula-decl nil cont_if_fun nil)
    (b2n const-decl "nbit" bit nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (fullset const-decl "set" sets nil)
    (convergence const-decl "bool" lim_of_functions nil))
   nil)
  (if_fun_cont-1 nil 3440853945
   ("" (skeep)
    (("" (expand "continuous?")
      (("" (skeep)
        (("" (expand "if_fun")
          (("" (inst -3 "x0")
            (("" (case "discont_pts(P)(x0)")
              (("1" (expand "continuous?")
                (("1" (expand "convergence")
                  (("1" (expand "convergence")
                    (("1" (expand "fullset")
                      (("1" (prop)
                        (("1" (grind) nil nil)
                         ("2" (skosimp*)
                          (("2" (inst - "x0")
                            (("2" (inst - "x0")
                              (("2"
                                (flatten)
                                (("2"
                                  (inst - "epsilon!1/2")
                                  (("2"
                                    (inst - "epsilon!1/2")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (case "P(x0)")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (inst
                                             +
                                             "min(delta!1,delta!2)")
                                            (("1"
                                              (skosimp*)
                                              (("1"
                                                (case "P(x!1)")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (inst - "x!1")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (inst -8 "x!1")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
                                          (("2"
                                            (inst
                                             +
                                             "min(delta!1,delta!2)")
                                            (("2"
                                              (skosimp*)
                                              (("2"
                                                (case "P(x!1)")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (inst - "x!1")
                                                    (("1"
                                                      (inst - "x!1")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  (("2"
                                                    (inst - "x!1")
                                                    (("2"
                                                      (inst - "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)
               ("2" (expand "discont_pts")
                (("2" (expand "continuous?")
                  (("2" (expand "convergence")
                    (("2" (expand "convergence")
                      (("2" (expand "fullset")
                        (("2" (prop)
                          (("1" (skosimp*)
                            (("1" (inst -4 "x0")
                              (("1"
                                (inst -5 "x0")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (hide -4 -6)
                                    (("1"
                                      (inst -4 "epsilon!1/2")
                                      (("1"
                                        (inst -5 "epsilon!1/2")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (inst
                                             +
                                             "min(delta!1,delta!2)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (case "P(x0)")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (case "P(x!1)")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (inst
                                                           -7
                                                           "x!1")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        (("2"
                                                          (inst
                                                           -7
                                                           "x!1")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (case "P(x!1)")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (inst
                                                             -6
                                                             "x!1")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (assert)
                                                          (("2"
                                                            (inst
                                                             -6
                                                             "x!1")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skosimp*)
                            (("2" (case "P(x0)")
                              (("1"
                                (inst -6 "x0")
                                (("1"
                                  (inst -7 "x0")
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (hide -6 -8)
                                      (("1"
                                        (inst -6 "epsilon!1/2")
                                        (("1"
                                          (inst -7 "epsilon!1/2")
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (inst
                                               +
                                               "min(delta!1,delta!2)")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (skosimp*)
                                                  (("1"
                                                    (lift-if)
                                                    (("1"
                                                      (case "P(x!1)")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (inst
                                                           -8
                                                           "x!1")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        (("2"
                                                          (inst
                                                           -8
                                                           "x!1")
                                                          (("2"
                                                            (postpone)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (postpone) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
(discont_pts_simple 0
  (discont_pts_simple-2 nil 3440940498
   ("" (skosimp*)
    (("" (expand "discont_pts")
      (("" (expand "b2n")
        (("" (expand "continuous?")
          (("" (expand "continuous?")
            (("" (skosimp*)
              (("" (lift-if)
                (("" (case "P!1(x!1)")
                  (("1" (assert)
                    (("1" (inst - "x!1")
                      (("1" (inst -3 "x!1")
                        (("1" (replace -4 * lr)
                          (("1" (hide -4)
                            (("1" (assert)
                              (("1"
                                (flatten)
                                (("1"
                                  (inst - "f1!1(x!1)/2")
                                  (("1"
                                    (inst - "f2!1(x!1)/2")
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (inst + "min(delta!1,delta!2)")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (lift-if)
                                            (("1"
                                              (prop)
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (inst -4 "x!2")
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (inst -4 "x!2")
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (prop)
                                      (("1" (assert) nil nil)
                                       ("2" (assert) nil nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (prop)
                                    (("1" (assert) nil nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert)
                    (("2" (inst - "x!1")
                      (("2" (inst -2 "x!1")
                        (("2" (replace -3 * lr)
                          (("2" (assert)
                            (("2" (split 1)
                              (("1"
                                (inst - "-f1!1(x!1)/2")
                                (("1"
                                  (case "f2!1(x!1) > 0")
                                  (("1"
                                    (inst - "f2!1(x!1)/2")
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (inst + "min(delta!1,delta!2)")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (inst - "x!2")
                                            (("1"
                                              (inst - "x!2")
                                              (("1"
                                                (assert)
                                                (("1" (grind) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (assert) nil nil))
                                    nil)
                                   ("2"
                                    (inst - "-f2!1(x!1)/2")
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (inst + "min(delta!1,delta!2)")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (inst - "x!2")
                                            (("1"
                                              (inst - "x!2")
                                              (("1"
                                                (assert)
                                                (("1" (grind) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("2" (assert) nil nil))
                                nil)
                               ("2"
                                (assert)
                                (("2"
                                  (inst -2 "-f2!1(x!1)/2")
                                  (("2"
                                    (case "f1!1(x!1) > 0")
                                    (("1"
                                      (inst - "f1!1(x!1)/2")
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (inst
                                           +
                                           "min(delta!1,delta!2)")
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (inst - "x!2")
                                              (("1"
                                                (inst - "x!2")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (assert) nil nil))
                                      nil)
                                     ("2"
                                      (inst - "-f1!1(x!1)/2")
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (inst
                                           +
                                           "min(delta!1,delta!2)")
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (inst - "x!2")
                                              (("1"
                                                (inst - "x!2")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((discont_pts const-decl "set[T]" cont_if_fun nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (abs_nat formula-decl nil abs_lems "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (f2!1 skolem-const-decl "[T -> real]" cont_if_fun nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
     real_defs nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (abs_0 formula-decl nil abs_lems "reals/")
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (>= const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (f1!1 skolem-const-decl "[T -> real]" cont_if_fun nil)
    (x!1 skolem-const-decl "T" cont_if_fun nil)
    (> const-decl "bool" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (T_pred const-decl "[real -> boolean]" cont_if_fun nil)
    (T formal-subtype-decl nil cont_if_fun nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (b2n const-decl "nbit" bit nil))
   nil)
  (discont_pts_simple-1 nil 3440935759
   ("" (skosimp*)
    (("" (expand "discont_pts")
      (("" (expand "b2n")
        (("" (expand "continuous?")
          (("" (expand "continuous?")
            (("" (expand "convergence")
              (("" (expand "convergence")
                (("" (expand "fullset")
                  (("" (prop)
                    (("1" (grind) nil nil)
                     ("2" (skosimp*)
                      (("2" (lift-if)
                        (("2" (case "P!1(x!1)")
                          (("1" (assert)
                            (("1" (inst - "x!1")
                              (("1"
                                (inst - "x!1")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (hide -2 -4)
                                    (("1"
                                      (replace -4 * lr)
                                      (("1"
                                        (hide -4)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (inst - "f1!1(x!1)/2")
                                              (("1"
                                                (inst - "f2!1(x!1)/2")
                                                (("1"
                                                  (skosimp*)
                                                  (("1"
                                                    (inst
                                                     +
                                                     "min(delta!1,delta!2)")
                                                    (("1"
                                                      (skosimp*)
                                                      (("1"
                                                        (lift-if)
                                                        (("1"
                                                          (prop)
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (assert)
                                                            (("2"
                                                              (inst
                                                               -5
                                                               "x!2")
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("3"
                                                            (assert)
                                                            (("3"
                                                              (inst
                                                               -5
                                                               "x!2")
                                                              (("3"
                                                                (assert)
                                                                (("3"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (prop)
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (prop)
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert)
                            (("2" (inst - "x!1")
                              (("2"
                                (inst - "x!1")
                                (("2"
                                  (flatten)
                                  (("2"
                                    (hide -1 -3)
                                    (("2"
                                      (replace -3 * lr)
                                      (("2"
                                        (assert)
                                        (("2"
                                          (split 1)
                                          (("1"
                                            (inst - "-f1!1(x!1)/2")
                                            (("1"
                                              (inst - "-f2!1(x!1)/2")
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (inst
                                                   +
                                                   "min(delta!1,delta!2)")
                                                  (("1"
                                                    (skosimp*)
                                                    (("1"
                                                      (lift-if)
                                                      (("1"
                                                        (prop)
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (inst
                                                             -
                                                             "x!2")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "x!2")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (inst
                                                           -
                                                           "x!2")
                                                          (("2"
                                                            (inst
                                                             -
                                                             "x!2")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("3"
                                                          (inst
                                                           -
                                                           "x!2")
                                                          (("3"
                                                            (inst
                                                             -
                                                             "x!2")
                                                            (("3"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (postpone)
                                                nil
                                                nil))
                                              nil)
                                             ("2" (postpone) nil nil))
                                            nil)
                                           ("2"
                                            (assert)
                                            (("2" (postpone) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
(prod_fun_lem 0
  (prod_fun_lem-2 nil 3440931691
   ("" (skeep)
    (("" (lemma "discont_pts_simple")
      (("" (inst?)
        (("" (inst - "x")
          (("" (assert)
            (("" (split -1)
              (("1" (replace -1) (("1" (assert) nil nil)) nil)
               ("2" (replace -1) (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((discont_pts_simple formula-decl nil cont_if_fun nil)
    (abs_0 formula-decl nil abs_lems "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil cont_if_fun nil)
    (T_pred const-decl "[real -> boolean]" cont_if_fun 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil)
  (prod_fun_lem-1 nil 3440931385
   ("" (skeep)
    (("" (expand "discont_pts")
      (("" (expand "b2n")
        (("" (replace -1 * lr)
          (("" (hide -1)
            (("" (expand "continuous?")
              (("" (expand "convergence")
                (("" (expand "fullset")
                  (("" (expand "convergence")
                    (("" (prop)
                      (("1" (expand "adh")
                        (("1" (assert)
                          (("1" (skosimp*)
                            (("1" (inst + "x") (("1" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (inst + "epsilon!1")
                          (("2" (skosimp*)
                            (("2" (lift-if)
                              (("2"
                                (case "f1(x!1) > 0 AND f2(x!1) > 0")
                                (("1"
                                  (assert)
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (lift-if)
                                        (("1" (postpone) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (postpone) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak)))

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