|
(atan_values
(atan0 0
(atan0-1 nil 3422179176
("" (lemma "atan_tan")
(("" (inst?)
(("1" (rewrite "tan_0") nil nil) ("2" (assert) nil nil)) nil))
nil)
((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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
nil)
(pi_ub const-decl "posreal" trig_basic nil)
(pi_lb const-decl "posreal" trig_basic nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(tan_0 formula-decl nil trig_basic nil)
(atan_0 formula-decl nil atan nil)
(atan_tan formula-decl nil trig_inverses nil))
shostak))
(atan1 0
(atan1-1 nil 3422179016
("" (lemma "atan_tan")
(("" (inst - "pi/4")
(("1" (expand "tan")
(("1" (rewrite "sin_pi4")
(("1" (rewrite "cos_pi4") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
nil)
(pi_ub const-decl "posreal" trig_basic nil)
(pi_lb const-decl "posreal" trig_basic nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(sin_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)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(cos_pi4 formula-decl nil trig_values nil)
(tan const-decl "real" trig_basic nil)
(atan_tan formula-decl nil trig_inverses nil))
shostak))
(atan_1sqrt3 0
(atan_1sqrt3-1 nil 3422178472
("" (lemma "atan_tan")
(("" (inst - "pi/6")
(("1" (expand "tan")
(("1" (rewrite "sin_pi6")
(("1" (rewrite "cos_pi6") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
nil)
(pi_ub const-decl "posreal" trig_basic nil)
(pi_lb const-decl "posreal" trig_basic nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan 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)
(cos_pi6 formula-decl nil trig_values nil)
(tan const-decl "real" trig_basic nil)
(atan_tan formula-decl nil trig_inverses nil))
nil))
(atan_sqrt3 0
(atan_sqrt3-1 nil 3422178501
("" (lemma "atan_tan")
(("" (inst - "pi/3")
(("1" (expand "tan")
(("1" (rewrite "sin_pi3")
(("1" (rewrite "cos_pi3") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
nil)
(pi_ub const-decl "posreal" trig_basic nil)
(pi_lb const-decl "posreal" trig_basic nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan 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/")
(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)
(atan_tan formula-decl nil trig_inverses nil))
nil))
(atan_m1sqrt3 0
(atan_m1sqrt3-1 nil 3422178651
("" (lemma "atan_neg")
(("" (inst - "1/sqrt(3)")
(("" (rewrite "atan_1sqrt3") (("" (assert) nil nil)) nil)) nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(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)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(atan_1sqrt3 formula-decl nil atan_values nil)
(atan_neg formula-decl nil atan nil))
shostak))
(atan_msqrt3 0
(atan_msqrt3-1 nil 3422178691
("" (lemma "atan_neg")
(("" (inst?)
(("" (rewrite "atan_sqrt3") (("" (assert) nil nil)) nil)) nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" 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)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(atan_sqrt3 formula-decl nil atan_values nil)
(atan_neg formula-decl nil atan nil))
shostak))
(atan_gt_0 0
(atan_gt_0-1 nil 3427470520
("" (skeep)
(("" (lemma "tan_atan")
(("" (inst?)
(("" (lemma "tan_gt_0")
(("" (inst?)
(("" (lemma "tan_lt_0")
(("" (inst?)
(("" (lemma "tan_0") (("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tan_atan formula-decl nil trig_inverses nil)
(tan_gt_0 formula-decl nil trig_ineq nil)
(tan_lt_0 formula-decl nil trig_ineq nil)
(tan_0 formula-decl nil trig_basic 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)
(real_gt_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)
(atan const-decl "real_abs_lt_pi2" atan nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
nil)
(pi_ub const-decl "posreal" trig_basic nil)
(pi_lb const-decl "posreal" trig_basic nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak)))
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
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.
|
