Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Sprache: Lisp

Original von: PVS^©

(deriv_dot_prod
(IMP_derivatives_TCC1 0
  (IMP_derivatives_TCC1-1 nil 3460377073
   ("" (lemma "deriv_domain")
    (("" (expand "deriv_domain?") (("" (propax) nil nil)) nil)) nil)
   ((deriv_domain formula-decl nil deriv_dot_prod nil)) nil))
(IMP_derivatives_TCC2 0
  (IMP_derivatives_TCC2-1 nil 3460377073
   ("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
   ((not_one_element formula-decl nil deriv_dot_prod nil)) nil))
(dot_prod_derivable 0
  (dot_prod_derivable-1 nil 3460464646
   ("" (skosimp*)
    (("" (expand "derivable?" -)
      (("" (expand "*")
        (("" (lemma "sigma_derivable")
          ((""
            (inst - "n" "x1!1"
             "(LAMBDA (x: T): LAMBDA (i: Index[n]): f1!1(x)(i) * f2!1(x)(i))")
            (("" (assert)
              (("" (hide 2)
                (("" (skosimp*)
                  (("" (lemma "prod_derivable")
                    ((""
                      (inst - "(LAMBDA (x: T): f1!1(x)(i!1))"
                       "(LAMBDA (x: T): f2!1(x)(i!1))" "x1!1")
                      (("" (assert)
                        (("" (expand "*")
                          (("" (hide 2)
                            (("" (inst?)
                              ((""
                                (inst?)
                                (("" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable? const-decl "bool" deriv_real_vect_def nil)
    (T formal-subtype-decl nil deriv_dot_prod nil)
    (T_pred const-decl "[real -> boolean]" deriv_dot_prod 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)
    (sigma_derivable formula-decl nil deriv_sigma nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (below type-eq-decl nil nat_types nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (prod_derivable formula-decl nil derivatives_def "analysis/")
    (Vector type-eq-decl nil vectors "vectors/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (Index type-eq-decl nil vectors "vectors/")
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (n formal-const-decl "posnat" deriv_dot_prod nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors "vectors/"))
   shostak))
(deriv_dot_prod_TCC1 0
  (deriv_dot_prod_TCC1-1 nil 3460377073
   ("" (skosimp*)
    (("" (lemma "dot_prod_derivable")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((dot_prod_derivable formula-decl nil deriv_dot_prod nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (n formal-const-decl "posnat" deriv_dot_prod nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (T formal-subtype-decl nil deriv_dot_prod nil)
    (T_pred const-decl "[real -> boolean]" deriv_dot_prod nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(deriv_dot_prod 0
  (deriv_dot_prod-1 nil 3460385133
   ("" (skosimp*)
    ((""
      (case "derivable?(LAMBDA (x: T):
                          LAMBDA (i: Index[n]): f1!1(x)(i) * f2!1(x)(i),
                        x1!1)")
      (("1" (lemma "deriv_sigma")
        (("1" (expand "*")
          (("1" (inst - "n " "x1!1")
            (("1" (assert)
              (("1"
                (inst -
                 "LAMBDA (x: T): LAMBDA (i: Index[n]): f1!1(x)(i) * f2!1(x)(i)")
                (("1" (split -1)
                  (("1" (replace -1)
                    (("1" (hide -1)
                      (("1" (lemma "sigma_sum")
                        (("1" (inst?)
                          (("1" (replace -1)
                            (("1" (hide -1)
                              (("1"
                                (rewrite "sigma_eq")
                                (("1"
                                  (hide 2)
                                  (("1"
                                    (skosimp*)
                                    (("1"
                                      (case-replace
                                       "deriv(LAMBDA (x: T): LAMBDA (i: Index[n]): f1!1(x)(i) * f2!1(x)(i), x1!1) (n1!1)
                           = deriv(LAMBDA (x: T): f1!1(x)(n1!1) * f2!1(x)(n1!1), x1!1)")
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (lemma "deriv_prod")
                                          (("1"
                                            (inst
                                             -
                                             "(LAMBDA (x: T): f1!1(x)(n1!1))"
                                             "(LAMBDA (x: T): f2!1(x)(n1!1))"
                                             "x1!1")
                                            (("1"
                                              (split -1)
                                              (("1"
                                                (expand "*")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (hide -1)
                                                      (("1"
                                                        (expand
                                                         "deriv"
                                                         1
                                                         3)
                                                        (("1"
                                                          (expand
                                                           "deriv"
                                                           1
                                                           2)
                                                          (("1"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide -1 2)
                                                (("2"
                                                  (expand
                                                   "derivable?"
                                                   -1)
                                                  (("2"
                                                    (inst?)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (hide -1 2)
                                                (("3"
                                                  (expand
                                                   "derivable?"
                                                   -2)
                                                  (("3"
                                                    (inst?)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (expand "deriv" 1 1)
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil)
                                       ("3"
                                        (hide 2)
                                        (("3"
                                          (assert)
                                          (("3"
                                            (expand "derivable?" -1)
                                            (("3" (inst?) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (skosimp*)
                      (("2" (assert)
                        (("2" (expand "derivable?" -1)
                          (("2" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (lemma "prod_derivable")
          (("2" (inst?)
            (("2" (expand "derivable?" 1)
              (("2" (skosimp*)
                (("2"
                  (inst - "(LAMBDA (x: T): f1!1(x)(i!1))"
                   "(LAMBDA (x: T): f2!1(x)(i!1))")
                  (("2" (assert)
                    (("2" (expand "*")
                      (("2" (hide 2)
                        (("2" (expand "derivable?" -)
                          (("2" (inst?)
                            (("2" (inst?) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (derivable? const-decl "bool" deriv_real_vect_def nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (n formal-const-decl "posnat" deriv_dot_prod nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (T formal-subtype-decl nil deriv_dot_prod nil)
    (T_pred const-decl "[real -> boolean]" deriv_dot_prod nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors "vectors/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (T_low type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (deriv const-decl "Vector[n]" deriv_real_vect_def nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (deriv const-decl "real" derivatives_def "analysis/")
    (derivable? const-decl "bool" derivatives_def "analysis/")
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (deriv_prod formula-decl nil derivatives_def "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (below type-eq-decl nil nat_types nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil naturalnumbers nil)
    (sigma_sum formula-decl nil sigma "reals/")
    (deriv_sigma formula-decl nil deriv_sigma nil)
    (prod_derivable formula-decl nil derivatives_def "analysis/"))
   shostak)))

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