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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: trig_inverses.prf   Sprache: Unknown

(trig_inverses
 (arcsin_TCC1 0
  (arcsin_TCC1-1 nil 3408970754
   ("" (skosimp*) (("" (rewrite "sin_asin") nil nil)) nil)
   ((sin_asin formula-decl nil sincos_def 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 sincos_def 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)
   ((arcsin const-decl "{x: real_abs_le_pi2 | y = sin(x)}"
     trig_inverses nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (trig_range type-eq-decl nil sincos_def nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (sin_asin formula-decl nil sincos_def nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak))
 (arcsin_sin 0
  (arcsin_sin-1 nil 3408970777
   ("" (skosimp*)
    (("" (expand "arcsin") (("" (rewrite "asin_sin") nil nil)) nil))
    nil)
   ((arcsin const-decl "{x: real_abs_le_pi2 | y = sin(x)}"
     trig_inverses nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (< const-decl "bool" reals nil)
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
    (pi const-decl "posreal" atan 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)
    (asin_sin formula-decl nil sincos_def nil)
    (real_le_is_total_order name-judgement "(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)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx 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" sincos_def nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx 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 sincos_def nil)
    (trig_range type-eq-decl nil sincos_def 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 const-decl "posreal" atan 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)
   ((arccos const-decl "{x: nnreal_le_pi | y = cos(x)}" trig_inverses
     nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (trig_range type-eq-decl nil sincos_def nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (cos_acos formula-decl nil sincos_def nil))
   shostak))
 (arccos_cos 0
  (arccos_cos-1 nil 3408971160
   ("" (skosimp*)
    (("" (expand "arccos") (("" (rewrite "acos_cos") nil nil)) nil))
    nil)
   ((arccos const-decl "{x: nnreal_le_pi | y = cos(x)}" trig_inverses
     nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (pi const-decl "posreal" atan 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)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (acos_cos formula-decl nil sincos_def nil))
   shostak))
 (arctan_prep 0
  (arctan_prep-1 nil 3408971369
   ("" (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" sincos_def 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" sincos_def 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)
    (pi const-decl "posreal" atan nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   nil))
 (arctan_TCC1 0
  (arctan_TCC1-1 nil 3408970754
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (lemma "tan_value_TCC")
        (("" (inst?) (("" (assert) (("" (postpone) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi const-decl "posreal" atan 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)
    (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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans 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)
    (tan_value_TCC formula-decl nil sincos_def nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   nil))
 (arctan_TCC2 0
  (arctan_TCC2-1 nil 3408970754
   ("" (skosimp*) (("" (rewrite "tan_atan") nil nil)) nil)
   ((tan_atan formula-decl nil sincos_def 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")
      (("" (assert)
        (("" (typepred "atan(y!1)")
          (("" (lemma "arctan_prep") (("" (inst?) nil nil)) nil)) 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi const-decl "posreal" atan 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)
    (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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (arctan_prep formula-decl nil trig_inverses nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   nil))
 (tan_arctan 0
  (tan_arctan-1 nil 3408971181
   ("" (skosimp*)
    (("" (expand "arctan") (("" (rewrite "tan_atan") nil nil)) nil))
    nil)
   ((arctan const-decl "{x: real_abs_lt_pi2 | y = tan(x)}"
     trig_inverses 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)
    (tan_atan formula-decl nil sincos_def nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak))
 (arctan_tan 0
  (arctan_tan-1 nil 3408971195
   ("" (skosimp*)
    (("" (expand "arctan")
      (("" (rewrite "atan_tan") (("" (postpone) nil nil)) nil)) nil))
    nil)
   ((arctan const-decl "{x: real_abs_lt_pi2 | y = tan(x)}"
     trig_inverses nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (pi const-decl "posreal" atan 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_tan formula-decl nil sincos_def nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak)))

[ Dauer der Verarbeitung: 0.24 Sekunden  (vorverarbeitet)  ]