Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: update-require Sprache: Lisp

Original von: PVS^©

(trig_degree
(rad_deg 0
  (rad_deg-1 nil 3269434094 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (toRad const-decl "real" trig_degree nil)
    (toDeg const-decl "real" trig_degree nil))
   nil))
(deg_rad 0
  (deg_rad-1 nil 3269434094 ("" (grind) nil nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (toDeg const-decl "real" trig_degree nil)
    (toRad const-decl "real" trig_degree nil))
   nil))
(tand_TCC1 0
  (tand_TCC1-1 nil 3269434094 ("" (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)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (toRad const-decl "real" trig_degree nil)
    (/= const-decl "boolean" notequal nil)
    (Tan? const-decl "bool" trig_basic nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   nil))
(sq_sin_cos_d_one 0
  (sq_sin_cos_d_one-1 nil 3269434094
   ("" (skolem 1 "a")
    (("" (expand "sind")
      (("" (expand "cosd")
        (("" (lemma "sin2_cos2")
          (("" (inst?) (("" (ground) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((sind const-decl "real" trig_degree nil)
    (sin2_cos2 formula-decl nil trig_basic nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (toRad const-decl "real" trig_degree 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)
    (cosd const-decl "real" trig_degree nil))
   nil))
(sind_bounds 0
  (sind_bounds-2 nil 3321628718
   ("" (skeep)
    (("" (expand "sind")
      (("" (expand "toRad")
        (("" (case "sin(a * pi / 180) >= sin(a*pi_lb/180)")
          (("1"
            (case "sin(a * pi_lb / 180)>= sin_lb(a * pi_lb / 180,n)")
            (("1" (ground) nil nil)
             ("2" (hide 2)
              (("2" (lemma "sin_bounds")
                (("2" (inst -1 "a * pi_lb / 180" "n")
                  (("2" (ground) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (case "a=0")
              (("1" (replace -1 :hide? t) (("1" (ground) nil nil)) nil)
               ("2" (case "a > 0")
                (("1" (hide 1)
                  (("1" (lemma "sin_increasing")
                    (("1" (inst -1 " a * pi / 180" "a * pi_lb / 180")
                      (("1" (ground)
                        (("1" (hide 2 3)
                          (("1" (cross-mult 1)
                            (("1" (cancel-by 1 "a*180") nil nil)) nil))
                          nil)
                         ("2" (cross-mult)
                          (("2" (hide 2)
                            (("2" (cancel-by 1 "2*pi") nil nil)) nil))
                          nil)
                         ("3" (cross-mult)
                          (("3" (hide 2)
                            (("3" (cancel-by 1 "2*pi") nil nil)) nil))
                          nil)
                         ("4" (hide 2)
                          (("4" (cross-mult 1)
                            (("4" (cancel-by 1 "2")
                              (("4" (grind-reals) nil nil)) nil))
                            nil))
                          nil)
                         ("5" (hide 2)
                          (("5" (cross-mult)
                            (("5" (cancel-by 1 "2")
                              (("5"
                                (typepred "pi")
                                (("5" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sind const-decl "real" trig_degree nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (< const-decl "bool" reals nil)
    (pi_lb const-decl "posreal" trig_basic nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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 "[numfield, 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)
    (sin const-decl "real" trig_basic 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)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (sin_bounds formula-decl nil trig_approx nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sin_lb const-decl "real" trig_approx nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (neg_mult formula-decl nil extra_tegies nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (div_mult_pos_ge2 formula-decl nil real_props nil)
    (both_sides_times_pos_ge1 formula-decl nil real_props nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (zero_times1 formula-decl nil real_props nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (CBD_12 skolem-const-decl "real" trig_degree nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (div_mult_pos_gt2 formula-decl nil extra_real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (times_div2 formula-decl nil real_props nil)
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (sin_increasing formula-decl nil trig_ineq nil)
    (toRad const-decl "real" trig_degree nil))
   nil))
(cosd_bounds 0
  (cosd_bounds-1 nil 3321628868
   ("" (skeep)
    (("" (expand "cosd")
      (("" (expand "toRad")
        (("" (case "cos(a * pi / 180) <= cos(a*pi_lb/180)")
          (("1"
            (case "cos(a * pi_lb / 180) <= cos_ub(a * pi_lb / 180,n)")
            (("1" (ground) nil nil)
             ("2" (hide 2)
              (("2" (lemma "cos_bounds")
                (("2" (inst -1 "a * pi_lb / 180" "n")
                  (("2" (ground) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (lemma "cos_decreasing")
              (("2" (inst -1 "a * pi / 180" "a * pi_lb / 180")
                (("2" (ground)
                  (("1" (hide 2 3)
                    (("1" (cross-mult 1)
                      (("1" (case "a=0")
                        (("1" (replace -1) (("1" (ground) nil nil))
                          nil)
                         ("2" (cancel-by 2 "180*a") nil nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (cross-mult 1)
                      (("2" (cancel-by 1 "pi") nil nil)) nil))
                    nil)
                   ("3" (hide 2)
                    (("3" (cross-mult 1)
                      (("3" (typepred "pi")
                        (("3" (grind-reals) nil nil)) nil))
                      nil))
                    nil)
                   ("4" (hide 2)
                    (("4" (cross-mult)
                      (("4" (typepred "pi")
                        (("4" (swap-rel -3)
                          (("4" (mult-ineq -3 -6)
                            (("4" (assert)
                              (("4"
                                (mult-ineq -4 -8)
                                (("4" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("5" (hide 2)
                    (("5" (cross-mult 1) (("5" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cosd const-decl "real" trig_degree nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (< const-decl "bool" reals nil)
    (pi_lb const-decl "posreal" trig_basic nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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 -> 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)
    (cos const-decl "real" trig_basic 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)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (cos_bounds formula-decl nil trig_approx nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (cos_ub const-decl "real" trig_approx nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (cos_decreasing formula-decl nil trig_ineq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (times_div2 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_mult_pos_gt2 formula-decl nil extra_real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (CBD_17 skolem-const-decl "real" trig_degree nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (both_sides_times_pos_le1 formula-decl nil real_props 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)
    (pos_times_ge formula-decl nil real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (abs_nat formula-decl nil abs_lems "reals/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (lt_times_lt_any1 formula-decl nil extra_real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (toRad const-decl "real" trig_degree nil))
   nil)))

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