|
(trig_values
(sin_cos_pi4 0
(sin_cos_pi4-1 nil 3285696499
("" (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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_shift formula-decl nil trig_basic nil))
nil))
(cos_pi4 0
(cos_pi4-1 nil 3285696499
("" (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))) = 1")
(("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)
("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (ground) 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)
(pi const-decl "posreal" atan nil)
(cos const-decl "real" sincos_def nil)
(sin const-decl "real" sincos_def 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_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/")
(sqrt_1 formula-decl nil sqrt "reals/")
(cos_range application-judgement "trig_range" sincos_def nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def 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 3285696499
("" (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" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_pi4 formula-decl nil trig_values nil))
nil))
(cos_3pi4 0
(cos_3pi4-1 nil 3422960636
("" (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)
(pi const-decl "posreal" atan 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)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def 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 3422963020
("" (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)
(pi const-decl "posreal" atan 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)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def 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 3285696499 ("" (rewrite "tan_pi2_def") nil 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)
(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)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tan_pi4 0
(tan_pi4-1 nil 3285696499
("" (expand "tan")
(("" (rewrite "sin_cos_pi4") (("" (assert) nil nil)) nil)) nil)
((sin_cos_pi4 formula-decl nil trig_values nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(tan const-decl "real" sincos_def nil))
nil))
(sin_pi3_cos_pi6 0
(sin_pi3_cos_pi6-1 nil 3285696499
("" (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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_shift formula-decl nil trig_basic nil))
nil))
(sin_pi6_cos_pi3 0
(sin_pi6_cos_pi3-1 nil 3285696499
("" (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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_shift formula-decl nil trig_basic nil))
nil))
(sin_pi6 0
(sin_pi6-1 nil 3285696499
("" (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" sincos_def 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)
(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" sincos_def 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" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_plus formula-decl nil 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_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 3285696499
("" (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" (case-replace "1 - sq(1 / 2) = 3/4")
(("1" (rewrite "sqrt_div")
(("1" (hide -1)
(("1" (case-replace "sqrt(4) = 2")
(("1" (hide 2)
(("1" (case-replace "4 = 2*2")
(("1"
(hide -1)
(("1" (rewrite "sqrt_square") nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "sq") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -2 2) (("2" (rewrite "cos_ge_0") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cos2 formula-decl nil trig_basic nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sqrt_eq formula-decl nil sqrt "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(cos const-decl "real" sincos_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sin const-decl "real" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(cos_ge_0 formula-decl nil trig_ineq 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)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqrt_4 formula-decl nil sqrt "reals/")
(sqrt_div formula-decl nil sqrt "reals/")
(= const-decl "[T, T -> boolean]" equalities 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 "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)
(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 3285696499
("" (expand "Tan?")
(("" (rewrite "cos_pi6") (("" (assert) nil nil)) nil)) nil)
((cos_pi6 formula-decl nil trig_values nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(Tan? const-decl "bool" sincos_def nil))
nil))
(tan_pi6 0
(tan_pi6-1 nil 3285696499
("" (expand "tan")
(("" (rewrite "sin_pi6")
(("" (rewrite "cos_pi6") (("" (assert) nil nil)) nil)) nil))
nil)
((sin_pi6 formula-decl nil trig_values nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def 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" sincos_def nil))
nil))
(sin_pi3 0
(sin_pi3-1 nil 3285696499
("" (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" sincos_def 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)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(cos_pi3 0
(cos_pi3-1 nil 3285696499
("" (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" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_pi6_cos_pi3 formula-decl nil trig_values nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tan_pi3_TCC1 0
(tan_pi3_TCC1-1 nil 3285696499
("" (expand "Tan?")
(("" (rewrite "cos_pi3") (("" (assert) nil nil)) nil)) nil)
((cos_pi3 formula-decl nil trig_values nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(Tan? const-decl "bool" sincos_def nil))
nil))
(tan_pi3 0
(tan_pi3-1 nil 3285696499
("" (expand "tan")
(("" (rewrite "sin_pi3")
(("" (rewrite "cos_pi3") (("" (assert) nil nil)) nil)) nil))
nil)
((sin_pi3 formula-decl nil trig_values nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def 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" sincos_def nil))
nil))
(sin_2pi3 0
(sin_2pi3-1 nil 3285696499
("" (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)
(pi const-decl "posreal" atan 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" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx 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 3285696499
("" (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)
(pi const-decl "posreal" atan 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" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def 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 3285696499
("" (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" sincos_def nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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)
(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 "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)
(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" sincos_def nil))
nil))
(tan_2pi3 0
(tan_2pi3-1 nil 3285696499
("" (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)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def 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" sincos_def nil))
nil))
(cos_5pi4 0
(cos_5pi4-1 nil 3285696499
("" (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)
(pi const-decl "posreal" atan 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" sincos_def 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)
(cos_pi formula-decl nil trig_basic nil)
(cos_plus formula-decl nil trig_basic nil))
nil))
(sin_5pi4 0
(sin_5pi4-1 nil 3285696499
("" (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)
(pi const-decl "posreal" atan 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" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx 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 3422960821
("" (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/")
(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)
(sin_5pi4 formula-decl nil trig_values nil))
nil)))
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
