Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: exponent_props.prf Sprache: Lisp

Original von: PVS^©

(exponent_props
(abs_expt 0
  (abs_expt-1 nil 3302968830
   ("" (induct-and-simplify "n" :rewrites "abs_mult") nil nil)
   ((abs_mult formula-decl nil real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_expt application-judgement "nnreal" exponentiation nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (expt def-decl "real" exponentiation nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types 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)
    (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))
(expt_ne_0 0
  (expt_ne_0-1 nil 3302968830
   ("" (induct "n")
    (("1" (skosimp*)
      (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "expt" -2)
        (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((nzreal_expt application-judgement "nzreal" exponentiation nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (expt def-decl "real" exponentiation nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (pred type-eq-decl nil defined_types 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)
    (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))
   shostak))
(abs_expt_inv 0
  (abs_expt_inv-1 nil 3302968830
   ("" (induct "n" 1)
    (("1" (grind) nil nil)
     ("2" (skosimp*)
      (("2" (expand "expt" 1)
        (("2" (lemma "div_times")
          (("2" (inst -1 "abs(z!1) " "expt(abs(z!1), j!1)" "1" "1")
            (("2" (assert)
              (("2" (replace -1 * rl)
                (("2" (hide -1)
                  (("2" (inst -1 "z!1")
                    (("2" (replace -1 * rl)
                      (("2" (hide -1)
                        (("2" (name-replace "EXPT" "expt(z!1, j!1)")
                          (("2"
                            (case-replace
                             "1 / (z!1 * EXPT) = 1 / z!1 * 1/EXPT")
                            (("1" (hide -1)
                              (("1"
                                (lemma "abs_mult")
                                (("1"
                                  (inst -1 "1/z!1" "1/EXPT")
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (case-replace
                                         "abs(1 / z!1) = 1/abs(z!1)")
                                        (("1"
                                          (hide 2)
                                          (("1"
                                            (lemma "pos_div_lt")
                                            (("1"
                                              (inst?)
                                              (("1" (grind) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((div_times formula-decl nil real_props nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pos_div_lt formula-decl nil real_props nil)
    (abs_mult formula-decl nil real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (expt def-decl "real" exponentiation nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (pred type-eq-decl nil defined_types 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)
    (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)
    (nzreal_expt application-judgement "nzreal" exponentiation nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_expt application-judgement "posreal" exponentiation nil))
   nil))
(zero_hat 0
  (zero_hat-1 nil 3302968830
   ("" (induct "pn")
    (("1" (grind) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (expand "^")
        (("3" (expand "expt" 1) (("3" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((expt def-decl "real" exponentiation nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (> const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types 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)
    (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))
(mult_hat_TCC1 0
  (mult_hat_TCC1-1 nil 3302968830 ("" (subtype-tcc) nil nil) nil nil))
(mult_hat_TCC2 0
  (mult_hat_TCC2-1 nil 3302968830 ("" (subtype-tcc) nil nil) nil nil))
(mult_hat 0
  (mult_hat-1 nil 3302968830
   ("" (skosimp*)
    (("" (expand "^")
      (("" (ground)
        (("" (lift-if)
          (("" (ground)
            (("1" (rewrite "expt_of_mult") nil nil)
             ("2" (rewrite "expt_of_mult") (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((^ const-decl "real" exponentiation nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (expt_of_mult formula-decl nil exponentiation 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nzreal_expt application-judgement "nzreal" exponentiation nil))
   nil))
(div_hat_TCC1 0
  (div_hat_TCC1-1 nil 3302968830 ("" (subtype-tcc) nil nil) nil nil))
(div_hat 0
  (div_hat-1 nil 3302968830
   ("" (skosimp*)
    (("" (expand "^")
      (("" (lift-if)
        (("" (ground)
          (("1" (rewrite "expt_of_div") nil nil)
           ("2" (rewrite "expt_of_div") (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((^ const-decl "real" exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nzreal_expt application-judgement "nzreal" exponentiation nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (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)
    (expt_of_div formula-decl nil exponentiation nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil))
   nil))
(inv_hat 0
  (inv_hat-1 nil 3302968830
   ("" (skosimp*)
    (("" (expand "^")
      (("" (lift-if)
        (("" (ground)
          (("1" (rewrite "expt_of_inv") nil nil)
           ("2" (rewrite "expt_of_inv") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((^ const-decl "real" exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nzreal_expt application-judgement "nzreal" exponentiation nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (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)
    (expt_of_inv formula-decl nil exponentiation nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil))
   nil))
(abs_hat_TCC1 0
  (abs_hat_TCC1-1 nil 3302968830 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(abs_hat 0
  (abs_hat-1 nil 3302968830
   ("" (skosimp*)
    (("" (expand "^")
      (("" (lift-if)
        (("" (ground)
          (("1" (rewrite "abs_expt") nil nil)
           ("2" (rewrite "abs_expt_inv") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((nzreal_expt application-judgement "nzreal" exponentiation nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (^ const-decl "real" exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_expt application-judgement "posreal" exponentiation nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (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)
    (abs_expt formula-decl nil exponent_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (abs_expt_inv formula-decl nil exponent_props nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil))
   nil)))

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