|
(asin (real_abs_le_pi2_TCC1 0
(real_abs_le_pi2_TCC1-1 nil 3323019118
("" (subtype-tcc) nil nil)
((minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types 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))
nil))
(asin_TCC1 0
(asin_TCC1-1 nil 3262199128
("" (skolem 1 ("x"))
(("" (flatten)
(("" (typepred "x")
(("" (expand "abs")
(("" (assert)
((""
(lemma "le_times_le_pos"
("nnx" "-x" "y" "1" "nnz" "-x" "w" "1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil))
shostak))
(asin_TCC2 0
(asin_TCC2-1 nil 3262199262
("" (grind)
(("1" (lemma "sq_lt_abs" ("a" "-x!1" "b" "1"))
(("1" (grind) nil nil)) nil)
("2" (rewrite "sq_rew")
(("2" (lemma "sq_lt" ("nna" "x!1" "nnb" "1"))
(("2" (grind) nil nil)) nil))
nil))
nil)
((minus_real_is_real application-judgement "real" reals nil)
(sq_lt_abs formula-decl nil sq "reals/")
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(sq const-decl "nonneg_real" sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_minus_real_is_real application-judgement "real" reals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(real_times_real_is_real application-judgement "real" reals
nil))
shostak))
(asin_TCC3 0
(asin_TCC3-1 nil 3262199449
("" (skolem 1 ("x"))
(("" (flatten)
(("" (typepred "x")
(("" (expand "abs")
(("" (case "x < 0")
(("1" (assert)
(("1"
(lemma "lt_times_lt_pos1"
("px" "-x" "y" "1" "nnz" "-x" "w" "1"))
(("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2"
(lemma "lt_times_lt_pos1"
("px" "x" "y" "1" "nnz" "x" "w" "1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((< const-decl "bool" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(lt_times_lt_pos1 formula-decl nil real_props 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)
(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)
(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)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(real_times_real_is_real application-judgement "real" reals
nil))
shostak))
(asin_TCC4 0
(asin_TCC4-1 nil 3262199280
("" (skolem 1 ("x"))
(("" (flatten)
(("" (typepred "x")
(("" (assert)
(("" (typepred "atan(x / sqrt(1 - x * x))")
(("1" (rewrite "pi_value" 2)
(("1" (expand "atan" 2 4)
(("1" (assert)
(("1" (expand "atan" -2 2)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (lemma "sqrt_pos" ("px" "1-x*x"))
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (lemma "sq_lt_abs" ("a" "x" "b" "1"))
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals
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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(sq const-decl "nonneg_real" sq "reals/")
(sq_lt_abs formula-decl nil sq "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqrt_pos judgement-tcc nil sqrt "reals/")
(pi_value formula-decl nil atan nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(< const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(>= const-decl "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 nil)
(pi_ub const-decl "posreal" trig_basic nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}"
trig_basic nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(atan const-decl "real_abs_lt_pi2" atan nil)
(nnreal type-eq-decl nil real_types 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/")
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(real_times_real_is_real application-judgement "real" reals
nil))
shostak))
(asin_TCC5 0
(asin_TCC5-1 nil 3262199369
("" (expand "abs")
(("" (skolem!)
(("" (flatten)
(("" (typepred "pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "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 nil)
(< const-decl "bool" reals nil)
(pi_ub const-decl "posreal" trig_basic nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}"
trig_basic nil))
shostak))
(asin_neg_restrict_TCC1 0
(asin_neg_restrict_TCC1-1 nil 3262231650
("" (skolem!)
(("" (typepred "nx!1")
(("" (expand "abs")
(("" (lemma "sq_le_abs" ("a" "-nx!1" "b" "1"))
(("" (grind) nil nil)) nil))
nil))
nil))
nil)
((< const-decl "bool" reals nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(sq const-decl "nonneg_real" sq "reals/")
(sq_le_abs formula-decl nil sq "reals/")
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(asin_neg_restrict_TCC2 0
(asin_neg_restrict_TCC2-1 nil 3262231879 ("" (grind) nil nil)
nil shostak))
(asin_neg_restrict 0
(asin_neg_restrict-2 nil 3322498655
("" (skolem 1 ("nx"))
(("" (typepred "nx")
(("" (expand "<=")
(("" (expand "asin")
(("" (split -1)
(("1" (assert)
(("1"
(lemma "both_sides_times_neg_lt1"
("nz" "-1" "x" "nx" "y" "-1"))
(("1"
(lemma "lt_times_lt_neg1"
("x" "-1" "ny" "nx" "z" "-1" "npw" "nx"))
(("1" (assert)
(("1"
(lemma "sqrt_lt"
("nny" "0" "nnz" "1-nx*nx"))
(("1" (rewrite "sqrt_0" -1)
(("1"
(lemma
"atan_inv_neg"
("nx" "sqrt(1 - nx * nx) / nx"))
(("1"
(rewrite "pi_value" 1)
(("1"
(lemma
"div_div1"
("x"
"1"
"n0y"
"sqrt(1-nx*nx)"
"n0z"
"nx"))
(("1"
(replace -1 -2)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma
"both_sides_div_neg_lt1"
("y"
"0"
"x"
"sqrt(1-nx*nx)"
"nz"
"nx"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "nx = -1")
(("1" (replace -1)
(("1" (rewrite "sqrt_0")
(("1" (rewrite "atan_0")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((< const-decl "bool" reals nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(asin const-decl "real_abs_le_pi2" asin nil)
(atan_0 formula-decl nil atan nil)
(int_times_even_is_even application-judgement "even_int"
integers nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(real_div_nzreal_is_real application-judgement "real" reals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_times_lt_neg1 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_lt formula-decl nil sqrt "reals/")
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(atan_inv_neg formula-decl nil atan nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(div_div1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(pi_value formula-decl nil atan nil)
(both_sides_div_neg_lt1 formula-decl nil real_props nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(odd_times_odd_is_odd application-judgement "odd_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(both_sides_times_neg_lt1 formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals
nil))
nil))
(asin_pos_restrict_TCC1 0
(asin_pos_restrict_TCC1-1 nil 3262251224
("" (skosimp*)
(("" (typepred "px!1")
(("" (expand "abs")
((""
(lemma "le_times_le_pos"
("nnx" "px!1" "y" "1" "nnz" "px!1" "w" "1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((< const-decl "bool" reals nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(real_times_real_is_real application-judgement "real" reals
nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
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)
(le_times_le_pos formula-decl nil real_props nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil))
shostak))
(asin_pos_restrict_TCC2 0
(asin_pos_restrict_TCC2-1 nil 3262251224 ("" (grind) nil nil)
nil shostak))
(asin_pos_restrict 0
(asin_pos_restrict-1 nil 3408901117
("" (skolem 1 ("px"))
(("" (case "abs(px) <= 1")
(("1" (expand "<=")
(("1" (split -1)
(("1" (expand "asin")
(("1" (assert)
(("1" (lemma "sq_nz_pos" ("nz" "px"))
(("1" (expand "sq")
(("1"
(lemma "lt_times_lt_pos1"
("px" "px" "y" "1" "nnz" "px" "w" "1"))
(("1" (assert)
(("1"
(lemma "sqrt_lt"
("nny" "0" "nnz" "1-px*px"))
(("1" (rewrite "sqrt_0")
(("1"
(lemma
"atan_inv"
("px" "sqrt(1 - px * px) / px"))
(("1"
(lemma
"div_div1"
("x"
"1"
"n0y"
"sqrt(1-px*px)"
"n0z"
"px"))
(("1"
(replace -1 -2)
(("1"
(rewrite "pi_value" 1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma
"posreal_div_posreal_is_posreal"
("px" "sqrt(1-px*px)" "py" "px"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "asin")
(("2" (assert)
(("2" (lift-if)
(("2" (expand "abs")
(("2" (assert)
(("2" (replace -1)
(("2" (assert)
(("2" (rewrite "atan_0")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "px")
(("2" (hide 2) (("2" (grind) nil nil)) nil)) nil))
nil))
nil)
((< const-decl "bool" reals nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(real_div_nzreal_is_real application-judgement "real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(posreal_div_posreal_is_posreal judgement-tcc nil real_types
nil)
(div_div1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(pi_value formula-decl nil atan nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_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)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(atan_inv formula-decl nil atan nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(sqrt_lt formula-decl nil sqrt "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(lt_times_lt_pos1 formula-decl nil real_props nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(sq_nz_pos judgement-tcc nil sq "reals/")
(asin const-decl "real_abs_le_pi2" asin nil)
(atan_0 formula-decl nil atan nil)
(int_times_even_is_even application-judgement "even_int"
integers nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(odd_minus_odd_is_even application-judgement "even_int"
integers nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_times_real_is_real application-judgement "real" reals
nil))
nil)
(asin_pos_restrict-2 nil 3322498693
("" (skolem 1 ("px"))
(("" (typepred "px")
(("" (expand "abs" -1)
(("" (expand "<=" -1)
(("" (split -1)
(("1" (expand "asin")
(("1" (assert)
(("1" (lemma "sq_nz_pos" ("nz" "px"))
(("1" (expand "sq")
(("1"
(lemma "lt_times_lt_pos1"
("px" "px" "y" "1" "nnz" "px" "w" "1"))
(("1" (assert)
(("1"
(lemma
"sqrt_lt"
("nny" "0" "nnz" "1-px*px"))
(("1"
(rewrite "sqrt_0")
(("1"
(lemma
"atan_inv_value"
("px" "sqrt(1 - px * px) / px"))
(("1"
(lemma
"div_div1"
("x"
"1"
"n0y"
"sqrt(1-px*px)"
"n0z"
"px"))
(("1"
(replace -1 -2)
(("1"
(rewrite "pi_value" 1)
(("1"
(expand "atan" 1)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"posreal_div_posreal_is_posreal"
("px" "sqrt(1-px*px)" "py" "px"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "asin")
(("2" (replace -1)
(("2" (hide -1 -2)
(("2" (rewrite "sqrt_0")
(("2" (rewrite "atan_0")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq "reals/")
(sqrt_0 formula-decl nil sqrt "reals/")
(pi_value formula-decl nil atan nil)
(atan const-decl "real_abs_lt_pi2" atan nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(sqrt_lt formula-decl nil sqrt "reals/")
(sq_nz_pos judgement-tcc nil sq "reals/")
(atan_0 formula-decl nil atan nil))
nil))
(asin_0 0
(asin_0-1 nil 3262232045
("" (expand "asin")
(("" (rewrite "sqrt_1") (("" (rewrite "atan_0") nil nil))
nil))
nil)
((sqrt_1 formula-decl nil sqrt "reals/")
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(atan_0 formula-decl nil atan nil)
(asin const-decl "real_abs_le_pi2" asin nil))
shostak))
(asin_sqrt_half_TCC1 0
(asin_sqrt_half_TCC1-1 nil 3263820156
("" (expand "abs")
(("" (typepred "sqrt(1/2)")
(("" (assert)
(("" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1"))
(("" (rewrite "sqrt_1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_le_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)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(sqrt_le formula-decl nil sqrt "reals/")
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "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 "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(> const-decl "bool" reals nil))
shostak))
(asin_sqrt_half 0
(asin_sqrt_half-2 nil 3322498751
("" (expand "asin")
(("" (typepred "sqrt(1/2)")
(("" (lemma "sqrt_lt" ("nny" "1/2" "nnz" "1"))
(("" (rewrite "sqrt_1" -1)
(("" (assert)
(("" (rewrite "sq_rew" 1)
(("" (rewrite "div_simp" 1)
(("" (rewrite "pi_value") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((> const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal 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)
(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)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sq_rew formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_sqrt formula-decl nil sqrt "reals/")
(pi_value formula-decl nil atan nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(real_div_nzreal_is_real application-judgement "real" reals
nil)
(div_simp formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(sqrt_lt formula-decl nil sqrt "reals/")
(asin const-decl "real_abs_le_pi2" asin nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/"))
nil))
(asin_1 0
(asin_1-1 nil 3262276037
("" (expand "asin") (("" (propax) nil nil)) nil)
((asin const-decl "real_abs_le_pi2" asin nil)) shostak))
(asin_neg_TCC1 0
(asin_neg_TCC1-1 nil 3262231915 ("" (grind) nil nil) nil
shostak))
(asin_neg 0
(asin_neg-1 nil 3262232085
("" (skolem 1 ("x"))
(("" (expand "asin")
(("" (case "x = -1")
(("1" (assert) nil nil)
("2" (case "x = 1")
(("1" (assert) nil nil)
("2" (case "-1 < x & x < 1")
(("1" (flatten -1)
(("1" (assert)
(("1"
(lemma "atan_neg" ("x" "x / sqrt(1 - -x * -x)"))
(("1" (assert) nil nil)
("2" (hide 4)
(("2" (lemma "asin_TCC3" ("x" "x"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 4)
(("2" (assert)
(("2" (typepred "x") (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(asin const-decl "real_abs_le_pi2" asin 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)
(nnreal 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, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(atan_neg formula-decl nil atan nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals
nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(< const-decl "bool" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types 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)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(real_abs_le1 nonempty-type-eq-decl nil asin nil))
shostak))
(asin_minus1 0
(asin_minus1-1 nil 3262276084
("" (expand "asin") (("" (propax) nil nil)) nil)
((asin const-decl "real_abs_le_pi2" asin nil)) shostak))
(asin_minus_sqrt_half_TCC1 0
(asin_minus_sqrt_half_TCC1-1 nil 3263821369
("" (expand "abs")
(("" (typepred "sqrt(1/2)")
(("" (assert)
(("" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1"))
(("" (rewrite "sqrt_1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_le_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)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(sqrt_le formula-decl nil sqrt "reals/")
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "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 "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(> const-decl "bool" reals nil))
shostak))
(asin_minus_sqrt_half 0
(asin_minus_sqrt_half-1 nil 3263819795
("" (lemma "asin_sqrt_half")
(("" (rewrite "asin_neg" 1)
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (expand "abs")
(("2" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1"))
(("2" (rewrite "sqrt_1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(asin_neg formula-decl nil asin 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)
(real_abs_le1 nonempty-type-eq-decl nil asin 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt
"reals/")
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(asin_sqrt_half formula-decl nil asin nil))
shostak))
(asin_strict_increasing 0
(asin_strict_increasing-3 nil 3322498826
("" (lemma "atan_strict_increasing")
(("" (expand "strict_increasing?")
(("" (skolem 1 ("x" "y"))
(("" (flatten)
(("" (expand "asin")
(("" (case "abs(x) <= 1")
(("1" (case "abs(y) <= 1")
(("1"
(case "FORALL (z:real): abs(z) < 1 => 0 < sqrt(1-z*z)")
(("1" (expand "<=" (-2 -3))
(("1" (split -3)
(("1" (inst-cp -2 "x")
(("1" (assert)
(("1"
(case "y = -1")
(("1"
(hide 1)
(("1"
(lemma "trichotomy" ("x" "x"))
(("1"
(split -1)
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3"
(expand "abs" -3)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(case "y < 1")
(("1"
(assert)
(("1"
(case "x= -1")
(("1" (assert) nil nil)
("2"
(expand "abs" -3)
(("2"
(assert)
(("2"
(inst -3 "y")
(("2"
(split -5)
(("1"
(assert)
(("1"
(inst
-
"x / sqrt(1 - x * x)"
"y / sqrt(1 - y * y)")
(("1"
(split -6)
(("1"
(propax)
nil
nil)
("2"
(hide 4)
(("2"
(lemma
"div_mult_pos_lt1"
("z"
"x"
"py"
"sqrt(1-x*x)"
"x"
"y / sqrt(1 - y * y)"))
(("2"
(replace
-1
1)
(("2"
(lemma
"div_mult_pos_lt2"
("x"
"x"
"z"
"y*sqrt(1-x*x)"
"py"
"sqrt(1-y*y)"))
(("1"
(replace
-1
1)
(("1"
(hide
-1
-2)
(("1"
(lemma
"trichotomy"
("x"
"x"))
(("1"
(split
-1)
(("1"
(lemma
"sq_lt"
("nna"
"x * sqrt(1 - y * y)"
"nnb"
"y * sqrt(1 - x * x)"))
(("1"
(replace
-1
1
rl)
(("1"
(rewrite
"sq_times"
1)
(("1"
(rewrite
"sq_times"
1)
(("1"
(expand
"sq"
1)
(("1"
(lemma
"sq_lt"
("nna"
"x"
"nnb"
"y"))
(("1"
(expand
"sq"
-1)
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"y"
"py"
"sqrt(1-x*x)"))
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil)
("3"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"x"
"py"
"sqrt(1-y*y)"))
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(replace
-1)
(("2"
(rewrite
"sqrt_1"
1)
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(case
"y < 0")
(("1"
(lemma
"both_sides_times_neg_lt1"
("nz"
"-1"
"y"
"x * sqrt(1 - y * y)"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.65 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.
|
