(polar
(argrng_TCC1 0
(argrng_TCC1-1
nil 3455850866 (
"" (subtype-tcc)
nil nil)
((minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil))
nil))
(abs_def 0
(abs_def-1
nil 3455850889 (
"" (grind)
nil nil)
((Re const-decl
"real" complex_types
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(Im const-decl
"real" complex_types
nil)
(sq_abs const-decl
"nnreal" complex_types
nil)
(abs const-decl
"nnreal" polar
nil)
(real_times_real_is_real application-judgement
"real" reals
nil))
shostak))
(abs_def2 0
(abs_def2-1
nil 3472820584
(
"" (skosimp)
((
"" (
rewrite "abs_def")
((
"" (
expand "sq_abs") ((
"" (propax)
nil nil))
nil))
nil))
nil)
((abs_def formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(sq_abs const-decl
"nnreal" complex_types
nil))
shostak))
(abs_nzcomplex 0
(abs_nzcomplex-1
nil 3455850866
(
"" (skosimp) ((
"" (
expand "abs") ((
"" (
assert)
nil nil))
nil))
nil)
((abs const-decl
"nnreal" polar
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sqrt_pos application-judgement
"posreal" sqrt
"reals/")
(nz_sq_abs_pos application-judgement
"posreal" complex_types
nil))
nil))
(abs_nz_iff_nz 0
(abs_nz_iff_nz-1
nil 3455850929
(
"" (skosimp)
((
"" (split)
((
"1" (flatten)
((
"1" (
rewrite "abs_def")
((
"1" (
expand "Re" -2 2)
((
"1" (
expand "Im" -3 2)
((
"1" (
replace -2)
((
"1" (
replace -3)
((
"1" (hide -2 -3) ((
"1" (grind)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (flatten)
((
"2" (typepred
"abs(z!1)")
((
"2" (
expand ">=")
((
"2" (
expand "<=")
((
"2" (split)
((
"1" (
assert)
nil nil)
(
"2" (
rewrite "abs_def")
((
"2" (hide 2)
((
"2"
(lemma
"sqrt_eq_0"
(
"nnx" "sq(Im(z!1)) + sq(Re(z!1))"))
((
"2" (split)
((
"1" (
expand "Re" 1 2)
((
"1" (
expand "Im" 1 2)
((
"1" (hide -2)
((
"1"
(
rewrite "sq_plus_eq_0")
((
"1"
(flatten)
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_def formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(real_plus_real_is_real application-judgement
"real" reals
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)
(nnint_plus_nnint_is_nnint application-judgement
"nonneg_int"
integers
nil)
(even_plus_even_is_even application-judgement
"even_int" integers
nil)
(sqrt_0 formula-decl
nil sqrt
"reals/")
(/= const-decl
"bool" complex_types
nil)
(Re const-decl
"real" complex_types
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(Im const-decl
"real" complex_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(abs const-decl
"nnreal" polar
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)
(<= const-decl
"bool" reals
nil)
(sq_plus_eq_0 formula-decl
nil sq
"reals/")
(sqrt_eq_0 formula-decl
nil sqrt
"reals/")
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(c_ne3 formula-decl
nil complex_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil))
shostak))
(abs_is_0 0
(abs_is_0-1
nil 3455851637
(
"" (skosimp)
((
"" (lemma
"abs_nz_iff_nz" (
"z" "z!1")) ((
"" (grind)
nil nil))
nil))
nil)
((complex type-decl
nil complex_types
nil)
(abs_nz_iff_nz formula-decl
nil polar
nil)
(= const-decl
"bool" complex_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(/= const-decl
"bool" complex_types
nil)
(abs const-decl
"nnreal" polar
nil)
(sq_abs const-decl
"nnreal" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(Re const-decl
"real" complex_types
nil))
shostak))
(abs_neg 0
(abs_neg-1
nil 3455851750 (
"" (grind)
nil nil)
((Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(- const-decl
"complex" complex_types
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(sq_abs const-decl
"nnreal" complex_types
nil)
(abs const-decl
"nnreal" polar
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(minus_real_is_real application-judgement
"real" reals
nil))
shostak))
(abs_mult 0
(abs_mult-1
nil 3455851754
(
"" (skosimp)
((
"" (
rewrite "abs_def")
((
"" (
rewrite "abs_def")
((
"" (
rewrite "abs_def")
((
"" (
rewrite "sqrt_times" 1 :dir rl)
((
"" (
rewrite "sqrt_eq") ((
"" (grind)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_def formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(* const-decl
"complex" complex_types
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(Re_mul1 formula-decl
nil complex_types
nil)
(Im_mul1 formula-decl
nil complex_types
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sqrt_eq formula-decl
nil sqrt
"reals/")
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(nonneg_real nonempty-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)
(sqrt_times formula-decl
nil sqrt
"reals/")
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil))
shostak))
(abs_inv 0
(abs_inv-1
nil 3455851970
(
"" (skosimp)
((
"" (
rewrite "abs_def")
((
"" (
rewrite "abs_def")
((
"" (
rewrite "sqrt_lem")
((
"1" (
rewrite "sq_rew")
((
"1" (
rewrite "sq_div")
((
"1" (
rewrite "div_cancel3")
((
"1" (
expand "c_div")
((
"1" (
expand "c_div")
((
"1" (
expand "Im")
((
"1" (
expand "Re")
((
"1" (
expand "sq_abs")
((
"1" (typepred
"n0z!1")
((
"1" (
expand "Im")
((
"1"
(
expand "Re")
((
"1"
(
rewrite "sq_rew")
((
"1"
(
rewrite "sq_rew")
((
"1"
(
rewrite "sq_div")
((
"1"
(
rewrite "sq_div")
((
"1"
(
rewrite "sq_times")
((
"1"
(
rewrite "sq_times")
((
"1"
(
assert)
((
"1"
(
rewrite "sq_neg")
((
"1"
(
assert)
((
"1"
(name
"DRL"
"sq(sq(x(n0z!1)) + sq(y(n0z!1)))")
((
"1"
(
replace -1)
((
"1"
(
assert)
((
"1"
(name-replace
"XX"
"sq(x(n0z!1))")
((
"1"
(name-replace
"YY"
"sq(y(n0z!1))")
((
"1"
(hide -2)
((
"1"
(
expand
"sq")
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
expand "/=")
((
"2"
(
rewrite "sq_plus_eq_0")
((
"2"
(flatten)
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2"
(
expand "/=")
((
"2"
(hide 1)
((
"2"
(
rewrite "sq_plus_eq_0")
((
"2"
(flatten)
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
expand "/=")
((
"2" (hide 1)
((
"2"
(lemma
"sqrt_eq_0"
(
"nnx" "sq(Im(n0z!1)) + sq(Re(n0z!1))"))
((
"2" (split)
((
"1" (hide -2)
((
"1" (
rewrite "sq_plus_eq_0")
((
"1" (flatten)
((
"1" (typepred
"n0z!1")
((
"1"
(split)
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (hide 2)
((
"2"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "1" "py" "sqrt(sq(Im(n0z!1)) + sq(Re(n0z!1)))"))
((
"1" (
assert)
nil nil)
(
"2" (hide 2)
((
"2" (
rewrite "sqrt_pos")
((
"2" (hide 2)
((
"2" (typepred
"n0z!1")
((
"2" (split)
((
"1" (
assert)
((
"1" (lemma
"sq_nz_pos" (
"nz" "Re(n0z!1)"))
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (lemma
"sq_nz_pos" (
"nz" "Im(n0z!1)"))
((
"1" (
assert)
nil nil)
(
"2" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_def formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(number nonempty-type-decl
nil numbers
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(real nonempty-type-from-decl
nil reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(/= const-decl
"boolean" notequal
nil)
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(/ const-decl
"complex" complex_types
nil)
(abs_nzcomplex application-judgement
"posreal" polar
nil)
(nz_sq_abs_pos application-judgement
"posreal" complex_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(div_nzcomplex2 application-judgement
"nzcomplex" complex_types
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(Re_div2 formula-decl
nil complex_types
nil)
(Im_div2 formula-decl
nil complex_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)
(sqrt_lem formula-decl
nil sqrt
"reals/")
(>= const-decl
"bool" reals
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(nnreal type-eq-decl
nil real_types
nil)
(sq_abs const-decl
"nnreal" complex_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(sqrt const-decl
"{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(nzreal_times_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(sq_div formula-decl
nil sq
"reals/")
(sq_1 formula-decl
nil sq
"reals/")
(sq_sqrt formula-decl
nil sqrt
"reals/")
(y adt-accessor-decl
"[complex -> real]" complex_types
nil)
(x adt-accessor-decl
"[complex -> real]" complex_types
nil)
(sq_plus_eq_0 formula-decl
nil sq
"reals/")
(sq_times formula-decl
nil sq
"reals/")
(real_plus_real_is_real application-judgement
"real" reals
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(div_cancel3 formula-decl
nil real_props
nil)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(sqrt_eq_0 formula-decl
nil sqrt
"reals/")
(sq_nz_pos application-judgement
"posreal" sq
"reals/")
(sq_rew formula-decl
nil sq
"reals/")
(posreal_div_posreal_is_posreal judgement-tcc
nil real_types
nil)
(> const-decl
"bool" reals
nil)
(posreal nonempty-type-eq-decl
nil real_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sqrt_pos judgement-tcc
nil sqrt
"reals/")
(nzreal nonempty-type-eq-decl
nil reals
nil)
(sq_nz_pos judgement-tcc
nil sq
"reals/"))
shostak))
(abs_div 0
(abs_div-1
nil 3455853159
(
"" (skosimp)
((
"" (lemma
"abs_inv" (
"n0z" "n0z!1"))
((
"" (lemma
"abs_mult" (
"z1" "z!1" "z2" "1/n0z!1"))
((
"" (
replace -2)
((
"" (hide -2)
((
"" (
replace -1 1 rl)
((
"" (hide -1)
((
"" (
expand "abs")
((
"" (
rewrite "sqrt_eq")
((
"" (
expand "sq_abs")
((
"" (
expand "sq") ((
"" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(Re const-decl
"real" complex_types
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
"boolean" notequal
nil)
(number nonempty-type-decl
nil numbers
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(complex type-decl
nil complex_types
nil)
(abs_inv formula-decl
nil polar
nil)
(abs_nzcomplex application-judgement
"posreal" polar
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(abs const-decl
"nnreal" polar
nil)
(Im_div1 formula-decl
nil complex_types
nil)
(Re_div1 formula-decl
nil complex_types
nil)
(Re_div2 formula-decl
nil complex_types
nil)
(Im_div2 formula-decl
nil complex_types
nil)
(Im_mul1 formula-decl
nil complex_types
nil)
(Re_mul1 formula-decl
nil complex_types
nil)
(nz_sq_abs_pos application-judgement
"posreal" complex_types
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(div_nzcomplex2 application-judgement
"nzcomplex" complex_types
nil)
(* const-decl
"complex" complex_types
nil)
(/ const-decl
"complex" complex_types
nil)
(sq_abs const-decl
"nnreal" complex_types
nil)
(nnreal type-eq-decl
nil real_types
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil)
(sqrt_eq formula-decl
nil sqrt
"reals/")
(abs_mult formula-decl
nil polar
nil)
(/ const-decl
"complex" complex_types
nil))
shostak))
(abs_triangle 0
(abs_triangle-1
nil 3455853469
(
"" (skosimp)
((
"" (
expand "abs")
((
"" (
rewrite "sq_le" 1 :dir rl)
((
"" (
assert)
((
"" (
rewrite "sq_plus")
((
"" (
rewrite "sqrt_times" 1 :dir rl)
((
"" (
expand "sq_abs")
((
"" (
assert)
((
"" (
rewrite "sq_plus")
((
"" (
rewrite "sq_plus")
((
"" (
assert)
((
""
(
case "Im(z1!1) * Im(z2!1)+Re(z1!1) * Re(z2!1) <=sqrt(sq(Im(z1!1)) * sq(Im(z2!1)) + sq(Im(z1!1)) * sq(Re(z2!1)) +
(sq(Im(z2!1)) * sq(Re(z1!1)) + sq(Re(z1!1)) * sq(Re(z2!1))))
")
((
"1" (
assert)
nil nil)
(
"2" (hide 2)
((
"2" (
rewrite "sq_times" 1 :dir rl)
((
"2"
(
rewrite "sq_times" 1 :dir rl)
((
"2"
(
rewrite "sq_times" 1 :dir rl)
((
"2"
(
rewrite "sq_times" 1 :dir rl)
((
"2"
(
rewrite "sq_le" 1 :dir rl)
((
"2"
(
rewrite "sq_plus")
((
"2"
(
assert)
((
"2"
(
case
"2*(Im(z1!1) * Im(z2!1) * Re(z1!1) * Re(z2!1)) <= sq(Im(z1!1) * Re(z2!1)) +
sq(Im(z2!1) * Re(z1!1))
")
((
"1" (
assert)
nil nil)
(
"2"
(hide 2)
((
"2"
(lemma
"sq_minus"
(
"a"
"Im(z1!1) * Re(z2!1)"
"b"
"Im(z2!1) * Re(z1!1)"))
((
"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)
((abs const-decl
"nnreal" polar
nil)
(sq_sqrt formula-decl
nil sqrt
"reals/")
(sqrt_times formula-decl
nil sqrt
"reals/")
(real_plus_real_is_real application-judgement
"real" reals
nil)
(Im_add1 formula-decl
nil complex_types
nil)
(Re_add1 formula-decl
nil complex_types
nil)
(Re const-decl
"real" complex_types
nil)
(<= const-decl
"bool" reals
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(sq_times formula-decl
nil sq
"reals/")
(real_minus_real_is_real application-judgement
"real" reals
nil)
(sq_minus formula-decl
nil sq
"reals/")
(real_times_real_is_real application-judgement
"real" reals
nil)
(Im const-decl
"real" complex_types
nil)
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(sq_plus formula-decl
nil sq
"reals/")
(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)
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(+ const-decl
"complex" complex_types
nil)
(sq_abs const-decl
"nnreal" complex_types
nil)
(complex type-decl
nil complex_types
nil)
(sqrt const-decl
"{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(nnreal type-eq-decl
nil real_types
nil)
(nonneg_real nonempty-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)
(sq_le formula-decl
nil sq
"reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil))
shostak))
(abs_abs 0
(abs_abs-1
nil 3455851919
(
"" (skosimp)
((
"" (
rewrite "abs_def")
((
"" (
expand "abs" 1) ((
"" (propax)
nil nil))
nil))
nil))
nil)
((abs_def formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil))
shostak))
(abs_i 0
(abs_i-1
nil 3455851913 (
"" (grind)
nil nil)
((complex_i const-decl
"nzcomplex" complex_types
nil)
(Re const-decl
"real" complex_types
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(Im const-decl
"real" complex_types
nil)
(sq_abs const-decl
"nnreal" complex_types
nil)
(sqrt_1 formula-decl
nil sqrt
"reals/")
(abs const-decl
"nnreal" polar
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(abs_nzcomplex application-judgement
"posreal" polar
nil))
shostak))
(abs_div2 0
(abs_div2-1
nil 3455991712
(
"" (skosimp)
((
"" (
rewrite "abs_def")
((
"" (
rewrite "abs_def")
((
"" (
rewrite "sq_eq" 1 :dir rl)
((
"" (
assert)
((
"" (
rewrite "sq_div")
((
"" (
rewrite "sq_div")
((
"" (
rewrite "sq_div") ((
"" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_def formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(number nonempty-type-decl
nil numbers
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(real nonempty-type-from-decl
nil reals
nil)
(/= const-decl
"boolean" notequal
nil)
(nzreal nonempty-type-eq-decl
nil reals
nil)
(/ const-decl
"complex" complex_types
nil)
(nonzero_abs_is_pos application-judgement
"{y: posreal | y >= x}"
real_defs
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(Re_div3 formula-decl
nil complex_types
nil)
(Im_div3 formula-decl
nil complex_types
nil)
(nnreal_div_posreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(sq_eq formula-decl
nil sq
"reals/")
(bool nonempty-type-eq-decl
nil booleans
nil)
(>= const-decl
"bool" reals
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(nnreal type-eq-decl
nil real_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sqrt const-decl
"{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(Im const-decl
"real" complex_types
nil)
(Re const-decl
"real" complex_types
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(sq_div formula-decl
nil sq
"reals/")
(sq_nz_pos application-judgement
"posreal" sq
"reals/")
(sq_abs formula-decl
nil sq
"reals/")
(sq_sqrt formula-decl
nil sqrt
"reals/"))
shostak))
(abs_div3 0
(abs_div3-1
nil 3455991811
(
"" (skosimp)
((
"" (
rewrite "abs_def")
((
"" (
rewrite "abs_def")
((
"" (
rewrite "sq_eq" 1 :dir rl)
((
"1" (
assert)
((
"1" (
rewrite "sq_div")
((
"1" (
rewrite "sq_div")
((
"1" (typepred
"sq_abs(n0z!1)")
((
"1" (name
"SQ" "sq_abs(n0z!1)")
((
"1" (
expand "sq_abs")
((
"1" (
replace -1)
((
"1" (
rewrite "sq_times")
((
"1" (
rewrite "sq_times")
((
"1" (
rewrite "sq_neg")
((
"1"
(lemma
"sqrt_pos" (
"px" "SQ"))
((
"1"
(
rewrite "sq_div" 1)
((
"1"
(
assert)
((
"1"
(case-replace
"(sq(x!1) * SQ)/sq(SQ) = sq(x!1) / SQ")
((
"1"
(
expand "SQ" -1 1)
((
"1"
(
assert)
((
"1"
(
expand "sq_abs")
((
"1" (
assert)
nil nil))
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(hide 2)
((
"2"
(
expand "sq")
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (hide 2)
((
"2" (typepred
"sq_abs(n0z!1)")
((
"2" (
assert)
((
"2" (
expand "sq_abs")
((
"2"
(lemma
"sqrt_pos"
(
"px" "sq(Im(n0z!1)) + sq(Re(n0z!1))"))
((
"1"
(lemma
"both_sides_div_pos_le1"
(
"pz" "sqrt(sq(Im(n0z!1)) + sq(Re(n0z!1)))" "x"
"0" "y" "abs(x!1)"))
((
"1" (
assert)
nil nil) (
"2" (propax)
nil nil))
nil)
(
"2" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_def formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(number nonempty-type-decl
nil numbers
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(real nonempty-type-from-decl
nil reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(/= const-decl
"boolean" notequal
nil)
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(/ const-decl
"complex" complex_types
nil)
(abs_nzcomplex application-judgement
"posreal" polar
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(nz_sq_abs_pos application-judgement
"posreal" complex_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(Re_div2 formula-decl
nil complex_types
nil)
(Im_div2 formula-decl
nil complex_types
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(sq_eq formula-decl
nil sq
"reals/")
(>= const-decl
"bool" reals
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(nnreal type-eq-decl
nil real_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sqrt const-decl
"{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(sq_abs const-decl
"nnreal" complex_types
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(sq_div formula-decl
nil sq
"reals/")
(sq_nz_pos application-judgement
"posreal" sq
"reals/")
(nnreal_div_posreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(> const-decl
"bool" reals
nil)
(sq_times formula-decl
nil sq
"reals/")
(sqrt_pos application-judgement
"posreal" sqrt
"reals/")
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(sq_neg formula-decl
nil sq
"reals/")
(sq_abs formula-decl
nil sq
"reals/")
(SQ skolem-const-decl
"posreal" polar
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)
(sqrt_pos judgement-tcc
nil sqrt
"reals/")
(posreal nonempty-type-eq-decl
nil real_types
nil)
(sq_sqrt formula-decl
nil sqrt
"reals/")
(both_sides_div_pos_le1 formula-decl
nil real_props
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil))
shostak))
(arg_TCC1 0
(arg_TCC1-1
nil 3455854430 (
"" (subtype-tcc)
nil nil)
((Im const-decl
"real" complex_types
nil)
(Re const-decl
"real" complex_types
nil)
(= const-decl
"bool" complex_types
nil))
nil))
(arg_TCC2 0
(arg_TCC2-1
nil 3455854430
(
"" (skosimp)
((
"" (
expand "Re" 1 2)
((
"" (
expand "Im" 1 2)
((
"" (
assert)
((
"" (lemma
"atan2_0_2pi" (
"x" "Re(z!1)" "y" "Im(z!1)"))
((
"" (
assert)
((
"" (case-replace
"Re(z!1) < 0")
((
"1" (flatten) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
assert)
((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(real_minus_real_is_real application-judgement
"real" reals
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(< const-decl
"bool" reals
nil)
(atan2_0_2pi formula-decl
nil atan2
"trig/")
(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)
(complex type-decl
nil complex_types
nil)
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil))
nil))
(arg_TCC3 0
(arg_TCC3-1
nil 3455854430 (
"" (subtype-tcc)
nil nil)
((Im const-decl
"real" complex_types
nil)
(Re const-decl
"real" complex_types
nil)
(= const-decl
"bool" complex_types
nil))
nil))
(arg_TCC4 0
(arg_TCC4-1
nil 3455854430
(
"" (skosimp)
((
"" (
expand "Re" 2 2)
((
"" (
expand "Im" 2 2)
((
"" (lemma
"atan2_0_2pi" (
"x" "Re(z!1)" "y" "Im(z!1)"))
((
"" (
assert)
((
"" (case-replace
"Im(z!1)=0")
((
"1" (
assert)
((
"1" (flatten)
((
"1" (case-replace
"Re(z!1) >= 0")
((
"1" (flatten) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
assert)
((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (flatten)
((
"2" (case-replace
"Re(z!1) >= 0")
((
"1" (flatten) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
assert)
((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Im const-decl
"real" complex_types
nil)
(Re const-decl
"real" complex_types
nil)
(complex type-decl
nil complex_types
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
"trig/")
(= const-decl
"[T, T -> boolean]" equalities
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)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(>= const-decl
"bool" reals
nil)
(c_eq3 formula-decl
nil complex_types
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)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/"))
nil))
(arg_is_0_nz 0
(arg_is_0_nz-1
nil 3455855531
(
"" (skosimp)
((
"" (
expand "arg")
((
"" (
expand "Re" 1 2)
((
"" (
expand "Im" 1 2)
((
"" (lemma
"atan2_0_2pi" (
"x" "Re(n0z!1)" "y" "Im(n0z!1)"))
((
"" (case-replace
"Im(n0z!1) =0")
((
"1" (
assert)
((
"1" (typepred
"n0z!1")
((
"1" (
assert)
((
"1" (flatten)
((
"1" (case-replace
"Re(n0z!1) >= 0")
((
"1" (flatten)
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1"
(
rewrite "atan_0")
((
"1"
(
expand "Re")
((
"1"
(
expand "Im")
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (flatten)
((
"2" (hide -2)
((
"2"
(
expand "atan2")
((
"2"
(
rewrite "atan_0")
((
"2"
(
assert)
((
"2"
(
expand "Im")
((
"2"
(
expand "Re")
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (case-replace
"Im(n0z!1) < 0")
((
"1" (flatten)
((
"1" (case-replace
"Re(n0z!1) >= 0")
((
"1" (flatten)
((
"1" (
assert)
((
"1" (
expand "Im")
((
"1" (
expand "Re")
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
expand "Re")
((
"2" (
expand "Im")
((
"2" (
assert)
((
"2"
(flatten)
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (flatten)
((
"2" (case-replace
"Re(n0z!1) >= 0")
((
"1" (flatten)
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1"
(
expand ">=" -1)
((
"1"
(
expand "<=" -1)
((
"1"
(split)
((
"1"
(
assert)
((
"1"
(lemma
"atan_strict_increasing")
((
"1"
(
expand "strict_increasing?")
((
"1"
(inst
-
"0"
"Im(n0z!1) / Re(n0z!1)")
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"Im(n0z!1)"
"py"
"Re(n0z!1)"))
((
"1"
(
assert)
((
"1"
(
rewrite "atan_0")
((
"1"
(
assert)
((
"1"
(
expand "Im")
((
"1"
(
expand "Re")
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(
expand "Re")
((
"2"
(
expand "Im")
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
expand "Re")
((
"2" (
expand "Im")
((
"2"
(
assert)
((
"2"
(flatten)
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((arg const-decl
"argrng" polar
nil)
(Im const-decl
"real" complex_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(nnreal_plus_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(atan2 const-decl
"real" atan2
"trig/")
(atan_0 formula-decl
nil atan
"trig/")
(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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(>= const-decl
"bool" reals
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(< const-decl
"bool" reals
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(<= const-decl
"bool" reals
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_div_nzreal_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)
(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)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(atan_strict_increasing formula-decl
nil atan
"trig/")
(atan2_0_2pi formula-decl
nil atan2
"trig/")
(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)
(complex type-decl
nil complex_types
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(/= const-decl
"boolean" notequal
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(Re const-decl
"real" complex_types
nil))
shostak))
(arg_is_0 0
(arg_is_0-1
nil 3455856156
(
"" (skosimp)
((
"" (case-replace
"z!1=0")
((
"1" (
expand "arg")
((
"1" (
replace -1 1)
((
"1" (
expand "Re")
((
"1" (
expand "Im")
((
"1" (
assert)
((
"1" (flatten)
((
"1" (
assert)
((
"1" (
expand "Re")
((
"1" (
expand "Im") ((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (lemma
"arg_is_0_nz" (
"n0z" "z!1"))
((
"1" (
replace -1)
((
"1" (hide -1) ((
"1" (grind)
nil nil))
nil))
nil)
(
"2" (hide 3) ((
"2" (grind)
nil nil))
nil))
nil))
nil))
nil)
((complex type-decl
nil complex_types
nil)
(number nonempty-type-decl
nil numbers
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(real nonempty-type-from-decl
nil reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(= const-decl
"bool" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(Re const-decl
"real" complex_types
nil)
(arg const-decl
"argrng" polar
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(arg_is_0_nz formula-decl
nil polar
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(/= const-decl
"boolean" notequal
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil))
shostak))
(arg_is_pi2 0
(arg_is_pi2-1
nil 3455856760
(
"" (skosimp)
((
"" (typepred
"arg(z!1)")
((
"" (
expand "arg")
((
"" (case-replace
"Re(z!1)=0")
((
"1" (case-replace
"Im(z!1)>0")
((
"1" (
assert)
((
"1" (
expand "atan2") ((
"1" (propax)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2" (case-replace
"Im(z!1)=0")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
((
"2" (
expand "atan2") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (case-replace
"Im(z!1) < 0")
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1" (
assert)
((
"1" (case-replace
"Re(z!1)>0")
((
"1" (
assert)
((
"1" (typepred
"atan(Im(z!1) / Re(z!1))")
((
"1" (
expand "abs") ((
"1" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (typepred
"atan(Im(z!1) / Re(z!1))")
((
"2" (
expand "abs") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
expand "atan2")
((
"2" (typepred
"atan(Im(z!1) / Re(z!1))")
((
"2" (
expand "abs")
((
"2" (
assert)
((
"2" (case-replace
"Re(z!1) > 0")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
((
"2"
(case-replace
"atan(Im(z!1) / Re(z!1)) < 0")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((arg const-decl
"argrng" polar
nil)
(argrng nonempty-type-eq-decl
nil polar
nil)
(<= const-decl
"bool" reals
nil)
(complex type-decl
nil complex_types
nil)
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi_lb const-decl
"posreal" trig_basic
"trig/")
(
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)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(< const-decl
"bool" reals
nil)
(real nonempty-type-from-decl
nil reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(number nonempty-type-decl
nil numbers
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(Re const-decl
"real" complex_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(real_minus_real_is_real application-judgement
"real" reals
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)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(atan2 const-decl
"real" atan2
"trig/")
(Im const-decl
"real" complex_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(atan const-decl
"real_abs_lt_pi2" atan
"trig/")
(real_abs_lt_pi2 nonempty-type-eq-decl
nil atan
"trig/")
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/= const-decl
"boolean" notequal
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil))
shostak))
(arg_is_pi 0
(arg_is_pi-1
nil 3455857439
(
"" (skosimp)
((
"" (
expand "arg")
((
"" (case-replace
"Im(z!1)=0")
((
"1" (
assert)
((
"1" (case-replace
"Re(z!1)=0")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
((
"2" (
expand "atan2")
((
"2" (
rewrite "atan_0")
((
"2" (
assert)
((
"2" (case-replace
"Re(z!1) > 0")
((
"1" (
assert)
nil nil) (
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
expand "atan2")
((
"2" (case-replace
"Re(z!1)=0")
((
"1" (
assert)
((
"1" (lift-if -2) ((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2" (typepred
"atan(Im(z!1) / Re(z!1))")
((
"2" (lift-if -3)
((
"2" (
assert)
((
"2" (prop)
((
"2" (lemma
"atan_strict_increasing")
((
"2" (
expand "strict_increasing?")
((
"2" (inst -
"Im(z!1) / Re(z!1)" "0")
((
"2"
(
rewrite "atan_0")
((
"2"
(lemma
"both_sides_div_neg_lt1"
(
"nz"
"Re(z!1)"
"y"
"0"
"x"
"Im(z!1)"))
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((arg const-decl
"argrng" polar
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(atan const-decl
"real_abs_lt_pi2" atan
"trig/")
(real_abs_lt_pi2 nonempty-type-eq-decl
nil atan
"trig/")
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi_lb const-decl
"posreal" trig_basic
"trig/")
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(posreal nonempty-type-eq-decl
nil real_types
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/= const-decl
"boolean" notequal
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(< const-decl
"bool" reals
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(real_div_nzreal_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)
(atan_strict_increasing formula-decl
nil atan
"trig/")
(both_sides_div_neg_lt1 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)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(strict_increasing? const-decl
"bool" real_fun_preds
"reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(atan_0 formula-decl
nil atan
"trig/")
(> 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)
(atan2 const-decl
"real" atan2
"trig/")
(Re const-decl
"real" complex_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(Im const-decl
"real" complex_types
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)
(complex type-decl
nil complex_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number nonempty-type-decl
nil numbers
nil))
shostak))
(arg_is_mpi2 0
(arg_is_mpi2-1
nil 3455857932
(
"" (skosimp)
((
"" (
expand "arg")
((
"" (case-replace
"Re(z!1)=0")
((
"1" (case-replace
"Im(z!1)<0")
((
"1" (
assert)
((
"1" (
expand "atan2") ((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
expand "atan2")
((
"2" (lift-if) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
expand "atan2")
((
"2" (lift-if)
((
"2" (
assert)
((
"2" (typepred
"atan(Im(z!1) / Re(z!1))")
((
"2" (
expand "abs")
((
"2"
(name-replace
"DRL" "atan(Im(z!1) / Re(z!1))")
((
"2" (case-replace
"DRL<0")
((
"1" (
assert)
nil nil) (
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((arg const-decl
"argrng" polar
nil)
(atan const-decl
"real_abs_lt_pi2" atan
"trig/")
(real_abs_lt_pi2 nonempty-type-eq-decl
nil atan
"trig/")
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi_lb const-decl
"posreal" trig_basic
"trig/")
(
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)
(- 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)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(Im const-decl
"real" complex_types
nil)
(< const-decl
"bool" reals
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(atan2 const-decl
"real" atan2
"trig/")
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(Re const-decl
"real" complex_types
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)
(complex type-decl
nil complex_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number nonempty-type-decl
nil numbers
nil))
shostak))
(arg_lt_0 0
(arg_lt_0-1
nil 3455858132
(
"" (skosimp)
((
"" (
expand "arg")
((
"" (case-replace
"Im(z!1) < 0")
((
"1" (
assert)
((
"1"
(lemma
"atan2_ge_0_lt_2pi" (
"x" "Re(z!1)" "y" "Im(z!1)"))
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2" (lift-if)
((
"2" (
assert)
((
"2" (case-replace
"Im(z!1)=0")
((
"1" (
expand "atan2")
((
"1" (case-replace
"Re(z!1) = 0")
((
"1" (
assert)
((
"1" (
rewrite "atan_0")
((
"1" (
assert)
((
"1" (lift-if)
((
"1" (
assert)
((
"1"
(prop)
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
replace 1 -1)
((
"2" (
expand "atan2")
((
"2" (lift-if)
((
"2" (
assert)
((
"2" (case-replace
"Re(z!1)>0")
((
"1" (lemma
"atan_strict_increasing")
((
"1" (
expand "strict_increasing?")
((
"1"
(inst -
"0" "Im(z!1) / Re(z!1)")
((
"1"
(
rewrite "atan_0")
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "Im(z!1)" "py" "Re(z!1)"))
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (case-replace
"Re(z!1)=0")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
((
"2"
(lemma
"both_sides_div_neg_lt1"
(
"nz"
"Re(z!1)"
"y"
"0"
"x"
"Im(z!1)"))
((
"2"
(
assert)
((
"2"
(lemma
"atan_strict_increasing")
((
"2"
(
expand "strict_increasing?")
((
"2"
(inst
-
"Im(z!1) / Re(z!1)"
"0")
((
"2"
(
rewrite "atan_0")
((
"2"
(split)
((
"1"
(typepred
"atan(Im(z!1) / Re(z!1))")
((
"1"
(
expand "abs")
((
"1"
(
assert)
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)
((arg const-decl
"argrng" polar
nil) (> const-decl
"bool" reals
nil)
(strict_increasing? const-decl
"bool" real_fun_preds
"reals/")
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(posreal nonempty-type-eq-decl
nil real_types
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil)
(posreal_div_posreal_is_posreal judgement-tcc
nil real_types
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)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(atan_strict_increasing formula-decl
nil atan
"trig/")
(real_plus_real_is_real application-judgement
"real" reals
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(atan2 const-decl
"real" atan2
"trig/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(atan_0 formula-decl
nil atan
"trig/")
(Re const-decl
"real" complex_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(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)
(Im const-decl
"real" complex_types
nil)
(complex type-decl
nil complex_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))
shostak))
(arg_p_lt_pi 0
(arg_p_lt_pi-1
nil 3455862135
(
"" (skosimp)
((
"" (lemma
"arg_lt_0" (
"z" "z!1"))
((
"" (lemma
"arg_is_0" (
"z" "z!1"))
((
"" (lemma
"arg_is_pi" (
"z" "z!1"))
((
"" (lemma
"trichotomy" (
"x" "arg(z!1)"))
((
"" (split)
((
"1" (
assert)
((
"1" (typepred
"arg(z!1)")
((
"1" (
expand "<=" -2)
((
"1" (split)
((
"1" (
assert) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
assert)
((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil)
(
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((complex type-decl
nil complex_types
nil)
(arg_lt_0 formula-decl
nil polar
nil)
(arg_is_pi formula-decl
nil polar
nil)
(
NOT const-decl
"[bool -> bool]" booleans
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)
(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)
(trichotomy formula-decl
nil real_axioms
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
"[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_lb const-decl
"posreal" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(<= const-decl
"bool" reals
nil)
(argrng nonempty-type-eq-decl
nil polar
nil)
(arg const-decl
"argrng" polar
nil)
(arg_is_0 formula-decl
nil polar
nil))
shostak))
(arg_gt_0 0
(arg_gt_0-1
nil 3455860679
(
"" (skosimp)
((
"" (lemma
"arg_lt_0" (
"z" "z!1"))
((
"" (lemma
"arg_is_0" (
"z" "z!1"))
((
"" (lemma
"trichotomy" (
"x" "arg(z!1)"))
((
"" (split)
((
"1" (
assert)
((
"1" (flatten) ((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil)
(
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
((complex type-decl
nil complex_types
nil)
(arg_lt_0 formula-decl
nil polar
nil)
(arg const-decl
"argrng" polar
nil)
(argrng nonempty-type-eq-decl
nil polar
nil)
(<= const-decl
"bool" reals
nil)
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi_lb const-decl
"posreal" trig_basic
"trig/")
(posreal nonempty-type-eq-decl
nil real_types
nil)
(> const-decl
"bool" reals
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(< const-decl
"bool" reals
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(real nonempty-type-from-decl
nil reals
nil)
(real_pred const-decl
"[number_field -> boolean]" reals
nil)
(number_field nonempty-type-from-decl
nil number_fields
nil)
(number_field_pred const-decl
"[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(number nonempty-type-decl
nil numbers
nil)
(trichotomy formula-decl
nil real_axioms
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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(arg_is_0 formula-decl
nil polar
nil))
shostak))
(arg_div_abs 0
(arg_div_abs-1
nil 3455860780
(
"" (skosimp)
((
"" (
expand "arg")
((
"" (
rewrite "abs_def")
((
"" (case-replace
"Re(n0x!1)=0")
((
"1" (
rewrite "sq_0")
((
"1" (
assert)
((
"1" (typepred
"n0x!1")
((
"1" (
assert)
((
"1" (
rewrite "sqrt_sq_abs") ((
"1" (grind)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (lemma
"sq_nz_pos" (
"nz" "Re(n0x!1)"))
((
"2"
(lemma
"sqrt_pos"
(
"px" "sq(Im(n0x!1)) + sq(Re(n0x!1))"))
((
"1"
(name
"DIV" "sqrt(sq(Im(n0x!1)) + sq(Re(n0x!1)))")
((
"1" (
replace -1)
((
"1" (
assert)
((
"1" (case-replace
"Im(n0x!1) < 0")
((
"1"
(lemma
"both_sides_div_pos_lt1"
(
"pz" "DIV" "x" "Im(n0x!1)" "y" "0"))
((
"1" (
assert)
((
"1"
(lemma
"atan2_cancel_pos"
(
"x"
"Re(n0x!1)"
"y"
"Im(n0x!1)"
"pz"
"1/DIV"))
((
"1" (
assert)
nil nil)
(
"2"
(
assert)
((
"2"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "1" "py" "DIV"))
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (case-replace
"Im(n0x!1)=0")
((
"1" (
assert)
((
"1"
(lemma
"atan2_cancel_pos"
(
"x"
"Re(n0x!1)"
"y"
"0"
"pz"
"1/DIV"))
((
"1" (
assert)
nil nil)
(
"2"
(
assert)
((
"2"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "1" "py" "DIV"))
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "1" "py" "DIV"))
((
"2"
(lemma
"both_sides_div_pos_lt1"
(
"pz" "DIV" "y" "Im(n0x!1)" "x" "0"))
((
"2"
(
assert)
((
"2"
(lemma
"atan2_cancel_pos"
(
"x"
"Re(n0x!1)"
"y"
"Im(n0x!1)"
"pz"
"1/DIV"))
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((arg const-decl
"argrng" polar
nil)
(= const-decl
"[T, T -> boolean]" equalities
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)
(div_nzcomplex3 application-judgement
"nzcomplex" complex_types
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(atan2 const-decl
"real" atan2
"trig/")
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(/ const-decl
"complex" complex_types
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(sqrt_sq_abs formula-decl
nil sqrt
"reals/")
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(sq_0 formula-decl
nil sq
"reals/")
(sq_nz_pos judgement-tcc
nil sq
"reals/")
(nzreal nonempty-type-eq-decl
nil reals
nil)
(nnreal type-eq-decl
nil real_types
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sqrt const-decl
"{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(Re_div3 formula-decl
nil complex_types
nil)
(Im_div3 formula-decl
nil complex_types
nil)
(both_sides_div_pos_lt1 formula-decl
nil real_props
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(atan2_cancel_pos formula-decl
nil atan2
"trig/")
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(posreal_div_posreal_is_posreal judgement-tcc
nil real_types
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(< const-decl
"bool" reals
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
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)
(sqrt_pos judgement-tcc
nil sqrt
"reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(Re const-decl
"real" complex_types
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
"boolean" notequal
nil)
(number nonempty-type-decl
nil numbers
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(complex type-decl
nil complex_types
nil)
(abs_def formula-decl
nil polar
nil))
shostak))
(Re_cos_abs1 0
(Re_cos_abs1-1
nil 3455859132
(
"" (skosimp)
((
"" (
expand "arg")
((
"" (
rewrite "abs_def")
((
"" (case-replace
"Re(n0x!1) = 0")
((
"1" (
rewrite "sq_0")
((
"1" (
assert)
((
"1" (lemma
"trichotomy" (
"x" "Im(n0x!1)"))
((
"1" (split)
((
"1" (
expand "atan2")
((
"1" (
assert) ((
"1" (
rewrite "cos_pi2")
nil nil))
nil))
nil)
(
"2" (
replace -1)
((
"2" (
rewrite "sq_0")
((
"2" (
rewrite "sqrt_0") ((
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"3" (
rewrite "sqrt_sq_neg")
((
"3" (case-replace
"Im(n0x!1) = -1")
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1" (
assert)
((
"1" (lemma
"cos_neg" (
"a" "pi/2"))
((
"1"
(
rewrite "cos_pi2")
((
"1"
(
replace -1)
((
"1" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2"
(lemma
"sq_eq"
(
"nna" "sqrt(sq(Im(n0x!1)) + sq(Re(n0x!1)))" "nnb" "1"))
((
"2" (flatten)
((
"2" (split -2)
((
"1" (
rewrite "sq_sqrt" -1)
((
"1" (hide -2 -3)
((
"1" (
rewrite "sq_1")
((
"1"
(lemma
"cos_atan2"
(
"x" "Re(n0x!1)" "y" "Im(n0x!1)"))
((
"1" (
assert)
((
"1"
(lemma
"cos_period"
(
"a"
"atan2(Re(n0x!1), Im(n0x!1))"
"j"
"-1"))
((
"1"
(
replace -1 2 rl)
((
"1"
(hide -1)
((
"1"
(case-replace
"1 + sq(Im(n0x!1) / Re(n0x!1)) = 1/sq(Re(n0x!1))")
((
"1"
(hide -1)
((
"1"
(case-replace
"Re(n0x!1) > 0")
((
"1"
(
rewrite "sqrt_div" -2)
((
"1" (
assert)
nil nil)
(
"2"
(
expand "/=")
((
"2"
(
rewrite "sq_eq_0")
nil
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(
rewrite "sqrt_div" -1)
((
"1"
(
rewrite "div_div1")
((
"1" (
assert)
nil nil))
nil)
(
"2"
(
expand "/=")
((
"2"
(
rewrite "sq_eq_0")
nil
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(hide -1 3)
((
"2"
(
rewrite "sq_div" 1)
((
"2"
(lemma
"add_div"
(
"x"
"1"
"n0x"
"1"
"y"
"sq(Im(n0x!1))"
"n0y"
"sq(Re(n0x!1))"))
((
"2"
(
replace -1)
((
"2"
(hide -1)
((
"2"
(
rewrite "cross_mult")
nil
nil))
nil))
nil))
nil))
nil))
nil)
(
"3"
(
assert)
((
"3"
(
expand "/=")
((
"3"
(
rewrite "sq_eq_0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((arg const-decl
"argrng" polar
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(cos_range application-judgement
"trig_range" trig_basic
"trig/")
(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)
(c_eq3 formula-decl
nil complex_types
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)
(sqrt_sq formula-decl
nil sqrt
"reals/")
(cos_pi2 formula-decl
nil trig_basic
"trig/")
(atan2 const-decl
"real" atan2
"trig/")
(sqrt_0 formula-decl
nil sqrt
"reals/")
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(cos_neg formula-decl
nil trig_basic
"trig/")
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> 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)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(pi_lb const-decl
"posreal" trig_basic
"trig/")
(< const-decl
"bool" reals
nil)
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(real_minus_real_is_real application-judgement
"real" reals
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(sqrt_sq_neg formula-decl
nil sqrt
"reals/")
(trichotomy formula-decl
nil real_axioms
nil)
(sq_0 formula-decl
nil sq
"reals/")
(sq const-decl
"nonneg_real" sq
"reals/")
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sqrt const-decl
"{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(nnreal type-eq-decl
nil real_types
nil)
(sq_eq formula-decl
nil sq
"reals/")
(cos_atan2 formula-decl
nil atan2
"trig/")
(cos_period formula-decl
nil trig_basic
"trig/")
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
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)
(add_div formula-decl
nil real_props
nil)
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(cross_mult formula-decl
nil real_props
nil)
(posrat_div_posrat_is_posrat application-judgement
"posrat"
rationals
nil)
(sq_div formula-decl
nil sq
"reals/")
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(div_div1 formula-decl
nil real_props
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(sqrt_div formula-decl
nil sqrt
"reals/")
(sqrt_1 formula-decl
nil sqrt
"reals/")
(sq_eq_0 formula-decl
nil sq
"reals/")
(sqrt_pos application-judgement
"posreal" sqrt
"reals/")
(npreal_div_posreal_is_npreal application-judgement
"npreal"
real_types
nil)
(odd_minus_odd_is_even application-judgement
"even_int" integers
nil)
(posreal_plus_nnreal_is_posreal application-judgement
"posreal"
real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(nzreal_times_nzreal_is_nzreal application-judgement
"nzreal"
real_types
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)
(nzint_times_nzint_is_nzint application-judgement
"nzint" integers
nil)
(sq_1 formula-decl
nil sq
"reals/")
(sq_sqrt formula-decl
nil sqrt
"reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(Re const-decl
"real" complex_types
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
"boolean" notequal
nil)
(number nonempty-type-decl
nil numbers
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(complex type-decl
nil complex_types
nil)
(abs_def formula-decl
nil polar
nil))
shostak))
(Im_sin_abs1 0
(Im_sin_abs1-1
nil 3455862298
(
"" (skosimp)
((
"" (
expand "arg")
((
"" (typepred
"n0x!1")
((
"" (
rewrite "sin_0")
((
"" (case-replace
"Im(n0x!1) = 0")
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1" (
rewrite "atan_0")
((
"1" (
assert)
((
"1" (
rewrite "sin_0")
((
"1" (
rewrite "sin_pi")
((
"1" (lift-if) ((
"1" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2"
(lemma
"sin_atan2" (
"x" "Re(n0x!1)" "y" "Im(n0x!1)"))
((
"2" (
assert)
((
"2" (
rewrite "abs_def" -3)
((
"2"
(lemma
"sq_eq"
(
"nna" "sqrt(sq(Im(n0x!1)) + sq(Re(n0x!1)))"
"nnb" "1"))
((
"2" (flatten -1)
((
"2" (split -2)
((
"1" (hide -2 -4)
((
"1" (
rewrite "sq_sqrt")
((
"1"
(
rewrite "sq_1")
((
"1"
(lemma
"sin_period"
(
"a"
"atan2(Re(n0x!1), Im(n0x!1))"
"j"
"-1"))
((
"1"
(
replace -1 2 rl)
((
"1"
(hide -1)
((
"1"
(case-replace
"Re(n0x!1)=0")
((
"1"
(
replace -3)
((
"1"
(
assert)
((
"1"
(hide -1 -3)
((
"1"
(
case "Im(n0x!1)<0")
((
"1"
(lemma
"sq_neg"
(
"a" "Im(n0x!1)"))
((
"1"
(lemma
"sq_eq"
(
"nna"
"-Im(n0x!1)"
"nnb"
"1"))
((
"1"
(
expand
"sq"
-1
2)
((
"1"
(
assert)
nil
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(lemma
"sq_eq"
(
"nna"
"Im(n0x!1)"
"nnb"
"1"))
((
"2"
(
expand
"sq"
-1
2)
((
"2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(case-replace
"1 + sq(Im(n0x!1) / Re(n0x!1)) = sq(1/Re(n0x!1))")
((
"1"
(
rewrite "sqrt_sq_abs")
((
"1"
(hide -1)
((
"1"
(
replace -2)
((
"1"
(hide -1 -2)
((
"1"
(lemma
"real_props.abs_div"
(
"x"
"1"
"n0y"
"Re(n0x!1)"))
((
"1"
(
replace -1)
((
"1"
(hide -1)
((
"1"
(
expand
"abs")
((
"1"
(
rewrite
"div_div1")
((
"1"
(
rewrite
"div_cancel3")
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(hide 4 -2)
((
"2"
(lemma
"add_div"
(
"x"
"1"
"n0x"
"1"
"y"
"sq(Im(n0x!1))"
"n0y"
"sq(Re(n0x!1))"))
((
"1"
(
rewrite "sq_div" 1)
((
"1"
(
replace -1)
((
"1"
(
assert)
((
"1"
(
replace -2)
((
"1"
(
rewrite
"sq_div"
1)
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
expand "/=")
((
"2"
(
rewrite "sq_eq_0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (propax)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((arg const-decl
"argrng" polar
nil)
(sin_0 formula-decl
nil trig_basic
"trig/")
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(sq_eq formula-decl
nil sq
"reals/")
(>= const-decl
"bool" reals
nil)
(nonneg_real nonempty-type-eq-decl
nil real_types
nil)
(nnreal type-eq-decl
nil real_types
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sqrt const-decl
"{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(sq_sqrt formula-decl
nil sqrt
"reals/")
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(sin_period formula-decl
nil trig_basic
"trig/")
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
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)
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(sq_eq_0 formula-decl
nil sq
"reals/")
(sq_div formula-decl
nil sq
"reals/")
(posrat_div_posrat_is_posrat application-judgement
"posrat"
rationals
nil)
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(add_div formula-decl
nil real_props
nil)
(sqrt_sq_abs formula-decl
nil sqrt
"reals/")
(nonzero_abs_is_pos application-judgement
"{y: posreal | y >= x}"
real_defs
nil)
(abs_div formula-decl
nil real_props
nil)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(div_div1 formula-decl
nil real_props
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(nnint_times_nnint_is_nnint application-judgement
"nonneg_int"
integers
nil)
(div_cancel3 formula-decl
nil real_props
nil)
(abs const-decl
"{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(posreal_plus_nnreal_is_posreal application-judgement
"posreal"
real_types
nil)
(sq_nz_pos application-judgement
"posreal" sq
"reals/")
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(sq_neg formula-decl
nil sq
"reals/")
(minus_real_is_real application-judgement
"real" reals
nil)
(< const-decl
"bool" reals
nil) (sq_0 formula-decl
nil sq
"reals/")
(nzreal_times_nzreal_is_nzreal application-judgement
"nzreal"
real_types
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)
(nzint_times_nzint_is_nzint application-judgement
"nzint" integers
nil)
(sq_1 formula-decl
nil sq
"reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(sqrt_pos application-judgement
"posreal" sqrt
"reals/")
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(abs_def formula-decl
nil polar
nil)
(sin_atan2 formula-decl
nil atan2
"trig/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(sin_range application-judgement
"trig_range" trig_basic
"trig/")
(abs_nzcomplex application-judgement
"posreal" polar
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(atan_0 formula-decl
nil atan
"trig/")
(sin_pi formula-decl
nil trig_basic
"trig/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(atan2 const-decl
"real" atan2
"trig/")
(= const-decl
"[T, T -> boolean]" equalities
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
nil)
(/= const-decl
"boolean" notequal
nil)
(complex type-decl
nil complex_types
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)
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil))
shostak))
(abs_cos_arg 0
(abs_cos_arg-1
nil 3456133110
(
"" (skosimp)
((
"" (
case "z!1=0")
((
"1" (
assert)
((
"1" (flatten)
((
"1" (
expand "abs")
((
"1" (
expand "arg")
((
"1" (
expand "sq_abs")
((
"1" (
expand "sq")
((
"1" (
replace -1)
((
"1" (
replace -2) ((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (lemma
"arg_div_abs" (
"n0x" "z!1"))
((
"1" (lemma
"Re_cos_abs1" (
"n0x" "z!1 / abs(z!1)"))
((
"1" (
replace -2 * rl) ((
"1" (
assert)
nil nil))
nil)
(
"2" (
assert) ((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (
assert) ((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
((= const-decl
"bool" complex_types
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)
(complex type-decl
nil complex_types
nil)
(arg const-decl
"argrng" polar
nil)
(sq const-decl
"nonneg_real" sq
"reals/")
(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)
(nnint_plus_nnint_is_nnint application-judgement
"nonneg_int"
integers
nil)
(even_plus_even_is_even application-judgement
"even_int" integers
nil)
(sqrt_0 formula-decl
nil sqrt
"reals/")
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(sq_abs const-decl
"nnreal" complex_types
nil)
(abs const-decl
"nnreal" polar
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(cos_range application-judgement
"trig_range" trig_basic
"trig/")
(nnreal type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil)
(/ const-decl
"complex" complex_types
nil)
(nzreal nonempty-type-eq-decl
nil reals
nil)
(Re_cos_abs1 formula-decl
nil polar
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(abs_abs formula-decl
nil polar
nil)
(abs_div2 formula-decl
nil polar
nil)
(Re_div3 formula-decl
nil complex_types
nil)
(arg_div_abs formula-decl
nil polar
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(/= const-decl
"boolean" notequal
nil)
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil))
shostak))
(abs_sin_arg 0
(abs_sin_arg-1
nil 3456133318
(
"" (skosimp)
((
"" (
case "z!1=0")
((
"1" (
assert)
((
"1" (flatten)
((
"1" (
expand "arg")
((
"1" (
expand "abs")
((
"1" (
expand "sq_abs")
((
"1" (
assert)
((
"1" (
rewrite "sin_0") ((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (lemma
"arg_div_abs" (
"n0x" "z!1"))
((
"1" (lemma
"Im_sin_abs1" (
"n0x" "z!1/abs(z!1)"))
((
"1" (
replace -2 -1 rl) ((
"1" (
assert)
nil nil))
nil)
(
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert) ((
"2" (flatten) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
((= const-decl
"bool" complex_types
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)
(complex type-decl
nil complex_types
nil)
(abs const-decl
"nnreal" polar
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(nnreal_times_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(sin_0 formula-decl
nil trig_basic
"trig/")
(sq_abs const-decl
"nnreal" complex_types
nil)
(arg const-decl
"argrng" polar
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(sin_range application-judgement
"trig_range" trig_basic
"trig/")
(nnreal type-eq-decl
nil real_types
nil)
(>= const-decl
"bool" reals
nil)
(/ const-decl
"complex" complex_types
nil)
(nzreal nonempty-type-eq-decl
nil reals
nil)
(Im_sin_abs1 formula-decl
nil polar
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(abs_abs formula-decl
nil polar
nil)
(abs_div2 formula-decl
nil polar
nil)
(Im_div3 formula-decl
nil complex_types
nil)
(arg_div_abs formula-decl
nil polar
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(/= const-decl
"boolean" notequal
nil)
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil))
shostak))
(arg_nnreal 0
(arg_nnreal-1
nil 3455859070
(
"" (skosimp)
((
"" (
rewrite "arg_is_0") ((
"" (
assert)
nil nil))
nil))
nil)
((arg_is_0 formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil))
shostak))
(arg_nreal 0
(arg_nreal-1
nil 3455859044
(
"" (skosimp)
((
"" (
rewrite "arg_is_pi") ((
"" (
assert)
nil nil))
nil))
nil)
((arg_is_pi formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil))
shostak))
(arg_i 0
(arg_i-1
nil 3455858988
(
"" (
rewrite "arg_is_pi2")
((
"" (
expand "complex_i")
((
"" (
expand "Re")
((
"" (
expand "Im") ((
"" (
assert)
nil nil))
nil))
nil))
nil))
nil)
((complex_i const-decl
"nzcomplex" complex_types
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(Re const-decl
"real" complex_types
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
"boolean" notequal
nil)
(number nonempty-type-decl
nil numbers
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(complex type-decl
nil complex_types
nil)
(arg_is_pi2 formula-decl
nil polar
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(Re_i formula-decl
nil complex_types
nil)
(Im_i formula-decl
nil complex_types
nil))
shostak))
(arg_neg 0
(arg_neg-1
nil 3455863741
(
"" (skosimp)
((
"" (
expand "arg")
((
"" (
assert)
((
"" (lemma
"trichotomy" (
"x" "Re(n0x!1)"))
((
"" (split)
((
"1" (lemma
"trichotomy" (
"x" "Im(n0x!1)"))
((
"1" (split)
((
"1" (
assert)
((
"1"
(lemma
"atan2_cancel_neg"
(
"x" "Re(n0x!1)" "y" "Im(n0x!1)" "nz" "-1"))
((
"1" (
assert)
((
"1" (
replace -1 1)
((
"1" (
assert)
((
"1" (lift-if)
((
"1" (
assert)
((
"1"
(prop)
((
"1"
(lemma
"atan_strict_increasing")
((
"1"
(
expand "strict_increasing?")
((
"1"
(
expand "atan2")
((
"1"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"Re(n0x!1)"
"y"
"Im(n0x!1)"
"x"
"0"))
((
"1"
(
assert)
((
"1"
(inst
-
"0"
"Im(n0x!1) / Re(n0x!1)")
((
"1"
(
rewrite "atan_0")
((
"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" (
expand "atan2")
((
"2" (
rewrite "atan_0") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"3" (
assert)
((
"3" (
expand "atan2")
((
"3" (
assert)
((
"3" (lift-if)
((
"3" (
assert)
((
"3" (prop)
((
"3" (lemma
"atan_strict_increasing")
((
"3"
(
expand "strict_increasing?")
((
"3"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"Re(n0x!1)"
"x"
"Im(n0x!1)"
"y"
"0"))
((
"3"
(inst
-
"Im(n0x!1) / Re(n0x!1)"
"0")
((
"3"
(
rewrite "atan_0")
((
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
replace -1)
((
"2" (
assert)
((
"2" (typepred
"n0x!1")
((
"2" (
assert)
((
"2" (
assert)
((
"2" (
expand "atan2")
((
"2" (
assert) ((
"2" (grind)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"3" (
assert)
((
"3" (lemma
"trichotomy" (
"x" "Im(n0x!1)"))
((
"3" (split)
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1" (lift-if)
((
"1" (
assert)
((
"1"
(typepred
"atan(Im(n0x!1) / Re(n0x!1))")
((
"1" (
expand "abs")
((
"1"
(case-replace
"atan(Im(n0x!1) / Re(n0x!1)) < 0")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
replace -1)
((
"2" (
expand "atan2")
((
"2" (
rewrite "atan_0")
((
"2" (
assert)
((
"2" (lift-if) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"3" (
assert)
((
"3" (
expand "atan2")
((
"3" (lift-if)
((
"3" (
assert)
((
"3"
(typepred
"atan(Im(n0x!1) / Re(n0x!1))")
((
"3" (
expand "abs")
((
"3"
(case-replace
"atan(Im(n0x!1) / Re(n0x!1)) < 0")
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((arg const-decl
"argrng" polar
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(/= const-decl
"boolean" notequal
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(Re const-decl
"real" complex_types
nil)
(complex type-decl
nil complex_types
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)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(pi_lb const-decl
"posreal" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(real_abs_lt_pi2 nonempty-type-eq-decl
nil atan
"trig/")
(atan const-decl
"real_abs_lt_pi2" atan
"trig/")
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(minus_even_is_even application-judgement
"even_int" integers
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/")
(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)
(nnreal_plus_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(atan_strict_increasing formula-decl
nil atan
"trig/")
(atan2 const-decl
"real" atan2
"trig/")
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(atan_0 formula-decl
nil atan
"trig/")
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(
AND const-decl
"[bool, bool -> bool]" booleans
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
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)
(both_sides_div_pos_lt1 formula-decl
nil real_props
nil)
(strict_increasing? const-decl
"bool" real_fun_preds
"reals/")
(- const-decl
"[numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl
nil number_fields
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)
(atan2_cancel_neg formula-decl
nil atan2
"trig/")
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(Im_neg1 formula-decl
nil complex_types
nil)
(Re_neg1 formula-decl
nil complex_types
nil)
(neg_nzcomplex application-judgement
"nzcomplex" complex_types
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil))
shostak))
(arg_conjugate 0
(arg_conjugate-1
nil 3456035972
(
"" (skosimp)
((
"" (case-replace
"arg(z!1) = 0")
((
"1" (
rewrite "arg_is_0")
((
"1" (
rewrite "arg_is_0")
((
"1" (flatten) ((
"1" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (case-replace
"arg(z!1) = pi")
((
"1" (
rewrite "arg_is_pi")
((
"1" (flatten)
((
"1" (
rewrite "arg_is_pi") ((
"1" (
assert)
nil nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (typepred
"arg(z!1)")
((
"2" (
case "arg(z!1)<0")
((
"1" (lemma
"arg_lt_0" (
"z" "z!1"))
((
"1" (
assert)
((
"1" (hide-all-but (-1 3))
((
"1" (
expand "arg")
((
"1" (
expand "atan2")
((
"1" (
assert)
((
"1" (lemma
"trichotomy" (
"x" "Re(z!1)"))
((
"1" (split)
((
"1"
(
assert)
((
"1"
(lemma
"atan_neg"
(
"x" "Im(z!1) / Re(z!1)"))
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
nil nil)
(
"3"
(
assert)
((
"3"
(lemma
"atan_neg"
(
"x" "Im(z!1) / Re(z!1)"))
((
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (lemma
"arg_p_lt_pi" (
"z" "z!1"))
((
"2" (
assert)
((
"2" (hide-all-but (-1 4))
((
"2" (
expand "arg")
((
"2" (
expand "atan2")
((
"2" (
assert)
((
"2" (lemma
"trichotomy" (
"x" "Re(z!1)"))
((
"2" (split)
((
"1"
(
assert)
((
"1"
(lemma
"atan_neg"
(
"x" "Im(z!1) / Re(z!1)"))
((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (
assert)
nil nil)
(
"3"
(lemma
"atan_neg"
(
"x" "Im(z!1) / Re(z!1)"))
((
"1" (
assert)
nil nil)
(
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl
nil numbers
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(complex type-decl
nil complex_types
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
"[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_lb const-decl
"posreal" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(<= const-decl
"bool" reals
nil)
(argrng nonempty-type-eq-decl
nil polar
nil)
(arg const-decl
"argrng" polar
nil)
(conjugate const-decl
"complex" complex_types
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(Re_conjugate formula-decl
nil complex_types
nil)
(Im_conjugate formula-decl
nil complex_types
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(arg_is_0 formula-decl
nil polar
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
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_minus_real_is_real application-judgement
"real" reals
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(atan_neg formula-decl
nil atan
"trig/")
(/= const-decl
"boolean" notequal
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(Im const-decl
"real" complex_types
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(Re const-decl
"real" complex_types
nil)
(trichotomy formula-decl
nil real_axioms
nil)
(atan2 const-decl
"real" atan2
"trig/")
(arg_lt_0 formula-decl
nil polar
nil)
(arg_p_lt_pi formula-decl
nil polar
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(arg_is_pi formula-decl
nil polar
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil))
shostak))
(arg_mult 0
(arg_mult-1
nil 3455875477
(
""
(
case "FORALL (n0x, n0y: nzcomplex):
arg(n0x * n0y) =arg(n0y * n0x)
")
((
"1"
(
case "FORALL (n0x, n0y: nzcomplex):arg(n0x)=0 =>
arg(n0x * n0y) =
LET r = arg(n0x) + arg(n0y) IN
IF r > pi THEN r - 2 * pi
ELSIF r <= -pi THEN r + 2 * pi
ELSE r
ENDIF
")
((
"1"
(
case "FORALL (n0x, n0y: nzcomplex):
arg(n0x) = pi =>
arg(n0x * n0y) =
LET r = arg(n0x) + arg(n0y) IN
IF r > pi THEN r - 2 * pi
ELSIF r <= -pi THEN r + 2 * pi
ELSE r
ENDIF
")
((
"1"
(
case "FORALL (n0x, n0y: nzcomplex):
0<arg(n0x) & arg(n0x)< pi =>
arg(n0x * n0y) =
LET r = arg(n0x) + arg(n0y) IN
IF r > pi THEN r - 2 * pi
ELSIF r <= -pi THEN r + 2 * pi
ELSE r
ENDIF
")
((
"1" (skosimp)
((
"1" (lemma
"trichotomy" (
"x" "arg(n0x!1)"))
((
"1" (split)
((
"1" (typepred
"arg(n0x!1)")
((
"1" (
expand "<=" -2)
((
"1" (split)
((
"1" (inst -4
"n0x!1" "n0y!1")
((
"1" (
assert) ((
"1" (
assert)
nil nil))
nil))
nil)
(
"2" (inst -5
"n0x!1" "n0y!1")
((
"2" (
assert) ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (inst -4
"n0x!1" "n0y!1")
((
"2" (
assert) ((
"2" (
assert)
nil nil))
nil))
nil)
(
"3" (typepred
"arg(n0x!1)")
((
"3" (hide -2)
((
"3" (lemma
"arg_neg" (
"n0x" "n0x!1"))
((
"3" (
assert)
((
"3" (inst -4
"-n0x!1" "n0y!1")
((
"3" (
assert)
((
"3" (
replace -1)
((
"3"
(
assert)
((
"3"
(lemma
"arg_neg"
(
"n0x" "n0x!1*n0y!1"))
((
"3"
(
expand "*" -1 1)
((
"3"
(
expand "*" -5 1)
((
"3"
(
expand "-" -1 1)
((
"3"
(
assert)
((
"3"
(
replace -1 -5)
((
"3"
(hide -1)
((
"3"
(lift-if -4)
((
"3"
(lift-if -4)
((
"3"
(
assert)
((
"3"
(lift-if 1)
((
"3"
(
case
"arg(n0x!1) + arg(n0y!1) <= -pi")
((
"1"
(
assert)
((
"1"
(prop)
((
"1"
(
assert)
nil
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(
replace
2
-4)
((
"2"
(
assert)
((
"2"
(ground)
((
"2"
(lift-if)
((
"2"
(ground)
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" (hide 2)
((
"2"
(
case "FORALL (n0x, n0y: nzcomplex):
0 < arg(n0x) & arg(n0x) < pi & -pi < arg(n0y) & arg(n0y)<0=>
arg(n0x * n0y) =
LET r = arg(n0x) + arg(n0y) IN
IF r > pi THEN r - 2 * pi
ELSIF r <= -pi THEN r + 2 * pi
ELSE r
ENDIF
")
((
"1" (skosimp)
((
"1" (lemma
"trichotomy" (
"x" "arg(n0y!1)"))
((
"1" (split)
((
"1" (typepred
"arg(n0y!1)")
((
"1" (
expand "<=" -2)
((
"1" (split)
((
"1" (hide -2)
((
"1" (lemma
"arg_neg" (
"n0x" "n0y!1"))
((
"1"
(
assert)
((
"1"
(inst -4
"n0x!1" "-n0y!1")
((
"1"
(
assert)
((
"1"
(lemma
"arg_neg"
(
"n0x" "n0x!1 * n0y!1"))
((
"1"
(
expand "-" -1 1)
((
"1"
(
expand "-" -5 1)
((
"1"
(
expand "*" -5 1)
((
"1"
(
expand "*" -1 1)
((
"1"
(
assert)
((
"1"
(
assert)
((
"1"
(
replace -1 -5)
((
"1"
(
replace -2 -5)
((
"1"
(
assert)
((
"1"
(lift-if -5)
((
"1"
(
assert)
((
"1"
(lift-if
1)
((
"1"
(case-replace
"0 < arg(n0x!1 * n0y!1)")
((
"1"
(
assert)
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)
(
"2" (inst -9
"n0x!1" "n0y!1")
((
"2" (inst -7
"n0y!1" "n0x!1")
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (inst -7
"n0x!1" "n0y!1")
((
"2" (inst -6
"n0y!1" "n0x!1")
((
"2" (
assert)
nil nil))
nil))
nil)
(
"3" (inst -2
"n0x!1" "n0y!1")
((
"3" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2" (hide-all-but 1)
((
"2" (skosimp)
((
"2" (
assert)
((
"2" (lemma
"arg_lt_0" (
"z" "n0y!1"))
((
"2" (
assert)
((
"2" (lemma
"arg_p_lt_pi" (
"z" "n0x!1"))
((
"2" (
assert)
((
"2" (hide -3 -4 -5 -6)
((
"2"
(
expand "arg")
((
"2"
(
expand "atan2")
((
"2"
(
assert)
((
"2"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Im(n0x!1)"
"x"
"Im(n0y!1)"
"y"
"0"))
((
"2"
(
assert)
((
"2"
(case-replace
"Re(n0x!1)=0")
((
"1"
(
assert)
((
"1"
(case-replace
"(Im(n0x!1) * Re(n0y!1) / (-1 * (Im(n0x!1) * Im(n0y!1))))=-(Re(n0y!1)/Im(n0y!1))")
((
"1"
(
rewrite "atan_neg")
((
"1"
(hide -1)
((
"1"
(lemma
"trichotomy"
(
"x" "Re(n0y!1)"))
((
"1"
(split)
((
"1"
(lemma
"both_sides_div_neg_lt1"
(
"nz"
"Im(n0y!1)"
"x"
"Re(n0y!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(lemma
"atan_inv_neg"
(
"nx"
"Re(n0y!1) / Im(n0y!1)"))
((
"1"
(
rewrite
"div_div1")
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(
assert)
((
"2"
(
replace
-1)
((
"2"
(
rewrite
"atan_0")
((
"2"
(
assert)
nil
nil))
nil))
nil))
nil))
nil)
(
"3"
(lemma
"negreal_div_negreal_is_posreal"
(
"nx"
"Re(n0y!1)"
"ny"
"Im(n0y!1)"))
((
"1"
(lemma
"atan_inv"
(
"px"
"Re(n0y!1) / Im(n0y!1)"))
((
"1"
(
rewrite
"div_div1")
((
"1"
(
assert)
nil
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(case-replace
"Re(n0y!1)=0")
((
"1"
(
assert)
((
"1"
(case-replace
"(Re(n0x!1) * Im(n0y!1) / (-1 * (Im(n0x!1) * Im(n0y!1))))=-(Re(n0x!1)/Im(n0x!1))")
((
"1"
(hide -1)
((
"1"
(
rewrite
"atan_neg")
((
"1"
(lemma
"trichotomy"
(
"x"
"Re(n0x!1)"))
((
"1"
(split)
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"Re(n0x!1)"
"py"
"Im(n0x!1)"))
((
"1"
(lemma
"atan_inv"
(
"px"
"Re(n0x!1) / Im(n0x!1)"))
((
"1"
(
rewrite
"div_div1")
((
"1"
(
assert)
nil
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil)
(
"2"
(propax)
nil
nil)
(
"3"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"Im(n0x!1)"
"x"
"Re(n0x!1)"
"y"
"0"))
((
"3"
(
assert)
((
"3"
(lemma
"atan_inv_neg"
(
"nx"
"Re(n0x!1) / Im(n0x!1)"))
((
"3"
(
rewrite
"div_div1")
((
"3"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(lemma
"trichotomy"
(
"x" "Re(n0x!1)"))
((
"2"
(split)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0x!1)"
"x"
"Im(n0y!1)"
"y"
"0"))
((
"1"
(
rewrite
"zero_times1")
((
"1"
(
assert)
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"Im(n0x!1)"
"py"
"Re(n0x!1)"))
((
"1"
(lemma
"trichotomy"
(
"x"
"Re(n0y!1)"))
((
"1"
(split)
((
"1"
(hide
1
2)
((
"1"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"Re(n0y!1)"
"x"
"Im(n0y!1)"
"y"
"0"))
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0y!1)"
"y"
"Im(n0x!1)"
"x"
"0"))
((
"1"
(
assert)
((
"1"
(
rewrite
"zero_times1")
((
"1"
(lemma
"posreal_times_posreal_is_posreal"
(
"px"
"Re(n0x!1)"
"py"
"Re(n0y!1)"))
((
"1"
(
assert)
((
"1"
(lemma
"atan_plus"
(
"x"
"Im(n0x!1) / Re(n0x!1)"
"y"
"Im(n0y!1) / Re(n0y!1)"))
((
"1"
(flatten)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Im(n0x!1) / Re(n0x!1)"
"x"
"Im(n0y!1) / Re(n0y!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(
replace
-2)
((
"1"
(
rewrite
"add_div")
((
"1"
(
rewrite
"div_times")
((
"1"
(lemma
"div_distributes_minus"
(
"x"
"Re(n0y!1) * Re(n0x!1)"
"n0z"
"Re(n0y!1) * Re(n0x!1)"
"y"
"Im(n0y!1) * Im(n0x!1)"))
((
"1"
(
rewrite
"div_simp")
((
"1"
(
replace
-1)
((
"1"
(
rewrite
"div_div1")
((
"1"
(
rewrite
"div_cancel2")
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil))
nil)
(
"2"
(propax)
nil
nil)
(
"3"
(lemma
"both_sides_div_neg_lt1"
(
"nz"
"Re(n0y!1)"
"y"
"Im(n0y!1)"
"x"
"0"))
((
"1"
(
assert)
((
"1"
(lemma
"both_sides_times_neg_lt1"
(
"nz"
"Re(n0y!1)"
"x"
"Im(n0x!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(lemma
"both_sides_times_neg_lt1"
(
"nz"
"Re(n0y!1)"
"x"
"Re(n0x!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(hide
1
2)
((
"1"
(
rewrite
"zero_times1")
((
"1"
(lemma
"atan_plus"
(
"x"
"Im(n0x!1) / Re(n0x!1)"
"y"
"Im(n0y!1) / Re(n0y!1)"))
((
"1"
(flatten)
((
"1"
(
assert)
((
"1"
(hide
-3)
((
"1"
(lemma
"trich_lt"
(
"x"
"Re(n0x!1) * Re(n0y!1)"
"y"
"Im(n0x!1) * Im(n0y!1)"))
((
"1"
(
rewrite
"div_times"
-2)
((
"1"
(split)
((
"1"
(
rewrite
"div_mult_neg_lt1"
-2)
((
"1"
(hide
-3)
((
"1"
(
assert)
((
"1"
(
replace
-2)
((
"1"
(hide
-2)
((
"1"
(lemma
"div_distributes_minus"
(
"x"
"Re(n0x!1) * Re(n0y!1)"
"n0z"
"Re(n0x!1) * Re(n0y!1)"
"y"
"Im(n0x!1) * Im(n0y!1)"))
((
"1"
(
rewrite
"div_simp")
((
"1"
(
replace
-1)
((
"1"
(
rewrite
"add_div")
((
"1"
(
rewrite
"div_div1")
((
"1"
(
rewrite
"div_cancel2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(hide
-2
-3)
((
"2"
(lemma
"cross_mult"
(
"x"
"Re(n0x!1)"
"n0x"
"Im(n0x!1)"
"y"
"Im(n0y!1)"
"n0y"
"Re(n0y!1)"))
((
"2"
(
assert)
((
"2"
(lemma
"atan_inv"
(
"px"
"Re(n0x!1) / Im(n0x!1)"))
((
"1"
(
rewrite
"div_div1")
((
"1"
(
replace
-2)
((
"1"
(
assert)
nil
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(
replace
-1)
((
"2"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"3"
(
rewrite
"div_mult_neg_lt2"
-3)
((
"3"
(
assert)
((
"3"
(hide
-2)
((
"3"
(
replace
-2
1)
((
"3"
(lemma
"div_distributes_minus"
(
"x"
"Re(n0x!1) * Re(n0y!1)"
"n0z"
"Re(n0x!1) * Re(n0y!1)"
"y"
"Im(n0x!1) * Im(n0y!1)"))
((
"3"
(
rewrite
"div_simp")
((
"3"
(
replace
-1)
((
"3"
(
rewrite
"add_div")
((
"3"
(
rewrite
"div_div1")
((
"3"
(
rewrite
"div_cancel2")
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)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil)
(
"2"
(propax)
nil
nil)
(
"3"
(lemma
"both_sides_div_neg_lt1"
(
"x"
"Im(n0x!1)"
"y"
"0"
"nz"
"Re(n0x!1)"))
((
"1"
(
assert)
((
"1"
(lemma
"both_sides_times_neg_lt1"
(
"y"
"Im(n0y!1)"
"x"
"0"
"nz"
"Re(n0x!1)"))
((
"1"
(
assert)
((
"1"
(
rewrite
"zero_times1")
((
"1"
(lemma
"trichotomy"
(
"x"
"Re(n0y!1)"))
((
"1"
(split)
((
"1"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"Re(n0y!1)"
"x"
"Im(n0y!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0y!1)"
"y"
"Im(n0x!1)"
"x"
"0"))
((
"1"
(
rewrite
"zero_times1")
((
"1"
(
assert)
((
"1"
(hide
1
2)
((
"1"
(lemma
"atan_plus"
(
"x"
"Im(n0x!1) / Re(n0x!1)"
"y"
"Im(n0y!1) / Re(n0y!1)"))
((
"1"
(flatten)
((
"1"
(
assert)
((
"1"
(hide
-2)
((
"1"
(lemma
"trich_lt"
(
"x"
"Re(n0x!1) * Re(n0y!1)"
"y"
"Im(n0x!1) * Im(n0y!1)"))
((
"1"
(
rewrite
"div_times"
-2)
((
"1"
(split)
((
"1"
(
rewrite
"div_mult_neg_lt1"
-2)
((
"1"
(
assert)
((
"1"
(hide
1)
((
"1"
(
replace
-2)
((
"1"
(lemma
"div_distributes_minus"
(
"x"
"Re(n0x!1) * Re(n0y!1)"
"n0z"
"Re(n0x!1) * Re(n0y!1)"
"y"
"Im(n0x!1) * Im(n0y!1)"))
((
"1"
(
rewrite
"div_simp")
((
"1"
(
replace
-1)
((
"1"
(
rewrite
"add_div")
((
"1"
(
rewrite
"div_div1")
((
"1"
(
rewrite
"div_cancel2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(hide
-2
-3)
((
"2"
(lemma
"cross_mult"
(
"x"
"Re(n0x!1)"
"n0x"
"Im(n0x!1)"
"y"
"Im(n0y!1)"
"n0y"
"Re(n0y!1)"))
((
"2"
(
assert)
((
"2"
(lemma
"atan_inv_neg"
(
"nx"
"Im(n0x!1) / Re(n0x!1)"))
((
"2"
(
rewrite
"div_div1")
((
"2"
(
replace
-2)
((
"2"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"3"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0y!1)"
"x"
"Re(n0x!1)"
"y"
"0"))
((
"3"
(
assert)
((
"3"
(
rewrite
"div_mult_neg_lt2"
-4)
((
"3"
(
assert)
((
"3"
(hide
1)
((
"3"
(
replace
-3)
((
"3"
(lemma
"div_distributes_minus"
(
"x"
"Re(n0x!1) * Re(n0y!1)"
"n0z"
"Re(n0x!1) * Re(n0y!1)"
"y"
"Im(n0x!1) * Im(n0y!1)"))
((
"3"
(
rewrite
"div_simp")
((
"3"
(
replace
-1)
((
"3"
(
rewrite
"add_div")
((
"3"
(
rewrite
"div_div1")
((
"3"
(
rewrite
"div_cancel2")
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)
nil
nil))
nil)
(
"2"
(propax)
nil
nil)
(
"3"
(lemma
"both_sides_div_neg_lt1"
(
"nz"
"Re(n0y!1)"
"y"
"Im(n0y!1)"
"x"
"0"))
((
"1"
(
assert)
((
"1"
(lemma
"both_sides_times_neg_lt1"
(
"nz"
"Re(n0y!1)"
"x"
"Im(n0x!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(lemma
"negreal_times_negreal_is_posreal"
(
"nx"
"Re(n0x!1)"
"ny"
"Re(n0y!1)"))
((
"1"
(
assert)
((
"1"
(lemma
"atan_plus"
(
"x"
"Im(n0x!1) / Re(n0x!1)"
"y"
"Im(n0y!1) / Re(n0y!1)"))
((
"1"
(flatten)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Im(n0y!1) / Re(n0y!1)"
"x"
"Im(n0x!1) / Re(n0x!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(
replace
-2)
((
"1"
(
rewrite
"div_times")
((
"1"
(lemma
"div_distributes_minus"
(
"x"
"Re(n0x!1) * Re(n0y!1)"
"n0z"
"Re(n0x!1) * Re(n0y!1)"
"y"
"Im(n0x!1) * Im(n0y!1)"))
((
"1"
(
rewrite
"div_simp")
((
"1"
(
replace
-1)
((
"1"
(lemma
"add_div"
(
"x"
"Im(n0x!1)"
"n0x"
"Re(n0x!1)"
"y"
"Im(n0y!1)"
"n0y"
"Re(n0y!1)"))
((
"1"
(
replace
-1)
((
"1"
(
rewrite
"div_div1")
((
"1"
(
rewrite
"div_cancel2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
nil
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))
nil))
nil))
nil))
nil))
nil)
(
"2" (hide 2)
((
"2" (skosimp)
((
"2" (
replace -1)
((
"2" (
assert)
((
"2" (typepred
"arg(n0y!1)")
((
"2" (
assert)
((
"2" (hide -1 -2)
((
"2" (
rewrite "arg_is_pi")
((
"2" (flatten)
((
"2" (hide -3)
((
"2" (hide -3)
((
"2"
(
expand "arg")
((
"2"
(
expand "atan2")
((
"2"
(
assert)
((
"2"
(
replace -2)
((
"2"
(
assert)
((
"2"
(lemma
"trichotomy"
(
"x" "Re(n0y!1)"))
((
"2"
(split -1)
((
"1"
(
assert)
((
"1"
(lemma
"trichotomy"
(
"x" "Im(n0y!1)"))
((
"1"
(split)
((
"1"
(
assert)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0y!1)"
"x"
"Re(n0x!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Im(n0y!1)"
"x"
"Re(n0x!1)"
"y"
"0"))
((
"1"
(
assert)
((
"1"
(lift-if)
((
"1"
(
assert)
((
"1"
(lemma
"atan_strict_increasing")
((
"1"
(
expand
"strict_increasing?")
((
"1"
(inst
-
"0"
"Im(n0y!1) / Re(n0y!1)")
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"Im(n0y!1)"
"py"
"Re(n0y!1)"))
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
replace -1)
((
"2"
(
assert)
((
"2"
(
assert)
((
"2"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0y!1)"
"x"
"Re(n0x!1)"
"y"
"0"))
((
"2"
(
assert)
nil
nil))
nil))
nil))
nil))
nil)
(
"3"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0y!1)"
"x"
"Re(n0x!1)"
"y"
"0"))
((
"3"
(
assert)
((
"3"
(lemma
"negreal_times_negreal_is_posreal"
(
"nx"
"Im(n0y!1)"
"ny"
"Re(n0x!1)"))
((
"3"
(
assert)
((
"3"
(lift-if)
((
"3"
(
assert)
((
"3"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"Re(n0y!1)"
"x"
"Im(n0y!1)"
"y"
"0"))
((
"3"
(lemma
"atan_strict_increasing")
((
"3"
(
expand
"strict_increasing?")
((
"3"
(inst
-
"Im(n0y!1) / Re(n0y!1)"
"0")
((
"3"
(
rewrite
"atan_0")
((
"3"
(
assert)
((
"3"
(split)
((
"1"
(
assert)
nil
nil)
(
"2"
(
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" "Im(n0y!1)"))
((
"2"
(split)
((
"1"
(
assert)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Im(n0y!1)"
"x"
"Re(n0x!1)"
"y"
"0"))
((
"1"
(
assert)
nil
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(typepred
"n0y!1")
((
"2"
(
assert)
nil
nil))
nil))
nil)
(
"3"
(
assert)
((
"3"
(lemma
"negreal_times_negreal_is_posreal"
(
"nx"
"Im(n0y!1)"
"ny"
"Re(n0x!1)"))
((
"3"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"3"
(lemma
"negreal_times_negreal_is_posreal"
(
"nx"
"Re(n0y!1)"
"ny"
"Re(n0x!1)"))
((
"1"
(
assert)
((
"1"
(lift-if)
((
"1"
(
assert)
((
"1"
(lift-if)
((
"1"
(
assert)
((
"1"
(lemma
"trichotomy"
(
"x"
"Im(n0y!1)"))
((
"1"
(split)
((
"1"
(
assert)
((
"1"
(typepred
"atan(Im(n0y!1) / Re(n0y!1))")
((
"1"
(lemma
"atan_strict_increasing")
((
"1"
(
expand
"strict_increasing?")
((
"1"
(lemma
"both_sides_div_neg_lt1"
(
"nz"
"Re(n0y!1)"
"x"
"Im(n0y!1)"
"y"
"0"))
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
replace
-1)
((
"2"
(
assert)
nil
nil))
nil)
(
"3"
(
assert)
((
"3"
(lemma
"negreal_div_negreal_is_posreal"
(
"nx"
"Im(n0y!1)"
"ny"
"Re(n0y!1)"))
((
"3"
(
assert)
nil
nil))
nil))
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))
nil))
nil)
(
"2" (hide 2 -1)
((
"2" (skosimp)
((
"2" (
replace -1)
((
"2" (
rewrite "arg_is_0_nz")
((
"2" (flatten)
((
"2" (
assert)
((
"2" (typepred
"arg(n0y!1)")
((
"2" (
assert)
((
"2" (hide -1 -2)
((
"2" (
expand "arg")
((
"2" (
assert)
((
"2" (
expand "atan2")
((
"2"
(
replace -2)
((
"2"
(
assert)
((
"2"
(typepred
"n0y!1")
((
"2"
(lemma
"trichotomy"
(
"x" "Re(n0y!1)"))
((
"2"
(split)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0x!1)"
"x"
"0"
"y"
"Re(n0y!1)"))
((
"1" (
assert)
nil nil))
nil)
(
"2"
(
assert)
((
"2"
(lemma
"trichotomy"
(
"x" "Im(n0y!1)"))
((
"2"
(split)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0x!1)"
"x"
"0"
"y"
"Im(n0y!1)"))
((
"1"
(
assert)
nil
nil))
nil)
(
"2" (
assert)
nil nil)
(
"3"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0x!1)"
"y"
"0"
"x"
"Im(n0y!1)"))
((
"3"
(
assert)
nil
nil))
nil))
nil))
nil))
nil)
(
"3"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0x!1)"
"y"
"0"
"x"
"Re(n0y!1)"))
((
"3"
(
assert)
((
"3"
(lemma
"trichotomy"
(
"x" "Im(n0y!1)"))
((
"3"
(split)
((
"1"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0x!1)"
"x"
"0"
"y"
"Im(n0y!1)"))
((
"1"
(
assert)
nil
nil))
nil)
(
"2" (
assert)
nil nil)
(
"3"
(lemma
"both_sides_times_pos_lt1"
(
"pz"
"Re(n0x!1)"
"y"
"0"
"x"
"Im(n0y!1)"))
((
"3"
(
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)
(
"2" (hide 2)
((
"2" (skosimp) ((
"2" (
expand "*") ((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil)
((+ const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(- const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(
IF const-decl
"[boolean, T, T -> T]" if_def
nil)
(IMPLIES const-decl
"[bool, bool -> bool]" booleans
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(real_plus_real_is_real application-judgement
"real" reals
nil)
(atan const-decl
"real_abs_lt_pi2" atan
"trig/")
(real_abs_lt_pi2 nonempty-type-eq-decl
nil atan
"trig/")
(atan_strict_increasing formula-decl
nil atan
"trig/")
(strict_increasing? const-decl
"bool" real_fun_preds
"reals/")
(arg_is_pi formula-decl
nil polar
nil)
(trichotomy formula-decl
nil real_axioms
nil)
(arg_neg formula-decl
nil polar
nil)
(- const-decl
"complex" complex_types
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)
(minus_real_is_real application-judgement
"real" reals
nil)
(Re_rew formula-decl
nil complex_types
nil)
(Im_rew formula-decl
nil complex_types
nil)
(Re_neg1 formula-decl
nil complex_types
nil)
(Im_neg1 formula-decl
nil complex_types
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(neg_nzcomplex application-judgement
"nzcomplex" complex_types
nil)
(real_le_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(mul_nzcomplex1 application-judgement
"nzcomplex" complex_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)
(Im_mul1 formula-decl
nil complex_types
nil)
(arg_lt_0 formula-decl
nil polar
nil)
(arg_p_lt_pi formula-decl
nil polar
nil)
(atan2 const-decl
"real" atan2
"trig/")
(both_sides_times_pos_lt1 formula-decl
nil real_props
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(div_div1 formula-decl
nil real_props
nil)
(nzreal_div_nzreal_is_nzreal application-judgement
"nzreal"
real_types
nil)
(atan_inv_neg formula-decl
nil atan
"trig/")
(negreal nonempty-type-eq-decl
nil real_types
nil)
(nonpos_real nonempty-type-eq-decl
nil real_types
nil)
(both_sides_div_neg_lt1 formula-decl
nil real_props
nil)
(atan_0 formula-decl
nil atan
"trig/")
(posreal_plus_nnreal_is_posreal application-judgement
"posreal"
real_types
nil)
(atan_inv formula-decl
nil atan
"trig/")
(negreal_div_negreal_is_posreal judgement-tcc
nil real_types
nil)
(atan_neg formula-decl
nil atan
"trig/")
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(posreal_div_posreal_is_posreal judgement-tcc
nil real_types
nil)
(both_sides_div_pos_lt1 formula-decl
nil real_props
nil)
(negreal_times_negreal_is_posreal judgement-tcc
nil real_types
nil)
(both_sides_times_neg_lt1 formula-decl
nil real_props
nil)
(trich_lt formula-decl
nil real_props
nil)
(div_mult_neg_lt1 formula-decl
nil real_props
nil)
(cross_mult formula-decl
nil real_props
nil)
(div_mult_neg_lt2 formula-decl
nil real_props
nil)
(add_div formula-decl
nil real_props
nil)
(div_distributes_minus formula-decl
nil real_props
nil)
(div_cancel2 formula-decl
nil real_props
nil)
(div_simp formula-decl
nil real_props
nil)
(div_times formula-decl
nil real_props
nil)
(atan_plus formula-decl
nil atan
"trig/")
(posreal_times_posreal_is_posreal judgement-tcc
nil real_types
nil)
(zero_times1 formula-decl
nil real_props
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(Re_mul1 formula-decl
nil complex_types
nil)
(arg_is_0_nz formula-decl
nil polar
nil)
(complex type-decl
nil complex_types
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(bool nonempty-type-eq-decl
nil booleans
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(number nonempty-type-decl
nil numbers
nil)
(/= const-decl
"boolean" notequal
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)
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(= const-decl
"[T, T -> boolean]" equalities
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
"[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_lb const-decl
"posreal" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(<= const-decl
"bool" reals
nil)
(argrng nonempty-type-eq-decl
nil polar
nil)
(arg const-decl
"argrng" polar
nil)
(* const-decl
"complex" complex_types
nil))
shostak))
(arg_inv 0
(arg_inv-1
nil 3455876354
(
"" (skosimp)
((
"" (case-replace
"arg(n0z!1)=0")
((
"1" (
rewrite "arg_is_0")
((
"1" (flatten)
((
"1" (
assert)
((
"1" (
expand "arg")
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1" (typepred
"n0z!1")
((
"1" (
assert)
((
"1" (lemma
"nz_sq_abs_pos" (
"n0z" "n0z!1"))
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px" "Re(n0z!1)" "py" "sq_abs(n0z!1)"))
((
"1" (
assert)
((
"1" (
rewrite "div_div1")
((
"1"
(
rewrite "div_cancel2")
((
"1"
(
replace -5)
((
"1"
(
assert)
((
"1" (
rewrite "atan_0")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (case-replace
"arg(n0z!1) = pi")
((
"1" (
rewrite "arg_is_pi")
((
"1" (flatten)
((
"1" (
assert)
((
"1" (lemma
"nz_sq_abs_pos" (
"n0z" "n0z!1"))
((
"1" (
expand "arg")
((
"1" (
assert)
((
"1" (
expand "atan2")
((
"1"
(lemma
"both_sides_div_pos_lt1"
(
"pz" "sq_abs(n0z!1)" "x" "Re(n0z!1)" "y"
"0"))
((
"1" (
assert)
((
"1" (
expand "sq_abs")
((
"1" (
replace -4)
((
"1"
(
rewrite "sq_0")
((
"1"
(hide -1)
((
"1" (
rewrite "atan_0")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (typepred
"n0z!1")
((
"2" (
assert)
((
"2" (
expand "arg")
((
"2" (
assert)
((
"2" (case-replace
"Re(n0z!1) = 0")
((
"1" (
assert)
((
"1" (case-replace
"Im(n0z!1) < 0")
((
"1" (
expand "atan2")
((
"1" (
assert)
((
"1" (
assert)
((
"1"
(lift-if 3)
((
"1"
(
assert)
((
"1"
(prop)
((
"1"
(lemma
"nz_sq_abs_pos"
(
"n0z" "n0z!1"))
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"-1*Im(n0z!1)"
"py"
"sq_abs(n0z!1)"))
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (
expand "atan2")
((
"2" (lift-if 4)
((
"2"
(
assert)
((
"2"
(prop)
((
"2"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"Im(n0z!1)"
"py"
"sq_abs(n0z!1)"))
((
"2" (
assert)
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (case-replace
"Im(n0z!1) < 0")
((
"1" (
expand "atan2")
((
"1" (
assert)
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"-1*Im(n0z!1)"
"py"
"sq_abs(n0z!1)"))
((
"1"
(
assert)
((
"1"
(case-replace
"Re(n0z!1) > 0")
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"Re(n0z!1)"
"py"
"sq_abs(n0z!1)"))
((
"1"
(
assert)
((
"1"
(
rewrite "div_div1")
((
"1"
(
rewrite "div_cancel2" 4)
((
"1"
(
rewrite
"atan_neg"
4
:dir
rl)
((
"1" (
assert)
nil nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil)
(
"2"
(
assert)
((
"2"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"sq_abs(n0z!1)"
"x"
"Re(n0z!1)"
"y"
"0"))
((
"2"
(
assert)
((
"2"
(
rewrite "div_div1")
((
"2"
(
rewrite "div_cancel2" 5)
((
"2"
(
assert)
((
"2"
(
rewrite "one_times")
((
"2"
(case-replace
"((-1 * Im(n0z!1) / Re(n0z!1)))=-(Im(n0z!1) / Re(n0z!1))")
((
"1"
(
rewrite
"atan_neg"
5)
((
"1"
(
assert)
nil
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
((
"2" (lift-if 5)
((
"2" (
expand "atan2")
((
"2"
(
assert)
((
"2"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"Im(n0z!1)"
"py"
"sq_abs(n0z!1)"))
((
"1"
(
assert)
((
"1"
(case-replace
"Re(n0z!1)>0")
((
"1"
(lemma
"posreal_div_posreal_is_posreal"
(
"px"
"Re(n0z!1)"
"py"
"sq_abs(n0z!1)"))
((
"1"
(
assert)
((
"1"
(
rewrite "div_div1")
((
"1"
(
rewrite "div_cancel2")
((
"1"
(
rewrite
"atan_neg"
5
:dir
rl)
((
"1"
(
assert)
nil
nil))
nil))
nil))
nil))
nil)
(
"2" (
assert)
nil nil))
nil)
(
"2"
(
assert)
((
"2"
(lemma
"both_sides_div_pos_lt1"
(
"pz"
"sq_abs(n0z!1)"
"x"
"Re(n0z!1)"
"y"
"0"))
((
"2"
(
assert)
((
"2"
(
rewrite "div_div1")
((
"2"
(
rewrite "div_cancel2")
((
"2"
(case-replace
"(-1 * Im(n0z!1) / (1 * Re(n0z!1)))=-(Im(n0z!1) / Re(n0z!1))")
((
"1"
(
rewrite
"atan_neg")
((
"1"
(
assert)
nil
nil))
nil)
(
"2"
(
assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
(
"2"
(
assert)
((
"2"
(case-replace
"Im(n0z!1) =0")
((
"1"
(
assert)
((
"1"
(
rewrite "atan_0")
((
"1"
(lift-if)
((
"1" (grind)
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)
((number nonempty-type-decl
nil numbers
nil)
(boolean nonempty-type-decl
nil booleans
nil)
(= const-decl
"[T, T -> boolean]" equalities
nil)
(complex type-decl
nil complex_types
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
"[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_lb const-decl
"posreal" trig_basic
"trig/")
(pi_ub const-decl
"posreal" trig_basic
"trig/")
(pi const-decl
"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(<= const-decl
"bool" reals
nil)
(argrng nonempty-type-eq-decl
nil polar
nil)
(arg const-decl
"argrng" polar
nil)
(
OR const-decl
"[bool, bool -> bool]" booleans
nil)
(/= const-decl
"boolean" notequal
nil)
(Re const-decl
"real" complex_types
nil)
(Im const-decl
"real" complex_types
nil)
(nzcomplex nonempty-type-eq-decl
nil complex_types
nil)
(atan2 const-decl
"real" atan2
"trig/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props
nil)
(posreal_div_posreal_is_posreal judgement-tcc
nil real_types
nil)
(nnreal type-eq-decl
nil real_types
nil)
(sq_abs const-decl
"nnreal" complex_types
nil)
(/ const-decl
"[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl
nil number_fields
nil)
(* const-decl
"[numfield, numfield -> numfield]" number_fields
nil)
(nonzero_real nonempty-type-eq-decl
nil reals
nil)
(div_div1 formula-decl
nil real_props
nil)
(int_times_even_is_even application-judgement
"even_int" integers
nil)
(mult_divides1 application-judgement
"(divides(n))" divides
nil)
(mult_divides2 application-judgement
"(divides(m))" divides
nil)
(atan_0 formula-decl
nil atan
"trig/")
(div_cancel2 formula-decl
nil real_props
nil)
(minus_nzreal_is_nzreal application-judgement
"nzreal" real_types
nil)
(nz_sq_abs_pos judgement-tcc
nil complex_types
nil)
(
NOT const-decl
"[bool -> bool]" booleans
nil)
(c_eq3 formula-decl
nil complex_types
nil)
(Im_div2 formula-decl
nil complex_types
nil)
(Re_div2 formula-decl
nil complex_types
nil)
(real_div_nzreal_is_real application-judgement
"real" reals
nil)
(real_times_real_is_real application-judgement
"real" reals
nil)
(nz_sq_abs_pos application-judgement
"posreal" complex_types
nil)
(div_nzcomplex2 application-judgement
"nzcomplex" complex_types
nil)
(real_ge_is_total_order name-judgement
"(total_order?[real])"
real_props
nil)
(arg_is_0 formula-decl
nil polar
nil)
(minus_real_is_real application-judgement
"real" reals
nil)
(atan_neg formula-decl
nil atan
"trig/")
(one_times formula-decl
nil extra_tegies
nil)
(minus_odd_is_odd application-judgement
"odd_int" integers
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal"
real_types
nil)
(real_minus_real_is_real application-judgement
"real" reals
nil)
(arg_is_pi formula-decl
nil polar
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)
(nnreal_div_posreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement
"nnreal"
real_types
nil)
(sq_0 formula-decl
nil sq
"reals/")
(both_sides_div_pos_lt1 formula-decl
nil real_props
nil)
(
nil application-judgement
"nnreal_lt_2pi" atan2
"trig/"))
shostak))
(arg_div 0
(arg_div-1
nil 3455878258
(
"" (skosimp)
((
"" (lemma
"arg_inv" (
"n0z" "n0y!1"))
((
"" (lemma
"arg_mult" (
"n0x" "n0x!1" "n0y" "1/n0y!1"))
((
"" (
replace -2 -1)
((
"" (hide -2)
((
"" (
expand "/")
((
"" (
expand "*")
((
"" (
assert)
((
""
(case-replace
"Re(n0x!1) * ((1 * Re(n0y!1)) / sq_abs(n0y!1)) -
Im(n0x!1) * (((-1) * Im(n0y!1)) / sq_abs(n0y!1))=(Im(n0x!1) * Im(n0y!1) + Re(n0x!1) * Re(n0y
!1)) /
sq_abs(n0y!1)")
(("1" (hide -1)
(("1"
(case-replace
"Im(n0x!1) * ((1 * Re(n0y!1)) / sq_abs(n0y!1)) +
Re(n0x!1) * (((-1) * Im(n0y!1)) / sq_abs(n0y!1))=(Im(n0x!1) * Re(n0y!1) - Re(n0x!1) * Im(n0y!1)) /
sq_abs(n0y!1)")
(("1" (assert)
(("1" (hide -1)
(("1" (replace -1 1)
(("1"
(hide -1)
(("1"
(case-replace "arg(n0y!1) = 0")
(("1"
(lift-if 1)
(("1" (assert) nil nil))
nil)
("2"
(case-replace "arg(n0y!1) = 0")
(("2"
(case-replace "arg(n0y!1) = pi")
(("1"
(assert)
(("1"
(lemma
"trichotomy"
("x" "arg(n0x!1)"))
(("1"
(split)
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lift-if 4)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nzcomplex nonempty-type-eq-decl nil complex_types nil)
(Im const-decl "real" complex_types nil)
(Re const-decl "real" complex_types 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 "boolean" notequal nil)
(number nonempty-type-decl nil numbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(complex type-decl nil complex_types nil)
(arg_inv formula-decl nil polar nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(/ const-decl "complex" complex_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(Re_rew formula-decl nil complex_types nil)
(Im_rew formula-decl nil complex_types nil)
(arg const-decl "argrng" polar nil)
(argrng nonempty-type-eq-decl nil polar nil)
(<= const-decl "bool" reals nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi_lb const-decl "posreal" trig_basic "trig/")
(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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(trichotomy formula-decl nil real_axioms nil)
(minus_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sq_abs const-decl "nnreal" complex_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "complex" complex_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nz_sq_abs_pos application-judgement "posreal" complex_types nil)
(div_nzcomplex2 application-judgement "nzcomplex" complex_types
nil)
(arg_mult formula-decl nil polar nil)
(/ const-decl "complex" complex_types nil))
shostak))
(idempotent_rectangular 0
(idempotent_rectangular-1 nil 3455991054
("" (skosimp)
(("" (expand "from_rectangular")
(("" (expand "rectangular")
(("" (assert)
(("" (assert)
(("" (expand "complex_i") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((from_rectangular const-decl "complex" polar nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_add2 formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Re_add2 formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_i formula-decl nil complex_types nil)
(rectangular const-decl "[real, real]" polar nil))
shostak))
(idempotent_polar 0
(idempotent_polar-1 nil 3455991097
("" (skosimp)
(("" (expand "polar")
(("" (expand "from_polar")
(("" (expand "complex_i")
(("" (assert)
(("" (lemma "arg_div_abs" ("n0x" "n0z!1"))
(("" (lemma "Re_cos_abs1" ("n0x" "n0z!1/abs(n0z!1)"))
(("" (lemma "Im_sin_abs1" ("n0x" "n0z!1/abs(n0z!1)"))
(("" (assert) (("" (postpone) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((polar const-decl "[nnreal, argrng]" polar nil)
(complex_i const-decl "nzcomplex" complex_types nil)
(arg_div_abs formula-decl nil polar nil)
(complex type-decl nil complex_types nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal 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)
(Re const-decl "real" complex_types nil)
(Im const-decl "real" complex_types nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(Im_sin_abs1 formula-decl nil polar nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(Re_div3 formula-decl nil complex_types nil)
(Im_div3 formula-decl nil complex_types nil)
(abs_div2 formula-decl nil polar nil)
(abs_abs formula-decl nil polar nil)
(abs const-decl "nnreal" polar nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(/ const-decl "complex" complex_types nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(Re_cos_abs1 formula-decl nil polar nil)
(div_nzcomplex3 application-judgement "nzcomplex" complex_types
nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_add2 formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_rew formula-decl nil complex_types nil)
(Re_add2 formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_rew formula-decl nil complex_types nil)
(abs_nzcomplex application-judgement "posreal" polar nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(from_polar const-decl "complex" polar nil))
shostak)))
