Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: evardefine.mli Sprache: Lisp

Original von: PVS^©

(trig_degree
(rad_deg 0
  (rad_deg-1 nil 3269434094 ("" (grind) nil nil)
   ((Integral const-decl "real" integral_def "analysis/")
    (atan_value const-decl "real" atan nil)
    (pi const-decl "posreal" atan nil)
    (toDeg const-decl "real" trig_degree nil)
    (toRad const-decl "real" trig_degree nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(deg_rad 0
  (deg_rad-1 nil 3269434094 ("" (grind) nil nil)
   ((Integral const-decl "real" integral_def "analysis/")
    (atan_value const-decl "real" atan nil)
    (pi const-decl "posreal" atan nil)
    (toRad const-decl "real" trig_degree nil)
    (toDeg const-decl "real" trig_degree nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(tand_TCC1 0
  (tand_TCC1-1 nil 3269434094 ("" (subtype-tcc) nil 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)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (Integral const-decl "real" integral_def "analysis/")
    (atan_value const-decl "real" atan nil)
    (pi const-decl "posreal" atan nil)
    (toRad const-decl "real" trig_degree nil)
    (cos const-decl "real" sincos_def nil)
    (Tan? const-decl "bool" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_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" sincos_def nil)
    (cos_range application-judgement "trig_range" sincos_def 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_lb const-decl "posreal" atan_approx 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 "[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" sincos_def 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" sincos_def 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)
    (Integral const-decl "real" integral_def "analysis/")
    (atan_value const-decl "real" atan nil)
    (pi_ub const-decl "posreal" atan_approx nil)
    (< const-decl "bool" reals 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_13 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) 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_lb const-decl "posreal" atan_approx 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 -> 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" sincos_def 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" sincos_def 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_18 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (pi_ub const-decl "posreal" atan_approx 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)
    (gt_times_gt_any1 formula-decl nil extra_real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (toRad const-decl "real" trig_degree nil))
   nil)))

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.