(tan_quad
(tan_value_def_TCC1 0
(tan_value_def_TCC1-1 nil 3264857198
("" (skosimp*) (("" (typepred "x!1") (("" (assert) nil nil)) nil))
nil)
((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< 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_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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil))
shostak))
(tan_value_def_TCC2 0
(tan_value_def_TCC2-1 nil 3264857222
("" (skosimp*)
(("" (typepred "x!1")
(("" (assert)
(("" (expand "abs")
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< 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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(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)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil))
shostak))
(tan_value_def_TCC3 0
(tan_value_def_TCC3-1 nil 3264857251
("" (skosimp*)
(("" (typepred "x!1")
(("" (lemma "cos_value_strict_decreasing")
(("" (expand "strict_decreasing?")
(("" (inst - "abs(x!1)" "pi/2")
(("" (rewrite "cos_value_pi2")
(("" (assert)
(("" (expand "abs")
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< 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)
(strict_decreasing? const-decl "bool" real_fun_preds "reals/")
(cos_value_pi2 formula-decl nil sincos_quad nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnreal type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(nnreal_le_pi nonempty-type-eq-decl nil acos nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(cos_value_strict_decreasing formula-decl nil sincos_quad nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil))
shostak))
(tan_value_def 0
(tan_value_def-3 nil 3408979579
("" (skosimp*)
(("" (typepred "x!1")
(("" (lemma "atan_bij")
(("" (expand "tan_value")
((""
(lemma "comp_inverse_right[real, real_abs_lt_pi2]"
("f" "atan" "y" "x!1"))
(("1" (expand "bijective?")
(("1" (expand "injective?")
(("1" (flatten)
(("1" (hide -3)
(("1"
(inst - "inverse(atan)(x!1)"
"sin_value(x!1) / cos_value(abs(x!1))")
(("1" (split -2)
(("1" (propax) nil nil)
("2"
(lemma "cos_eqv_sqrt_sin_value"
("q1" "abs(x!1)"))
(("1"
(case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))")
(("1" (replace -1)
(("1"
(replace -3 1)
(("1"
(replace -2 1 rl)
(("1"
(hide -1 -2 -3 2)
(("1"
(lemma
"asin_sin_value"
("xs" "x!1"))
(("1"
(expand "asin")
(("1"
(lemma
"sin_value_strict_increasing")
(("1"
(expand
"strict_increasing?")
(("1"
(inst-cp - "-pi/2" "x!1")
(("1"
(inst - "x!1" "pi/2")
(("1"
(rewrite
"sin_value_pi2")
(("1"
(rewrite
"sin_value_minus_pi2")
(("1"
(case "x!1<0")
(("1"
(assert)
(("1"
(case
"-pi / 2 < x!1")
(("1"
(rewrite
"sq_rew"
-5)
(("1"
(assert)
nil
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite
"sq_rew"
-3)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(expand "abs")
(("2"
(case "x!1<0")
(("1"
(lemma
"sin_value_neg"
("xs" "x!1"))
(("1"
(assert)
(("1"
(replace -1 1)
(("1"
(rewrite "sq_neg" 1)
nil
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "abs")
(("2" (hide 2 3)
(("2"
(ground)
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< 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)
(tan_value const-decl "[real_abs_lt_pi2 -> real]" tan_quad nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(inverse const-decl "D" function_inverse nil)
(<= const-decl "bool" reals nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
sincos_quad nil)
(nnreal type-eq-decl nil real_types nil)
(nnreal_le_pi nonempty-type-eq-decl nil acos nil)
(cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil)
(nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(sq_neg formula-decl nil sq "reals/")
(sin_value_neg formula-decl nil sincos_quad nil)
(asin_sin_value formula-decl nil sincos_quad nil)
(sin_value_strict_increasing formula-decl nil sincos_quad nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(sin_value_pi2 formula-decl nil sincos_quad nil)
(sq_rew formula-decl nil sq "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_value_minus_pi2 formula-decl nil sincos_quad nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(asin const-decl "real_abs_le_pi2" asin nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(injective? const-decl "bool" functions nil)
(atan const-decl "real_abs_lt_pi2" atan nil)
(bijective? const-decl "bool" functions nil)
(comp_inverse_right formula-decl nil function_inverse nil)
(atan_bij formula-decl nil atan nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil))
nil)
(tan_value_def-2 nil 3408966564
("" (skosimp*)
(("" (typepred "x!1")
(("" (lemma "atan_bij")
(("" (expand "tan_value")
((""
(lemma "comp_inverse_right[real, real_abs_lt_pi]"
("f" "atan" "y" "x!1"))
(("1" (expand "bijective?")
(("1" (expand "injective?")
(("1" (flatten)
(("1" (hide -3)
(("1"
(inst - "inverse(atan)(x!1)"
"sin_value(x!1) / cos_value(abs(x!1))")
(("1" (split -2)
(("1" (propax) nil nil)
("2"
(lemma "cos_eqv_sqrt_sin_value"
("q1" "abs(x!1)"))
(("1"
(case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))")
(("1" (replace -1)
(("1"
(replace -3 1)
(("1"
(replace -2 1 rl)
(("1"
(hide -1 -2 -3 2)
(("1"
(lemma
"asin_sin_value"
("xs" "x!1"))
(("1"
(expand "asin")
(("1"
(lemma
"sin_value_strict_increasing")
(("1"
(expand
"strict_increasing?")
(("1"
(inst-cp - "-pi/2" "x!1")
(("1"
(inst - "x!1" "pi/2")
(("1"
(rewrite
"sin_value_pi2")
(("1"
(rewrite
"sin_value_minus_pi2")
(("1"
(case "x!1<0")
(("1"
(assert)
(("1"
(case
"-pi / 2 < x!1")
(("1"
(rewrite
"sq_rew"
-5)
(("1"
(assert)
nil
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite
"sq_rew"
-3)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(expand "abs")
(("2"
(case "x!1<0")
(("1"
(lemma
"sin_value_neg"
("xs" "x!1"))
(("1"
(assert)
(("1"
(replace -1 1)
(("1"
(rewrite "sq_neg" 1)
nil
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "abs")
(("2" (hide 2 3)
(("2"
(ground)
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((atan_bij formula-decl nil atan nil)
(atan const-decl "real_abs_lt_pi2" atan nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(sq const-decl "nonneg_real" sq "reals/")
(asin const-decl "real_abs_le_pi2" asin nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(sin_value_minus_pi2 formula-decl nil sincos_quad nil)
(sq_rew formula-decl nil sq "reals/")
(sin_value_pi2 formula-decl nil sincos_quad nil)
(sin_value_strict_increasing formula-decl nil sincos_quad nil)
(asin_sin_value formula-decl nil sincos_quad nil)
(sin_value_neg formula-decl nil sincos_quad nil)
(sq_neg formula-decl nil sq "reals/")
(nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil)
(cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil)
(cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
nil)
(nnreal_le_pi nonempty-type-eq-decl nil acos nil)
(sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
sincos_quad nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
(pi const-decl "posreal" atan nil))
nil)
(tan_value_def-1 nil 3264857402
("" (skosimp*)
(("" (typepred "x!1")
(("" (lemma "atan_bij")
(("" (expand "tan_value")
((""
(lemma "comp_inverse_right[real, real_mpi_ppi]"
("f" "atan" "y" "x!1"))
(("1" (expand "bijective?")
(("1" (expand "injective?")
(("1" (flatten)
(("1" (hide -3)
(("1"
(inst - "inverse(atan)(x!1)"
"sin_value(x!1) / cos_value(abs(x!1))")
(("1" (split -2)
(("1" (propax) nil nil)
("2"
(lemma "cos_eqv_sqrt_sin_value"
("q1" "abs(x!1)"))
(("1"
(case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))")
(("1" (replace -1)
(("1"
(replace -3 1)
(("1"
(replace -2 1 rl)
(("1"
(hide -1 -2 -3 2)
(("1"
(lemma
"asin_sin_value"
("xs" "x!1"))
(("1"
(expand "asin")
(("1"
(lemma
"sin_value_strict_increasing")
(("1"
(expand
"strict_increasing?")
(("1"
(inst-cp - "-pi/2" "x!1")
(("1"
(inst - "x!1" "pi/2")
(("1"
(rewrite
"sin_value_pi2")
(("1"
(rewrite
"sin_value_minus_pi2")
(("1"
(case "x!1<0")
(("1"
(assert)
(("1"
(case
"-pi / 2 < x!1")
(("1"
(rewrite
"sq_rew"
-5)
(("1"
(assert)
nil
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite
"sq_rew"
-3)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(expand "abs")
(("2"
(case "x!1<0")
(("1"
(lemma
"sin_value_neg"
("xs" "x!1"))
(("1"
(assert)
(("1"
(replace -1 1)
(("1"
(rewrite "sq_neg" 1)
nil
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "abs")
(("2" (hide 2 3)
(("2"
(ground)
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((atan_bij formula-decl nil atan nil)
(atan_value const-decl "real" atan nil)
(atan const-decl "real_abs_lt_pi2" atan nil)
(sq const-decl "nonneg_real" sq "reals/")
(asin const-decl "real_abs_le_pi2" asin nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(sin_value_minus_pi2 formula-decl nil sincos_quad nil)
(sq_rew formula-decl nil sq "reals/")
(sin_value_pi2 formula-decl nil sincos_quad nil)
(sin_value_strict_increasing formula-decl nil sincos_quad nil)
(asin_sin_value formula-decl nil sincos_quad nil)
(sin_value_neg formula-decl nil sincos_quad nil)
(sq_neg formula-decl nil sq "reals/")
(nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil)
(cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil)
(cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
nil)
(nnreal_le_pi nonempty-type-eq-decl nil acos nil)
(sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
sincos_quad nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
(pi const-decl "posreal" atan nil))
shostak))
(tan_value_0_TCC1 0
(tan_value_0_TCC1-1 nil 3264857350
("" (assert) (("" (assert) nil nil)) 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)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil))
shostak))
(tan_value_0 0
(tan_value_0-1 nil 3264858476
("" (lemma "tan_value_def" ("x" "0"))
(("1" (rewrite "sin_value_0")
(("1" (expand "abs")
(("1" (rewrite "cos_value_0") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "abs") (("2" (assert) nil nil)) nil))
nil)
((sin_value_0 formula-decl nil sincos_quad nil)
(cos_value_0 formula-decl nil sincos_quad nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(tan_value_def formula-decl nil tan_quad nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(>= 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 const-decl "posreal" atan nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil))
shostak))
(tan_value_pi4_TCC1 0
(tan_value_pi4_TCC1-1 nil 3264857364
("" (expand "abs")
(("" (typepred "pi") (("" (assert) 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_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)
(pi const-decl "posreal" atan nil))
shostak))
(tan_value_pi4 0
(tan_value_pi4-1 nil 3264858541
("" (lemma "tan_value_def" ("x" "pi/4"))
(("1" (rewrite "sin_value_pi4")
(("1" (expand "abs")
(("1" (assert)
(("1" (rewrite "cos_value_pi4")
(("1" (rewrite "div_simp" -1) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "abs" 1)
(("2" (typepred "pi") (("2" (assert) nil nil)) nil)) nil))
nil)
((sin_value_pi4 formula-decl nil sincos_quad nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(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)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_simp formula-decl nil real_props nil)
(cos_value_pi4 formula-decl nil sincos_quad nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(tan_value_def formula-decl nil tan_quad nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(>= 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 const-decl "posreal" atan nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil))
shostak)))
¤ Dauer der Verarbeitung: 0.21 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.
|