Quelle interm_value_thm.prf Sprache: Lisp

(interm_value_thm
(interm_value1_TCC1 0
  (interm_value1_TCC1-1 nil 3424520920 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (real nonempty-type-from-decl nil reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(interm_value1_TCC2 0
  (interm_value1_TCC2-1 nil 3424520920 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (real nonempty-type-from-decl nil reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(interm_value1 0
  (interm_value1-1 nil 3424520931
   ("" (skosimp*)
    (("" (lemma "intermediate_value1[a!1,b!1]")
      (("1" (inst?) (("1" (assert) nil nil)) nil)
       ("2" (assert) nil nil))
      nil))
    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)
    (intermediate_value1 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
(interm_value2_TCC1 0
  (interm_value2_TCC1-1 nil 3424520920 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (real nonempty-type-from-decl nil reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(interm_value2 0
  (interm_value2-1 nil 3424525492
   ("" (skosimp*)
    (("" (lemma "intermediate_value2[a!1,b!1]")
      (("1" (inst?) (("1" (assert) nil nil)) nil)
       ("2" (assert) nil nil))
      nil))
    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)
    (intermediate_value2 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil))
(interm_value3_TCC1 0
  (interm_value3_TCC1-1 nil 3424520920 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (real nonempty-type-from-decl nil reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(interm_value3 0
  (interm_value3-1 nil 3424525507
   ("" (skosimp*)
    (("" (lemma "intermediate_value3[a!1,b!1]")
      (("1" (inst?) (("1" (assert) nil nil)) nil)
       ("2" (assert) nil nil))
      nil))
    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)
    (intermediate_value3 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil))
(interm_value4 0
  (interm_value4-2 nil 3424525620
   ("" (skosimp*)
    (("" (lemma "intermediate_value4[a!1,b!1]")
      (("1" (inst?) (("1" (assert) nil nil)) nil)
       ("2" (assert) nil nil))
      nil))
    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)
    (intermediate_value4 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil)
  (interm_value4-1 nil 3424525518
   (";;; Proof interm_value1-1 for formula continuity_intv.interm_value1"
    (skosimp*)
    ((";;; Proof interm_value1-1 for formula continuity_intv.interm_value1"
      (lemma "intermediate_value1[a!1,b!1]")
      (("1" (inst?) (("1" (assert) nil))) ("2" (assert) nil))))
    ";;; developed with shostak decision procedures")
   nil nil))
(interm_value5 0
  (interm_value5-1 nil 3501251206
   ("" (skeep)
    (("" (skeep)
      (("" (lemma "interm_value2")
        (("" (case "p)
          (("1" (inst - "p" "q" "x")
            (("1" (assert)
              (("1"
                (name "fpq"
                      "(LAMBDA (xy:closed_interval(p,q)): f(xy))")
                (("1" (inst - "fpq")
                  (("1" (split -)
                    (("1" (skosimp*)
                      (("1" (inst + "c!1")
                        (("1" (assert)
                          (("1" (expand "fpq") (("1" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (hide -1)
                        (("2" (expand "continuous?")
                          (("2" (skosimp*)
                            (("2" (inst - "x0!1")
                              (("2"
                                (expand "continuous?")
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (inst - "epsilon!1")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst + "delta!1")
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (inst - "x!1")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (expand "fpq")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("3" (expand "fpq") (("3" (propax) nil nil)) nil)
                     ("4" (expand "fpq") (("4" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide -1)
            (("2" (lemma "interm_value4")
              (("2" (inst - "q" "p" "x")
                (("2" (case "q/=p")
                  (("1" (flatten)
                    (("1" (assert)
                      (("1"
                        (name "fqp"
                              "(LAMBDA (xy:closed_interval(q,p)): f(xy))")
                        (("1" (inst - "fqp")
                          (("1" (split -)
                            (("1" (skosimp*)
                              (("1"
                                (inst + "c!1")
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "fqp")
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 4)
                              (("2"
                                (hide -1)
                                (("2"
                                  (expand "continuous?")
                                  (("2"
                                    (skosimp*)
                                    (("2"
                                      (inst - "x0!1")
                                      (("2"
                                        (expand "continuous?")
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (inst - "epsilon!1")
                                            (("2"
                                              (skosimp*)
                                              (("2"
                                                (inst + "delta!1")
                                                (("2"
                                                  (skosimp*)
                                                  (("2"
                                                    (inst - "x!1")
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (expand "fqp")
                                                        (("2"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (expand "fqp")
                              (("3" (propax) nil nil)) nil)
                             ("4" (expand "fqp")
                              (("4" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (flatten)
                    (("2" (inst + "p") (("2" (ground) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((closed_interval type-eq-decl nil intervals_real "reals/")
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (fpq skolem-const-decl "[closed_interval[real](p, q) -> real]"
     interm_value_thm nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (interm_value4 formula-decl nil interm_value_thm nil)
    (/= const-decl "boolean" notequal nil)
    (fqp skolem-const-decl "[closed_interval[real](q, p) -> real]"
     interm_value_thm nil)
    (interm_value2 formula-decl nil interm_value_thm nil))
   nil))
(cont_intv 0
  (cont_intv-1 nil 3424526031
   ("" (skosimp*)
    (("" (expand "continuous?")
      (("" (skosimp*)
        (("" (inst - "x0!1")
          (("" (expand "continuous?")
            (("" (skosimp*)
              (("" (inst - "epsilon!1")
                (("" (skosimp*)
                  (("" (inst + "delta!1")
                    (("" (skosimp*)
                      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous? const-decl "bool" continuous_functions 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (closed_interval type-eq-decl nil intervals_real "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)
    (>= 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)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(cont_intv1 0
  (cont_intv1-1 nil 3424525844
   ("" (skosimp*)
    (("" (expand "restrict") (("" (propax) nil nil)) nil)) nil)
   ((restrict const-decl "R" restrict nil)) nil))
(interm_val1 0
  (interm_val1-2 nil 3424525975
   ("" (skosimp*)
    (("" (lemma "intermediate_value1[a!1,b!1]")
      (("1" (inst?)
        (("1" (assert)
          (("1" (split -1)
            (("1" (propax) nil nil)
             ("2" (hide 2)
              (("2" (assert)
                (("2" (expand "restrict") (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    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)
    (intermediate_value1 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (restrict const-decl "R" restrict nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil)
  (interm_val1-1 nil 3424521582
   ("" (skosimp*)
    (("" (lemma "intermediate_value1[a!1,b!1]")
      (("1" (inst?)
        (("1" (assert)
          (("1" (split -1)
            (("1" (propax) nil nil)
             ("2" (hide 2)
              (("2" (lemma "help")
                (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((J nonempty-type-eq-decl nil continuity_interval nil)
    (intermediate_value1 formula-decl nil continuity_interval nil))
   shostak))
(interm_val2 0
  (interm_val2-2 nil 3424526085
   ("" (skosimp*)
    (("" (lemma "intermediate_value2[a!1,b!1]")
      (("1" (inst?)
        (("1" (assert)
          (("1" (split -1)
            (("1" (propax) nil nil)
             ("2" (hide 2)
              (("2" (assert)
                (("2" (expand "restrict") (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    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)
    (intermediate_value2 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (restrict const-decl "R" restrict nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil)
  (interm_val2-1 nil 3424525950
   (";;; Proof interm_val1-1 for formula continuity_intv.interm_val1"
    (skosimp*)
    ((";;; Proof interm_val1-1 for formula continuity_intv.interm_val1"
      (lemma "intermediate_value2[a!1,b!1]")
      (("1" (inst?)
        (("1" (assert)
          (("1" (split -1)
            (("1" (propax) nil)
             ("2" (hide 2)
              (("2" (lemma "help")
                (("2" (inst?) (("2" (assert) nil)))))))))))))
       ("2" (assert) nil))))
    ";;; developed with shostak decision procedures")
   nil nil))
(interm_val3 0
  (interm_val3-1 nil 3424526101
   ("" (skosimp*)
    (("" (lemma "intermediate_value3[a!1,b!1]")
      (("1" (inst?)
        (("1" (assert)
          (("1" (split -1)
            (("1" (propax) nil nil)
             ("2" (hide 2)
              (("2" (assert)
                (("2" (expand "restrict") (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    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)
    (intermediate_value3 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (restrict const-decl "R" restrict nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil))
(interm_val4 0
  (interm_val4-1 nil 3424526115
   ("" (skosimp*)
    (("" (lemma "intermediate_value4[a!1,b!1]")
      (("1" (inst?)
        (("1" (assert)
          (("1" (split -1)
            (("1" (propax) nil nil)
             ("2" (hide 2)
              (("2" (assert)
                (("2" (expand "restrict") (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    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)
    (intermediate_value4 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (restrict const-decl "R" restrict nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil))
(zeros_interm 0
  (zeros_interm-1 nil 3424527168
   ("" (skeep)
    (("" (skosimp*)
      (("" (case-replace "x!1 < x!2")
        (("1" (lemma "intermediate_value1[x!1,x!2]")
          (("1" (inst - "(LAMBDA (x:J[x!1, x!2]): f(x))" "0")
            (("1" (assert)
              (("1" (split -1)
                (("1" (skosimp*)
                  (("1" (inst - "c!1") (("1" (assert) nil nil)) nil))
                  nil)
                 ("2" (assert)
                  (("2" (lemma "cont_intv")
                    (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                  nil)
                 ("3" (assert)
                  (("3" (inst -5 "x!1") (("3" (assert) nil nil)) nil))
                  nil)
                 ("4" (assert)
                  (("4" (inst -5 "x!2") (("4" (assert) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil)
           ("2" (assert) nil nil))
          nil)
         ("2" (case "x!2 = x!1")
          (("1" (assert)
            (("1" (inst - "x!2") (("1" (assert) nil nil)) nil)) nil)
           ("2" (lemma "intermediate_value4[x!2,x!1]")
            (("1" (inst - "(LAMBDA (x:J[x!2, x!1]): f(x))" "0")
              (("1" (assert)
                (("1" (split -1)
                  (("1" (skosimp*)
                    (("1" (assert)
                      (("1" (inst - "c!1") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert)
                    (("2" (lemma "cont_intv")
                      (("2" (inst?) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (intermediate_value4 formula-decl nil continuity_interval nil)
    (intermediate_value1 formula-decl nil continuity_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (cont_intv formula-decl nil interm_value_thm nil)
    (J nonempty-type-eq-decl nil continuity_interval nil)
    (xl skolem-const-decl "real" interm_value_thm nil)
    (xu skolem-const-decl "real" interm_value_thm nil)
    (x!1 skolem-const-decl "open_interval[real](xl, xu)"
     interm_value_thm nil)
    (x!2 skolem-const-decl "open_interval[real](xl, xu)"
     interm_value_thm nil)
    (open_interval type-eq-decl nil intervals_real "reals/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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))
   nil))
(IntermediateValue 0
  (IntermediateValue-2 nil 3460800416
   ("" (skosimp*)
    (("" (case "x!1 < y!1")
      (("1" (case "f!1(x!1) > 0")
        (("1" (lemma "interm_value4")
          (("1" (inst -1 "x!1" "y!1" "0")
            (("1" (assert)
              (("1"
                (inst -1
                 "LAMBDA (z:closed_interval[real](x!1,y!1)): f!1(z)")
                (("1" (split -1)
                  (("1" (skeep -1)
                    (("1" (inst -5 "c")
                      (("1" (assert) nil nil)
                       ("2" (typepred "ab!1")
                        (("2" (inst -1 "x!1" "y!1" "c")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (lemma "cont_intv")
                    (("2" (inst -1 "x!1" "y!1" "f!1")
                      (("2" (assert) nil nil)) nil))
                    nil)
                   ("3" (mult-cases 2) nil nil) ("4" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "interm_value2")
          (("2" (inst -1 "x!1" "y!1" "0")
            (("2" (assert)
              (("2"
                (inst -1
                 "LAMBDA (z:closed_interval[real](x!1,y!1)): f!1(z)")
                (("2" (split -1)
                  (("1" (skeep -1)
                    (("1" (inst -4 "c")
                      (("1" (assert) nil nil)
                       ("2" (typepred "ab!1")
                        (("2" (inst -1 "x!1" "y!1" "c")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (lemma "cont_intv")
                    (("2" (inst -1 "x!1" "y!1" "f!1")
                      (("2" (assert) nil nil)) nil))
                    nil)
                   ("3" (assert) nil nil)
                   ("4" (mult-cases 3)
                    (("4" (inst -3 "x!1") (("4" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (case "x!1 > y!1")
        (("1" (case "f!1(y!1) > 0")
          (("1" (lemma "interm_value4")
            (("1" (inst -1 "y!1" "x!1" "0")
              (("1" (assert)
                (("1"
                  (inst -1
                   "LAMBDA (z:closed_interval[real](y!1,x!1)): f!1(z)")
                  (("1" (split -1)
                    (("1" (skeep -1)
                      (("1" (inst -5 "c")
                        (("1" (assert) nil nil)
                         ("2" (typepred "ab!1")
                          (("2" (inst -1 "y!1" "x!1" "c")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (lemma "cont_intv")
                      (("2" (inst -1 "y!1" "x!1" "f!1")
                        (("2" (assert) nil nil)) nil))
                      nil)
                     ("3" (mult-cases 3) nil nil)
                     ("4" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (lemma "interm_value2")
            (("2" (inst -1 "y!1" "x!1" "0")
              (("2" (assert)
                (("2"
                  (inst -1
                   "LAMBDA (z:closed_interval[real](y!1,x!1)): f!1(z)")
                  (("2" (split -1)
                    (("1" (skeep -1)
                      (("1" (inst -4 "c")
                        (("1" (assert) nil nil)
                         ("2" (typepred "ab!1")
                          (("2" (inst -1 "y!1" "x!1" "c")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (lemma "cont_intv")
                      (("2" (inst -1 "y!1" "x!1" "f!1")
                        (("2" (assert) nil nil)) nil))
                      nil)
                     ("3" (assert) nil nil)
                     ("4" (mult-cases 4)
                      (("4" (inst -3 "y!1") (("4" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case-replace "x!1 = y!1")
          (("1" (inst -3 "y!1")
            (("1" (rewrite "sq" :dir rl)
              (("1" (assert)
                (("1" (lemma "sq_gt_0")
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((Connected type-eq-decl nil connected_set "reals/")
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil) (< const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (interm_value2 formula-decl nil interm_value_thm nil)
    (c skolem-const-decl "closed_interval[real](x!1, y!1)"
     interm_value_thm nil)
    (interm_value4 formula-decl nil interm_value_thm nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ab!1 skolem-const-decl "Connected" interm_value_thm nil)
    (x!1 skolem-const-decl "(ab!1)" interm_value_thm nil)
    (y!1 skolem-const-decl "(ab!1)" interm_value_thm nil)
    (c skolem-const-decl "closed_interval[real](x!1, y!1)"
     interm_value_thm nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (cont_intv formula-decl nil interm_value_thm nil)
    (pos_times_gt formula-decl nil real_props nil)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (> const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_gt_0 formula-decl nil sq "reals/")
    (c skolem-const-decl "closed_interval[real](y!1, x!1)"
     interm_value_thm nil)
    (c skolem-const-decl "closed_interval[real](y!1, x!1)"
     interm_value_thm nil))
   nil)
  (IntermediateValue-1 nil 3459853237
   ("" (skosimp*)
    (("" (case "x!1 < y!1")
      (("1" (case "f!1(x!1) > 0")
        (("1" (lemma "interm_value4")
          (("1" (inst -1 "x!1" "y!1" "0")
            (("1" (assert)
              (("1"
                (inst -1 "LAMBDA (z:closed_interval(x!1,y!1)): f!1(z)")
                (("1" (split -1)
                  (("1" (skeep -1)
                    (("1" (inst -5 "c")
                      (("1" (assert) nil nil)
                       ("2" (typepred "ab!1")
                        (("2" (inst -1 "x!1" "y!1" "c")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (lemma "cont_intv")
                    (("2" (inst -1 "x!1" "y!1" "f!1")
                      (("2" (assert) nil nil)) nil))
                    nil)
                   ("3" (mult-cases 2) nil nil) ("4" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "interm_value2")
          (("2" (inst -1 "x!1" "y!1" "0")
            (("2" (assert)
              (("2"
                (inst -1 "LAMBDA (z:closed_interval(x!1,y!1)): f!1(z)")
                (("2" (split -1)
                  (("1" (skeep -1)
                    (("1" (inst -4 "c")
                      (("1" (assert) nil nil)
                       ("2" (typepred "ab!1")
                        (("2" (inst -1 "x!1" "y!1" "c")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (lemma "cont_intv")
                    (("2" (inst -1 "x!1" "y!1" "f!1")
                      (("2" (assert) nil nil)) nil))
                    nil)
                   ("3" (assert) nil nil)
                   ("4" (mult-cases 3)
                    (("4" (inst -3 "x!1") (("4" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (case "x!1 > y!1")
        (("1" (case "f!1(y!1) > 0")
          (("1" (lemma "interm_value4")
            (("1" (inst -1 "y!1" "x!1" "0")
              (("1" (assert)
                (("1"
                  (inst -1
                   "LAMBDA (z:closed_interval(y!1,x!1)): f!1(z)")
                  (("1" (split -1)
                    (("1" (skeep -1)
                      (("1" (inst -5 "c")
                        (("1" (assert) nil nil)
                         ("2" (typepred "ab!1")
                          (("2" (inst -1 "y!1" "x!1" "c")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (lemma "cont_intv")
                      (("2" (inst -1 "y!1" "x!1" "f!1")
                        (("2" (assert) nil nil)) nil))
                      nil)
                     ("3" (mult-cases 3) nil nil)
                     ("4" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (lemma "interm_value2")
            (("2" (inst -1 "y!1" "x!1" "0")
              (("2" (assert)
                (("2"
                  (inst -1
                   "LAMBDA (z:closed_interval(y!1,x!1)): f!1(z)")
                  (("2" (split -1)
                    (("1" (skeep -1)
                      (("1" (inst -4 "c")
                        (("1" (assert) nil nil)
                         ("2" (typepred "ab!1")
                          (("2" (inst -1 "y!1" "x!1" "c")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (lemma "cont_intv")
                      (("2" (inst -1 "y!1" "x!1" "f!1")
                        (("2" (assert) nil nil)) nil))
                      nil)
                     ("3" (assert) nil nil)
                     ("4" (mult-cases 4)
                      (("4" (inst -3 "y!1") (("4" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case-replace "x!1 = y!1")
          (("1" (inst -3 "y!1")
            (("1" (rewrite "sq" :dir rl)
              (("1" (assert)
                (("1" (lemma "sq_gt_0")
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((Connected type-eq-decl nil connected_set "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_gt_0 formula-decl nil sq "reals/"))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.