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") (("" (assert) nil 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_ax/")
    (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_ax/")
    (sin_range application-judgement "trig_range" trig_basic 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_ax/")
    (continuous? const-decl "bool" continuous_functions "analysis_ax/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions "analysis_ax/")
    (sin_continuous formula-decl nil sincos nil)
    (O const-decl "T3" function_props nil)
    (composition_cont_fun formula-decl nil composition_continuous
     "analysis_ax/")
    (* 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" trig_basic 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_ax/")
    (cos_range application-judgement "trig_range" trig_basic 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_ax/")
    (continuous? const-decl "bool" continuous_functions "analysis_ax/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions "analysis_ax/")
    (cos_continuous formula-decl nil sincos nil)
    (O const-decl "T3" function_props nil)
    (composition_cont_fun formula-decl nil composition_continuous
     "analysis_ax/")
    (* 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" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(sin_derivable_TCC1 0
  (sin_derivable_TCC1-1 nil 3602322963
   ("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
   ((deriv_domain formula-decl nil deriv_sincos nil)) nil))
(sin_derivable_TCC2 0
  (sin_derivable_TCC2-1 nil 3602322963
   ("" (lemma "not_one_element") (("" (propax) nil 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" (expand "derivable?")
                          (("2" (lemma "sin_derivable")
                            (("2" (skosimp*)
                              (("2"
                                (inst?)
                                (("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)
                 ("2" (lemma "not_one_element")
                  (("2" (propax) nil nil)) nil)
                 ("3" (lemma "deriv_domain") (("3" (propax) 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_derivable_fun formula-decl nil derivatives "analysis_ax/")
    (sin_range application-judgement "trig_range" trig_basic nil)
    (deriv_domain formula-decl nil deriv_sincos nil)
    (not_one_element formula-decl nil deriv_sincos nil)
    (derivable? const-decl "bool" derivatives "analysis_ax/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sin_derivable formula-decl nil sincos nil)
    (id_derivable_fun formula-decl nil derivatives "analysis_ax/")
    (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_ax/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/")
    (comp_derivable_fun formula-decl nil chain_rule "analysis_ax/")
    (* 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" trig_basic 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" (expand "derivable?")
                          (("2" (skosimp*)
                            (("2" (lemma "cos_derivable")
                              (("2"
                                (inst?)
                                (("2"
                                  (assert)
                                  (("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)
                 ("2" (lemma "not_one_element")
                  (("2" (propax) nil nil)) nil)
                 ("3" (lemma "deriv_domain") (("3" (propax) 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_derivable_fun formula-decl nil derivatives "analysis_ax/")
    (cos_range application-judgement "trig_range" trig_basic nil)
    (deriv_domain formula-decl nil deriv_sincos nil)
    (not_one_element formula-decl nil deriv_sincos nil)
    (derivable? const-decl "bool" derivatives "analysis_ax/")
    (cos_derivable formula-decl nil sincos nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (id_derivable_fun formula-decl nil derivatives "analysis_ax/")
    (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_ax/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/")
    (comp_derivable_fun formula-decl nil chain_rule "analysis_ax/")
    (* 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" trig_basic 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_ax@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" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable_const_lam formula-decl nil derivatives_lam
     "analysis_ax/")
    (sin_derivable formula-decl nil deriv_sincos nil)
    (deriv_scal_fun formula-decl nil derivatives "analysis_ax/")
    (cos_range application-judgement "trig_range" trig_basic nil)
    (deriv_scal1_lam formula-decl nil derivatives_lam "analysis_ax/")
    (derivable_id_lam formula-decl nil derivatives_lam "analysis_ax/")
    (derivable_scal1_lam formula-decl nil derivatives_lam
     "analysis_ax/")
    (deriv_id_lam formula-decl nil derivatives_lam "analysis_ax/")
    (id_derivable_fun formula-decl nil derivatives "analysis_ax/")
    (deriv_id_fun formula-decl nil derivatives "analysis_ax/")
    (= 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_ax/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/")
    (deriv_comp_fun formula-decl nil chain_rule "analysis_ax/")
    (cos const-decl "real" trig_basic nil)
    (deriv const-decl "[T -> real]" derivatives "analysis_ax/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives "analysis_ax/")
    (alpha!1 skolem-const-decl "real" deriv_sincos nil)
    (sin_range application-judgement "trig_range" trig_basic 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_ax/")
    (sin const-decl "real" trig_basic 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-3 nil 3602324889
   ("" (skosimp*)
    (("" (auto-rewrite-theory "analysis_ax@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" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable_const_lam formula-decl nil derivatives_lam
     "analysis_ax/")
    (cos_derivable formula-decl nil deriv_sincos nil)
    (deriv_scal_fun formula-decl nil derivatives "analysis_ax/")
    (minus_real_is_real application-judgement "real" reals nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (deriv_scal1_lam formula-decl nil derivatives_lam "analysis_ax/")
    (derivable_id_lam formula-decl nil derivatives_lam "analysis_ax/")
    (derivable_scal1_lam formula-decl nil derivatives_lam
     "analysis_ax/")
    (deriv_id_lam formula-decl nil derivatives_lam "analysis_ax/")
    (id_derivable_fun formula-decl nil derivatives "analysis_ax/")
    (deriv_id_fun formula-decl nil derivatives "analysis_ax/")
    (= 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_ax/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/")
    (deriv_comp_fun formula-decl nil chain_rule "analysis_ax/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (sin const-decl "real" trig_basic nil)
    (deriv const-decl "[T -> real]" derivatives "analysis_ax/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives "analysis_ax/")
    (alpha!1 skolem-const-decl "real" deriv_sincos nil)
    (cos_range application-judgement "trig_range" trig_basic 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_ax/")
    (cos const-decl "real" trig_basic nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil)
  (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" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable_const_lam formula-decl nil derivatives_lam
     "analysis_ax/")
    (deriv_scal_fun formula-decl nil derivatives "analysis_ax/")
    (deriv_scal1_lam formula-decl nil derivatives_lam "analysis_ax/")
    (derivable_id_lam formula-decl nil derivatives_lam "analysis_ax/")
    (derivable_scal1_lam formula-decl nil derivatives_lam
     "analysis_ax/")
    (deriv_id_lam formula-decl nil derivatives_lam "analysis_ax/")
    (id_derivable_fun formula-decl nil derivatives "analysis_ax/")
    (deriv_id_fun formula-decl nil derivatives "analysis_ax/")
    (not_one_element? const-decl "bool" deriv_domain_def
     "analysis_ax/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/")
    (deriv_comp_fun formula-decl nil chain_rule "analysis_ax/")
    (deriv const-decl "[T -> real]" derivatives "analysis_ax/")
    (deriv_fun type-eq-decl nil derivatives "analysis_ax/")
    (derivable? const-decl "bool" derivatives "analysis_ax/"))
   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" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable_const_lam formula-decl nil derivatives_lam
     "analysis_ax/")
    (deriv_scal_fun formula-decl nil derivatives "analysis_ax/")
    (deriv_scal1_lam formula-decl nil derivatives_lam "analysis_ax/")
    (derivable_id_lam formula-decl nil derivatives_lam "analysis_ax/")
    (derivable_scal1_lam formula-decl nil derivatives_lam
     "analysis_ax/")
    (deriv_id_lam formula-decl nil derivatives_lam "analysis_ax/")
    (id_derivable_fun formula-decl nil derivatives "analysis_ax/")
    (deriv_id_fun formula-decl nil derivatives "analysis_ax/")
    (not_one_element? const-decl "bool" deriv_domain_def
     "analysis_ax/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis_ax/")
    (deriv_comp_fun formula-decl nil chain_rule "analysis_ax/")
    (deriv const-decl "[T -> real]" derivatives "analysis_ax/")
    (deriv_fun type-eq-decl nil derivatives "analysis_ax/")
    (derivable? const-decl "bool" derivatives "analysis_ax/"))
   nil)))

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