Quelle trig_values.prf Sprache: Lisp

(trig_values
(sin_cos_pi4 0
  (sin_cos_pi4-1 nil 3285696344
   ("" (lemma "sin_shift")
    (("" (inst -1 "pi/4") (("" (assert) nil nil)) nil)) nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (< 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)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_shift formula-decl nil trig_basic nil))
   nil))
(cos_pi4 0
  (cos_pi4-1 nil 3285696344
   ("" (lemma "sin2_cos2")
    (("" (inst -1 "pi/4")
      (("" (lemma "sin_cos_pi4")
        (("" (case "sq(sin(pi / 4)) = sq(cos(pi / 4))")
          (("1" (replace -1 :hide? t)
            (("1" (hide -1)
              (("1" (ground)
                (("1" (case "sqrt(2 * sq(cos(pi / 4))) = sqrt(1)")
                  (("1" (case "sqrt(1)=1")
                    (("1" (replace -1 :hide? t)
                      (("1" (rewrite "sqrt_times")
                        (("1" (rewrite "sqrt_sq")
                          (("1" (hide -2)
                            (("1" (lemma "both_sides_div1")
                              (("1"
                                (inst
                                 -1
                                 "sqrt(2)"
                                 "sqrt(2) * cos(pi / 4)"
                                 "1")
                                (("1" (ground) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide -1 -2 2)
                            (("2" (lemma "cos_decreasing")
                              (("2"
                                (inst -1 "pi/2" "pi/4")
                                (("2"
                                  (ground)
                                  (("2"
                                    (rewrite "cos_pi2")
                                    (("2" (ground) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide -1 -2 2) (("2" (assert) nil nil)) nil))
                    nil)
                   ("2" (expand "sq")
                    (("2" (ground)
                      (("2" (replace -1) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (< 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)
    (cos const-decl "real" trig_basic nil)
    (sin const-decl "real" trig_basic nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sqrt_1 formula-decl nil sqrt "reals/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (sqrt_sq_neg formula-decl nil sqrt "reals/")
    (both_sides_div1 formula-decl nil real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_decreasing formula-decl nil trig_ineq nil)
    (real_le_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)
    (cos_pi2 formula-decl nil trig_basic nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqrt_times formula-decl nil sqrt "reals/")
    (cos_range application-judgement "trig_range" trig_basic nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sin_range application-judgement "trig_range" trig_basic nil)
    (sin_cos_pi4 formula-decl nil trig_values nil)
    (sin2_cos2 formula-decl nil trig_basic nil))
   nil))
(sin_pi4 0
  (sin_pi4-1 nil 3285696344
   ("" (lemma "cos_pi4")
    (("" (lemma "sin_cos_pi4") (("" (ground) nil nil)) nil)) nil)
   ((sin_cos_pi4 formula-decl nil trig_values nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (cos_range application-judgement "trig_range" trig_basic nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_pi4 formula-decl nil trig_values nil))
   nil))
(cos_3pi4 0
  (cos_3pi4-1 nil 3422012245
   ("" (lemma "cos_plus")
    (("" (inst -1 "pi/2" "pi/4")
      (("" (case-replace "pi / 2 + pi / 4 = 3*pi/4")
        (("1" (hide -1)
          (("1" (rewrite "cos_pi2")
            (("1" (rewrite "cos_pi4")
              (("1" (rewrite "sin_pi4")
                (("1" (rewrite "sin_pi2") (("1" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (< 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)
    (cos_pi4 formula-decl nil trig_values nil)
    (sin_pi2 formula-decl nil trig_basic nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sin_pi4 formula-decl nil trig_values nil)
    (cos_pi2 formula-decl nil trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos_plus formula-decl nil trig_basic nil))
   nil))
(sin_3pi4 0
  (sin_3pi4-1 nil 3422012282
   ("" (lemma "sin_plus")
    (("" (inst -1 "pi/4" "pi/2")
      (("" (case-replace "pi/2 + pi / 4 = 3*pi/4")
        (("1" (hide -1)
          (("1" (rewrite "cos_pi4")
            (("1" (rewrite "sin_pi4")
              (("1" (rewrite "sin_pi2")
                (("1" (rewrite "cos_pi2") (("1" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (< 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)
    (sin_pi4 formula-decl nil trig_values nil)
    (cos_pi2 formula-decl nil trig_basic nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sin_pi2 formula-decl nil trig_basic nil)
    (cos_pi4 formula-decl nil trig_values nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_plus formula-decl nil trig_basic nil))
   nil))
(tan_pi4_TCC1 0
  (tan_pi4_TCC1-1 nil 3285696344 ("" (rewrite "tan_pi2_def") nil 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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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_pi2_def formula-decl nil trig_ineq nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   nil))
(tan_pi4 0
  (tan_pi4-1 nil 3285696344
   ("" (expand "tan")
    (("" (rewrite "sin_cos_pi4") (("" (assert) nil nil)) nil)) nil)
   ((sin_cos_pi4 formula-decl nil trig_values nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (tan const-decl "real" trig_basic nil))
   nil))
(sin_pi3_cos_pi6 0
  (sin_pi3_cos_pi6-1 nil 3285696344
   ("" (lemma "sin_shift")
    (("" (inst -1 "pi/6") (("" (assert) nil nil)) nil)) nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (< 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)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_shift formula-decl nil trig_basic nil))
   nil))
(sin_pi6_cos_pi3 0
  (sin_pi6_cos_pi3-1 nil 3285696344
   ("" (lemma "sin_shift")
    (("" (inst -1 "pi/3") (("" (assert) nil nil)) nil)) nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (< 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)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_shift formula-decl nil trig_basic nil))
   nil))
(sin_pi6 0
  (sin_pi6-1 nil 3285696344
   ("" (lemma "sin_pi6_cos_pi3")
    (("" (case "cos(pi / 6) = sin(pi / 3)")
      (("1" (case "sin(pi / 3) = sin(pi/6+pi/6)")
        (("1" (rewrite "sin_plus" -1)
          (("1" (hide -2)
            (("1"
              (case-replace
               "cos(pi / 6) * sin(pi / 6) + sin(pi / 6) * cos(pi / 6) = 2 * cos(pi / 6) * sin(pi / 6)")
              (("1" (hide -1)
                (("1" (lemma "both_sides_times1")
                  (("1" (inst -1 "cos(pi/6)" "sin(pi/6)" "1/2")
                    (("1" (assert) nil nil)
                     ("2" (lemma "cos_eq_0")
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (skosimp*)
                            (("2" (hide -2 -3 1)
                              (("2"
                                (case "1/6 = 1/2 +i!1")
                                (("1"
                                  (hide -2)
                                  (("1" (assert) nil nil))
                                  nil)
                                 ("2"
                                  (assert)
                                  (("2"
                                    (lemma "both_sides_times1")
                                    (("2"
                                      (inst
                                       -1
                                       "pi"
                                       "1 / 6"
                                       "1 / 2 + i!1")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil)
       ("2" (rewrite "sin_pi3_cos_pi6") nil nil))
      nil))
    nil)
   ((sin const-decl "real" trig_basic 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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_plus formula-decl nil trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (cos_eq_0 formula-decl nil trig_basic nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_pi3_cos_pi6 formula-decl nil trig_values nil)
    (sin_pi6_cos_pi3 formula-decl nil trig_values nil))
   nil))
(cos_pi6 0
  (cos_pi6-1 nil 3285696344
   ("" (lemma "sin_pi6")
    (("" (lemma "cos2")
      (("" (inst?)
        (("" (rewrite "sqrt_eq" :dir rl)
          (("" (rewrite "sqrt_sq")
            (("1" (replace -2)
              (("1" (replace -1)
                (("1" (hide -1 -2)
                  (("1" (both-sides-f 1 "sq")
                    (("1" (sq-simp)
                      (("1" (grind) nil nil)
                       ("2" (hide 2) (("2" (grind) nil nil)) nil))
                      nil)
                     ("2" (rewrite "sq_eq") (("2" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (rewrite "cos_ge_0") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cos2 formula-decl nil trig_basic nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sqrt_eq formula-decl nil sqrt "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (cos const-decl "real" trig_basic nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sin const-decl "real" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (real_lt_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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_ge_0 formula-decl nil trig_ineq nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sq_eq formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sq_div formula-decl nil sq "reals/")
    (sq_1 formula-decl nil sq "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (sqrt_sq_neg formula-decl nil sqrt "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_pi6 formula-decl nil trig_values nil))
   nil))
(tan_pi6_TCC1 0
  (tan_pi6_TCC1-1 nil 3285696344
   ("" (expand "Tan?")
    (("" (rewrite "cos_pi6") (("" (assert) nil nil)) nil)) nil)
   ((cos_pi6 formula-decl nil trig_values nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (Tan? const-decl "bool" trig_basic nil))
   nil))
(tan_pi6 0
  (tan_pi6-1 nil 3285696344
   ("" (expand "tan")
    (("" (rewrite "sin_pi6")
      (("" (rewrite "cos_pi6") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sin_pi6 formula-decl nil trig_values nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos_pi6 formula-decl nil trig_values nil)
    (tan const-decl "real" trig_basic nil))
   nil))
(sin_pi3 0
  (sin_pi3-1 nil 3285696344
   ("" (rewrite "sin_pi3_cos_pi6") (("" (rewrite "cos_pi6") nil nil))
    nil)
   ((cos_pi6 formula-decl nil trig_values nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sin_pi3_cos_pi6 formula-decl nil trig_values nil))
   nil))
(cos_pi3 0
  (cos_pi3-1 nil 3285696344
   ("" (rewrite "sin_pi6_cos_pi3" :dir rl)
    (("" (rewrite "sin_pi6") nil nil)) nil)
   ((sin_pi6 formula-decl nil trig_values nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_pi6_cos_pi3 formula-decl nil trig_values nil))
   nil))
(tan_pi3_TCC1 0
  (tan_pi3_TCC1-1 nil 3285696344
   ("" (expand "Tan?")
    (("" (rewrite "cos_pi3") (("" (assert) nil nil)) nil)) nil)
   ((cos_pi3 formula-decl nil trig_values nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (Tan? const-decl "bool" trig_basic nil))
   nil))
(tan_pi3 0
  (tan_pi3-1 nil 3285696344
   ("" (expand "tan")
    (("" (rewrite "sin_pi3")
      (("" (rewrite "cos_pi3") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sin_pi3 formula-decl nil trig_values nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (cos_pi3 formula-decl nil trig_values nil)
    (tan const-decl "real" trig_basic nil))
   nil))
(sin_2pi3 0
  (sin_2pi3-1 nil 3285696344
   ("" (lemma "sin_2a")
    (("" (inst -1 "pi/3")
      (("" (rewrite "sin_pi3")
        (("" (rewrite "cos_pi3") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (< 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)
    (cos_pi3 formula-decl nil trig_values nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posreal_times_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)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (sin_pi3 formula-decl nil trig_values nil)
    (sin_2a formula-decl nil trig_basic nil))
   nil))
(cos_2pi3 0
  (cos_2pi3-1 nil 3285696344
   ("" (lemma "cos_2a")
    (("" (inst -1 "pi/3")
      (("" (rewrite "sin_pi3")
        (("" (rewrite "cos_pi3") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (< 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)
    (cos_pi3 formula-decl nil trig_values nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_pi3 formula-decl nil trig_values nil)
    (cos_2a formula-decl nil trig_basic nil))
   nil))
(tan_2pi3_TCC1 0
  (tan_2pi3_TCC1-1 nil 3285696344
   ("" (expand "Tan?")
    (("" (lemma "cos_eq_0")
      (("" (inst?)
        (("" (ground)
          (("" (skosimp*)
            (("" (hide -1 -3)
              (("" (case-replace "pi / 2 + i!1 * pi = (1/2+i!1)*pi")
                (("1" (hide -1)
                  (("1" (lemma "both_sides_times1")
                    (("1" (inst -1 "pi" "(1 / 2 + i!1) " "2/3")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cos_eq_0 formula-decl nil trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (Tan? const-decl "bool" trig_basic nil))
   nil))
(tan_2pi3 0
  (tan_2pi3-1 nil 3285696344
   ("" (expand "tan")
    (("" (rewrite "sin_2pi3")
      (("" (rewrite "cos_2pi3") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sin_2pi3 formula-decl nil trig_values nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cos_2pi3 formula-decl nil trig_values nil)
    (tan const-decl "real" trig_basic nil))
   nil))
(cos_5pi4 0
  (cos_5pi4-1 nil 3285696344
   ("" (lemma "cos_plus")
    (("" (inst -1 "pi" "pi/4")
      (("" (rewrite "cos_pi")
        (("" (rewrite "cos_pi4")
          (("" (rewrite "sin_pi")
            (("" (rewrite "sin_pi4") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (>= 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)
    (< 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)
    (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)
    (cos_pi4 formula-decl nil trig_values nil)
    (sin_pi4 formula-decl nil trig_values nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (sin_pi formula-decl nil trig_basic nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (cos_pi formula-decl nil trig_basic nil)
    (cos_plus formula-decl nil trig_basic nil))
   nil))
(sin_5pi4 0
  (sin_5pi4-1 nil 3285696344
   ("" (lemma "sin_plus")
    (("" (inst -1 "pi" "pi/4")
      (("" (rewrite "sin_pi")
        (("" (rewrite "sin_pi4")
          (("" (rewrite "cos_pi")
            (("" (rewrite "cos_pi4") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (>= 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)
    (< 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)
    (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)
    (sin_pi4 formula-decl nil trig_values nil)
    (cos_pi4 formula-decl nil trig_values nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (cos_pi formula-decl nil trig_basic nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (sin_pi formula-decl nil trig_basic nil)
    (sin_plus formula-decl nil trig_basic nil))
   nil))
(sin_cos_5pi4 0
  (sin_cos_5pi4-1 nil 3422012315
   ("" (rewrite "sin_5pi4") (("" (rewrite "cos_5pi4") nil nil)) nil)
   ((cos_5pi4 formula-decl nil trig_values nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sin_5pi4 formula-decl nil trig_values nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.