(trig_ineq
(cos_gt_0 0
(cos_gt_0-1
nil 3321111622
(
"" (skosimp)
((
"" (
case "forall (x:posreal): x cos(x) > 0")
((
"1" (lemma
"trichotomy" (
"x" "a!1"))
((
"1" (split -1)
((
"1" (inst -
"a!1")
((
"1" (
assert)
nil nil) (
"2" (
assert)
nil nil))
nil)
(
"2" (
replace -1)
((
"2" (
rewrite "cos_0") ((
"2" (
assert)
nil nil))
nil))
nil)
(
"3" (inst -
"-a!1")
((
"1" (
assert) ((
"1" (
rewrite "cos_neg")
nil nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (hide-all-but 1)
((
"2" (skosimp)
((
"2" (
expand "cos")
((
"2" (typepred
"x!1")
((
"2"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "x!1" "py" "2*pi"))
((
"2"
(lemma
"both_sides_div_pos_lt1"
(
"pz" "2*pi" "x" "x!1" "y" "pi/2"))
((
"2" (
assert)
((
"2" (
rewrite "div_div2" -1)
((
"2"
(lemma
"div_cancel1" (
"n0z" "pi" "x" "1/4"))
((
"2" (
replace -1)
((
"2" (hide -1)
((
"2"
(lemma
"floor_def"
(
"x" "x!1 / (2 * pi)"))
((
"2"
(flatten)
((
"2"
(lemma
"trichotomy"
(
"x" "floor(x!1 / (2 * pi))"))
((
"2"
(split -1)
((
"1" (
assert)
nil nil)
(
"2"
(
replace -1)
((
"2"
(
assert)
((
"2"
(hide -1 -2 -3 -4 -5)
((
"2"
(
expand "cos_phase")
((
"2"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "x!1" "py" "pi"))
((
"2"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"pi"
"x"
"x!1"
"y"
"pi/2"))
((
"2"
(
replace -5 -1)
((
"2"
(lemma
"div_cancel1"
(
"n0z"
"pi"
"x"
"1/2"))
((
"2"
(
replace -1)
((
"2"
(flatten -2)
((
"2"
(hide -1)
((
"2"
(lemma
"floor_def"
(
"x"
"x!1 / pi"))
((
"2"
(flatten)
((
"2"
(lemma
"trichotomy"
(
"x"
"floor(x!1 / pi)"))
((
"2"
(split
-1)
((
"1"
(
assert)
nil
nil)
(
"2"
(
replace
-1)
((
"2"
(lemma
"cos_value_strict_decreasing")
((
"2"
(
expand
"strict_decreasing?")
((
"2"
(inst
-
"x!1"
"pi/2")
((
"2"
(
assert)
((
"2"
(
rewrite
"cos_value_pi2")
((
"2"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"3"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cos_neg formula-decl
nil trig_basic
nil)
(cos_0 formula-decl
nil trig_basic
nil))
shostak))
(sin_gt_0 0
(sin_gt_0-1
nil 3321113131
(
"" (skosimp)
((
"" (lemma
"cos_sin" (
"a" "a!1-pi/2"))
((
"" (lemma
"cos_gt_0" (
"a" "a!1-pi/2")) ((
"" (
assert)
nil nil))
nil))
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)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
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)
(cos_sin formula-decl
nil trig_basic
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_plus_real_is_real application-judgement
"real" reals
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)
(cos_gt_0 formula-decl
nil trig_ineq
nil))
shostak))
(sin_ge_0 0
(sin_ge_0-1
nil 3321111692
(
"" (skosimp)
((
"" (
expand "<=")
((
"" (split -1)
((
"1" (split -2)
((
"1" (lemma
"sin_gt_0" (
"a" "a!1")) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
replace -1)
((
"2" (
rewrite "sin_pi") ((
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (
replace -1)
((
"2" (
replace -1 1 rl)
((
"2" (
rewrite "sin_0") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((<= const-decl
"bool" reals
nil)
(sin_0 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sin_gt_0 formula-decl
nil trig_ineq
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)
(sin_pi formula-decl
nil trig_basic
nil))
shostak))
(cos_ge_0 0
(cos_ge_0-1
nil 3321111792
(
"" (skosimp)
((
"" (
expand "<=")
((
"" (split -1)
((
"1" (split -2)
((
"1" (lemma
"cos_gt_0" (
"a" "a!1")) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
replace -1)
((
"2" (
rewrite "cos_pi2") ((
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (
replace -1 * rl)
((
"2" (lemma
"cos_neg" (
"a" "pi/2"))
((
"2" (
rewrite "cos_pi2") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(<= const-decl
"bool" reals
nil)
(cos_neg formula-decl
nil 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)
(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_range application-judgement
"trig_range" trig_basic
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
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)
(cos_gt_0 formula-decl
nil trig_ineq
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)
(cos_pi2 formula-decl
nil trig_basic
nil))
shostak))
(sin_lt_0 0
(sin_lt_0-1
nil 3321112483
(
"" (skosimp)
((
"" (lemma
"neg_sin" (
"a" "a!1-pi"))
((
"" (lemma
"sin_gt_0" (
"a" "a!1-pi")) ((
"" (
assert)
nil nil))
nil))
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, numfield -> numfield]" number_fields
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)
(neg_sin formula-decl
nil trig_basic
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(posreal_times_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_plus_real_is_real application-judgement
"real" reals
nil)
(sin_range application-judgement
"trig_range" trig_basic
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(sin_gt_0 formula-decl
nil trig_ineq
nil))
shostak))
(cos_lt_0 0
(cos_lt_0-1
nil 3321112640
(
"" (skosimp)
((
"" (lemma
"neg_cos" (
"a" "a!1-pi"))
((
"" (
assert)
((
"" (lemma
"cos_gt_0" (
"a" "a!1-pi")) ((
"" (
assert)
nil nil))
nil))
nil))
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, numfield -> numfield]" number_fields
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)
(neg_cos formula-decl
nil trig_basic
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(cos_gt_0 formula-decl
nil trig_ineq
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(cos_range application-judgement
"trig_range" trig_basic
nil)
(real_plus_real_is_real application-judgement
"real" reals
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)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil))
shostak))
(sin_le_0 0
(sin_le_0-1
nil 3321112929
(
"" (skosimp)
((
"" (
expand "<=" (-1 -2))
((
"" (split -1)
((
"1" (split -2)
((
"1" (lemma
"sin_lt_0" (
"a" "a!1")) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
replace -1)
((
"2" (
rewrite "sin_2pi") ((
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (
replace -1 1 rl)
((
"2" (
rewrite "sin_pi") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
((<= const-decl
"bool" reals
nil)
(sin_pi formula-decl
nil trig_basic
nil)
(sin_range application-judgement
"trig_range" trig_basic
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sin_lt_0 formula-decl
nil trig_ineq
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)
(sin_2pi formula-decl
nil trig_basic
nil))
shostak))
(cos_le_0 0
(cos_le_0-1
nil 3321113009
(
"" (skosimp)
((
"" (
expand "<=" (-1 -2))
((
"" (split -1)
((
"1" (split -2)
((
"1" (lemma
"cos_lt_0" (
"a" "a!1")) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
replace -1)
((
"2" (
rewrite "cos_3pi2") ((
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (
replace -1 * rl)
((
"2" (
rewrite "cos_pi2") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
((posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(<= const-decl
"bool" reals
nil)
(cos_pi2 formula-decl
nil trig_basic
nil)
(cos_range application-judgement
"trig_range" trig_basic
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
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)
(cos_lt_0 formula-decl
nil trig_ineq
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)
(cos_3pi2 formula-decl
nil trig_basic
nil))
shostak))
(tan_gt_0_TCC1 0
(tan_gt_0_TCC1-1
nil 3321111953
(
"" (skosimp)
((
"" (
expand "Tan?")
((
"" (lemma
"cos_eq_0_2pi" (
"a" "a!1")) ((
"" (
assert)
nil nil))
nil))
nil))
nil)
((Tan? const-decl
"bool" trig_basic
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(cos_range application-judgement
"trig_range" 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)
(cos_eq_0_2pi formula-decl
nil trig_basic
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))
shostak))
(tan_gt_0 0
(tan_gt_0-1
nil 3321112029
(
"" (skosimp)
((
"" (
expand "tan")
((
"" (lemma
"sin_gt_0" (
"a" "a!1"))
((
"" (lemma
"cos_gt_0" (
"a" "a!1"))
((
"" (
assert)
((
""
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "sin(a!1)" "py" "cos(a!1)"))
((
"" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tan const-decl
"real" trig_basic
nil)
(cos_gt_0 formula-decl
nil trig_ineq
nil)
(posreal_div_posreal_is_posreal judgement-tcc
nil real_types
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)
(sin const-decl
"real" trig_basic
nil)
(cos const-decl
"real" trig_basic
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_div_nzreal_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)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(sin_gt_0 formula-decl
nil trig_ineq
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))
shostak))
(tan_lt_0_TCC1 0
(tan_lt_0_TCC1-1
nil 3321111953
(
"" (skosimp)
((
"" (
expand "Tan?")
((
"" (lemma
"cos_eq_0_2pi" (
"a" "-a!1"))
((
"" (
assert)
((
"" (
rewrite "cos_neg") ((
"" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
((Tan? const-decl
"bool" trig_basic
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(cos_range application-judgement
"trig_range" trig_basic
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)
(cos_neg formula-decl
nil trig_basic
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(cos_eq_0_2pi formula-decl
nil trig_basic
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
"[numfield -> numfield]" number_fields
nil))
shostak))
(tan_lt_0 0
(tan_lt_0-1
nil 3321112133
(
"" (skosimp)
((
"" (lemma
"tan_gt_0" (
"a" "-a!1"))
((
"" (
assert)
((
"" (
rewrite "tan_neg") ((
"" (
assert)
nil nil))
nil))
nil))
nil))
nil)
((- const-decl
"[numfield -> numfield]" number_fields
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_gt_0 formula-decl
nil trig_ineq
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(Tan? const-decl
"bool" trig_basic
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(tan_neg formula-decl
nil trig_basic
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
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)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil))
shostak))
(tan_pi2_def 0
(tan_pi2_def-1
nil 3312284516
(
"" (skeep)
((
"" (
expand "Tan?")
((
"" (
case "cos(a)>0")
((
"1" (
assert)
nil nil) (
"2" (
rewrite "cos_gt_0")
nil nil))
nil))
nil))
nil)
((Tan? const-decl
"bool" trig_basic
nil)
(cos_gt_0 formula-decl
nil trig_ineq
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)
(cos_range application-judgement
"trig_range" trig_basic
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
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)
(cos const-decl
"real" trig_basic
nil))
shostak))
(tan_npi_def 0
(tan_npi_def-1
nil 3323008332
(
"" (skeep)
((
"" (
expand "Tan?")
((
"" (lemma
"cos_k_pi")
((
"" (inst -1
"n")
((
"" (replaces -1) ((
"" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
((Tan? const-decl
"bool" trig_basic
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)
(rational_pred const-decl
"[real -> boolean]" rationals
nil)
(rational nonempty-type-from-decl
nil rationals
nil)
(integer_pred const-decl
"[rational -> boolean]" integers
nil)
(integer nonempty-type-from-decl
nil integers
nil)
(int nonempty-type-eq-decl
nil integers
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(nzreal_exp application-judgement
"nzreal" exponentiation
nil)
(rat_exp application-judgement
"rat" exponentiation
nil)
(cos_k_pi formula-decl
nil trig_basic
nil))
shostak))
(cos_ge_0_3pi2 0
(cos_ge_0_3pi2-1
nil 3279136307
(
"" (skosimp*)
((
"" (name
"BB" "a!1 - 2 * pi")
((
"" (case-replace
"a!1 = BB + 2*pi")
((
"1" (hide -1 -2)
((
"1" (
assert)
((
"1" (case-replace
"-pi/2 <= BB AND BB <= 0")
((
"1" (hide -2 -3)
((
"1" (
rewrite "cos_plus")
((
"1" (
rewrite "cos_2pi")
((
"1" (
rewrite "sin_2pi")
((
"1" (flatten)
((
"1" (
assert)
((
"1" (lemma
"cos_gt_0")
((
"1" (inst?)
((
"1"
(lemma
"cos_pi2")
((
"1"
(lemma
"cos_neg")
((
"1"
(inst -1
"pi/2")
((
"1" (ground)
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))
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, numfield -> numfield]" 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)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-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)
(real_minus_real_is_real application-judgement
"real" 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)
(<= const-decl
"bool" reals
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(cos_plus formula-decl
nil trig_basic
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(sin_range application-judgement
"trig_range" trig_basic
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(sin_2pi formula-decl
nil trig_basic
nil)
(cos_neg formula-decl
nil trig_basic
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)
(cos_pi2 formula-decl
nil trig_basic
nil)
(cos_gt_0 formula-decl
nil trig_ineq
nil)
(cos_2pi formula-decl
nil trig_basic
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(cos_range application-judgement
"trig_range" trig_basic
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(minus_nzint_is_nzint application-judgement
"nzint" integers
nil)
(minus_even_is_even application-judgement
"even_int" integers
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil))
nil))
(sin_increasing_imp 0
(sin_increasing_imp-1
nil 3279136307
(
"" (skosimp)
((
"" (
case "sin(a!1) - sin(b!1) > 0")
((
"1" (
assert)
nil nil)
(
"2" (hide 2)
((
"2" (
assert)
((
"2" (lemma
"sin_plus")
((
"2" (inst -1
"(a!1+b!1)/2" "(a!1-b!1)/2")
((
"2" (lemma
"sin_minus")
((
"2" (inst -1
"(a!1+b!1)/2" "(a!1-b!1)/2")
((
"2" (
replace -2 * lr)
((
"2" (
replace -1 * lr)
((
"2" (hide -2 -1)
((
"2" (
assert)
((
"2" (
assert)
((
"2" (lemma
"pos_times_gt")
((
"2"
(inst
-1
"2"
"sin((a!1 - b!1) / 2) * cos((a!1 + b!1) / 2)")
((
"2"
(
replace -1 * lr)
((
"2"
(hide -1)
((
"2"
(flatten)
((
"2"
(hide 1)
((
"2"
(
rewrite "pos_times_gt" 1)
((
"2"
(
assert)
((
"2"
(flatten)
((
"2"
(hide 1)
((
"2"
(
rewrite "sin_gt_0")
((
"2"
(
rewrite
"cos_gt_0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sin const-decl
"real" trig_basic
nil)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(> const-decl
"bool" reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(real nonempty-type-from-decl
nil reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number nonempty-type-decl
nil numbers
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sin_range application-judgement
"trig_range" trig_basic
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_ge_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)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/= const-decl
"boolean" notequal
nil)
(pos_times_gt formula-decl
nil real_props
nil)
(sin_gt_0 formula-decl
nil trig_ineq
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(cos_gt_0 formula-decl
nil trig_ineq
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(cos const-decl
"real" trig_basic
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(cos_range application-judgement
"trig_range" trig_basic
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(sin_minus formula-decl
nil trig_basic
nil)
(sin_plus formula-decl
nil trig_basic
nil))
nil))
(sin_increasing 0
(sin_increasing-1
nil 3279136307
(
"" (skosimp)
((
"" (prop)
((
"1" (lemma
"sin_increasing_imp")
((
"1" (inst -1
"b!1" "a!1") ((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
rewrite "sin_increasing_imp")
nil nil))
nil))
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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sin_range application-judgement
"trig_range" trig_basic
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_ge_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)
(sin_increasing_imp formula-decl
nil trig_ineq
nil))
nil))
(sin_decreasing 0
(sin_decreasing-1
nil 3279136307
(
"" (lemma
"sin_increasing")
((
"" (skosimp)
((
"" (inst -1
"pi-b!1" "pi-a!1")
((
"" (
rewrite "sin_minus")
((
"" (
rewrite "sin_pi")
((
"" (
rewrite "cos_pi")
((
"" (
rewrite "sin_minus")
((
"" (
rewrite "sin_pi")
((
"" (
rewrite "cos_pi")
((
"" (
assert)
((
""
(case-replace
"-1 * (sin(b!1) * -1) = sin(b!1)")
((
"1" (hide -1)
((
"1"
(case-replace
"-1 * (sin(a!1) * -1) = sin(a!1)")
((
"1" (hide -1) ((
"1" (ground)
nil nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sin_minus formula-decl
nil trig_basic
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
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)
(cos_pi formula-decl
nil trig_basic
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)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(sin const-decl
"real" trig_basic
nil)
(sin_pi formula-decl
nil 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, numfield -> numfield]" number_fields
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)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(sin_increasing formula-decl
nil trig_ineq
nil))
nil))
(cos_increasing 0
(cos_increasing-1
nil 3279136307
(
"" (skosimp)
((
"" (lemma
"sin_increasing")
((
"" (inst -1
"a!1-3*pi/2" "b!1-3*pi/2")
((
"" (
assert)
((
"" (
rewrite "sin_minus")
((
"" (
rewrite "cos_3pi2")
((
"" (
rewrite "sin_3pi2")
((
"" (
rewrite "sin_minus")
((
"" (
rewrite "cos_3pi2")
((
"" (
rewrite "sin_3pi2") ((
"" (ground)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sin_increasing formula-decl
nil trig_ineq
nil)
(cos_range application-judgement
"trig_range" trig_basic
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(cos_3pi2 formula-decl
nil trig_basic
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(sin_3pi2 formula-decl
nil trig_basic
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(sin_range application-judgement
"trig_range" trig_basic
nil)
(sin_minus formula-decl
nil 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, 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)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
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)
(real_minus_real_is_real application-judgement
"real" reals
nil))
nil))
(cos_decreasing 0
(cos_decreasing-1
nil 3279136307
(
"" (skosimp)
((
"" (lemma
"sin_increasing")
((
"" (inst -1
"a!1-pi/2" "b!1-pi/2")
((
"" (
assert)
((
"" (
rewrite "sin_minus")
((
"" (
rewrite "sin_pi2")
((
"" (
rewrite "cos_pi2")
((
"" (
assert)
((
"" (
rewrite "sin_minus")
((
"" (
rewrite "sin_pi2")
((
"" (
rewrite "cos_pi2")
((
"" (
assert) ((
"" (ground)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sin_increasing formula-decl
nil trig_ineq
nil)
(cos_range application-judgement
"trig_range" trig_basic
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(sin_pi2 formula-decl
nil trig_basic
nil)
(cos_pi2 formula-decl
nil trig_basic
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(sin_range application-judgement
"trig_range" trig_basic
nil)
(sin_minus formula-decl
nil 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)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
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)
(real_minus_real_is_real application-judgement
"real" reals
nil))
nil))
(tan_increasing_imp_TCC1 0
(tan_increasing_imp_TCC1-1
nil 3279136307
(
"" (skosimp) ((
"" (
rewrite "tan_pi2_def")
nil nil))
nil)
((tan_pi2_def formula-decl
nil trig_ineq
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))
nil))
(tan_increasing_imp_TCC2 0
(tan_increasing_imp_TCC2-2
nil 3312284395
(
"" (skosimp) ((
"" (
rewrite "tan_pi2_def")
nil nil))
nil)
((tan_pi2_def formula-decl
nil trig_ineq
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))
nil))
(tan_increasing_imp 0
(tan_increasing_imp-1
nil 3279136307
(
"" (skosimp)
((
"" (
expand "tan")
((
"" (lemma
"cos_gt_0")
((
"" (inst -1
"a!1")
((
"" (lemma
"cos_gt_0")
((
"" (inst -1
"b!1")
((
"" (
assert)
((
"" (
case "a!1>0" "b!1<0")
((
"1"
(
case "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)")
((
"1" (skosimp*) ((
"1" (
assert)
nil nil))
nil)
(
"2" (hide 2)
((
"2" (inst 1
"0")
((
"2" (
rewrite "pos_div_gt" 1)
((
"2" (
rewrite "sin_gt_0")
((
"2" (
rewrite "neg_div_ge" 1)
((
"2"
(lemma
"sin_gt_0")
((
"2"
(inst -1
"-b!1")
((
"2"
(
rewrite "sin_neg" -1)
((
"2"
(
case
"0 < -b!1 AND -b!1 < pi IMPLIES sin(b!1) < 0")
((
"1"
(hide -2)
((
"1" (
assert)
nil nil))
nil)
(
"2" (ground)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
case "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)")
((
"1" (skosimp*) ((
"1" (
assert)
nil nil))
nil)
(
"2" (hide 3)
((
"2" (inst +
"sin(b!1)/cos(a!1)")
((
"2" (split)
((
"1" (lemma
"both_sides_div_pos_lt1")
((
"1"
(inst -1
"cos(a!1)" "sin(b!1)"
"sin(a!1)")
((
"1"
(
assert)
((
"1"
(lemma
"sin_increasing")
((
"1"
(inst -1
"a!1" "b!1")
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
case "(sin(b!1) = 0 OR
sin(b!1) > 0
AND cos(a!1) <= cos(b!1)
OR
sin(b!1) < 0
AND cos(a!1) >= cos(b!1))
")
((
"1" (
assert)
((
"1"
(split -1)
((
"1"
(flatten)
((
"1"
(lemma
"both_sides_div_pos_le2")
((
"1"
(inst
-1
"cos(b!1)"
"cos(a!1)"
"sin(b!1)")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2"
(flatten)
((
"2"
(lemma
"both_sides_div_pos_le3")
((
"2"
(inst
-1
"sin(b!1)"
"cos(b!1)"
"cos(a!1)")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (lemma
"cos_decreasing")
((
"2"
(inst -1
"a!1" "b!1")
((
"2"
(
assert)
((
"2"
(lemma
"sin_ge_0")
((
"2"
(inst -1
"b!1")
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"3"
(
case "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)")
((
"1" (skosimp*) ((
"1" (
assert)
nil nil))
nil)
(
"2" (hide 3)
((
"2" (inst +
"sin(b!1)/cos(a!1)")
((
"2" (split)
((
"1" (lemma
"both_sides_div_pos_gt1")
((
"1"
(inst -1
"cos(a!1)" "sin(a!1)"
"sin(b!1)")
((
"1"
(
assert)
((
"1"
(hide 2)
((
"1"
(
rewrite "sin_increasing")
nil
nil))
nil))
nil))
nil))
nil)
(
"2"
(
case "(sin(b!1) = 0 OR
sin(b!1) > 0
AND cos(a!1) <= cos(b!1)
OR
sin(b!1) < 0
AND cos(a!1) >= cos(b!1))
")
((
"1" (
assert)
((
"1"
(split -1)
((
"1"
(flatten)
((
"1"
(lemma
"both_sides_div_pos_le2")
((
"1"
(inst
-1
"cos(b!1)"
"cos(a!1)"
"sin(b!1)")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2"
(lemma
"both_sides_div_pos_le3")
((
"2"
(inst
-1
"sin(b!1)"
"cos(b!1)"
"cos(a!1)")
((
"1" (
assert)
nil nil)
(
"2"
(flatten)
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (hide 2)
((
"2"
(lemma
"sin_gt_0")
((
"2"
(inst -1
"-b!1")
((
"2"
(
rewrite "sin_neg" -1)
((
"2"
(
case
"0 < -b!1 AND -b!1 < pi IMPLIES sin(b!1) < 0")
((
"1"
(hide -2)
((
"1"
(
assert)
((
"1"
(lemma
"cos_decreasing")
((
"1"
(inst -1
"-b!1" "-a!1")
((
"1"
(
rewrite "cos_neg" -1)
((
"1"
(
rewrite
"cos_neg"
-1)
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tan const-decl
"real" trig_basic
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)
(< const-decl
"bool" reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(> const-decl
"bool" reals
nil)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(pos_div_gt formula-decl
nil real_props
nil)
(neg_div_ge formula-decl
nil real_props
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(posreal nonempty-type-eq-decl
nil real_types
nil)
(pi_lb const-decl
"posreal" trig_basic
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_neg formula-decl
nil trig_basic
nil)
(sin_gt_0 formula-decl
nil trig_ineq
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(>= const-decl
"bool" reals
nil)
(cos const-decl
"real" trig_basic
nil)
(sin const-decl
"real" trig_basic
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)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(sin_increasing formula-decl
nil trig_ineq
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(both_sides_div_pos_lt1 formula-decl
nil real_props
nil)
(cos_decreasing formula-decl
nil trig_ineq
nil)
(sin_ge_0 formula-decl
nil trig_ineq
nil)
(negreal nonempty-type-eq-decl
nil real_types
nil)
(nonpos_real nonempty-type-eq-decl
nil real_types
nil)
(both_sides_div_pos_le3 formula-decl
nil real_props
nil)
(b!1 skolem-const-decl
"real" trig_ineq
nil)
(both_sides_div_pos_le2 formula-decl
nil real_props
nil)
(<= const-decl
"bool" reals
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(both_sides_div_pos_gt1 formula-decl
nil real_props
nil)
(cos_neg formula-decl
nil trig_basic
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
--> --------------------
--> maximum size reached
--> --------------------
