(atan2
(atan2_TCC1 0
(atan2_TCC1-1
nil 3269553691 (
"" (grind)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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)
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(/= const-decl
"boolean" notequal
nil))
shostak))
(atan2_TCC2 0
(atan2_TCC2-1
nil 3269553735 (
"" (grind)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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)
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(/= const-decl
"boolean" notequal
nil))
shostak))
(atan2_TCC3 0
(atan2_TCC3-1
nil 3269553749 (
"" (grind)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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)
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(/= const-decl
"boolean" notequal
nil))
shostak))
(atan2_0_2pi_TCC1 0
(atan2_0_2pi_TCC1-1
nil 3269553757 (
"" (grind)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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
"boolean" notequal
nil))
shostak))
(atan2_0_2pi_TCC2 0
(atan2_0_2pi_TCC2-1
nil 3269553764 (
"" (grind)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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_times_real_is_real application-judgement
"real" reals
nil)
(/= const-decl
"boolean" notequal
nil)
(Integral const-decl
"real" integral_def
"analysis/")
(atan_value const-decl
"real" atan
nil)
(atan const-decl
"real_abs_lt_pi2" atan
nil)
(pi const-decl
"posreal" atan
nil)
(atan2 const-decl
"real" atan2
nil))
shostak))
(atan2_0_2pi_TCC3 0
(atan2_0_2pi_TCC3-1
nil 3269553778
(
"" (skosimp*) ((
"" (
assert)
nil nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil))
shostak))
(atan2_0_2pi_TCC4 0
(atan2_0_2pi_TCC4-1
nil 3269554070
(
"" (skosimp*) ((
"" (
assert)
nil nil))
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))
shostak))
(atan2_0_2pi 0
(atan2_0_2pi-1
nil 3269554130
(
"" (skosimp*)
((
"" (lemma
"trichotomy" (
"x" "x!1"))
((
"" (
expand "atan2")
((
"" (split -1)
((
"1" (
assert)
((
"1" (lemma
"trichotomy" (
"x" "y!1"))
((
"1" (split -1)
((
"1" (
assert)
((
"1" (typepred
"atan(y!1 / x!1)")
((
"1" (
expand "pi")
((
"1" (
expand "pi")
((
"1" (lemma
"atan_strict_increasing")
((
"1" (
expand "strict_increasing?")
((
"1" (inst -
"0" "y!1/x!1")
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "y!1" "py" "x!1"))
((
"1"
(
assert)
((
"1"
(
rewrite "atan_0")
((
"1"
(
expand "abs")
((
"1"
(
assert)
((
"1"
(
expand "atan")
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
replace -1)
((
"2" (
assert)
((
"2" (
rewrite "atan_0") ((
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"3" (
assert)
((
"3" (lemma
"atan_strict_increasing")
((
"3" (
expand "strict_increasing?")
((
"3" (typepred
"atan(y!1 / x!1)")
((
"3" (inst -
"y!1/x!1" "0")
((
"3"
(lemma
"both_sides_div_pos_gt1"
(
"x" "0" "y" "y!1" "pz" "x!1"))
((
"3" (
assert)
((
"3"
(
rewrite "atan_0")
((
"3"
(
expand "abs")
((
"3"
(
assert)
((
"3"
(
expand "pi")
((
"3"
(
expand "pi")
((
"3"
(
expand "atan")
((
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
replace -1)
((
"2" (
assert)
((
"2" (lemma
"trichotomy" (
"x" "y!1"))
((
"2" (split -1)
((
"1" (
assert)
nil nil) (
"2" (
assert)
nil nil)
(
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"3" (
assert)
((
"3" (hide -2)
((
"3" (lemma
"trichotomy" (
"x" "y!1"))
((
"3" (split -1)
((
"1" (
assert)
((
"1" (lemma
"both_sides_div_neg_gt1")
((
"1" (inst -
"x!1" "0" "y!1")
((
"1" (
assert)
((
"1" (lemma
"atan_strict_increasing")
((
"1" (
expand "strict_increasing?")
((
"1"
(inst -
"y!1/x!1" "0")
((
"1"
(
rewrite "atan_0")
((
"1"
(typepred
"atan(y!1/x!1)")
((
"1"
(
expand "abs")
((
"1"
(
assert)
((
"1"
(
assert)
((
"1"
(
expand "pi")
((
"1"
(
expand "pi")
((
"1"
(
expand "atan")
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
replace -1)
((
"2" (
rewrite "atan_0") ((
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"3"
(lemma
"negreal_div_negreal_is_posreal"
(
"nx" "y!1" "ny" "x!1"))
((
"1" (lemma
"atan_strict_increasing")
((
"1" (
expand "strict_increasing?")
((
"1" (inst -
"0" "y!1/x!1")
((
"1" (
rewrite "atan_0")
((
"1" (
assert)
((
"1"
(typepred
"atan(y!1/x!1)")
((
"1"
(
expand "abs")
((
"1"
(
expand "pi")
((
"1"
(
expand "pi")
((
"1"
(
expand "atan")
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl
nil reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number nonempty-type-decl
nil numbers
nil)
(trichotomy formula-decl
nil real_axioms
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(both_sides_div_pos_gt1 formula-decl
nil real_props
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(strict_increasing? const-decl
"bool" real_fun_preds
"reals/")
(posreal_div_posreal_is_posreal judgement-tcc
nil real_types
nil)
(atan_0 formula-decl
nil atan
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(atan_strict_increasing formula-decl
nil atan
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(< const-decl
"bool" 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)
(- const-decl
"[numfield -> numfield]" number_fields
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)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(real_abs_lt_pi2 nonempty-type-eq-decl
nil atan
nil)
(atan const-decl
"real_abs_lt_pi2" atan
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
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)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(both_sides_div_neg_gt1 formula-decl
nil real_props
nil)
(<= const-decl
"bool" reals
nil)
(nonpos_real nonempty-type-eq-decl
nil real_types
nil)
(negreal nonempty-type-eq-decl
nil real_types
nil)
(nnreal_plus_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(negreal_div_negreal_is_posreal judgement-tcc
nil real_types
nil)
(atan2 const-decl
"real" atan2
nil)
(pi_bound name-judgement
"{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx
nil))
shostak))
(atan2_ge_0_lt_2pi_TCC1 0
(atan2_ge_0_lt_2pi_TCC1-1
nil 3269553812 (
"" (grind)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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
"boolean" notequal
nil))
shostak))
(atan2_ge_0_lt_2pi 0
(atan2_ge_0_lt_2pi-1
nil 3269552776
(
"" (skosimp*)
((
"" (lemma
"atan2_0_2pi" (
"x" "x!1" "y" "y!1"))
((
"" (
replace -2 -1)
((
"" (flatten -1)
((
"" (lemma
"trichotomy" (
"x" "x!1"))
((
"" (split -1)
((
"1" (
assert)
((
"1" (hide -3 -4 -6)
((
"1" (
case "y!1>=0")
((
"1" (
assert)
((
"1" (flatten -3) ((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2" (flatten -3) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (lemma
"trichotomy" (
"x" "y!1"))
((
"2" (split -1)
((
"1" (
assert)
((
"1" (flatten (-3 -4)) ((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
nil nil)
(
"3" (
assert)
((
"3" (flatten (-5 -6)) ((
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"3" (
assert)
((
"3" (hide -2 -5 -6)
((
"3" (
case "y!1>=0")
((
"1" (
assert)
((
"1" (flatten -3) ((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2" (flatten -3) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl
nil reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number nonempty-type-decl
nil numbers
nil)
(atan2_0_2pi formula-decl
nil atan2
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
"bool" reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(pi_bound name-judgement
"{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(trichotomy formula-decl
nil real_axioms
nil))
nil))
(nnreal_lt_2pi_TCC1 0
(nnreal_lt_2pi_TCC1-1
nil 3414423407
(
"" (inst +
"0") ((
"" (
assert)
nil 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
"[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(< const-decl
"bool" reals
nil)
(nnreal type-eq-decl
nil real_types
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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
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))
nil))
(atan2_TCC4 0
(atan2_TCC4-1
nil 3414423407
(
"" (skosimp*)
((
"" (typepred
"y!1")
((
"" (
rewrite "atan2_ge_0_lt_2pi") ((
"" (ground)
nil nil))
nil))
nil))
nil)
((/= const-decl
"boolean" notequal
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)
(number nonempty-type-decl
nil numbers
nil)
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(pi_bound name-judgement
"{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx
nil)
(atan2_ge_0_lt_2pi formula-decl
nil atan2
nil))
nil))
(atan2_cancel_pos_TCC1 0
(atan2_cancel_pos_TCC1-1
nil 3269628375
(
"" (skosimp*)
((
"" (
assert)
((
"" (split -1)
((
"1"
(lemma
"both_sides_times1" (
"x" "x!1" "y" "0" "n0z" "pz!1"))
((
"1" (
assert)
nil nil))
nil)
(
"2"
(lemma
"both_sides_times1" (
"x" "y!1" "y" "0" "n0z" "pz!1"))
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement
"real" reals
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)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(/= const-decl
"boolean" notequal
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)
(both_sides_times1 formula-decl
nil real_props
nil)
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil))
shostak))
(atan2_cancel_pos 0
(atan2_cancel_pos-1
nil 3269616367
(
"" (skosimp*)
((
"" (
expand "atan2")
((
""
(lemma
"both_sides_times_pos_gt1"
(
"x" "x!1" "y" "0" "pz" "pz!1"))
((
"" (
replace -1)
((
"" (
case "x!1>0")
((
"1" (
assert)
((
"1"
(lemma
"both_sides_times_pos_ge1"
(
"x" "y!1" "y" "0" "pz" "pz!1"))
((
"1" (
replace -1)
((
"1" (
case "y!1>=0")
((
"1" (
assert)
nil nil) (
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
case "x!1=0")
((
"1" (
assert)
((
"1"
(lemma
"both_sides_times_pos_gt1"
(
"x" "y!1" "y" "0" "pz" "pz!1"))
((
"1" (
replace -1) ((
"1" (propax)
nil nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement
"real" reals
nil)
(pi_bound name-judgement
"{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx
nil)
(atan2 const-decl
"real" atan2
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(both_sides_times_pos_ge1 formula-decl
nil real_props
nil)
(both_sides_times_pos_gt1 formula-decl
nil 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)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(> const-decl
"bool" reals
nil)
(posreal nonempty-type-eq-decl
nil real_types
nil))
shostak))
(atan2_cancel_neg_TCC1 0
(atan2_cancel_neg_TCC1-1
nil 3269628375
(
"" (skosimp*)
((
"" (lemma
"both_sides_times1" (
"x" "y!1" "y" "0" "n0z" "nz!1"))
((
"" (lemma
"both_sides_times1" (
"x" "x!1" "y" "0" "n0z" "nz!1"))
((
"" (
assert)
nil nil))
nil))
nil))
nil)
((negreal nonempty-type-eq-decl
nil real_types
nil)
(< const-decl
"bool" reals
nil)
(nonpos_real nonempty-type-eq-decl
nil real_types
nil)
(<= const-decl
"bool" reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(/= const-decl
"boolean" notequal
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)
(both_sides_times1 formula-decl
nil real_props
nil)
(real_times_real_is_real application-judgement
"real" reals
nil))
shostak))
(atan2_cancel_neg 0
(atan2_cancel_neg-1
nil 3269628659
(
"" (skosimp*)
((
"" (
expand "atan2")
((
"" (lemma
"both_sides_times1" (
"x" "x!1" "y" "0" "n0z" "nz!1"))
((
"" (
replace -1)
((
"" (
case "y!1=0")
((
"1" (
replace -1)
((
"1" (
rewrite "atan_0")
((
"1" (simplify 1)
((
"1" (
case "x!1>0")
((
"1" (
assert)
((
"1"
(lemma
"both_sides_times_neg_lt1"
(
"x" "x!1" "y" "0" "nz" "nz!1"))
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2"
(lemma
"both_sides_times_neg_lt1"
(
"x" "x!1" "y" "0" "nz" "nz!1"))
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
case "y!1>0")
((
"1" (hide -2)
((
"1" (
assert)
((
"1"
(lemma
"both_sides_times_neg_gt1"
(
"x" "0" "y" "y!1" "nz" "nz!1"))
((
"1" (
assert)
((
"1" (
case "x!1>0")
((
"1" (
assert)
((
"1"
(lemma
"both_sides_times_neg_gt1"
(
"x" "0" "y" "x!1" "nz" "nz!1"))
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2"
(lemma
"both_sides_times_neg_gt1"
(
"x" "0" "y" "x!1" "nz" "nz!1"))
((
"2" (
assert)
((
"2"
(
case "x!1=0")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
case "x!1=0")
((
"1" (
assert)
((
"1"
(lemma
"both_sides_times_neg_gt1"
(
"x" "0" "y" "y!1" "nz" "nz!1"))
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
case "x!1>0")
((
"1" (
assert)
((
"1"
(lemma
"both_sides_times_neg_gt1"
(
"x" "0" "y" "x!1" "nz" "nz!1"))
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2"
(lemma
"both_sides_times_neg_gt1"
(
"y" "0" "x" "x!1" "nz" "nz!1"))
((
"2" (
assert)
((
"2"
(lemma
"both_sides_times_neg_gt1"
(
"y" "0" "x" "y!1" "nz" "nz!1"))
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement
"real" reals
nil)
(pi_bound name-judgement
"{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx
nil)
(atan2 const-decl
"real" atan2
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(both_sides_times_neg_gt1 formula-decl
nil real_props
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_gt_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_minus_real_is_real application-judgement
"real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(both_sides_times_neg_lt1 formula-decl
nil real_props
nil)
(> const-decl
"bool" reals
nil) (atan_0 formula-decl
nil atan
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(both_sides_times1 formula-decl
nil 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)
(/= const-decl
"boolean" notequal
nil)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(<= const-decl
"bool" reals
nil)
(nonpos_real nonempty-type-eq-decl
nil real_types
nil)
(< const-decl
"bool" reals
nil)
(negreal nonempty-type-eq-decl
nil real_types
nil))
shostak))
(atan2_swap_pos_TCC1 0
(atan2_swap_pos_TCC1-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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)
(nnint_times_nnint_is_nnint application-judgement
"nonneg_int"
integers
nil)
(even_times_int_is_even application-judgement
"even_int" integers
nil)
(mult_divides1 application-judgement
"(divides(n))" divides
nil)
(/= const-decl
"boolean" notequal
nil))
nil))
(atan2_swap_pos_TCC2 0
(atan2_swap_pos_TCC2-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((/= const-decl
"boolean" notequal
nil))
nil))
(atan2_swap_pos_TCC3 0
(atan2_swap_pos_TCC3-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((/= const-decl
"boolean" notequal
nil))
nil))
(atan2_swap_pos_TCC4 0
(atan2_swap_pos_TCC4-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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)
(/= const-decl
"boolean" notequal
nil)
(real_times_real_is_real application-judgement
"real" reals
nil))
nil))
(atan2_swap_pos 0
(atan2_swap_pos-1
nil 3514306980
(
"" (skeep)
((
"" (
case "x > 0 AND y > 0")
((
"1" (flatten)
((
"1" (hide -3)
((
"1" (
expand "atan2")
((
"1" (
assert)
((
"1" (lemma
"atan_sub_swap")
((
"1" (inst?) ((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
case "x < 0 AND y < 0")
((
"1" (flatten)
((
"1" (hide -3 1)
((
"1" (
expand "atan2")
((
"1" (
assert)
((
"1" (lemma
"atan_sub_swap")
((
"1" (inst?) ((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (hide 3) ((
"2" (grind-reals)
nil nil))
nil))
nil))
nil))
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)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(atan_sub_swap formula-decl
nil atan
nil)
(atan2 const-decl
"real" atan2
nil)
(pi_bound name-judgement
"{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx
nil)
(pos_times_gt formula-decl
nil real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(< const-decl
"bool" reals
nil))
shostak))
(atan2_swap_neg_TCC1 0
(atan2_swap_neg_TCC1-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(nnint_times_nnint_is_nnint application-judgement
"nonneg_int"
integers
nil)
(even_times_int_is_even application-judgement
"even_int" integers
nil)
(mult_divides1 application-judgement
"(divides(n))" divides
nil)
(/= const-decl
"boolean" notequal
nil))
nil))
(atan2_swap_neg_TCC2 0
(atan2_swap_neg_TCC2-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((/= const-decl
"boolean" notequal
nil))
nil))
(atan2_swap_neg_TCC3 0
(atan2_swap_neg_TCC3-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((/= const-decl
"boolean" notequal
nil))
nil))
(atan2_swap_neg_TCC4 0
(atan2_swap_neg_TCC4-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(/= const-decl
"boolean" notequal
nil)
(real_times_real_is_real application-judgement
"real" reals
nil))
nil))
(atan2_swap_neg 0
(atan2_swap_neg-1
nil 3514307142
(
"" (skeep)
((
"" (
case "x > 0 AND y < 0")
((
"1" (hide -2)
((
"1" (flatten)
((
"1" (
expand "atan2")
((
"1" (
assert)
((
"1" (
expand "sign")
((
"1" (lemma
"atan_sub_swap")
((
"1" (inst?) ((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
case "x < 0 AND y > 0")
((
"1" (hide -2 1)
((
"1" (flatten)
((
"1" (
expand "sign")
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1" (lemma
"atan_sub_swap")
((
"1" (inst?) ((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (hide 3) ((
"2" (grind-reals)
nil nil))
nil))
nil))
nil))
nil)
((< const-decl
"bool" reals
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)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(nzreal_times_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(atan_sub_swap formula-decl
nil atan
nil)
(sign const-decl
"Sign" sign
"reals/")
(atan2 const-decl
"real" atan2
nil)
(pi_bound name-judgement
"{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx
nil)
(neg_times_lt formula-decl
nil real_props
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil))
shostak))
(atan2_swap_zero_TCC1 0
(atan2_swap_zero_TCC1-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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
"boolean" notequal
nil))
nil))
(atan2_swap_zero_TCC2 0
(atan2_swap_zero_TCC2-1
nil 3514306973 (
"" (subtype-tcc)
nil nil)
((boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
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
"boolean" notequal
nil)
(Integral const-decl
"real" integral_def
"analysis/")
(atan_value const-decl
"real" atan
nil)
(pi const-decl
"posreal" atan
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil))
nil))
(atan2_swap_zero 0
(atan2_swap_zero-1
nil 3514307173
(
"" (skeep)
((
"" (lemma
"atan_0")
((
"" (split)
((
"1" (flatten)
((
"1" (replaces -1)
((
"1" (
case "y > 0")
((
"1" (
expand "atan2") ((
"1" (
assert)
nil nil))
nil)
(
"2" (
expand "atan2") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2" (flatten)
((
"2" (replaces -1)
((
"2" (
case "x > 0")
((
"1" (
expand "atan2") ((
"1" (
assert)
nil nil))
nil)
(
"2" (
expand "atan2") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((atan_0 formula-decl
nil atan
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(> const-decl
"bool" reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(real nonempty-type-from-decl
nil reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number nonempty-type-decl
nil numbers
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(atan2 const-decl
"real" atan2
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)
(
nil application-judgement
"nnreal_lt_2pi" atan2
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil))
shostak))
(atan2_cos_sin_TCC1 0
(atan2_cos_sin_TCC1-1
nil 3269553823
(
"" (skosimp*)
((
"" (typepred
"a!1")
((
"" (lemma
"sin_eq_0_2pi" (
"a" "a!1"))
((
"" (lemma
"cos_eq_0_2pi" (
"a" "a!1"))
((
"" (
assert)
((
"" (split -1)
((
"1" (split -2)
((
"1" (
assert)
nil nil) (
"2" (
assert)
nil nil))
nil)
(
"2" (split -2)
((
"1" (
assert)
nil nil) (
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
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
"[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(< const-decl
"bool" reals
nil)
(nnreal type-eq-decl
nil real_types
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)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(cos_eq_0_2pi formula-decl
nil trig_basic
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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(cos_range application-judgement
"trig_range" sincos_def
nil)
(sin_range application-judgement
"trig_range" sincos_def
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(sin_eq_0_2pi formula-decl
nil trig_basic
nil)
(pi_bound name-judgement
"{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx
nil))
shostak))
(atan2_cos_sin 0
(atan2_cos_sin-2
nil 3279154016
(
"" (
case "FORALL (x:posreal): x < pi => sin(x) > 0")
((
"1"
(
case "FORALL (x: nnreal): x < pi => atan2(cos(x), sin(x)) = x")
((
"1" (skolem 1 (
"a"))
((
"1" (
case "a < pi")
((
"1" (inst -2
"a") ((
"1" (
assert)
nil nil))
nil)
(
"2" (inst -1
"a-pi")
((
"1" (
assert)
((
"1" (
rewrite "cos_minus")
((
"1" (
rewrite "sin_minus")
((
"1" (
rewrite "sin_pi")
((
"1" (
rewrite "cos_pi")
((
"1" (
assert)
((
"1"
(lemma
"atan2_cancel_neg"
(
"x" "cos(a)" "y" "sin(a)" "nz" "-1"))
((
"1" (case-replace
"a=pi")
((
"1" (
rewrite "sin_pi")
((
"1"
(
rewrite "cos_pi")
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (lemma
"sin_eq_0_2pi" (
"a" "a"))
((
"2"
(
assert)
((
"2"
(inst -
"a-pi")
((
"2"
(
assert)
((
"2"
(
rewrite "sin_minus" -3)
((
"2"
(
rewrite "cos_pi")
((
"2"
(
rewrite "sin_pi")
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (hide 2)
((
"2" (skolem 1 (
"a"))
((
"2" (flatten)
((
"2" (inst -
"a")
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1" (lemma
"trichotomy" (
"x" "cos(a)"))
((
"1" (split)
((
"1" (
assert)
((
"1" (
case "a)
(("1" (rewrite "tan_rew")
(("1" (rewrite "atan_tan")
(("1"
(expand "abs")
(("1" (propax) nil nil))
nil))
nil)
("2" (expand "Tan?")
(("2" (assert) nil nil)) nil))
nil)
("2" (lemma "cos_value_strict_decreasing")
(("2" (case-replace "a=pi/2")
(("1"
(rewrite "cos_pi2")
(("1" (assert) nil nil))
nil)
("2"
(expand "strict_decreasing?")
(("2"
(inst - "pi/2" "a")
(("2"
(rewrite "cos_value_pi2")
(("2"
(assert)
(("2"
(lemma
"cos_cos_value"
("a" "a"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (lemma "cos_eq_0_2pi" ("a" "a"))
(("2" (assert) nil nil)) nil))
nil)
("3" (assert)
(("3" (lemma "cos_value_strict_decreasing")
(("3" (expand "strict_decreasing?")
(("3"
(lemma "trich_lt" ("x" "a" "y" "pi/2"))
(("3"
(split)
(("1"
(inst - "a" "pi/2")
(("1"
(rewrite "cos_value_pi2")
(("1"
(assert)
(("1"
(rewrite "cos_cos_value" -3)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(rewrite "cos_pi2")
(("2" (assert) nil nil))
nil))
nil)
("3"
(hide -2)
(("3"
(name "b" "a-pi/2")
(("3"
(lemma "sin_plus")
(("3"
(lemma "cos_plus")
(("3"
(inst - "b" "pi/2")
(("3"
(inst - "b" "pi/2")
(("3"
(rewrite "cos_pi2")
(("3"
(rewrite "sin_pi2")
(("3"
(assert)
(("3"
(replace -3 -1 rl)
(("3"
(replace
-3
-2
rl)
(("3"
(assert)
(("3"
(replace -3)
(("3"
(replace
-1)
(("3"
(replace
-2)
(("3"
(hide
-1
-2)
(("3"
(lemma
"atan_neg"
("x"
"cos(b)/sin(b)"))
(("3"
(replace
-1
1)
(("3"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"cos(b)"
"py"
"sin(b)"))
(("3"
(lemma
"atan_inv"
("px"
"cos(b) / sin(b)"))
(("1"
(rewrite
"div_div1"
-1)
(("1"
(assert)
(("1"
(case-replace
"((1 * sin(b)) / cos(b))=tan(b)")
(("1"
(rewrite
"atan_tan"
-2)
(("1"
(assert)
nil
nil)
("2"
(expand
"abs")
(("2"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"tan")
(("2"
(assert)
nil
nil))
nil)
("3"
(expand
"Tan?")
(("3"
(assert)
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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case-replace "a=0")
(("1" (rewrite "cos_0")
(("1" (rewrite "sin_0")
(("1" (expand "atan2")
(("1" (rewrite "atan_0") nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp)
(("3" (lemma "sin2_cos2" ("a" "x!1"))
(("3" (replace -3)
(("3" (replace -4)
(("3" (expand "sq") (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (case "x!1<=pi/2")
(("1" (rewrite "sin_sin_value")
(("1" (lemma "sin_value_strict_increasing")
(("1" (expand "strict_increasing?")
(("1" (inst - "0" "x!1")
(("1" (rewrite "sin_value_0")
(("1" (assert) nil nil)) nil)
("2" (expand "abs") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sin_sin_phase")
(("2" (expand "sin_phase")
(("2" (lemma "floor_div" ("x" "2*x!1" "py" "pi" "i" "1"))
(("2" (assert)
(("2" (lemma "sin_value_strict_increasing")
(("2" (expand "strict_increasing?")
(("2" (inst - "0" "pi-x!1")
(("1" (rewrite "sin_value_0")
(("1" (assert) nil nil)) nil)
("2" (expand "abs") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sin_value_strict_increasing formula-decl nil sincos_quad nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
(sin_value_0 formula-decl nil sincos_quad nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(sin_sin_value formula-decl nil sincos_def nil)
(sin_phase const-decl "real_abs_le1" sincos_phase nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(integer nonempty-type-from-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)
(floor_div formula-decl nil floor_ceil nil)
(sin_sin_phase formula-decl nil sincos_def nil)
(cos const-decl "real" sincos_def nil)
(atan2 const-decl "real" atan2 nil)
--> --------------------
--> maximum size reached
--> --------------------
