(atanx
(cauchy_ssmallreal_TCC1 0
(cauchy_ssmallreal_TCC1-1
nil 3288497283
(
"" (
expand "cauchy_ssmallreal?")
((
"" (inst +
"0")
((
"" (
expand "cauchy_prop") ((
"" (propax)
nil 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)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
AND const-decl
"[bool, 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)
(ssmallreal nonempty-type-eq-decl
nil atanx
nil)
(cauchy_prop const-decl
"bool" cauchy
nil)
(posint_exp application-judgement
"posint" exponentiation
nil)
(cauchy_ssmallreal? const-decl
"bool" atanx
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil))
shostak))
(subtype_TCC1 0
(subtype_TCC1-1
nil 3288497283
(
"" (skosimp*)
((
"" (typepred
"x!1")
((
"" (
expand "cauchy_ssmallreal?")
((
"" (skosimp*)
((
"" (
expand "cauchy_real?") ((
"" (inst +
"x!2")
nil nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_ssmallreal nonempty-type-eq-decl
nil atanx
nil)
(cauchy_ssmallreal? const-decl
"bool" atanx
nil)
(nat nonempty-type-eq-decl
nil naturalnumbers
nil)
(>= const-decl
"bool" reals
nil)
(int nonempty-type-eq-decl
nil integers
nil)
(integer_pred const-decl
"[rational -> boolean]" integers
nil)
(rational nonempty-type-from-decl
nil rationals
nil)
(rational_pred const-decl
"[real -> boolean]" rationals
nil)
(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)
(ssmallreal nonempty-type-eq-decl
nil atanx
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)
(cauchy_real? const-decl
"bool" cauchy
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil))
shostak))
(cauchy_vsmallreal_TCC1 0
(cauchy_vsmallreal_TCC1-1
nil 3288497283
(
"" (
expand "cauchy_vsmallreal?")
((
"" (inst +
"0")
((
"" (
expand "cauchy_prop") ((
"" (propax)
nil 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)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(<= const-decl
"bool" reals
nil) (< const-decl
"bool" reals
nil)
(vsmallreal nonempty-type-eq-decl
nil atanx
nil)
(cauchy_prop const-decl
"bool" cauchy
nil)
(posint_exp application-judgement
"posint" exponentiation
nil)
(cauchy_vsmallreal? const-decl
"bool" atanx
nil))
shostak))
(subtype_TCC2 0
(subtype_TCC2-1
nil 3288497283
(
"" (skosimp*)
((
"" (typepred
"x!1")
((
"" (
expand "cauchy_vsmallreal?")
((
"" (
expand "cauchy_real?")
((
"" (skosimp*) ((
"" (inst +
"x!2")
nil nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_vsmallreal nonempty-type-eq-decl
nil atanx
nil)
(cauchy_vsmallreal? const-decl
"bool" atanx
nil)
(nat nonempty-type-eq-decl
nil naturalnumbers
nil)
(>= const-decl
"bool" reals
nil)
(int nonempty-type-eq-decl
nil integers
nil)
(integer_pred const-decl
"[rational -> boolean]" integers
nil)
(rational nonempty-type-from-decl
nil rationals
nil)
(rational_pred const-decl
"[real -> boolean]" rationals
nil)
(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)
(cauchy_real? const-decl
"bool" cauchy
nil)
(vsmallreal nonempty-type-eq-decl
nil atanx
nil)
(< const-decl
"bool" reals
nil) (<= const-decl
"bool" reals
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil))
shostak))
(cauchy_atan_drx_series_TCC1 0
(cauchy_atan_drx_series_TCC1-1
nil 3392689913
(
"" (skosimp)
((
"" (
expand "cauchy_nzreal?")
((
"" (inst +
"1+2*n!1")
((
"" (
expand "cauchy_prop")
((
"" (skosimp)
((
"" (
expand "cauchy_int") ((
"" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((int_times_int_is_int application-judgement
"int" integers
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)
(mult_divides2 application-judgement
"(divides(m))" divides
nil)
(cauchy_nzreal? const-decl
"bool" cauchy
nil)
(posint_exp application-judgement
"posint" exponentiation
nil)
(cauchy_prop const-decl
"bool" cauchy
nil)
(int_minus_int_is_int application-judgement
"int" integers
nil)
(cauchy_int const-decl
"cauchy_real" int
nil)
(nat nonempty-type-eq-decl
nil naturalnumbers
nil)
(>= const-decl
"bool" reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(int nonempty-type-eq-decl
nil integers
nil)
(integer_pred const-decl
"[rational -> boolean]" integers
nil)
(rational nonempty-type-from-decl
nil rationals
nil)
(rational_pred const-decl
"[real -> boolean]" rationals
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(nzreal 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)
(posint_plus_nnint_is_posint application-judgement
"posint"
integers
nil)
(odd_plus_even_is_odd application-judgement
"odd_int" integers
nil))
nil))
(cauchy_atan_drx_series_TCC2 0
(cauchy_atan_drx_series_TCC2-1
nil 3392689913
(
"" (skosimp)
((
"" (hide 1)
((
"" (
expand "cauchy_nzreal?")
((
"" (inst +
"1+2*n!1")
((
"" (
expand "cauchy_prop")
((
"" (skosimp)
((
"" (
expand "cauchy_int") ((
"" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((odd_plus_even_is_odd application-judgement
"odd_int" integers
nil)
(posint_plus_nnint_is_posint application-judgement
"posint"
integers
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)
(nzreal nonempty-type-eq-decl
nil reals
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(rational_pred const-decl
"[real -> boolean]" rationals
nil)
(rational nonempty-type-from-decl
nil rationals
nil)
(integer_pred const-decl
"[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl
nil integers
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(>= const-decl
"bool" reals
nil)
(nat nonempty-type-eq-decl
nil naturalnumbers
nil)
(cauchy_int const-decl
"cauchy_real" int
nil)
(int_minus_int_is_int application-judgement
"int" integers
nil)
(cauchy_prop const-decl
"bool" cauchy
nil)
(posint_exp application-judgement
"posint" exponentiation
nil)
(cauchy_nzreal? const-decl
"bool" cauchy
nil)
(mult_divides2 application-judgement
"(divides(m))" divides
nil)
(mult_divides1 application-judgement
"(divides(n))" divides
nil)
(even_times_int_is_even application-judgement
"even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement
"nonneg_int"
integers
nil)
(int_times_int_is_int application-judgement
"int" integers
nil))
nil))
(atan_series_lemma 0
(atan_series_lemma-1
nil 3288496910
(
"" (
expand "atan_series_coef")
((
"" (
expand "cauchy_atan_drx_series")
((
"" (skosimp*)
((
"" (lemma
"int_lemma" (
"n" "1+2*n!1"))
((
"" (lemma
"int_lemma" (
"n" "1"))
((
"" (lemma
"int_lemma" (
"n" "-1"))
((
"" (
assert)
((
"" (typepred
"n!1")
((
"" (lemma
"expt_minus1" (
"i" "n!1"))
((
"" (case-replace
"even?(n!1)")
((
"1" (
assert)
((
"1" (flatten)
((
"1" (
replace -2)
((
"1"
(lemma
"div_lemma"
(
"x"
"1"
"cx"
"cauchy_int(1)"
"nzy"
"1+2*n!1"
"nzcy"
"cauchy_int(1 + 2 * n!1)"))
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
rewrite "even_or_odd")
((
"2" (
assert)
((
"2" (
replace -2)
((
"2"
(lemma
"div_lemma"
(
"x"
"-1"
"cx"
"cauchy_int(-1)"
"nzy"
"1+2*n!1"
"nzcy"
"cauchy_int(1 + 2 * n!1)"))
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_atan_drx_series const-decl
"cauchy_real" atanx
nil)
(nat nonempty-type-eq-decl
nil naturalnumbers
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, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(int nonempty-type-eq-decl
nil integers
nil)
(integer_pred const-decl
"[rational -> boolean]" integers
nil)
(rational nonempty-type-from-decl
nil rationals
nil)
(rational_pred const-decl
"[real -> boolean]" rationals
nil)
(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)
(int_lemma formula-decl
nil int
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(even? const-decl
"bool" integers
nil)
(div_lemma formula-decl
nil div
nil)
(cauchy_real? const-decl
"bool" cauchy
nil)
(cauchy_real nonempty-type-eq-decl
nil cauchy
nil)
(cauchy_int const-decl
"cauchy_real" int
nil)
(cauchy_nzreal? const-decl
"bool" cauchy
nil)
(cauchy_nzreal nonempty-type-eq-decl
nil cauchy
nil)
(/= const-decl
"boolean" notequal
nil)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(posrat_div_posrat_is_posrat application-judgement
"posrat"
rationals
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(even_or_odd formula-decl
nil naturalnumbers
nil)
(expt_minus1 formula-decl
nil prelude_aux
nil)
(nzrat_div_nzrat_is_nzrat application-judgement
"nzrat" rationals
nil)
(atan_series_coef const-decl
"rat" atan
"trig_fnd/")
(odd_plus_even_is_odd application-judgement
"odd_int" integers
nil)
(posint_plus_nnint_is_posint application-judgement
"posint"
integers
nil)
(nzreal_exp application-judgement
"nzreal" exponentiation
nil)
(int_exp application-judgement
"int" exponentiation
nil)
(mult_divides2 application-judgement
"(divides(m))" divides
nil)
(mult_divides1 application-judgement
"(divides(n))" divides
nil)
(even_times_int_is_even application-judgement
"even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement
"nonneg_int"
integers
nil)
(int_times_int_is_int application-judgement
"int" integers
nil))
shostak))
(cauchy_atan_drxx_TCC1 0
(cauchy_atan_drxx_TCC1-1
nil 3288497284
(
"" (
expand "cauchys_real?")
((
"" (inst +
"atan_series_coef")
((
"" (
expand "cauchys_prop")
((
"" (skosimp*)
((
"" (lemma
"atan_series_lemma" (
"n" "n!1"))
((
"" (propax)
nil nil))
nil))
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)
(rational_pred const-decl
"[real -> boolean]" rationals
nil)
(rational nonempty-type-from-decl
nil rationals
nil)
(integer_pred const-decl
"[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl
nil integers
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(>= const-decl
"bool" reals
nil)
(nat nonempty-type-eq-decl
nil naturalnumbers
nil)
(rat nonempty-type-eq-decl
nil rationals
nil)
(atan_series_coef const-decl
"rat" atan
"trig_fnd/")
(atan_series_lemma formula-decl
nil atanx
nil)
(cauchys_prop const-decl
"bool" sum
nil)
(cauchys_real? const-decl
"bool" sum
nil))
shostak))
(cauchy_atan_drxx_prop_TCC1 0
(cauchy_atan_drxx_prop_TCC1-1
nil 3288506197
(
"" (skosimp*) ((
"" (typepred
"vsx!1") ((
"" (
assert)
nil nil))
nil))
nil)
((vsmallreal nonempty-type-eq-decl
nil atanx
nil)
(< const-decl
"bool" reals
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
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)
(real_le_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_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil))
shostak))
(cauchy_atan_drxx_prop_TCC2 0
(cauchy_atan_drxx_prop_TCC2-1
nil 3288506197
(
"" (skosimp*)
((
"" (typepred
"vsx!1")
((
"" (lemma
"sqrt_eq_0")
((
"" (inst -
"vsx!1") ((
"" (
assert)
nil nil))
nil))
nil))
nil))
nil)
((vsmallreal nonempty-type-eq-decl
nil atanx
nil)
(< const-decl
"bool" reals
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
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)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sqrt_eq_0 formula-decl
nil sqrt
"reals/"))
shostak))
(cauchy_atan_drxx_prop 0
(cauchy_atan_drxx_prop-1
nil 3288524114
(
"" (skosimp*)
((
"" (typepred
"vsx!1")
((
"" (
expand "cauchy_atan_drxx")
((
""
(lemma
"powerseries_lemma"
(
"x" "vsx!1" "cx" "cvsx!1" "xs" "atan_series_coef" "cxs"
"cauchy_atan_drx_series"))
((
"" (
replace -4)
((
"" (lemma
"atan_series_lemma")
((
"" (
replace -1)
((
"" (hide -1)
((
"" (
expand "cauchy_prop")
((
"" (skosimp*)
((
"" (inst -1
"2+p!1")
((
"" (inst -1
"2+p!1")
((
"" (flatten -1)
((
""
(name-replace
"CPS"
"cauchy_powerseries(cvsx!1, cauchy_atan_drx_series, 2 + p!1)(2 + p!1)")
((
""
(case-replace
"2^(2+p!1)=4*2^p!1")
((
"1"
(lemma
"lemma_A2"
(
"r"
"round(CPS/4)"
"p"
"CPS"
"q"
"4"))
((
"1"
(
assert)
((
"1"
(flatten -1)
((
"1"
(lemma
"atan_series"
(
"x"
"sqrt(vsx!1)"
"n"
"2+p!1"))
((
"1"
(
expand "atan_series_n")
((
"1"
(
expand "atan_series_term")
((
"1"
(
case
"FORALL (n:nat): sqrt(vsx!1) ^ (1 + 2 * n) = sqrt(vsx!1)* vsx!1^n")
((
"1"
(case-replace
"sigma(0, 2 + p!1,
LAMBDA (n: nat):
(sqrt(vsx!1) ^ (1 + 2 * n)) * atan_series_coef(n)) = sqrt(vsx!1)*sigma(0, 2 + p!1,
LAMBDA (n: na
t): vsx!1^n * atan_series_coef(n))")
(("1"
(hide -1)
(("1"
(inst - "3+p!1")
(("1"
(replace -1 -2)
(("1"
(expand
"powerseries")
(("1"
(case-replace
"(LAMBDA (i:nat):
IF i = 0 THEN atan_series_coef(i)
ELSE atan_series_coef(i) * vsx!1 ^ i
ENDIF) = (LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n))")
(("1"
(hide
-1
-2
-6)
(("1"
(name-replace
"PS"
"sigma(0, 2 + p!1,
LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n))")
(("1"
(name-replace
"RR"
"round(CPS / 4)")
(("1"
(expand
"<="
-6)
(("1"
(split
-6)
(("1"
(assert)
(("1"
(lemma
"sqrt_pos"
("px"
"vsx!1"))
(("1"
(lemma
"expt_pos"
("px"
"vsx!1"
"i"
"3+p!1"))
(("1"
(lemma
"sqrt_lt"
("nny"
"vsx!1"
"nnz"
"sq(1/2)"))
(("1"
(rewrite
"sqrt_sq")
(("1"
(expand
"sq"
-1)
(("1"
(rewrite
"abs_mult"
-5)
(("1"
(expand
"abs"
-5
2)
(("1"
(expand
"abs"
-5
2)
(("1"
(assert)
(("1"
(lemma
"both_sides_div_pos_le1"
("x"
"abs(atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS)"
"y"
"(sqrt(vsx!1) * vsx!1 ^ (3 + p!1)) / (7 + 2 * p!1)"
"pz"
"sqrt(vsx!1)"))
(("1"
(replace
-1
-6
rl)
(("1"
(hide
-1)
(("1"
(case-replace
"(sqrt(vsx!1) * vsx!1 ^ (3 + p!1)) / (7 + 2 * p!1) / sqrt(vsx!1) = vsx!1 ^ (3 + p!1) / (7 + 2 * p!1)")
(("1"
(hide
-1)
(("1"
(case-replace
"abs(atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS) / sqrt(vsx!1) = abs(atan(sqrt(vsx!1)) / sqrt(vsx!1) -PS)")
(("1"
(hide
-1)
(("1"
(name-replace
"TMP1"
"atan(sqrt(vsx!1)) / sqrt(vsx!1)")
(("1"
(lemma
"both_sides_expt_pos_lt"
("px"
"vsx!1"
"py"
"1/4"
"pm"
"3+p!1"))
(("1"
(assert)
(("1"
(hide
-12)
(("1"
(case
"abs(TMP1 - PS)*2^p!1 < 1/4")
(("1"
(expand
"abs"
-1)
(("1"
(case
"TMP1)
(("1"
(assert)
(("1"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"-(TMP1 - PS)"
"py"
"2 ^ p!1"))
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"TMP1-PS"
"py"
"2 ^ p!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"both_sides_div_pos_lt2"
("pz"
"vsx!1 ^ (3 + p!1)"
"px"
"7 + 2 * p!1"
"py"
"1"))
(("2"
(hide
2)
(("2"
(assert)
(("2"
(lemma
"both_sides_expt_pos_lt"
("px"
"1/4"
"py"
"1/2"
"pm"
"3+p!1"))
(("2"
(assert)
(("2"
(lemma
"both_sides_expt_lt1_lt"
("lt1x"
"1/2"
"i"
"3+p!1"
"j"
"2+p!1"))
(("2"
(assert)
(("2"
(lemma
"inv_expt"
("n0x"
"2"
"i"
"2+p!1"))
(("2"
(lemma
"expt_pos"
("px"
"2"
"i"
"p!1"))
(("2"
(lemma
"div_mult_pos_lt2"
("py"
"2^p!1"
"x"
"abs(TMP1 - PS)"
"z"
"1/4"))
(("2"
(replace
-1
1
rl)
(("2"
(case-replace
"1 / 4 / 2 ^ p!1 = 1 / 2 ^ (2 + p!1)")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
(-2
1))
(("2"
(case-replace
"2 ^ (2 + p!1) = 4*2^p!1")
(("1"
(name-replace
"TMP4"
"2^p!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(lemma
"expt_plus"
("n0x"
"2"
"i"
"2"
"j"
"p!1"))
(("2"
(replace
-1)
(("2"
(expand
"^"
1
1)
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(propax)
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"
(hide-all-but
(-3
1))
(("2"
(lemma
"abs_div")
(("2"
(inst
-
"sqrt(vsx!1)"
"atan(sqrt(vsx!1)) - sqrt(vsx!1) * PS")
(("2"
(expand
"abs"
-1
3)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-3
1))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-1
*
rl)
(("2"
(rewrite
"sqrt_0")
(("2"
(expand
"PS")
(("2"
(case-replace
"sigma(0, 2 + p!1,
LAMBDA (n: nat): vsx!1 ^ n * atan_series_coef(n)) =1")
(("1"
--> --------------------
--> maximum size reached
--> --------------------
