products/Sources/formale Sprachen/PVS/digraphs image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: deriv_sincos.prf   Sprache: Lisp

Original von: PVS©

(deriv_sincos
 (deriv_domain 0
  (deriv_domain-1 nil 3479041446
   ("" (lemma "connected_deriv_domain[T]")
    (("" (lemma "connected_domain")
      (("" (lemma "not_one_element") (("" (assertnil nil)) nil))
      nil))
    nil)
   ((connected_domain formula-decl nil deriv_sincos nil)
    (not_one_element formula-decl nil deriv_sincos nil)
    (connected_deriv_domain formula-decl nil deriv_domain_def
     "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)
    (T_pred const-decl "[real -> boolean]" deriv_sincos nil)
    (T formal-subtype-decl nil deriv_sincos nil))
   shostak))
 (sin_continuous 0
  (sin_continuous-1 nil 3479039819
   ("" (skosimp*)
    (("" (lemma "scal_cont_fun[T]")
      (("" (inst - "(LAMBDA (x: T): sin(alpha!1 * x))" "k!1")
        (("" (assert)
          (("" (expand "*" -1)
            (("" (hide 2)
              (("" (lemma "composition_cont_fun[T,real]")
                ((""
                  (inst - "(LAMBDA (x:T): alpha!1*x)"
                   "(LAMBDA (x:real): sin(x))")
                  (("" (expand "o ")
                    (("" (assert)
                      (("" (hide 2)
                        (("" (split +)
                          (("1" (lemma "scal_cont_fun[T]")
                            (("1" (inst - "id[T]" "alpha!1")
                              (("1"
                                (expand "id")
                                (("1"
                                  (expand "*")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (hide 2)
                                      (("1"
                                        (lemma "identity_cont_fun[T]")
                                        (("1"
                                          (expand "I")
                                          (("1" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma "sin_continuous")
                            (("2" (expand "continuous?" 1)
                              (("2"
                                (skosimp*)
                                (("2"
                                  (inst?)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "continuous?")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-subtype-decl nil deriv_sincos nil)
    (T_pred const-decl "[real -> boolean]" deriv_sincos 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)
    (scal_cont_fun formula-decl nil continuous_functions "analysis/")
    (sin_range application-judgement "trig_range" sincos_def nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (I const-decl "(bijective?[T, T])" identity nil)
    (identity_cont_fun formula-decl nil continuous_functions
     "analysis/")
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (sin_continuous formula-decl nil sincos nil)
    (O const-decl "T3" function_props nil)
    (composition_cont_fun formula-decl nil composition_continuous
     "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sin const-decl "real" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (cos_continuous 0
  (cos_continuous-1 nil 3479041340
   ("" (skosimp*)
    (("" (lemma "scal_cont_fun[T]")
      (("" (inst - "(LAMBDA (x: T): cos(alpha!1 * x))" "k!1")
        (("" (assert)
          (("" (expand "*" -1)
            (("" (hide 2)
              (("" (lemma "composition_cont_fun[T,real]")
                ((""
                  (inst - "(LAMBDA (x:T): alpha!1*x)"
                   "(LAMBDA (x:real): cos(x))")
                  (("" (expand "o ")
                    (("" (assert)
                      (("" (hide 2)
                        (("" (split +)
                          (("1" (lemma "scal_cont_fun[T]")
                            (("1" (inst - "id[T]" "alpha!1")
                              (("1"
                                (expand "id")
                                (("1"
                                  (expand "*")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (hide 2)
                                      (("1"
                                        (lemma "identity_cont_fun[T]")
                                        (("1"
                                          (expand "I")
                                          (("1" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma "cos_continuous")
                            (("2" (expand "continuous?" 1)
                              (("2"
                                (skosimp*)
                                (("2"
                                  (inst?)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "continuous?")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-subtype-decl nil deriv_sincos nil)
    (T_pred const-decl "[real -> boolean]" deriv_sincos 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)
    (scal_cont_fun formula-decl nil continuous_functions "analysis/")
    (cos_range application-judgement "trig_range" sincos_def nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (I const-decl "(bijective?[T, T])" identity nil)
    (identity_cont_fun formula-decl nil continuous_functions
     "analysis/")
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (cos_continuous formula-decl nil sincos nil)
    (O const-decl "T3" function_props nil)
    (composition_cont_fun formula-decl nil composition_continuous
     "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cos const-decl "real" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (sin_derivable_TCC1 0
  (sin_derivable_TCC1-1 nil 3476447874
   ("" (rewrite "deriv_domain"nil nil)
   ((deriv_domain formula-decl nil deriv_sincos nil)) nil))
 (sin_derivable_TCC2 0
  (sin_derivable_TCC2-1 nil 3476447874
   ("" (rewrite "not_one_element"nil nil)
   ((not_one_element formula-decl nil deriv_sincos nil)) nil))
 (sin_derivable 0
  (sin_derivable-1 nil 3479041533
   ("" (skosimp*)
    (("" (lemma "scal_derivable_fun[T]")
      (("" (inst - "k!1" "(LAMBDA (x: T): sin(alpha!1 * x))")
        (("" (assert)
          (("" (expand "*")
            (("" (hide 2)
              (("" (lemma "comp_derivable_fun[T,real]")
                (("1"
                  (inst - "(LAMBDA (x:T): alpha!1*x)"
                   "(LAMBDA (x:real): sin(x))")
                  (("1" (assert)
                    (("1" (hide 2)
                      (("1" (split +)
                        (("1" (lemma "scal_derivable_fun[T]")
                          (("1" (inst - "alpha!1" "id[T]")
                            (("1" (assert)
                              (("1"
                                (expand "id")
                                (("1"
                                  (expand "*")
                                  (("1"
                                    (hide 2)
                                    (("1"
                                      (lemma "id_derivable_fun[T]")
                                      (("1" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (lemma "sin_derivable")
                          (("2" (expand "derivable?")
                            (("2" (skosimp*)
                              (("2"
                                (expand "derivable?")
                                (("2"
                                  (expand "convergent?")
                                  (("2"
                                    (inst - "x!1")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst + "l!1")
                                        (("2"
                                          (expand "convergence")
                                          (("2"
                                            (expand "convergence")
                                            (("2"
                                              (flatten)
                                              (("2"
                                                (split +)
                                                (("1" (propax) nil nil)
                                                 ("2"
                                                  (skosimp*)
                                                  (("2"
                                                    (inst
                                                     -
                                                     "epsilon!1")
                                                    (("2"
                                                      (skosimp*)
                                                      (("2"
                                                        (inst
                                                         +
                                                         delta!1)
                                                        (("2"
                                                          (skosimp*)
                                                          (("2"
                                                            (inst?)
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (expand
                                                                 "NQ")
                                                                (("2"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (lemma "not_one_element")
                  (("2" (propax) nil nil)) nil)
                 ("3" (rewrite "deriv_domain"nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-subtype-decl nil deriv_sincos nil)
    (T_pred const-decl "[real -> boolean]" deriv_sincos 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)
    (scal_derivable_fun formula-decl nil derivatives "analysis/")
    (sin_range application-judgement "trig_range" sincos_def nil)
    (deriv_domain formula-decl nil deriv_sincos nil)
    (not_one_element formula-decl nil deriv_sincos nil)
    (sin_derivable formula-decl nil sincos nil)
    (convergent? const-decl "bool" lim_of_functions "analysis/")
    (convergence const-decl "bool" lim_of_functions "analysis/")
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NQ const-decl "real" derivatives_def "analysis/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def "analysis/")
    (minus_odd_is_odd application-judgement "odd_int" integers 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)
    (convergence const-decl "bool" convergence_functions "analysis/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives_def "analysis/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (id_derivable_fun formula-decl nil derivatives "analysis/")
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (comp_derivable_fun formula-decl nil chain_rule "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sin const-decl "real" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (cos_derivable 0
  (cos_derivable-1 nil 3479041957
   ("" (skosimp*)
    (("" (lemma "scal_derivable_fun[T]")
      (("" (inst - "k!1" "(LAMBDA (x: T): cos(alpha!1 * x))")
        (("" (assert)
          (("" (expand "*")
            (("" (hide 2)
              (("" (lemma "comp_derivable_fun[T,real]")
                (("1"
                  (inst - "(LAMBDA (x:T): alpha!1*x)"
                   "(LAMBDA (x:real): cos(x))")
                  (("1" (assert)
                    (("1" (hide 2)
                      (("1" (split +)
                        (("1" (lemma "scal_derivable_fun[T]")
                          (("1" (inst - "alpha!1" "id[T]")
                            (("1" (assert)
                              (("1"
                                (expand "id")
                                (("1"
                                  (expand "*")
                                  (("1"
                                    (hide 2)
                                    (("1"
                                      (lemma "id_derivable_fun[T]")
                                      (("1" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (lemma "cos_derivable")
                          (("2" (expand "derivable?")
                            (("2" (skosimp*)
                              (("2"
                                (expand "derivable?")
                                (("2"
                                  (expand "convergent?")
                                  (("2"
                                    (inst - "x!1")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst + "l!1")
                                        (("2"
                                          (expand "convergence")
                                          (("2"
                                            (expand "convergence")
                                            (("2"
                                              (flatten)
                                              (("2"
                                                (split +)
                                                (("1" (propax) nil nil)
                                                 ("2"
                                                  (skosimp*)
                                                  (("2"
                                                    (inst
                                                     -
                                                     "epsilon!1")
                                                    (("2"
                                                      (skosimp*)
                                                      (("2"
                                                        (inst
                                                         +
                                                         delta!1)
                                                        (("2"
                                                          (skosimp*)
                                                          (("2"
                                                            (inst?)
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (expand
                                                                 "NQ")
                                                                (("2"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (lemma "not_one_element")
                  (("2" (propax) nil nil)) nil)
                 ("3" (rewrite "deriv_domain"nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-subtype-decl nil deriv_sincos nil)
    (T_pred const-decl "[real -> boolean]" deriv_sincos 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)
    (scal_derivable_fun formula-decl nil derivatives "analysis/")
    (cos_range application-judgement "trig_range" sincos_def nil)
    (deriv_domain formula-decl nil deriv_sincos nil)
    (not_one_element formula-decl nil deriv_sincos nil)
    (cos_derivable formula-decl nil sincos nil)
    (convergent? const-decl "bool" lim_of_functions "analysis/")
    (convergence const-decl "bool" lim_of_functions "analysis/")
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NQ const-decl "real" derivatives_def "analysis/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def "analysis/")
    (minus_odd_is_odd application-judgement "odd_int" integers 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)
    (convergence const-decl "bool" convergence_functions "analysis/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives_def "analysis/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (id_derivable_fun formula-decl nil derivatives "analysis/")
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (comp_derivable_fun formula-decl nil chain_rule "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cos const-decl "real" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (deriv_sin_TCC1 0
  (deriv_sin_TCC1-1 nil 3476447874
   ("" (skosimp*)
    (("" (lemma "sin_derivable") (("" (inst?) nil nil)) nil)) nil)
   ((sin_derivable formula-decl nil deriv_sincos 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))
   nil))
 (deriv_sin 0
  (deriv_sin-1 nil 3479041982
   ("" (skosimp*)
    (("" (auto-rewrite-theory "analysis@derivatives_lam[T]")
      (("" (case "derivable?[T](LAMBDA (x: T): sin(alpha!1 * x))")
        (("1" (lemma "deriv_scal_fun[T]")
          (("1" (inst - "k!1" "(LAMBDA (x: T): sin(alpha!1 * x))")
            (("1" (assert)
              (("1" (expand "*")
                (("1" (assert)
                  (("1" (apply-extensionality 2 :hide? t)
                    (("1" (hide -1)
                      (("1" (lemma "deriv_comp_fun[T,real]")
                        (("1"
                          (inst - "(LAMBDA (x:T): alpha!1*x)"
                           "(LAMBDA (x:real): sin(x))")
                          (("1" (expand "o ")
                            (("1" (replace -1)
                              (("1"
                                (hide -1)
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "*")
                                    (("1"
                                      (lemma deriv_scal_fun[T])
                                      (("1"
                                        (inst - "alpha!1" "id[T]")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "id")
                                            (("1"
                                              (expand "*")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (lemma
                                                   "deriv_id_fun[T]")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (lemma
                                                         "deriv_sin_fun")
                                                        (("1"
                                                          (case-replace
                                                           "(LAMBDA (x: real): sin(x)) = sin")
                                                          (("1"
                                                            (replace
                                                             -2)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (apply-extensionality
                                                             1
                                                             :hide?
                                                             t)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (lemma "id_derivable_fun[T]")
                                          (("2"
                                            (expand "id")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma sin_derivable_fun)
                            (("2"
                              (case-replace
                               "(LAMBDA (x: real): sin(x)) = sin")
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (hide 3)
            (("2" (lemma "sin_derivable")
              (("2" (inst?)
                (("2" (inst - "1") (("2" (assertnil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable_const_lam formula-decl nil derivatives_lam "analysis/")
    (sin_derivable formula-decl nil deriv_sincos nil)
    (deriv_scal_fun formula-decl nil derivatives "analysis/")
    (cos_range application-judgement "trig_range" sincos_def nil)
    (deriv_scal1_lam formula-decl nil derivatives_lam "analysis/")
    (derivable_id_lam formula-decl nil derivatives_lam "analysis/")
    (derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
    (deriv_id_lam formula-decl nil derivatives_lam "analysis/")
    (id_derivable_fun formula-decl nil derivatives "analysis/")
    (deriv_id_fun formula-decl nil derivatives "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (deriv_sin_fun formula-decl nil sincos nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (O const-decl "T3" function_props nil)
    (sin_derivable_fun formula-decl nil sincos nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_comp_fun formula-decl nil chain_rule "analysis/")
    (cos const-decl "real" sincos_def nil)
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (alpha!1 skolem-const-decl "real" deriv_sincos nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" deriv_sincos nil)
    (T formal-subtype-decl nil deriv_sincos nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (sin const-decl "real" sincos_def nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   shostak))
 (deriv_cos_TCC1 0
  (deriv_cos_TCC1-1 nil 3476447874
   ("" (skosimp*)
    (("" (lemma "cos_derivable") (("" (inst?) nil nil)) nil)) nil)
   ((cos_derivable formula-decl nil deriv_sincos 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))
   nil))
 (deriv_cos 0
  (deriv_cos-2 nil 3565742105
   ("" (skosimp*)
    (("" (auto-rewrite-theory "analysis@derivatives_lam[T]")
      (("" (case "derivable?[T](LAMBDA (x: T): cos(alpha!1 * x))")
        (("1" (lemma "deriv_scal_fun[T]")
          (("1" (inst - "k!1" "(LAMBDA (x: T): cos(alpha!1 * x))")
            (("1" (assert)
              (("1" (expand "*")
                (("1" (assert)
                  (("1" (apply-extensionality 2 :hide? t)
                    (("1" (hide -1)
                      (("1" (lemma "deriv_comp_fun[T,real]")
                        (("1"
                          (inst - "(LAMBDA (x:T): alpha!1*x)"
                           "(LAMBDA (x:real): cos(x))")
                          (("1" (expand "o ")
                            (("1" (replace -1)
                              (("1"
                                (hide -1)
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "*")
                                    (("1"
                                      (lemma deriv_scal_fun[T])
                                      (("1"
                                        (inst - "alpha!1" "id[T]")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "id")
                                            (("1"
                                              (expand "*")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (lemma
                                                   "deriv_id_fun[T]")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (lemma
                                                         "deriv_cos_fun")
                                                        (("1"
                                                          (case-replace
                                                           "(LAMBDA (x: real): cos(x)) = cos")
                                                          (("1"
                                                            (replace
                                                             -2)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (hide
                                                                 -)
                                                                (("1"
                                                                  (expand
                                                                   "-")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (apply-extensionality
                                                             1
                                                             :hide?
                                                             t)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (lemma "id_derivable_fun[T]")
                                          (("2"
                                            (expand "id")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma cos_derivable_fun)
                            (("2"
                              (case-replace
                               "(LAMBDA (x: real): cos(x)) = cos")
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (hide 3)
            (("2" (lemma "cos_derivable")
              (("2" (inst?)
                (("2" (inst - "1") (("2" (assertnil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable_const_lam formula-decl nil derivatives_lam "analysis/")
    (cos_derivable formula-decl nil deriv_sincos nil)
    (deriv_scal_fun formula-decl nil derivatives "analysis/")
    (minus_real_is_real application-judgement "real" reals nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (deriv_scal1_lam formula-decl nil derivatives_lam "analysis/")
    (derivable_id_lam formula-decl nil derivatives_lam "analysis/")
    (derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
    (deriv_id_lam formula-decl nil derivatives_lam "analysis/")
    (id_derivable_fun formula-decl nil derivatives "analysis/")
    (deriv_id_fun formula-decl nil derivatives "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_cos_fun formula-decl nil sincos nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (O const-decl "T3" function_props nil)
    (cos_derivable_fun formula-decl nil sincos nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_comp_fun formula-decl nil chain_rule "analysis/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (sin const-decl "real" sincos_def nil)
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (alpha!1 skolem-const-decl "real" deriv_sincos nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" deriv_sincos nil)
    (T formal-subtype-decl nil deriv_sincos nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (cos const-decl "real" sincos_def nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil)
  (deriv_cos-1 nil 3479042601
   ("" (skosimp*)
    (("" (auto-rewrite-theory "derivatives_lam[T]")
      (("" (case "derivable?[T](LAMBDA (x: T): cos(alpha!1 * x))")
        (("1" (lemma "deriv_scal_fun[T]")
          (("1" (inst - "k!1" "(LAMBDA (x: T): cos(alpha!1 * x))")
            (("1" (assert)
              (("1" (expand "*")
                (("1" (assert)
                  (("1" (apply-extensionality 2 :hide? t)
                    (("1" (hide -1)
                      (("1" (lemma "deriv_comp_fun[T,real]")
                        (("1"
                          (inst - "(LAMBDA (x:T): alpha!1*x)"
                           "(LAMBDA (x:real): cos(x))")
                          (("1" (expand "o ")
                            (("1" (replace -1)
                              (("1"
                                (hide -1)
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "*")
                                    (("1"
                                      (lemma deriv_scal_fun[T])
                                      (("1"
                                        (inst - "alpha!1" "id[T]")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "id")
                                            (("1"
                                              (expand "*")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (lemma
                                                   "deriv_id_fun[T]")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (lemma
                                                         "deriv_cos_fun")
                                                        (("1"
                                                          (case-replace
                                                           "(LAMBDA (x: real): cos(x)) = cos")
                                                          (("1"
                                                            (replace
                                                             -2)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (hide
                                                                 -)
                                                                (("1"
                                                                  (expand
                                                                   "-")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (apply-extensionality
                                                             1
                                                             :hide?
                                                             t)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (lemma "id_derivable_fun[T]")
                                          (("2"
                                            (expand "id")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma cos_derivable_fun)
                            (("2"
                              (case-replace
                               "(LAMBDA (x: real): cos(x)) = cos")
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (hide 3)
            (("2" (lemma "cos_derivable")
              (("2" (inst?)
                (("2" (inst - "1") (("2" (assertnil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable_const_lam formula-decl nil derivatives_lam "analysis/")
    (deriv_scal_fun formula-decl nil derivatives "analysis/")
    (sin_range application-judgement "trig_range" sincos_def nil)
    (deriv_scal1_lam formula-decl nil derivatives_lam "analysis/")
    (derivable_id_lam formula-decl nil derivatives_lam "analysis/")
    (derivable_scal1_lam formula-decl nil derivatives_lam "analysis/")
    (deriv_id_lam formula-decl nil derivatives_lam "analysis/")
    (id_derivable_fun formula-decl nil derivatives "analysis/")
    (deriv_id_fun formula-decl nil derivatives "analysis/")
    (deriv_cos_fun formula-decl nil sincos nil)
    (cos_derivable_fun formula-decl nil sincos nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_comp_fun formula-decl nil chain_rule "analysis/")
    (sin const-decl "real" sincos_def nil)
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (cos_range application-judgement "trig_range" sincos_def nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (cos const-decl "real" sincos_def nil))
   nil)))


¤ Dauer der Verarbeitung: 0.31 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

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


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff