|
(acos (nnreal_le_pi_TCC1 0
(nnreal_le_pi_TCC1-1 nil 3262275870 ("" (assert) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(acos_TCC1 0
(acos_TCC1-1 nil 3262275879
("" (skolem 1 ("x"))
(("" (typepred "asin(x)")
(("" (expand "abs" -1)
(("" (case "asin(x) < 0")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((asin const-decl "real_abs_le_pi2" asin nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}"
trig_basic nil)
(pi_ub const-decl "posreal" trig_basic nil)
(< const-decl "bool" reals nil)
(pi_lb const-decl "posreal" trig_basic nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= 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_minus_real_is_real application-judgement "real" reals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" 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_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(acos_neg_TCC1 0
(acos_neg_TCC1-1 nil 3262871574 ("" (grind) nil nil) nil
shostak))
(acos_neg 0
(acos_neg-1 nil 3262871521
("" (skolem 1 ("x"))
(("" (expand "acos")
(("" (rewrite "asin_neg") (("" (assert) nil nil)) nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(acos const-decl "nnreal_le_pi" acos nil)
(real_plus_real_is_real application-judgement "real" reals
nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(asin_neg formula-decl nil asin nil))
shostak))
(acos_0 0
(acos_0-1 nil 3262276429
("" (expand "acos")
(("" (rewrite "asin_0") (("" (assert) nil nil)) nil)) nil)
((asin_0 formula-decl nil asin nil)
(int_times_even_is_even application-judgement "even_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(acos const-decl "nnreal_le_pi" acos nil))
shostak))
(acos_sqrt_half_TCC1 0
(acos_sqrt_half_TCC1-1 nil 3263920337
("" (expand "abs")
(("" (typepred "sqrt(1/2)")
(("" (assert)
(("" (lemma "sq_le" ("nna" "sqrt(1/2)" "nnb" "1"))
(("" (rewrite "sq_sqrt")
(("" (expand "sq" -1) (("" (propax) nil 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)
(sq_sqrt formula-decl nil sqrt "reals/")
(sq const-decl "nonneg_real" sq "reals/")
(sq_le formula-decl nil sq "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))
(acos_sqrt_half 0
(acos_sqrt_half-1 nil 3263920536
("" (expand "acos")
(("" (rewrite "asin_sqrt_half") (("" (assert) nil nil)) nil))
nil)
((asin_sqrt_half formula-decl nil asin nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(acos const-decl "nnreal_le_pi" acos nil))
shostak))
(acos_1 0
(acos_1-1 nil 3262276459
("" (expand "acos")
(("" (rewrite "asin_1") (("" (assert) nil nil)) nil)) nil)
((asin_1 formula-decl nil asin nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(acos const-decl "nnreal_le_pi" acos nil))
shostak))
(acos_minus1 0
(acos_minus1-1 nil 3262276496
("" (expand "acos")
(("" (rewrite "asin_minus1") (("" (assert) nil nil)) nil))
nil)
((asin_minus1 formula-decl nil asin 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_minus_real_is_real application-judgement "real" reals
nil)
(acos const-decl "nnreal_le_pi" acos nil))
shostak))
(acos_minus_sqrt_half_TCC1 0
(acos_minus_sqrt_half_TCC1-1 nil 3263920463
("" (lemma "acos_sqrt_half_TCC1") (("" (grind) nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(acos_sqrt_half_TCC1 subtype-tcc nil acos nil))
shostak))
(acos_minus_sqrt_half 0
(acos_minus_sqrt_half-1 nil 3263920585
("" (expand "acos")
(("" (rewrite "asin_minus_sqrt_half") (("" (assert) nil nil))
nil))
nil)
((asin_minus_sqrt_half formula-decl nil asin nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(posreal_times_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_minus_real_is_real application-judgement "real" reals
nil)
(acos const-decl "nnreal_le_pi" acos nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/"))
shostak))
(acos_strict_decreasing 0
(acos_strict_decreasing-1 nil 3262276758
("" (expand "strict_decreasing?")
(("" (skolem 1 ("x" "y"))
(("" (flatten)
(("" (expand "acos")
(("" (lemma "asin_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst - "x" "y") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((acos const-decl "nnreal_le_pi" acos nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(asin_strict_increasing formula-decl nil asin nil)
(strict_decreasing? const-decl "bool" real_fun_preds
"reals/"))
shostak))
(acos_bij 0
(acos_bij-1 nil 3262277267
("" (lemma "asin_bij")
(("" (expand "bijective?")
(("" (expand "injective?")
(("" (expand "surjective?")
(("" (expand "acos")
(("" (flatten)
(("" (split 1)
(("1" (skolem 1 ("x" "y"))
(("1" (inst -1 "x" "y")
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (hide -1)
(("2" (skolem 1 ("y"))
(("2" (inst - "pi/2-y")
(("1" (skolem - ("x"))
(("1" (inst + "x")
(("1" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (typepred "y")
(("2"
(expand "abs")
(("2"
(case "pi/2-y<0")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bijective? const-decl "bool" functions nil)
(minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(surjective? const-decl "bool" functions 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)
(real_minus_real_is_real application-judgement "real" 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)
(< 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)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(nnreal type-eq-decl nil real_types nil)
(nnreal_le_pi nonempty-type-eq-decl nil acos nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(real_abs_le1 nonempty-type-eq-decl nil asin nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(acos const-decl "nnreal_le_pi" acos nil)
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(injective? const-decl "bool" functions nil)
(asin_bij formula-decl nil asin nil))
shostak))
(acos_sum_TCC1 0
(acos_sum_TCC1-1 nil 3263920917
("" (skosimp*)
(("" (typepred "nnx!1") (("" (assert) nil nil)) nil)) nil)
((<= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil))
shostak))
(acos_sum_TCC2 0
(acos_sum_TCC2-1 nil 3263920948
("" (skosimp*)
(("" (typepred "nny!1")
(("" (lemma "sq_le" ("nna" "nny!1" "nnb" "1"))
(("" (expand "sq") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((<= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(sq_le formula-decl nil sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil))
shostak))
(acos_sum_TCC3 0
(acos_sum_TCC3-1 nil 3263921002
("" (skosimp*)
(("" (typepred "nnx!1")
(("" (typepred "nny!1")
(("" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1"))
(("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1"))
(("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1"))
(("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1"))
(("" (rewrite "sq_0")
(("" (rewrite "sq_1")
(("" (expand ">=")
(("" (flatten)
(("" (replace -9)
((""
(replace -9)
((""
(replace -9)
((""
(replace -9)
((""
(case "0 <= 1 - sq(nny!1)")
(("1"
(case "0 <= 1 - sq(nnx!1)")
(("1"
(lemma
"sqrt_le"
("nny"
"1 - sq(nny!1)"
"nnz"
"1"))
(("1"
(lemma
"sqrt_le"
("nny"
"1 - sq(nnx!1)"
"nnz"
"1"))
(("1"
(assert)
(("1"
(rewrite "sqrt_1")
(("1"
(typepred
"sqrt(1 - sq(nnx!1)) ")
(("1"
(typepred
"sqrt(1 - sq(nny!1)) ")
(("1"
(hide -2 -4)
(("1"
(lemma
"nnreal_times_nnreal_is_nnreal"
("nnx"
"nnx!1"
"nny"
"nny!1"))
(("1"
(lemma
"nnreal_times_nnreal_is_nnreal"
("nnx"
"sqrt(1 - sq(nnx!1))"
"nny"
"sqrt(1 - sq(nny!1))"))
(("1"
(lemma
"le_times_le_pos"
("nnx"
"sqrt(1 - sq(nny!1))"
"y"
"1"
"nnz"
"sqrt(1 - sq(nnx!1))"
"w"
"1"))
(("1"
(assert)
(("1"
(lemma
"le_times_le_pos"
("nnx"
"nnx!1"
"y"
"1"
"nnz"
"nny!1"
"w"
"1"))
(("1"
(assert)
(("1"
(lemma
"le_minus_le"
("x"
"nnx!1 * nny!1"
"y"
"1"
"w"
"0"
"z"
"(sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1)))"))
(("1"
(lemma
"le_minus_le"
("y"
"nnx!1 * nny!1"
"x"
"0"
"z"
"1"
"w"
"(sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1)))"))
(("1"
(expand
">=")
(("1"
(replace
-3)
(("1"
(replace
-4)
(("1"
(replace
-5)
(("1"
(replace
-6)
(("1"
(expand
"abs"
1)
(("1"
(case
"nnx!1 * nny!1 - (sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1))) < 0")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((<= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq_le formula-decl nil sq "reals/")
(sq_0 formula-decl nil sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqrt_le formula-decl nil sqrt "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sqrt_pos application-judgement "posreal" sqrt "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_1 formula-decl nil sqrt "reals/")
(nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types
nil)
(le_times_le_pos formula-decl nil real_props 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)
(sq_1 formula-decl nil sq "reals/"))
shostak))
(acos_sum 0
(acos_sum-1 nil 3263922185
("" (skosimp*)
(("" (typepred "nnx!1")
(("" (typepred "nny!1")
(("" (expand ">=")
(("" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1"))
(("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1"))
(("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1"))
(("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1"))
(("" (rewrite "sq_0")
(("" (rewrite "sq_1")
(("" (simplify -1)
(("" (simplify -2)
((""
(flatten)
((""
(replace -7)
((""
(replace -8)
((""
(expand "<=" -8)
((""
(split -8)
(("1"
(expand "<=" -7)
(("1"
(split -7)
(("1"
(expand "<=" -8)
(("1"
(split -8)
(("1"
(expand "<=" -8)
(("1"
(split -8)
(("1"
(expand
"acos"
1)
(("1"
(lemma
"div_cancel1"
("x"
"pi"
"n0z"
"2"))
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(hide
-5
-6
-7
-8)
(("1"
(lemma
"sq_lt"
("nna"
"0"
"nnb"
"nnx!1"))
(("1"
(lemma
"sq_lt"
("nna"
"0"
"nnb"
"nny!1"))
(("1"
(lemma
"sq_lt"
("nnb"
"1"
"nna"
"nnx!1"))
(("1"
(lemma
"sq_lt"
("nnb"
"1"
"nna"
"nny!1"))
(("1"
(rewrite
"sq_0")
(("1"
(rewrite
"sq_1")
(("1"
(replace
-5)
(("1"
(replace
-6)
(("1"
(replace
-7)
(("1"
(replace
-8)
(("1"
(simplify)
(("1"
(case
"0 < 1-sq(nnx!1)")
(("1"
(case
"0 < 1-sq(nny!1)")
(("1"
(case
"1-sq(nnx!1)<1")
(("1"
(case
"1-sq(nny!1)<1")
(("1"
(lemma
"sqrt_lt"
("nny"
"0"
"nnz"
"1-sq(nnx!1)"))
(("1"
(lemma
"sqrt_lt"
("nny"
"0"
"nnz"
"1-sq(nny!1)"))
(("1"
(lemma
"sqrt_lt"
("nnz"
"1"
"nny"
"1-sq(nnx!1)"))
(("1"
(lemma
"sqrt_lt"
("nnz"
"1"
"nny"
"1-sq(nny!1)"))
(("1"
(replace
-5)
(("1"
(replace
-6)
(("1"
(replace
-7)
(("1"
(replace
-8)
(("1"
(rewrite
"sqrt_1")
(("1"
(rewrite
"sqrt_0")
(("1"
(simplify)
(("1"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"nnx!1"
"py"
"nny!1"))
(("1"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"sqrt(1 - sq(nny!1))"
"py"
"sqrt(1 - sq(nnx!1))"))
(("1"
(lemma
"lt_times_lt_pos1"
("px"
"nnx!1"
"y"
"1"
"nnz"
"nny!1"
"w"
"1"))
(("1"
(lemma
"lt_times_lt_pos1"
("px"
"sqrt(1 - sq(nny!1))"
"y"
"1"
"nnz"
"sqrt(1 - sq(nnx!1))"
"w"
"1"))
(("1"
(assert)
(("1"
(lemma
"lt_minus_lt1"
("x"
"nnx!1 * nny!1"
"y"
"1"
"w"
"0"
"z"
"sqrt(1 - sq(nny!1)) * sqrt(1 - sq(nnx!1))"))
(("1"
(lemma
"lt_minus_lt1"
("x"
"0"
"y"
"nnx!1 * nny!1"
"w"
"sqrt(1 - sq(nny!1)) * sqrt(1 - sq(nnx!1))"
"z"
"1"))
(("1"
(replace
-3)
(("1"
(expand
">"
-5)
(("1"
(replace
-5)
(("1"
(split
-1)
(("1"
(split
-2)
(("1"
(simplify
(-1
-2))
(("1"
(expand
"asin")
(("1"
(rewrite
"sq_rew"
1)
(("1"
(rewrite
"sq_rew"
1)
(("1"
(lemma
"sq_sqrt"
("x"
"1-sq(nnx!1)"))
(("1"
(lemma
"sq_sqrt"
("x"
"1-sq(nny!1)"))
(("1"
(assert)
(("1"
(name-replace
"SX"
"sqrt(1 - sq(nnx!1))")
(("1"
(name-replace
"SY"
"sqrt(1 - sq(nny!1))")
(("1"
(rewrite
"sq_rew"
1)
(("1"
(case
"1 - sq(nnx!1) * nny!1 * nny!1 - sq(SX) * SY * SY = 1-sq(nnx!1)*sq(nny!1) - sq(SX)*sq(SY)")
(("1"
(replace
-1
1)
(("1"
(simplify
1)
(("1"
(hide
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.56Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
