Quelle ln_exp.prf Sprache: Lisp

(ln_exp
(conn_posreal 0
  (conn_posreal-1 nil 3477844344
   ("" (expand "connected?")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/"))
   shostak))
(one_over_t_cont 0
  (one_over_t_cont-1 nil 3253532189
   ("" (lemma "div_fun_continuous[posreal]")
    ((""
      (inst -1 "(LAMBDA (t: posreal): 1)" "(LAMBDA (t: posreal): t)")
      (("1" (expand "/") (("1" (propax) nil nil)) nil)
       ("2" (assert)
        (("2" (hide 2)
          (("2" (lemma "id_fun_continuous[posreal]")
            (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil))
          nil))
        nil)
       ("3" (hide 2)
        (("3" (lemma "const_fun_continuous[posreal]")
          (("3" (inst?)
            (("3" (expand "const_fun") (("3" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous? const-decl "bool" continuous_functions "analysis/")
    (continuous_fun nonempty-type-eq-decl nil continuous_functions
     "analysis/")
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nz_continuous_fun type-eq-decl nil continuous_functions
     "analysis/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (I const-decl "(bijective?[T, T])" identity nil)
    (id_fun_continuous judgement-tcc nil continuous_functions
     "analysis/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (const_fun_continuous judgement-tcc nil continuous_functions
     "analysis/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (div_fun_continuous judgement-tcc nil continuous_functions
     "analysis/")
    (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))
   nil))
(ln_prep_TCC1 0
  (ln_prep_TCC1-1 nil 3253532189 ("" (assuming-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)
    (>= 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)
    (real_le_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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
(ln_prep_TCC2 0
  (ln_prep_TCC2-1 nil 3253532189
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (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)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
(ln_prep 0
  (ln_prep-1 nil 3253532189
   ("" (skosimp*)
    (("" (lemma "continuous_Integrable?[posreal]")
      (("1" (inst?)
        (("1" (assert)
          (("1" (hide 2)
            (("1" (skosimp*)
              (("1" (lemma "one_over_t_cont")
                (("1" (expand "continuous?" -1) (("1" (inst?) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (ground)
          (("2" (expand "connected?")
            (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    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)
    (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)
    (continuous_Integrable? formula-decl nil integral "analysis/")
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (Closed_interval type-eq-decl nil intervals_real "reals/")
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (one_over_t_cont formula-decl nil ln_exp 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_div_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil))
(ln_TCC1 0
  (ln_TCC1-1 nil 3253532189
   ("" (skosimp*) (("" (rewrite "ln_prep") nil nil)) nil)
   ((ln_prep formula-decl nil ln_exp 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))
   nil))
(ln_derivable_TCC1 0
  (ln_derivable_TCC1-1 nil 3471688875
   ("" (lemma "deriv_domain_posreal") (("" (propax) nil nil)) nil)
   ((deriv_domain_posreal formula-decl nil deriv_domain "analysis/"))
   nil))
(ln_derivable 0
  (ln_derivable-1 nil 3253532189
   ("" (lemma "fundamental[posreal]")
    (("1" (inst -1 "ln" "1" "(LAMBDA (t: posreal): 1 / t)")
      (("1" (split -1)
        (("1" (propax) nil nil)
         ("2" (hide 2) (("2" (rewrite "one_over_t_cont") nil nil)) nil)
         ("3" (hide 2)
          (("3" (skosimp*)
            (("3" (expand "ln") (("3" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil)
     ("2" (assert)
      (("2" (expand "not_one_element?")
        (("2" (skosimp*)
          (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil)
     ("3" (assert)
      (("3" (expand "connected?")
        (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (ln const-decl "real" ln_exp 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)
    (one_over_t_cont formula-decl nil ln_exp nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (fundamental formula-decl nil fundamental_theorem "analysis/")
    (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))
   nil))
(ln_continuous 0
  (ln_continuous-2 nil 3445353494
   ("" (lemma "ln_derivable")
    (("" (lemma "derivable_continuous[posreal]")
      (("1" (inst?)
        (("1" (flatten)
          (("1" (expand "continuous?" 1)
            (("1" (skosimp*)
              (("1" (inst?)
                (("1" (assert)
                  (("1" (expand "derivable?" -1)
                    (("1" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (inst-cp + "1")
          (("2" (assert)
            (("2" (inst + "2") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil)
       ("3" (skosimp*)
        (("3" (assert)
          (("3" (lemma "deriv_domain_posreal")
            (("3" (expand "deriv_domain?") (("3" (inst?) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (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)
    (derivable_continuous formula-decl nil derivatives_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (ln const-decl "real" ln_exp nil)
    (ln_derivable formula-decl nil ln_exp nil))
   nil)
  (ln_continuous-1 nil 3253532189
   ("" (lemma "ln_derivable")
    (("" (lemma "derivable_continuous[posreal]")
      (("1" (inst?)
        (("1" (flatten)
          (("1" (expand "continuous?" 1)
            (("1" (skosimp*)
              (("1" (inst?)
                (("1" (assert)
                  (("1" (expand "derivable" -1) (("1" (inst?) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (inst-cp + "1")
          (("2" (assert)
            (("2" (inst + "2") (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil)
       ("3" (skosimp*) (("3" (assert) nil nil)) nil))
      nil))
    nil)
   ((derivable_continuous formula-decl nil derivatives_def
     "analysis/"))
   nil))
(ln_1 0
  (ln_1-1 nil 3253532189
   ("" (expand "ln")
    (("" (expand "Integral") (("" (propax) nil nil)) nil)) nil)
   ((Integral const-decl "real" integral_def "analysis/")
    (ln const-decl "real" ln_exp nil))
   nil))
(ln_mult 0
  (ln_mult-3 nil 3445353567
   ("" (skosimp*)
    ((""
      (case "derivable?[posreal](LAMBDA (x: posreal): ln(py!1 * x))")
      (("1" (lemma "ln_derivable")
        (("1" (flatten)
          (("1"
            (case "deriv(LAMBDA (x: posreal): ln(py!1*x)) = deriv(LAMBDA (x: posreal): ln(x))")
            (("1" (lemma "derivs_eq[posreal]")
              (("1" (inst?)
                (("1" (assert)
                  (("1"
                    (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
                    (("1" (assert)
                      (("1" (hide -1)
                        (("1" (replace -3)
                          (("1" (assert)
                            (("1" (skosimp*)
                              (("1"
                                (expand "+ ")
                                (("1"
                                  (expand "const_fun")
                                  (("1"
                                    (case
                                     "(LAMBDA (x: posreal): ln(py!1 * x))(1) = (LAMBDA (x_824: posreal): ln(x_824) + c!1)(1)")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (hide -2)
                                        (("1"
                                          (rewrite "ln_1")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (reveal -1)
                                              (("1"
                                                (replace -2 * rl)
                                                (("1"
                                                  (case-replace
                                                   "(LAMBDA (x: posreal): ln(py!1 * x))(px!1) = (LAMBDA (x_824: posreal): ln(x_824) + ln(py!1))(px!1)")
                                                  (("1"
                                                    (hide -2)
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (replace -1)
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (replace -1)
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (apply-extensionality 1 :hide? t) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (expand "not_one_element?")
                  (("2" (skosimp*)
                    (("2" (assert)
                      (("2" (inst + "x!1+1") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (assert)
                (("3" (expand "connected?")
                  (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (lemma "deriv_composition[posreal,posreal]")
                (("1"
                  (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
                  (("1" (hide -1)
                    (("1" (replace -3)
                      (("1" (apply-extensionality 1 :hide? t)
                        (("1"
                          (inst - "(LAMBDA (t: posreal): py!1*t)" "ln"
                           "x!1")
                          (("1" (assert)
                            (("1"
                              (case "derivable?((LAMBDA (t: posreal): py!1 * t), x!1) ")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "derivable?" -3)
                                  (("1"
                                    (inst -3 "py!1*x!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (expand "o ")
                                        (("1"
                                          (expand "deriv" 1)
                                          (("1"
                                            (case
                                             "deriv(ln)(py!1*x!1) = (LAMBDA (t: posreal): 1 / t)(py!1*x!1)")
                                            (("1"
                                              (expand "deriv" -1)
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (hide -1)
                                                  (("1"
                                                    (case-replace
                                                     "deriv[posreal]((LAMBDA (t: posreal): py!1 * t), x!1) = py!1")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil)
                                                     ("2"
                                                      (hide 2)
                                                      (("2"
                                                        (lemma
                                                         "deriv_scal[posreal]")
                                                        (("2"
                                                          (inst
                                                           -1
                                                           "py!1"
                                                           "I[posreal]"
                                                           "x!1")
                                                          (("2"
                                                            (split -1)
                                                            (("1"
                                                              (expand
                                                               "I")
                                                              (("1"
                                                                (expand
                                                                 "*")
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (lemma
                                                                     "deriv_identity[posreal]")
                                                                    (("1"
                                                                      (expand
                                                                       "I")
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (hide-all-but
                                                               1)
                                                              (("2"
                                                                (lemma
                                                                 "identity_derivable[posreal]")
                                                                (("2"
                                                                  (inst?)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (assert)
                                              (("2"
                                                (hide 2)
                                                (("2"
                                                  (replace -4)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (lemma "scal_derivable[posreal]")
                                  (("2"
                                    (inst -1 "py!1" "I" "x!1")
                                    (("2"
                                      (lemma
                                       "identity_derivable[posreal]")
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (split -2)
                                          (("1"
                                            (expand "I")
                                            (("1"
                                              (expand "*")
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil)
                                           ("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (lemma "deriv_domain_posreal")
                                (("3"
                                  (expand "deriv_domain?")
                                  (("3" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (apply-extensionality 1 :hide? t) nil nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil))
                  nil)
                 ("3" (assert)
                  (("3" (lemma "deriv_domain_posreal")
                    (("3" (propax) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("3" (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
              (("3" (apply-extensionality 1 :hide? t) nil nil)) nil)
             ("4" (propax) nil nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (assert)
          (("2" (lemma "ln_derivable")
            (("2" (flatten)
              (("2" (assert)
                (("2" (lemma "scal_derivable[posreal]")
                  (("1" (expand "derivable?" 1)
                    (("1" (skosimp*)
                      (("1" (inst -1 "py!1" "I" "x!1")
                        (("1" (lemma "identity_derivable[posreal]")
                          (("1" (inst?)
                            (("1"
                              (lemma
                               "composition_derivable[posreal,posreal]")
                              (("1"
                                (inst
                                 -1
                                 "(LAMBDA (t:posreal): py!1*t)"
                                 "ln"
                                 "x!1")
                                (("1"
                                  (expand "o ")
                                  (("1"
                                    (split -1)
                                    (("1" (propax) nil nil)
                                     ("2"
                                      (expand "derivable?" -3)
                                      (("2"
                                        (inst -3 "py!1*x!1")
                                        (("2"
                                          (hide 2)
                                          (("2"
                                            (expand "I")
                                            (("2"
                                              (expand "*")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("3"
                                      (hide 2)
                                      (("3"
                                        (expand "derivable?" -3)
                                        (("3"
                                          (inst -3 "py!1*x!1")
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (lemma "deriv_domain_posreal")
                                (("2" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp*)
                    (("2" (inst-cp + "1")
                      (("2" (inst + "2") (("2" (assert) nil nil)) nil))
                      nil))
                    nil)
                   ("3" (skosimp*)
                    (("3" (assert)
                      (("3" (lemma "deriv_domain_posreal")
                        (("3" (expand "deriv_domain?")
                          (("3" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (ln const-decl "real" ln_exp nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (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)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (derivable? const-decl "bool" derivatives_def "analysis/")
    (I const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (identity_derivable formula-decl nil derivatives_def "analysis/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (deriv_identity formula-decl nil derivatives_def "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_scal formula-decl nil derivatives_def "analysis/")
    (deriv const-decl "real" derivatives_def "analysis/")
    (O const-decl "T3" function_props nil)
    (scal_derivable formula-decl nil derivatives_def "analysis/")
    (py!1 skolem-const-decl "posreal" ln_exp nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_composition formula-decl nil chain_rule "analysis/")
    (derivs_eq formula-decl nil indefinite_integral "analysis/")
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (ln_1 formula-decl nil ln_exp nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (ln_derivable formula-decl nil ln_exp nil)
    (composition_derivable formula-decl nil chain_rule "analysis/"))
   nil)
  (ln_mult-2 nil 3445353520
   (";;; Proof ln_mult-1 for formula ln_exp.ln_mult" (skosimp*)
    ((";;; Proof ln_mult-1 for formula ln_exp.ln_mult"
      (case "derivable?[posreal](LAMBDA (x: posreal): ln(py!1 * x))")
      (("1" (lemma "ln_derivable")
        (("1" (flatten)
          (("1"
            (case "deriv(LAMBDA (x: posreal): ln(py!1*x)) = deriv(LAMBDA (x: posreal): ln(x))")
            (("1" (lemma "derivs_eq[posreal]")
              (("1" (inst?)
                (("1" (assert)
                  (("1"
                    (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
                    (("1" (assert)
                      (("1" (hide -1)
                        (("1" (replace -3)
                          (("1" (assert)
                            (("1" (skosimp*)
                              (("1"
                                (expand "+ ")
                                (("1"
                                  (expand "const_fun")
                                  (("1"
                                    (case
                                     "(LAMBDA (x: posreal): ln(py!1 * x))(1) = (LAMBDA (x_824: posreal): ln(x_824) + c!1)(1)")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (hide -2)
                                        (("1"
                                          (rewrite "ln_1")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (reveal -1)
                                              (("1"
                                                (replace -2 * rl)
                                                (("1"
                                                  (case-replace
                                                   "(LAMBDA (x: posreal): ln(py!1 * x))(px!1) = (LAMBDA (x_824: posreal): ln(x_824) + ln(py!1))(px!1)")
                                                  (("1"
                                                    (hide -2)
                                                    (("1"
                                                      (assert)
                                                      nil)))
                                                   ("2"
                                                    (replace -1)
                                                    (("2"
                                                      (propax)
                                                      nil)))))))))))))))))
                                     ("2"
                                      (replace -1)
                                      (("2"
                                        (propax)
                                        nil)))))))))))))))))))
                     ("2" (apply-extensionality 1 :hide? t) nil)))))))
               ("2" (skosimp*)
                (("2" (inst + "x!1/2")
                  (("2" (skosimp*) (("2" (assert) nil)))))))
               ("3" (skosimp*) (("3" (assert) nil)))))
             ("2" (hide 2)
              (("2" (lemma "deriv_composition[posreal,posreal]")
                (("1"
                  (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
                  (("1" (hide -1)
                    (("1" (replace -3)
                      (("1" (apply-extensionality 1 :hide? t)
                        (("1"
                          (inst - "(LAMBDA (t: posreal): py!1*t)" "ln"
                           "x!1")
                          (("1" (assert)
                            (("1"
                              (case "derivable?((LAMBDA (t: posreal): py!1 * t), x!1) ")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "derivable?" -3)
                                  (("1"
                                    (inst -3 "py!1*x!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (expand "o ")
                                        (("1"
                                          (expand "deriv" 1)
                                          (("1"
                                            (case
                                             "deriv(ln)(py!1*x!1) = (LAMBDA (t: posreal): 1 / t)(py!1*x!1)")
                                            (("1"
                                              (expand "deriv" -1)
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (hide -1)
                                                  (("1"
                                                    (case-replace
                                                     "deriv[posreal]((LAMBDA (t: posreal): py!1 * t), x!1) = py!1")
                                                    (("1" (assert) nil)
                                                     ("2"
                                                      (hide 2)
                                                      (("2"
                                                        (lemma
                                                         "deriv_scal[posreal]")
                                                        (("2"
                                                          (inst
                                                           -1
                                                           "py!1"
                                                           "I[posreal]"
                                                           "x!1")
                                                          (("2"
                                                            (split -1)
                                                            (("1"
                                                              (expand
                                                               "I")
                                                              (("1"
                                                                (expand
                                                                 "*")
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (lemma
                                                                     "deriv_identity[posreal]")
                                                                    (("1"
                                                                      (expand
                                                                       "I")
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (assert)
                                                                          nil)))))))))))))
                                                             ("2"
                                                              (hide-all-but
                                                               1)
                                                              (("2"
                                                                (lemma
                                                                 "identity_derivable[posreal]")
                                                                (("2"
                                                                  (inst?)
                                                                  nil)))))))))))))))))))))
                                             ("2"
                                              (assert)
                                              (("2"
                                                (hide 2)
                                                (("2"
                                                  (replace -4)
                                                  (("2"
                                                    (assert)
                                                    nil)))))))))))))))))))))
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (lemma "scal_derivable[posreal]")
                                  (("2"
                                    (inst -1 "py!1" "I" "x!1")
                                    (("2"
                                      (lemma
                                       "identity_derivable[posreal]")
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (split -2)
                                          (("1"
                                            (expand "I")
                                            (("1"
                                              (expand "*")
                                              (("1" (propax) nil)))))
                                           ("2"
                                            (propax)
                                            nil)))))))))))))))))))))))))
                   ("2" (apply-extensionality 1 :hide? t) nil)))
                 ("2" (skosimp*)
                  (("2" (inst + "x!1+1") (("2" (assert) nil)))))
                 ("3" (skosimp*) (("3" (assert) nil)))))))
             ("3" (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
              (("3" (apply-extensionality 1 :hide? t) nil)))
             ("4" (propax) nil)))))))
       ("2" (hide 2)
        (("2" (assert)
          (("2" (lemma "ln_derivable")
            (("2" (flatten)
              (("2" (assert)
                (("2" (lemma "scal_derivable[posreal]")
                  (("1" (expand "derivable" 1)
                    (("1" (skosimp*)
                      (("1" (inst -1 "py!1" "I" "x!1")
                        (("1" (lemma "identity_derivable[posreal]")
                          (("1" (inst?)
                            (("1"
                              (lemma
                               "composition_derivable[posreal,posreal]")
                              (("1"
                                (inst
                                 -1
                                 "(LAMBDA (t:posreal): py!1*t)"
                                 "ln"
                                 "x!1")
                                (("1"
                                  (expand "o ")
                                  (("1"
                                    (split -1)
                                    (("1" (propax) nil)
                                     ("2"
                                      (expand "derivable" -3)
                                      (("2"
                                        (inst -3 "py!1*x!1")
                                        (("2"
                                          (hide 2)
                                          (("2"
                                            (expand "I")
                                            (("2"
                                              (expand "*")
                                              (("2"
                                                (assert)
                                                nil)))))))))))
                                     ("3"
                                      (hide 2)
                                      (("3"
                                        (expand "derivable" -3)
                                        (("3"
                                          (inst -3 "py!1*x!1")
                                          nil)))))))))))))))))))))))
                   ("2" (skosimp*)
                    (("2" (inst-cp + "1")
                      (("2" (inst + "2") (("2" (assert) nil)))))))
                   ("3" (skosimp*) (("3" (assert) nil))))))))))))))))))
    ";;; developed with shostak decision procedures")
   nil nil)
  (ln_mult-1 nil 3253532189
   ("" (skosimp*)
    ((""
      (case "derivable?[posreal](LAMBDA (x: posreal): ln(py!1 * x))")
      (("1" (lemma "ln_derivable")
        (("1" (flatten)
          (("1"
            (case "deriv(LAMBDA (x: posreal): ln(py!1*x)) = deriv(LAMBDA (x: posreal): ln(x))")
            (("1" (lemma "derivs_eq[posreal]")
              (("1" (inst?)
                (("1" (assert)
                  (("1"
                    (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
                    (("1" (assert)
                      (("1" (hide -1)
                        (("1" (replace -3)
                          (("1" (assert)
                            (("1" (skosimp*)
                              (("1"
                                (expand "+ ")
                                (("1"
                                  (expand "const_fun")
                                  (("1"
                                    (case
                                     "(LAMBDA (x: posreal): ln(py!1 * x))(1) = (LAMBDA (x_824: posreal): ln(x_824) + c!1)(1)")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (hide -2)
                                        (("1"
                                          (rewrite "ln_1")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (reveal -1)
                                              (("1"
                                                (replace -2 * rl)
                                                (("1"
                                                  (case-replace
                                                   "(LAMBDA (x: posreal): ln(py!1 * x))(px!1) = (LAMBDA (x_824: posreal): ln(x_824) + ln(py!1))(px!1)")
                                                  (("1"
                                                    (hide -2)
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (replace -1)
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (replace -1)
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (apply-extensionality 1 :hide? t) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (skosimp*)
                (("2" (inst + "x!1/2")
                  (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil))
                nil)
               ("3" (skosimp*) (("3" (assert) nil nil)) nil))
              nil)
             ("2" (hide 2)
              (("2" (lemma "deriv_composition[posreal,posreal]")
                (("1"
                  (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
                  (("1" (hide -1)
                    (("1" (replace -3)
                      (("1" (apply-extensionality 1 :hide? t)
                        (("1"
                          (inst - "(LAMBDA (t: posreal): py!1*t)" "ln"
                           "x!1")
                          (("1" (assert)
                            (("1"
                              (case "derivable?((LAMBDA (t: posreal): py!1 * t), x!1) ")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "derivable" -3)
                                  (("1"
                                    (inst -3 "py!1*x!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (expand "o ")
                                        (("1"
                                          (expand "deriv" 1)
                                          (("1"
                                            (case
                                             "deriv(ln)(py!1*x!1) = (LAMBDA (t: posreal): 1 / t)(py!1*x!1)")
                                            (("1"
                                              (expand "deriv" -1)
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (hide -1)
                                                  (("1"
                                                    (case-replace
                                                     "deriv[posreal]((LAMBDA (t: posreal): py!1 * t), x!1) = py!1")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil)
                                                     ("2"
                                                      (hide 2)
                                                      (("2"
                                                        (lemma
                                                         "deriv_scal[posreal]")
                                                        (("2"
                                                          (inst
                                                           -1
                                                           "py!1"
                                                           "I[posreal]"
                                                           "x!1")
                                                          (("2"
                                                            (split -1)
                                                            (("1"
                                                              (expand
                                                               "I")
                                                              (("1"
                                                                (expand
                                                                 "*")
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (lemma
                                                                     "deriv_identity[posreal]")
                                                                    (("1"
                                                                      (expand
                                                                       "I")
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (hide-all-but
                                                               1)
                                                              (("2"
                                                                (lemma
                                                                 "identity_derivable[posreal]")
                                                                (("2"
                                                                  (inst?)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (assert)
                                              (("2"
                                                (hide 2)
                                                (("2"
                                                  (replace -4)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (lemma "scal_derivable[posreal]")
                                  (("2"
                                    (inst -1 "py!1" "I" "x!1")
                                    (("2"
                                      (lemma
                                       "identity_derivable[posreal]")
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (split -2)
                                          (("1"
                                            (expand "I")
                                            (("1"
                                              (expand "*")
                                              (("1" (propax) nil nil))
                                              nil))
                                            nil)
                                           ("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (apply-extensionality 1 :hide? t) nil nil))
                  nil)
                 ("2" (skosimp*)
                  (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil))
                  nil)
                 ("3" (skosimp*) (("3" (assert) nil nil)) nil))
                nil))
              nil)
             ("3" (case-replace "(LAMBDA (x: posreal): ln(x)) = ln")
              (("3" (apply-extensionality 1 :hide? t) nil nil)) nil)
             ("4" (propax) nil nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (assert)
          (("2" (lemma "ln_derivable")
            (("2" (flatten)
              (("2" (assert)
                (("2" (lemma "scal_derivable[posreal]")
                  (("1" (expand "derivable" 1)
                    (("1" (skosimp*)
                      (("1" (inst -1 "py!1" "I" "x!1")
                        (("1" (lemma "identity_derivable[posreal]")
                          (("1" (inst?)
                            (("1"
                              (lemma
                               "composition_derivable[posreal,posreal]")
                              (("1"
                                (inst
                                 -1
                                 "(LAMBDA (t:posreal): py!1*t)"
                                 "ln"
                                 "x!1")
                                (("1"
                                  (expand "o ")
                                  (("1"
                                    (split -1)
                                    (("1" (propax) nil nil)
                                     ("2"
                                      (expand "derivable" -3)
                                      (("2"
                                        (inst -3 "py!1*x!1")
                                        (("2"
                                          (hide 2)
                                          (("2"
                                            (expand "I")
                                            (("2"
                                              (expand "*")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("3"
                                      (hide 2)
                                      (("3"
                                        (expand "derivable" -3)
                                        (("3"
                                          (inst -3 "py!1*x!1")
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp*)
                    (("2" (inst-cp + "1")
                      (("2" (inst + "2") (("2" (assert) nil nil)) nil))
                      nil))
                    nil)
                   ("3" (skosimp*) (("3" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((composition_derivable formula-decl nil chain_rule "analysis/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_composition formula-decl nil chain_rule "analysis/")
    (scal_derivable formula-decl nil derivatives_def "analysis/")
    (deriv const-decl "real" derivatives_def "analysis/")
    (deriv_scal formula-decl nil derivatives_def "analysis/")
    (deriv_identity formula-decl nil derivatives_def "analysis/")
    (identity_derivable formula-decl nil derivatives_def "analysis/"))
   nil))
(ln_div 0
  (ln_div-1 nil 3253532189
   ("" (skosimp*)
    (("" (lemma "ln_mult")
      (("" (inst -1 "1/py!1" "py!1")
        (("" (assert)
          (("" (rewrite "ln_1")
            (("" (lemma "ln_mult")
              (("" (inst -1 "px!1" "1/py!1") (("" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((ln_mult formula-decl nil ln_exp nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (ln_1 formula-decl nil ln_exp 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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil))
(ln_expt_TCC1 0
  (ln_expt_TCC1-1 nil 3253532189 ("" (subtype-tcc) nil nil) nil nil))
(ln_expt 0
  (ln_expt-1 nil 3253532189
   ("" (skosimp*)
    (("" (case "(FORALL (n:nat): ln(px!1 ^ n) = n * ln(px!1))")
      (("1" (case-replace "i!1 >= 0")
        (("1" (inst?) nil nil)
         ("2" (expand "^")
          (("2" (assert)
            (("2" (rewrite "ln_div")
              (("2" (rewrite "ln_1")
                (("2" (assert)
--> --------------------

--> maximum size reached

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

quality100%

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