Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: trig_inverses.prf Sprache: Lisp

Original von: PVS^©

(trig_inverses
(atan_prep 0
  (atan_prep-1 nil 3408978488
   ("" (skosimp*)
    (("" (expand "Tan?")
      (("" (typepred "x!1")
        (("" (flatten)
          (("" (lemma "cos_eq_0")
            (("" (inst?)
              (("" (assert)
                (("" (skosimp*)
                  (("" (hide -4)
                    (("" (replace -1)
                      (("" (hide -1)
                        (("" (case "i!1 = 0")
                          (("1" (assert) nil nil)
                           ("2" (mult-by -1 "2")
                            (("2" (assert)
                              (("2"
                                (mult-by -2 "2")
                                (("2"
                                  (assert)
                                  (("2"
                                    (case-replace "2 * (pi / 2) = pi")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (case "i!1 > 0")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (mult-by -1 "2*pi")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (case "i!1 < -1")
                                            (("1"
                                              (mult-by -1 "2*pi")
                                              (("1" (assert) nil nil))
                                              nil)
                                             ("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Tan? const-decl "bool" trig_basic nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_eq_0 formula-decl nil trig_basic nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi_lb const-decl "posreal" trig_basic nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   shostak))
(tan_atan_TCC1 0
  (tan_atan_TCC1-1 nil 3408978481
   ("" (skosimp*) (("" (rewrite "atan_prep") nil nil)) nil)
   ((atan_prep formula-decl nil trig_inverses nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (pi_lb const-decl "posreal" trig_basic nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (atan const-decl "real_abs_lt_pi2" atan nil))
   nil))
(atan_tan_TCC1 0
  (atan_tan_TCC1-1 nil 3408978481
   ("" (skosimp*) (("" (rewrite "atan_prep") nil nil)) nil)
   ((atan_prep formula-decl nil trig_inverses nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (pi_lb const-decl "posreal" trig_basic nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   nil))
(arcsin_TCC1 0
  (arcsin_TCC1-1 nil 3408970754
   ("" (skosimp*) (("" (rewrite "sin_asin") nil nil)) nil)
   ((sin_asin formula-decl nil trig_inverses nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (trig_range type-eq-decl nil trig_basic nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil))
   nil))
(sin_arcsin 0
  (sin_arcsin-1 nil 3408970763
   ("" (skosimp*)
    (("" (expand "arcsin") (("" (rewrite "sin_asin") nil nil)) nil))
    nil)
   ((real_abs_le1 nonempty-type-eq-decl nil asin nil)) shostak))
(arcsin_sin 0
  (arcsin_sin-1 nil 3408970777
   ("" (skosimp*)
    (("" (expand "arcsin") (("" (rewrite "asin_sin") nil nil)) nil))
    nil)
   ((real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)) shostak))
(arccos_TCC1 0
  (arccos_TCC1-1 nil 3408970754
   ("" (skosimp*)
    (("" (assert)
      (("" (typepred "acos(y!1)")
        (("" (assert) (("" (rewrite "cos_acos") nil nil)) nil)) nil))
      nil))
    nil)
   ((cos_range application-judgement "trig_range" trig_basic nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_acos formula-decl nil trig_inverses nil)
    (trig_range type-eq-decl nil trig_basic nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (nnreal type-eq-decl nil real_types 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)
    (pi_lb const-decl "posreal" trig_basic nil)
    (< const-decl "bool" reals nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (acos const-decl "nnreal_le_pi" acos nil))
   nil))
(cos_arccos 0
  (cos_arccos-1 nil 3408970791
   ("" (skosimp*)
    (("" (expand "arccos") (("" (rewrite "cos_acos") nil nil)) nil))
    nil)
   ((real_abs_le1 nonempty-type-eq-decl nil asin nil)) shostak))
(arccos_cos 0
  (arccos_cos-1 nil 3408971160
   ("" (skosimp*)
    (("" (expand "arccos") (("" (rewrite "acos_cos") nil nil)) nil))
    nil)
   ((nnreal_le_pi nonempty-type-eq-decl nil acos nil)) shostak))
(arctan_prep 0
  (arctan_prep-1 nil 3422961014
   ("" (skosimp*)
    (("" (expand "Tan?")
      (("" (typepred "x!1")
        (("" (lemma "cos_eq_0_2pi")
          (("" (inst?)
            (("" (assert)
              (("" (lemma "cos_period")
                (("" (inst?)
                  (("" (inst -1 "1")
                    (("" (replace -1)
                      (("" (hide -1)
                        (("" (lemma "cos_eq_0_2pi")
                          (("" (inst?) (("" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Tan? const-decl "bool" trig_basic nil)
    (cos_eq_0_2pi formula-decl nil trig_basic nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" 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)
    (integer nonempty-type-from-decl nil integers nil)
    (cos_period formula-decl nil trig_basic nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi_lb const-decl "posreal" trig_basic nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   nil))
(arctan_TCC1 0
  (arctan_TCC1-1 nil 3408970754
   ("" (skosimp*) (("" (rewrite "tan_atan") nil nil)) nil)
   ((tan_atan formula-decl nil trig_inverses 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))
(tan_arctan_TCC1 0
  (tan_arctan_TCC1-1 nil 3408970754
   ("" (skosimp*)
    (("" (expand "arctan") (("" (rewrite "atan_prep") nil nil)) nil))
    nil)
   ((arctan const-decl "{x: real_abs_lt_pi2 | y = tan(x)}"
     trig_inverses nil)
    (atan const-decl "real_abs_lt_pi2" atan nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi_lb const-decl "posreal" trig_basic nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (atan_prep formula-decl nil trig_inverses nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   nil))
(tan_arctan 0
  (tan_arctan-1 nil 3408971181
   ("" (skosimp*)
    (("" (expand "arctan") (("" (rewrite "tan_atan") nil nil)) nil))
    nil)
   nil shostak))
(arctan_tan 0
  (arctan_tan-1 nil 3408971195
   ("" (skosimp*)
    (("" (expand "arctan")
      (("" (rewrite "atan_tan") (("" (postpone) nil nil)) nil)) nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)) shostak)))

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