|
(complex_sqrt
(sqrt_TCC1 0
(sqrt_TCC1-1 nil 3385156197 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(complex nonempty-type-from-decl nil complex_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(minus_complex_is_complex application-judgement "complex"
complex_types nil)
(minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
complex_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(complex_div_nzcomplex_is_complex application-judgement "complex"
complex_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(sqrt_nz_is_nz 0
(sqrt_nz_is_nz-1 nil 3385156197
("" (skosimp)
(("" (expand "sqrt")
(("" (expand "from_polar")
((""
(lemma "unique_characterization"
("y0" "sin(arg(n0z!1) / 2) * sqrt.sqrt(abs(n0z!1))" "x0"
"sqrt.sqrt(abs(n0z!1)) * cos(arg(n0z!1) / 2)" "x1" "0" "y1"
"0"))
(("" (rewrite "zero_times1")
(("" (replace -1 -2)
(("" (flatten)
(("" (hide -1 -2)
(("" (lemma "abs_nzcomplex" ("n0z" "n0z!1"))
(("" (lemma "sqrt_pos" ("px" "abs(n0z!1)"))
(("1" (name-replace "R" "sqrt.sqrt(abs(n0z!1))")
(("1" (rewrite "zero_times3" -3)
(("1" (assert)
(("1" (rewrite "cos_eq_0" -3)
(("1"
(skosimp)
(("1"
(replace -3)
(("1"
(hide -3)
(("1"
(rewrite "sin_k_pi2")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "complex" complex_sqrt nil)
(sin const-decl "real" trig_basic "trig/")
(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)
(- const-decl "[numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(cos const-decl "real" trig_basic "trig/")
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(/= const-decl "boolean" notequal nil)
(abs const-decl "nnreal" polar nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(= 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(unique_characterization formula-decl nil complex_types nil)
(complex_div_nzcomplex_is_complex application-judgement "complex"
complex_types nil)
(sqrt_pos judgement-tcc nil sqrt "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero_times3 formula-decl nil number_fields_bis nil)
(cos_eq_0 formula-decl nil trig_basic "trig/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(nznum_div_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(int nonempty-type-eq-decl nil integers nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(sin_k_pi2 formula-decl nil trig_basic "trig/")
(minus_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(rat_exp application-judgement "rat" exponentiation nil)
(abs_nzcomplex formula-decl nil polar nil)
(zero_times1 formula-decl nil number_fields_bis nil)
(i const-decl "complex" complex_types nil)
(from_polar const-decl "complex" polar nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(sin_range application-judgement "trig_range" trig_basic "trig/"))
nil))
(sqrt_nnz 0
(sqrt_nnz-1 nil 3385196945
("" (skosimp)
(("" (expand "sqrt")
(("" (expand "abs")
(("" (expand "conjugate")
(("" (expand "arg")
(("" (rewrite "Re_real")
(("" (rewrite "Im_real")
(("" (rewrite "zero_times1")
(("" (rewrite "zero_times1")
(("" (expand "atan2")
(("" (assert)
(("" (rewrite "atan_0")
(("" (lift-if)
(("" (expand "from_polar")
((""
(rewrite "sin_0")
((""
(rewrite "cos_0")
((""
(rewrite "zero_times1")
((""
(rewrite "zero_times1")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "complex" complex_sqrt nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(Im_is_real application-judgement "real" complex_types nil)
(Re_is_real application-judgement "real" complex_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(conjugate const-decl "complex" arithmetic nil)
(Re_real formula-decl nil arithmetic nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(nznum_times_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(nzcomplex_times_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(i const-decl "complex" complex_types nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(zero_times1 formula-decl nil number_fields_bis nil)
(atan2 const-decl "real" atan2 "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(from_polar const-decl "complex" polar nil)
(cos_0 formula-decl nil trig_basic "trig/")
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonneg_real nonempty-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/")
(sin_0 formula-decl nil trig_basic "trig/")
(atan_0 formula-decl nil atan "trig/")
(sqrt_square formula-decl nil sqrt "reals/")
(complex_div_nzcomplex_is_complex application-judgement "complex"
complex_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(Im_real formula-decl nil arithmetic nil)
(arg const-decl "argrng" polar nil)
(abs const-decl "nnreal" polar nil))
shostak))
(sqrt_npz_TCC1 0
(sqrt_npz_TCC1-1 nil 3385196849
("" (skosimp) (("" (typepred "npx!1") (("" (assert) nil nil)) nil))
nil)
((npreal 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)
(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)
(minus_complex_is_complex application-judgement "complex"
complex_types nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(sqrt_npz 0
(sqrt_npz-1 nil 3385197188
("" (skosimp)
(("" (expand "sqrt")
(("" (expand "abs")
(("" (expand "conjugate")
(("" (expand "arg")
(("" (rewrite "Re_real")
(("" (rewrite "Im_real")
(("" (rewrite "zero_times1")
(("" (rewrite "zero_times1")
(("" (assert)
(("" (lift-if)
(("" (assert)
(("" (expand "from_polar")
(("" (prop)
(("1"
(assert)
(("1"
(rewrite "sin_0")
(("1"
(rewrite "cos_0")
(("1"
(rewrite "zero_times1")
(("1"
(rewrite "zero_times1")
(("1"
(replace -1)
(("1"
(rewrite "sqrt.sqrt_0")
(("1"
(rewrite "zero_times2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand "atan2")
(("2"
(rewrite "atan_0")
(("2"
(rewrite "sin_pi2")
(("2"
(rewrite "cos_pi2")
(("2"
(rewrite "identity_mult")
(("2"
(rewrite "zero_times2")
(("2"
(lemma
"sqrt_sq_neg"
("x" "npx!1"))
(("2"
(split -1)
(("1"
(expand "sq")
(("1"
(replace -1)
(("1"
(assert)
(("1"
(rewrite
"commutative_mult"
2)
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)
((sqrt const-decl "complex" complex_sqrt nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(Im_is_real application-judgement "real" complex_types nil)
(Re_is_real application-judgement "real" complex_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(conjugate const-decl "complex" arithmetic nil)
(Re_real formula-decl nil arithmetic nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(<= const-decl "bool" reals nil)
(npreal type-eq-decl nil real_types nil)
(npreal_times_npreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(nznum_times_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(nzcomplex_times_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(i const-decl "complex" complex_types nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(zero_times1 formula-decl nil number_fields_bis nil)
(minus_complex_is_complex application-judgement "complex"
complex_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(complex_div_nzcomplex_is_complex application-judgement "complex"
complex_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(sqrt_square formula-decl nil sqrt "reals/")
(sin_0 formula-decl nil trig_basic "trig/")
(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)
(zero_times2 formula-decl nil number_fields_bis nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(cos_0 formula-decl nil trig_basic "trig/")
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(atan2 const-decl "real" atan2 "trig/")
(sin_pi2 formula-decl nil trig_basic "trig/")
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(identity_mult formula-decl nil number_fields nil)
(sqrt_sq_neg formula-decl nil sqrt "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(commutative_mult formula-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(cos_pi2 formula-decl nil trig_basic "trig/")
(atan_0 formula-decl nil atan "trig/")
(from_polar const-decl "complex" polar nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(Im_real formula-decl nil arithmetic nil)
(arg const-decl "argrng" polar nil)
(abs const-decl "nnreal" polar nil))
shostak))
(sqrt_0 0
(sqrt_0-1 nil 3385156772
("" (expand "sqrt")
(("" (expand "abs")
(("" (expand "arg")
(("" (expand "conjugate")
(("" (rewrite "sqrt_0")
(("" (rewrite "sqrt_0")
(("" (expand "from_polar") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs const-decl "nnreal" polar nil)
(Im_is_real application-judgement "real" complex_types nil)
(conjugate const-decl "complex" arithmetic nil)
(from_polar const-decl "complex" polar nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(arg const-decl "argrng" polar nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(sqrt const-decl "complex" complex_sqrt nil))
shostak))
(sqrt_1 0
(sqrt_1-1 nil 3385156811
("" (expand "sqrt")
(("" (expand "abs")
(("" (expand "conjugate")
(("" (expand "arg")
(("" (rewrite "Re_real")
(("" (rewrite "Im_real")
(("" (rewrite "zero_times1")
(("" (assert)
(("" (expand "atan2")
(("" (rewrite "atan_0")
(("" (expand "from_polar")
(("" (rewrite "cos_0")
(("" (rewrite "sin_0")
(("" (rewrite "zero_times1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs const-decl "nnreal" polar nil)
(arg const-decl "argrng" polar nil)
(Im_real formula-decl nil arithmetic nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(complex_div_nzcomplex_is_complex application-judgement "complex"
complex_types nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(atan_0 formula-decl nil atan "trig/")
(cos_0 formula-decl nil trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(sin_0 formula-decl nil trig_basic "trig/")
(from_polar const-decl "complex" polar nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(atan2 const-decl "real" atan2 "trig/")
(zero_times1 formula-decl nil number_fields_bis nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(complex nonempty-type-from-decl nil complex_types nil)
(i const-decl "complex" complex_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzcomplex_times_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(nznum_times_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
complex_types nil)
(minus_complex_is_complex application-judgement "complex"
complex_types nil)
(minus_nznum_is_nznum application-judgement "nznum"
number_fields_bis 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)
(Re_real formula-decl nil arithmetic nil)
(conjugate const-decl "complex" arithmetic nil)
(Re_is_real application-judgement "real" complex_types nil)
(Im_is_real application-judgement "real" complex_types nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(sqrt const-decl "complex" complex_sqrt nil))
shostak))
(sqrt_neg1 0
(sqrt_neg1-1 nil 3385197557
("" (lemma "sqrt_npz" ("npx" "-1")) (("" (assert) nil nil)) nil)
((sqrt_1 formula-decl nil sqrt "reals/")
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(sqrt_nz_is_nz application-judgement "nzcomplex" complex_sqrt nil)
(minus_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(minus_complex_is_complex application-judgement "complex"
complex_types nil)
(minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
complex_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sqrt_npz formula-decl nil complex_sqrt nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(<= const-decl "bool" reals nil)
(npreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil))
shostak))
(sqrt_eq_0 0
(sqrt_eq_0-1 nil 3385156991
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (lemma "sqrt_nz_is_nz" ("n0z" "z!1"))
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (replace -1) (("2" (rewrite "sqrt_0") nil nil)) nil))
nil))
nil))
nil)
((nzcomplex nonempty-type-eq-decl nil complex_types nil)
(/= const-decl "boolean" notequal nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
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_nz_is_nz judgement-tcc nil complex_sqrt nil)
(sqrt_0 formula-decl nil complex_sqrt nil))
shostak))
(sqrt_sq_TCC1 0
(sqrt_sq_TCC1-1 nil 3385192826 ("" (subtype-tcc) nil nil)
((sq const-decl "numfield" number_fields_sq nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil))
nil))
(sqrt_sq 0
(sqrt_sq-1 nil 3385193372
("" (skosimp)
(("" (lift-if)
(("" (expand "sqrt")
(("" (expand "sq")
(("" (rewrite "abs_mult")
(("" (rewrite "sq.sq_rew")
(("" (rewrite "sqrt_sq")
(("" (case-replace "z!1=0")
(("1" (expand "arg")
(("1" (assert)
(("1" (expand "abs")
(("1" (expand "conjugate")
(("1" (rewrite "sqrt.sqrt_0")
(("1" (expand "from_polar")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "arg_mult" ("n0x" "z!1" "n0y" "z!1"))
(("1" (assert)
(("1" (prop)
(("1" (assert)
(("1" (replace -3)
(("1"
(lemma "div_cancel1"
("x" "arg(z!1)" "n0z" "2"))
(("1"
(assert)
(("1"
(replace -1 1)
(("1"
(lemma
"idempotent_polar"
("n0z" "z!1"))
(("1"
(expand "polar")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (replace -1)
(("2"
(lemma "div_cancel1"
("x" "arg(z!1)+pi" "n0z" "2"))
(("2"
(replace -1 2)
(("2"
(lemma
"minus_nznum_is_nznum"
("nzx" "z!1"))
(("2"
(lemma
"idempotent_polar"
("n0z" "-z!1"))
(("1"
(expand "polar")
(("1"
(rewrite "arg_neg")
(("1"
(rewrite "abs_neg")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(lemma "minus_nznum_is_nznum" ("nzx" "z!1"))
(("3"
(lemma "idempotent_polar" ("n0z" "-z!1"))
(("1" (expand "polar")
(("1"
(rewrite "abs_neg")
(("1"
(rewrite "arg_neg")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "numfield" number_fields_sq nil)
(abs const-decl "nnreal" polar nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(sq_rew formula-decl nil sq "reals/")
(= 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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(complex_div_nzcomplex_is_complex application-judgement "complex"
complex_types nil)
(nznum_div_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Im_is_real application-judgement "real" complex_types nil)
(conjugate const-decl "complex" arithmetic nil)
(from_polar const-decl "complex" polar nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(arg const-decl "argrng" polar nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(nznum_times_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_nznum_is_nznum judgement-tcc nil number_fields_bis nil)
(abs_neg formula-decl nil polar nil)
(arg_neg formula-decl nil polar nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_cancel1 formula-decl nil number_fields_bis nil)
(nznum nonempty-type-eq-decl nil number_fields 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)
(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)
(polar const-decl "[nnreal, argrng]" polar nil)
(idempotent_polar formula-decl nil polar nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(/= const-decl "boolean" notequal nil)
(arg_mult formula-decl nil polar nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_sq formula-decl nil sqrt "reals/")
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
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)
(abs_mult formula-decl nil polar nil)
(sqrt const-decl "complex" complex_sqrt nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
complex_types nil)
(minus_complex_is_complex application-judgement "complex"
complex_types nil)
(minus_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil))
shostak))
(sq_sqrt 0
(sq_sqrt-1 nil 3385159230
("" (skosimp)
(("" (expand "sqrt")
(("" (case-replace "z!1=0")
(("1" (expand "sq")
(("1" (expand "abs")
(("1" (expand "conjugate")
(("1" (expand "arg")
(("1" (rewrite "sqrt.sqrt_0")
(("1" (rewrite "sqrt.sqrt_0")
(("1" (expand "from_polar")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (lemma "abs_nzcomplex" ("n0z" "z!1"))
(("2" (expand "arg")
(("2" (expand "from_polar")
(("2" (expand "sq")
(("2" (case-replace "Im(z!1) < 0")
(("1" (rewrite "sq.sq_rew" 2)
(("1" (assert)
(("1" (assert)
(("1"
(case-replace
"cos((atan2(Re(z!1), Im(z!1)) - 2 * pi) / 2) *
sin((atan2(Re(z!1), Im(z!1)) - 2 * pi) / 2) = sin(atan2(Re(z!1), Im(z!1)) - 2 * pi)/2")
(("1" (hide -1)
(("1"
(case-replace
"sin((atan2(Re(z!1), Im(z!1)) - 2 * pi) / 2) *
sin((atan2(Re(z!1), Im(z!1)) - 2 * pi) / 2)= (1-cos(atan2(Re(z!1), Im(z!1)) - 2 * pi))/2")
(("1"
(hide -1)
(("1"
(lemma
"idempotent_polar"
("n0z" "z!1"))
(("1"
(expand "polar")
(("1"
(expand "from_polar")
(("1"
(expand "arg")
(("1"
(name-replace
"TH"
"atan2(Re(z!1), Im(z!1)) - 2 * pi")
(("1"
(assert)
(("1"
(expand "sq" 2)
(("1"
(case-replace
"cos(TH / 2) * cos(TH / 2)=(cos(TH)+1)/2")
(("1"
(assert)
(("1"
(rewrite
"sq.sq_rew"
2)
(("1"
(rewrite
"times_div1"
2)
(("1"
(rewrite
"times_div2"
2)
(("1"
(rewrite
"div_cancel1"
2)
(("1"
(name-replace
"DRL1"
"abs(z!1) * sin(TH) * i")
(("1"
(rewrite
"minus_div2"
2
:dir
rl)
(("1"
(rewrite
"div_distributes"
2
:dir
rl)
(("1"
(hide
-1)
(("1"
(lemma
"both_sides_times2"
("n0z"
"abs(z!1)"
"x"
"cos(TH)"
"y"
"(1 / 2 - cos(TH) / 2) * i * i+((1 / 2) + (cos(TH) / 2))"))
(("1"
(flatten)
(("1"
(hide
-1)
(("1"
(split
-1)
(("1"
(replace
-1
-2)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide
3
-1)
(("2"
(assert)
(("2"
(lemma
"associative_mult"
("y"
"i"
"z"
"i"))
(("2"
(inst-cp
-
"1/2")
(("2"
(inst
-
"cos(TH)/2")
(("2"
(lemma
"i_axiom")
(("2"
(replace
-1)
(("2"
(replace
-2
1
rl)
(("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)
("2"
(hide-all-but 1)
(("2"
(lemma
"cos_2a_cos"
("a" "TH/2"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(name-replace
"TH"
"atan2(Re(z!1), Im(z!1)) - 2 * pi")
(("2"
(lemma "cos_2a_sin" ("a" "TH/2"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(name-replace
"TH"
"atan2(Re(z!1), Im(z!1)) - 2 * pi")
(("2"
(lemma "sin_2a" ("a" "TH/2"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(case-replace
"cos(atan2(Re(z!1), Im(z!1)) / 2) * sin(atan2(Re(z!1), Im(z!1)) / 2) = sin(atan2(Re(z!1), Im(z!1)))/2")
(("1" (hide -1)
(("1"
(case-replace
"sin(atan2(Re(z!1), Im(z!1)) / 2) * sin(atan2(Re(z!1), Im(z!1)) / 2) = (1-cos(atan2(Re(z!1), Im(z!1))))/2")
(("1" (hide -1)
(("1"
(case-replace
"cos(atan2(Re(z!1), Im(z!1)) / 2) * cos(atan2(Re(z!1), Im(z!1)) / 2) = (cos(atan2(Re(z!1), Im(z!1)))+1)/2")
(("1"
(hide -1)
(("1"
(assert)
(("1"
(rewrite "sq.sq_rew")
(("1"
(lemma
"complex_is_ne_0_Re_Im"
("z" "z!1"))
(("1"
(assert)
(("1"
(lemma
"sin_atan2"
("x"
"Re(z!1)"
"y"
"Im(z!1)"))
(("1"
(lemma
"cos_atan2"
("x"
"Re(z!1)"
"y"
"Im(z!1)"))
(("1"
(assert)
(("1"
(replace -3)
(("1"
(case-replace
"2 * (abs(z!1) * (sin(atan2(Re(z!1), Im(z!1))) / 2) * i) +
abs(z!1) * ((1 - cos(atan2(Re(z!1), Im(z!1)))) / 2) * i * i
+ abs(z!1) * ((1 + cos(atan2(Re(z!1), Im(z!1)))) / 2) = abs(z!1)*(sin(atan2(Re(z!1), Im(z!1)))*i + cos(atan2(Re(z!1), Im(z!1))))")
(("1"
(hide -1)
(("1"
(case-replace
"Re(z!1)=0")
(("1"
(replace -2)
(("1"
(assert)
(("1"
(lemma
"complex_is_Re_Im"
("z"
"z!1"))
(("1"
(replace
-2)
(("1"
(assert)
(("1"
(replace
-4)
(("1"
(assert)
(("1"
(case-replace
"abs(z!1)=Im(z!1)")
(("1"
(assert)
nil
nil)
("2"
(expand
"abs")
(("2"
(expand
"conjugate")
(("2"
(replace
-2)
(("2"
(rewrite
"zero_times1")
(("2"
(case-replace
"0 - Im(z!1) * i * z!1 = sq(Im(z!1))")
(("1"
(lemma
"sqrt.sqrt_sq")
(("1"
(inst
-
"Im(z!1)")
(("1"
(split
-1)
(("1"
(expand
"sq")
(("1"
(propax)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"sq")
(("2"
(name-replace
"IMMM"
"Im(z!1)")
(("2"
(replace
-1
1)
(("2"
(hide-all-but
1)
(("2"
(rewrite
"sq_rew")
(("2"
(rewrite
"sq_times")
(("2"
(rewrite
"sq_rew")
(("2"
(case-replace
"sq(i)=-1")
(("1"
(assert)
(("1"
(expand
"sq")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(expand
"sq")
(("2"
(lemma
"i_axiom")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.125 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
