|
(complex_sqrt
(sqrt_TCC1 0
(sqrt_TCC1-1 nil 3385156197 ("" (subtype-tcc) nil 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_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(Re const-decl "real" complex_types nil)
(Im const-decl "real" complex_types nil)
(= const-decl "bool" complex_types nil))
nil))
(sqrt_nz_is_nz 0
(sqrt_nz_is_nz-1 nil 3385156197
("" (skosimp)
(("" (expand "sqrt")
(("" (expand "abs")
(("" (expand "arg")
(("" (expand "from_polar")
(("" (assert)
(("" (lift-if)
(("" (rewrite "cos_0")
(("" (rewrite "sin_0")
(("" (assert)
(("" (typepred "n0z!1")
((""
(lemma "sin_minus"
("a" "atan2(Re(n0z!1), Im(n0z!1)) / 2" "b"
"pi"))
(("1" (replace -1)
(("1"
(lemma "cos_minus"
("a"
"atan2(Re(n0z!1), Im(n0z!1)) / 2"
"b"
"pi"))
(("1"
(replace -1)
(("1"
(hide -1 -2)
(("1"
(rewrite "cos_pi")
(("1"
(rewrite "sin_pi")
(("1"
(assert)
(("1"
(rewrite
"real_props.zero_times3")
(("1"
(rewrite
"real_props.zero_times3")
(("1"
(rewrite
"real_props.zero_times3")
(("1"
(rewrite
"real_props.zero_times3")
(("1"
(rewrite
"real_props.zero_times3")
(("1"
(lemma
"sin_cos_eq_0"
("a"
"atan2(Re(n0z!1), Im(n0z!1)) / 2"))
(("1"
(case-replace
"Re(n0z!1) = 0 AND Im(n0z!1) = 0")
(("1"
(replace 1)
(("1"
(case-replace
"Im(n0z!1) < 0")
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sqrt const-decl "complex" complex_sqrt nil)
(arg const-decl "argrng" polar nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(nz_sq_abs_pos application-judgement "posreal" complex_types nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(c_eq3 formula-decl nil complex_types nil)
(Re_i formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_add2 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_add2 formula-decl nil complex_types nil)
(cos_0 formula-decl nil trig_basic "trig/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin_minus formula-decl nil trig_basic "trig/")
(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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(atan2 const-decl "real" atan2 "trig/")
(>= 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/")
(cos_minus formula-decl nil trig_basic "trig/")
(sin_pi formula-decl nil trig_basic "trig/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(cos const-decl "real" trig_basic "trig/")
(sq_abs const-decl "nnreal" complex_types 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)
(zero_times3 formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sin_cos_eq_0 formula-decl nil trig_aux nil)
(sin const-decl "real" trig_basic "trig/")
(cos_pi formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(complex type-decl nil complex_types nil)
(/= const-decl "boolean" notequal nil)
(number nonempty-type-decl nil numbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sin_0 formula-decl nil trig_basic "trig/")
(from_polar const-decl "complex" polar nil)
(abs const-decl "nnreal" polar nil))
nil))
(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)
(("1" (split)
(("1" (flatten) nil nil) ("2" (flatten) nil nil)) nil))
nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (expand "sqrt")
(("2" (assert)
(("2" (flatten)
(("2" (expand "abs")
(("2" (expand "arg")
(("2" (expand "sq_abs")
(("2" (assert)
(("2" (expand "sq")
(("2" (replace -1)
(("2" (replace -2)
(("2" (assert)
(("2"
(expand "from_polar")
(("2" (assert) nil nil))
nil))
nil))
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)
(sqrt_nz_is_nz judgement-tcc nil complex_sqrt nil)
(c_eq3 formula-decl nil complex_types nil)
(sqrt const-decl "complex" complex_sqrt nil)
(arg const-decl "argrng" polar nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(Re_i formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_add2 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_add2 formula-decl nil complex_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(from_polar const-decl "complex" polar nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(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)
(sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(sq_abs const-decl "nnreal" complex_types nil)
(abs const-decl "nnreal" polar nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
shostak))
(sqrt_sq 0
(sqrt_sq-1 nil 3385193372
("" (skosimp)
(("" (expand "sqrt")
(("" (expand "from_polar")
(("" (assert)
(("" (assert)
(("" (case "z!1=0")
(("1" (assert)
(("1" (flatten)
(("1" (expand "*")
(("1" (expand "arg")
(("1" (assert)
(("1" (rewrite "cos_0")
(("1" (rewrite "sin_0")
(("1" (expand "abs")
(("1"
(expand "sq_abs")
(("1"
(expand "sq")
(("1"
(assert)
(("1"
(replace -2)
(("1"
(replace -1)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "arg_mult" ("n0x" "z!1" "n0y" "z!1"))
(("1" (assert)
(("1" (replace -1)
(("1" (assert)
(("1" (hide -1)
(("1" (case "-pi / 2 < arg(z!1)")
(("1" (assert)
(("1"
(lemma "div_mult_pos_lt1"
("py" "2" "z" "-pi" "x" "arg(z!1)"))
(("1"
(copy -2)
(("1"
(replace -2 -1)
(("1"
(replace -1)
(("1"
(assert)
(("1"
(case "arg(z!1) <= pi / 2")
(("1"
(assert)
(("1"
(rewrite "abs_cos_arg")
(("1"
(use "abs_sin_arg")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"cos_minus"
("a" "arg(z!1)" "b" "pi"))
(("2"
(lemma
"sin_minus"
("a"
"arg(z!1)"
"b"
"pi"))
(("2"
(rewrite "cos_pi")
(("2"
(rewrite "sin_pi")
(("2"
(assert)
(("2"
(replace -1)
(("2"
(replace -2)
(("2"
(hide -1 -2)
(("2"
(assert)
(("2"
(use
"abs_cos_arg")
(("2"
(assert)
(("2"
(lemma
"abs_sin_arg"
("z"
"z!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)
("2" (assert)
(("2"
(lemma "cos_plus"
("a" "arg(z!1)" "b" "pi"))
(("2"
(lemma
"sin_plus"
("a" "arg(z!1)" "b" "pi"))
(("2"
(rewrite "sin_pi")
(("2"
(rewrite "cos_pi")
(("2"
(replace -1)
(("2"
(replace -2)
(("2"
(hide -1 -2)
(("2"
(assert)
(("2"
(use "abs_cos_arg")
(("2"
(assert)
(("2"
(assert)
(("2"
(lemma
"abs_sin_arg"
("z" "z!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(sqrt const-decl "complex" complex_sqrt nil)
(real_plus_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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(complex_sq_def formula-decl nil complex_types nil)
(abs_mult formula-decl nil polar nil)
(sqrt_square formula-decl nil sqrt "reals/")
(Re_i formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_add2 formula-decl nil complex_types nil)
(Re_neg1 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_add2 formula-decl nil complex_types nil)
(Im_neg1 formula-decl nil complex_types nil)
(c_eq1 formula-decl nil complex_types 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)
(arg const-decl "argrng" polar nil)
(cos_0 formula-decl nil trig_basic "trig/")
(abs const-decl "nnreal" polar nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqrt_0 formula-decl nil sqrt "reals/")
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(sq_abs const-decl "nnreal" complex_types nil)
(sin_0 formula-decl nil trig_basic "trig/")
(Im_rew formula-decl nil complex_types nil)
(Re_rew formula-decl nil complex_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "complex" complex_types 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)
(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)
(- 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)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_minus formula-decl nil trig_basic "trig/")
(sin_pi formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(cos_pi formula-decl nil trig_basic "trig/")
(cos_minus formula-decl nil trig_basic "trig/")
(abs_sin_arg formula-decl nil polar nil)
(abs_cos_arg formula-decl nil polar nil)
(cos_plus formula-decl nil trig_basic "trig/")
(sin_plus formula-decl nil trig_basic "trig/")
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(Im const-decl "real" complex_types nil)
(Re const-decl "real" complex_types nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(arg_mult formula-decl nil polar nil)
(minus_real_is_real application-judgement "real" reals nil)
(from_polar const-decl "complex" polar nil))
shostak))
(sq_sqrt 0
(sq_sqrt-1 nil 3385159230
("" (skosimp)
(("" (expand "sqrt")
(("" (expand "sq")
(("" (expand "from_polar")
(("" (assert)
(("" (rewrite "sq_rew")
(("" (rewrite "sq_rew")
(("" (rewrite "cos2")
(("" (lemma "sin_2a" ("a" "arg(z!1) / 2"))
(("" (lemma "abs_sin_arg" ("z" "z!1"))
(("" (replace -2 -1)
(("" (assert)
(("" (hide -1 -2)
((""
(lemma "cos_2a_sin" ("a" "arg(z!1) / 2"))
((""
(lemma "abs_cos_arg" ("z" "z!1"))
((""
(replace -2 -1)
((""
(assert)
((""
(expand "sq")
(("" (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)
(from_polar const-decl "complex" polar nil)
(sq_rew formula-decl nil sq "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(cos const-decl "real" trig_basic "trig/")
(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)
(complex type-decl nil complex_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals 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)
(cos2 formula-decl nil trig_basic "trig/")
(abs_sin_arg formula-decl nil polar nil)
(cos_2a_sin formula-decl nil trig_basic "trig/")
(sq const-decl "nonneg_real" sq "reals/")
(abs_cos_arg formula-decl nil polar nil)
(sin_2a formula-decl nil trig_basic "trig/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin const-decl "real" trig_basic "trig/")
(Re_i formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_add2 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_add2 formula-decl nil complex_types nil)
(Re_mul1 formula-decl nil complex_types nil)
(Im_mul1 formula-decl nil complex_types nil)
(c_eq1 formula-decl nil complex_types 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_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq const-decl "complex" complex_types nil))
shostak))
(sqrt_times 0
(sqrt_times-1 nil 3385198032
("" (skosimp)
(("" (case-replace "x!1=0")
(("1" (lift-if)
(("1" (lemma "abs_is_0" ("z" "x!1"))
(("1" (lemma "arg_is_0" ("z" "x!1"))
(("1" (flatten)
(("1" (hide -1 -3)
(("1" (split)
(("1" (split)
(("1" (replace -2)
(("1" (typepred "arg(y!1)")
(("1" (assert)
(("1" (flatten)
(("1" (expand "sqrt")
(("1"
(expand "from_polar")
(("1"
(rewrite "abs_mult")
(("1"
(replace -3)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "y!1=0")
(("1" (lift-if)
(("1" (lemma "abs_is_0" ("z" "y!1"))
(("1" (flatten -1)
(("1" (hide -1)
(("1" (split)
(("1" (lemma "arg_is_0" ("z" "y!1"))
(("1" (flatten -1)
(("1" (hide -1)
(("1" (split)
(("1" (replace -1)
(("1" (typepred "arg(x!1)")
(("1"
(assert)
(("1"
(expand "sqrt")
(("1"
(expand "from_polar")
(("1"
(rewrite "abs_mult")
(("1"
(replace -4)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "arg_mult" ("n0x" "x!1" "n0y" "y!1"))
(("1" (assert)
(("1" (expand "sqrt")
(("1" (rewrite "abs_mult")
(("1" (rewrite "sqrt_times")
(("1" (name-replace "RX" "sqrt.sqrt(abs(x!1))")
(("1" (name-replace "RY" "sqrt.sqrt(abs(y!1))")
(("1" (name-replace "TX" "arg(x!1)")
(("1" (name-replace "TY" "arg(y!1)")
(("1" (case-replace "TX + TY > pi")
(("1" (assert)
(("1"
(replace -2)
(("1"
(assert)
(("1"
(hide -2)
(("1"
(case-replace
"(TX - 2 * pi + TY) / 2 = TX/2+TY/2-pi")
(("1"
(hide -1)
(("1"
(expand "from_polar")
(("1"
(rewrite "sin_minus")
(("1"
(rewrite "cos_minus")
(("1"
(rewrite "cos_pi")
(("1"
(rewrite "sin_pi")
(("1"
(rewrite
"zero_times1")
(("1"
(assert)
(("1"
(rewrite
"cos_plus")
(("1"
(rewrite
"sin_plus")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "TX + TY <= -pi")
(("1"
(assert)
(("1"
(replace -2)
(("1"
(hide -2)
(("1"
(case-replace
"(TX + TY + 2 * pi) / 2 = TX/2+TY/2+pi")
(("1"
(hide -1)
(("1"
(expand "from_polar")
(("1"
(rewrite "sin_plus")
(("1"
(rewrite "sin_plus")
(("1"
(rewrite "cos_plus")
(("1"
(rewrite "cos_plus")
(("1"
(rewrite "cos_pi")
(("1"
(rewrite
"sin_pi")
(("1"
(rewrite
"zero_times2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(assert)
(("2"
(rewrite
"div_distributes"
5
:dir
rl)
(("2"
(expand "from_polar")
(("2"
(rewrite "sin_plus")
(("2"
(rewrite "cos_plus")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil))
nil)
("3" (assert) (("3" (flatten) (("3" (assert) nil nil)) 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)
(abs_is_0 formula-decl nil polar nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_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)
(c_eq3 formula-decl nil complex_types nil)
(Re_mul1 formula-decl nil complex_types nil)
(Im_mul1 formula-decl nil complex_types nil)
(c_eq1 formula-decl nil complex_types nil)
(sqrt const-decl "complex" complex_sqrt nil)
(abs_mult formula-decl nil polar nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(Re_i formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_add2 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_add2 formula-decl nil complex_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(from_polar const-decl "complex" polar nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(NOT const-decl "[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)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(arg_is_0 formula-decl nil polar nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(Im const-decl "real" complex_types nil)
(Re const-decl "real" complex_types nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(arg_mult formula-decl nil polar nil)
(abs const-decl "nnreal" polar nil)
(nnreal type-eq-decl nil real_types nil)
(sqrt_times formula-decl nil sqrt "reals/")
(zero_times2 formula-decl nil real_props nil)
(sin const-decl "real" trig_basic "trig/")
(div_distributes formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(cos_minus formula-decl nil trig_basic "trig/")
(sin_pi formula-decl nil trig_basic "trig/")
(sin_plus formula-decl nil trig_basic "trig/")
(cos_plus formula-decl nil trig_basic "trig/")
(zero_times1 formula-decl nil real_props nil)
(cos const-decl "real" trig_basic "trig/")
(cos_pi formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_minus formula-decl nil trig_basic "trig/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(Im_neg1 formula-decl nil complex_types nil)
(Re_neg1 formula-decl nil complex_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(sqrt_neg 0
(sqrt_neg-1 nil 3385196467
("" (skosimp)
(("" (assert)
(("" (expand "sqrt")
(("" (rewrite "abs_neg")
(("" (case "z!1=0")
(("1" (assert)
(("1" (flatten)
(("1" (expand "arg")
(("1" (assert)
(("1" (expand "abs")
(("1" (expand "sq_abs")
(("1" (expand "sq")
(("1" (assert)
(("1" (replace -1)
(("1"
(replace -2)
(("1"
(assert)
(("1"
(expand "from_polar")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "arg_neg" ("n0x" "z!1"))
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "from_polar")
(("1" (assert)
(("1" (lemma "trichotomy" ("x" "arg(z!1)"))
(("1" (split)
(("1" (assert)
(("1"
(lemma "sin_minus"
("a" "arg(z!1)/2" "b" "pi/2"))
(("1"
(lemma
"cos_minus"
("a" "arg(z!1)/2" "b" "pi/2"))
(("1"
(rewrite "sin_pi2")
(("1"
(rewrite "cos_pi2")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (assert)
(("2"
(rewrite "sin_0")
(("2"
(rewrite "cos_0")
(("2"
(rewrite "cos_pi2")
(("2"
(rewrite "sin_pi2")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert)
(("3" (lemma "cos_sin" ("a" "arg(z!1)/2"))
(("3"
(replace -1 2 rl)
(("3"
(assert)
(("3"
(hide -1)
(("3"
(rewrite "sin_cos")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (flatten) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_mul1 formula-decl nil complex_types nil)
(Im_neg1 formula-decl nil complex_types nil)
(Re_neg1 formula-decl nil complex_types nil)
(Re_mul1 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Re_i formula-decl nil complex_types nil)
(complex type-decl nil complex_types nil)
(abs_neg formula-decl nil polar nil)
(arg_neg 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_minus formula-decl nil trig_basic "trig/")
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(sin_pi2 formula-decl nil trig_basic "trig/")
(cos_pi2 formula-decl nil trig_basic "trig/")
(cos_minus formula-decl nil trig_basic "trig/")
(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)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_0 formula-decl nil trig_basic "trig/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin_0 formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(cos_sin formula-decl nil trig_basic "trig/")
(sin_cos formula-decl nil trig_basic "trig/")
(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)
(trichotomy formula-decl nil real_axioms nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(c_eq3 formula-decl nil complex_types nil)
(arg const-decl "argrng" polar nil)
(abs const-decl "nnreal" polar nil)
(sq const-decl "nonneg_real" sq "reals/")
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(Re_mul2 formula-decl nil complex_types nil)
(Re_add2 formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_add2 formula-decl nil complex_types nil)
(from_polar const-decl "complex" polar nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(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)
(real_plus_real_is_real application-judgement "real" reals nil)
(sq_abs const-decl "nnreal" complex_types nil)
(minus_real_is_real application-judgement "real" reals 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)
(sqrt const-decl "complex" complex_sqrt nil))
shostak))
(sqrt_inv 0
(sqrt_inv-1 nil 3385200646
("" (skosimp)
(("" (case "arg(n0z!1) = pi")
(("1" (replace -1)
(("1" (lemma "arg_is_pi" ("z" "n0z!1"))
(("1" (replace -2 -1)
(("1" (flatten -1)
(("1" (expand "sqrt")
(("1" (replace -3)
(("1" (lemma "arg_inv" ("n0z" "n0z!1"))
(("1" (replace -4)
(("1" (simplify -1)
(("1" (case-replace "arg(1 / n0z!1) = pi")
(("1" (hide -1 -2 -5)
(("1" (typepred "abs(n0z!1)")
(("1"
(hide -1)
(("1"
(case-replace
"sqrt(abs(1 / n0z!1))=1/sqrt(abs(n0z!1))")
(("1"
(hide -1 -3 -4)
(("1"
(name-replace "X" "abs(n0z!1)")
(("1"
(expand "from_polar")
(("1"
(rewrite "cos_pi2")
(("1"
(rewrite "sin_pi2")
(("1"
(rewrite "zero_times2")
(("1"
(lemma
"sqrt_pos"
("px" "X"))
(("1"
(name-replace
"Y"
"sqrt(X)")
(("1"
(assert)
(("1"
(rewrite
"neg_neg")
(("1"
(rewrite
"one_times")
(("1"
(case-replace
"sq_abs(0 + Y * complex_i)=sq(Y)")
(("1"
(hide -1)
(("1"
(expand
"sq")
(("1"
(rewrite
"cross_mult")
nil
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"sq_abs")
(("2"
(expand
"sq")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "abs_inv")
(("2"
(rewrite "sqrt_div" 1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "arg(n0z!1)")
(("2" (expand "<=" -2)
(("2" (replace 1)
(("2" (hide 1)
(("2"
(lemma "complex_div_cancel4"
("z2" "sqrt(1 / n0z!1)" "z1" "complex_(1,0)" "n0z"
"sqrt(n0z!1)"))
(("2" (flatten)
(("2" (split -2)
(("1" (hide -2)
(("1" (assert)
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2 -1)
(("2"
(lemma "sqrt_times"
("x" "1/n0z!1" "y" "n0z!1"))
(("2" (lemma "arg_inv" ("n0z" "n0z!1"))
(("2" (case-replace "arg(n0z!1) = 0")
(("1" (replace -2)
(("1"
(simplify -3)
(("1"
(assert)
(("1"
(flatten)
(("1"
(replace -3 1 rl)
(("1"
(replace -4 1 rl)
(("1"
(hide -3 -4)
(("1"
(expand "sqrt")
(("1"
(lemma
"arg_mult"
("n0x"
"1 / n0z!1"
"n0y"
"n0z!1"))
(("1"
(replace -2)
(("1"
(replace -3)
(("1"
(assert)
(("1"
(replace -1)
(("1"
(expand
"from_polar")
(("1"
(rewrite
"cos_0")
(("1"
(rewrite
"sin_0")
(("1"
(assert)
nil
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.133 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.
|
