|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
FOLP.thy
Sprache: PVS
Original von: PVS©
|
|
(atan2
(atan2_TCC1 0
(atan2_TCC1-1 nil 3269553691 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(/= const-decl "boolean" notequal nil))
shostak))
(atan2_TCC2 0
(atan2_TCC2-1 nil 3269553735 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(/= const-decl "boolean" notequal nil))
shostak))
(atan2_TCC3 0
(atan2_TCC3-1 nil 3269553749 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil))
shostak))
(atan2_0_2pi_TCC1 0
(atan2_0_2pi_TCC1-1 nil 3269553757 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil))
shostak))
(atan2_0_2pi_TCC2 0
(atan2_0_2pi_TCC2-1 nil 3269553764 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(/= const-decl "boolean" notequal nil)
(Integral const-decl "real" integral_def "analysis/")
(atan_value const-decl "real" atan nil)
(atan const-decl "real_abs_lt_pi2" atan nil)
(pi const-decl "posreal" atan nil)
(atan2 const-decl "real" atan2 nil))
shostak))
(atan2_0_2pi_TCC3 0
(atan2_0_2pi_TCC3-1 nil 3269553778
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(atan2_0_2pi_TCC4 0
(atan2_0_2pi_TCC4-1 nil 3269554070
("" (skosimp*) (("" (assert) nil nil)) 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))
shostak))
(atan2_0_2pi 0
(atan2_0_2pi-1 nil 3269554130
("" (skosimp*)
(("" (lemma "trichotomy" ("x" "x!1"))
(("" (expand "atan2")
(("" (split -1)
(("1" (assert)
(("1" (lemma "trichotomy" ("x" "y!1"))
(("1" (split -1)
(("1" (assert)
(("1" (typepred "atan(y!1 / x!1)")
(("1" (expand "pi")
(("1" (expand "pi")
(("1" (lemma "atan_strict_increasing")
(("1" (expand "strict_increasing?")
(("1" (inst - "0" "y!1/x!1")
(("1"
(lemma
"posreal_div_posreal_is_posreal"
("px" "y!1" "py" "x!1"))
(("1"
(assert)
(("1"
(rewrite "atan_0")
(("1"
(expand "abs")
(("1"
(assert)
(("1"
(expand "atan")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (assert)
(("2" (rewrite "atan_0") (("2" (assert) nil nil))
nil))
nil))
nil)
("3" (assert)
(("3" (lemma "atan_strict_increasing")
(("3" (expand "strict_increasing?")
(("3" (typepred "atan(y!1 / x!1)")
(("3" (inst - "y!1/x!1" "0")
(("3"
(lemma "both_sides_div_pos_gt1"
("x" "0" "y" "y!1" "pz" "x!1"))
(("3" (assert)
(("3"
(rewrite "atan_0")
(("3"
(expand "abs")
(("3"
(assert)
(("3"
(expand "pi")
(("3"
(expand "pi")
(("3"
(expand "atan")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (assert)
(("2" (lemma "trichotomy" ("x" "y!1"))
(("2" (split -1)
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (assert)
(("3" (hide -2)
(("3" (lemma "trichotomy" ("x" "y!1"))
(("3" (split -1)
(("1" (assert)
(("1" (lemma "both_sides_div_neg_gt1")
(("1" (inst - "x!1" "0" "y!1")
(("1" (assert)
(("1" (lemma "atan_strict_increasing")
(("1" (expand "strict_increasing?")
(("1"
(inst - "y!1/x!1" "0")
(("1"
(rewrite "atan_0")
(("1"
(typepred "atan(y!1/x!1)")
(("1"
(expand "abs")
(("1"
(assert)
(("1"
(assert)
(("1"
(expand "pi")
(("1"
(expand "pi")
(("1"
(expand "atan")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (replace -1)
(("2" (rewrite "atan_0") (("2" (assert) nil nil))
nil))
nil))
nil)
("3"
(lemma "negreal_div_negreal_is_posreal"
("nx" "y!1" "ny" "x!1"))
(("1" (lemma "atan_strict_increasing")
(("1" (expand "strict_increasing?")
(("1" (inst - "0" "y!1/x!1")
(("1" (rewrite "atan_0")
(("1" (assert)
(("1"
(typepred "atan(y!1/x!1)")
(("1"
(expand "abs")
(("1"
(expand "pi")
(("1"
(expand "pi")
(("1"
(expand "atan")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(trichotomy formula-decl nil real_axioms nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_div_pos_gt1 formula-decl nil real_props nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(atan_0 formula-decl nil atan nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(atan_strict_increasing formula-decl nil atan nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(atan const-decl "real_abs_lt_pi2" atan 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(both_sides_div_neg_gt1 formula-decl nil real_props nil)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(negreal_div_negreal_is_posreal judgement-tcc nil real_types nil)
(atan2 const-decl "real" atan2 nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
shostak))
(atan2_ge_0_lt_2pi_TCC1 0
(atan2_ge_0_lt_2pi_TCC1-1 nil 3269553812 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil))
shostak))
(atan2_ge_0_lt_2pi 0
(atan2_ge_0_lt_2pi-1 nil 3269552776
("" (skosimp*)
(("" (lemma "atan2_0_2pi" ("x" "x!1" "y" "y!1"))
(("" (replace -2 -1)
(("" (flatten -1)
(("" (lemma "trichotomy" ("x" "x!1"))
(("" (split -1)
(("1" (assert)
(("1" (hide -3 -4 -6)
(("1" (case "y!1>=0")
(("1" (assert)
(("1" (flatten -3) (("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2" (flatten -3) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (lemma "trichotomy" ("x" "y!1"))
(("2" (split -1)
(("1" (assert)
(("1" (flatten (-3 -4)) (("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil)
("3" (assert)
(("3" (flatten (-5 -6)) (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert)
(("3" (hide -2 -5 -6)
(("3" (case "y!1>=0")
(("1" (assert)
(("1" (flatten -3) (("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2" (flatten -3) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(atan2_0_2pi formula-decl nil atan2 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)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(trichotomy formula-decl nil real_axioms nil))
nil))
(nnreal_lt_2pi_TCC1 0
(nnreal_lt_2pi_TCC1-1 nil 3414423407
("" (inst + "0") (("" (assert) nil nil)) 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(atan2_TCC4 0
(atan2_TCC4-1 nil 3414423407
("" (skosimp*)
(("" (typepred "y!1")
(("" (rewrite "atan2_ge_0_lt_2pi") (("" (ground) nil nil)) nil))
nil))
nil)
((/= const-decl "boolean" notequal 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 "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(IMPLIES 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(atan2_ge_0_lt_2pi formula-decl nil atan2 nil))
nil))
(atan2_cancel_pos_TCC1 0
(atan2_cancel_pos_TCC1-1 nil 3269628375
("" (skosimp*)
(("" (assert)
(("" (split -1)
(("1"
(lemma "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "pz!1"))
(("1" (assert) nil nil)) nil)
("2"
(lemma "both_sides_times1" ("x" "y!1" "y" "0" "n0z" "pz!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals 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)
(bool nonempty-type-eq-decl nil booleans nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(both_sides_times1 formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(atan2_cancel_pos 0
(atan2_cancel_pos-1 nil 3269616367
("" (skosimp*)
(("" (expand "atan2")
((""
(lemma "both_sides_times_pos_gt1"
("x" "x!1" "y" "0" "pz" "pz!1"))
(("" (replace -1)
(("" (case "x!1>0")
(("1" (assert)
(("1"
(lemma "both_sides_times_pos_ge1"
("x" "y!1" "y" "0" "pz" "pz!1"))
(("1" (replace -1)
(("1" (case "y!1>=0")
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "x!1=0")
(("1" (assert)
(("1"
(lemma "both_sides_times_pos_gt1"
("x" "y!1" "y" "0" "pz" "pz!1"))
(("1" (replace -1) (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(atan2 const-decl "real" atan2 nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(both_sides_times_pos_ge1 formula-decl nil real_props nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil))
shostak))
(atan2_cancel_neg_TCC1 0
(atan2_cancel_neg_TCC1-1 nil 3269628375
("" (skosimp*)
(("" (lemma "both_sides_times1" ("x" "y!1" "y" "0" "n0z" "nz!1"))
(("" (lemma "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "nz!1"))
(("" (assert) nil nil)) nil))
nil))
nil)
((negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(both_sides_times1 formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(atan2_cancel_neg 0
(atan2_cancel_neg-1 nil 3269628659
("" (skosimp*)
(("" (expand "atan2")
(("" (lemma "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "nz!1"))
(("" (replace -1)
(("" (case "y!1=0")
(("1" (replace -1)
(("1" (rewrite "atan_0")
(("1" (simplify 1)
(("1" (case "x!1>0")
(("1" (assert)
(("1"
(lemma "both_sides_times_neg_lt1"
("x" "x!1" "y" "0" "nz" "nz!1"))
(("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2"
(lemma "both_sides_times_neg_lt1"
("x" "x!1" "y" "0" "nz" "nz!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "y!1>0")
(("1" (hide -2)
(("1" (assert)
(("1"
(lemma "both_sides_times_neg_gt1"
("x" "0" "y" "y!1" "nz" "nz!1"))
(("1" (assert)
(("1" (case "x!1>0")
(("1" (assert)
(("1"
(lemma "both_sides_times_neg_gt1"
("x" "0" "y" "x!1" "nz" "nz!1"))
(("1" (assert) nil nil)) nil))
nil)
("2"
(lemma "both_sides_times_neg_gt1"
("x" "0" "y" "x!1" "nz" "nz!1"))
(("2" (assert)
(("2"
(case "x!1=0")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "x!1=0")
(("1" (assert)
(("1"
(lemma "both_sides_times_neg_gt1"
("x" "0" "y" "y!1" "nz" "nz!1"))
(("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2" (case "x!1>0")
(("1" (assert)
(("1"
(lemma "both_sides_times_neg_gt1"
("x" "0" "y" "x!1" "nz" "nz!1"))
(("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2"
(lemma "both_sides_times_neg_gt1"
("y" "0" "x" "x!1" "nz" "nz!1"))
(("2" (assert)
(("2"
(lemma
"both_sides_times_neg_gt1"
("y" "0" "x" "y!1" "nz" "nz!1"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(atan2 const-decl "real" atan2 nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(both_sides_times_neg_gt1 formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(both_sides_times_neg_lt1 formula-decl nil real_props nil)
(> const-decl "bool" reals nil) (atan_0 formula-decl nil atan nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(both_sides_times1 formula-decl nil real_props 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)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil))
shostak))
(atan2_swap_pos_TCC1 0
(atan2_swap_pos_TCC1-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(/= const-decl "boolean" notequal nil))
nil))
(atan2_swap_pos_TCC2 0
(atan2_swap_pos_TCC2-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(atan2_swap_pos_TCC3 0
(atan2_swap_pos_TCC3-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(atan2_swap_pos_TCC4 0
(atan2_swap_pos_TCC4-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(atan2_swap_pos 0
(atan2_swap_pos-1 nil 3514306980
("" (skeep)
(("" (case "x > 0 AND y > 0")
(("1" (flatten)
(("1" (hide -3)
(("1" (expand "atan2")
(("1" (assert)
(("1" (lemma "atan_sub_swap")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (case "x < 0 AND y < 0")
(("1" (flatten)
(("1" (hide -3 1)
(("1" (expand "atan2")
(("1" (assert)
(("1" (lemma "atan_sub_swap")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 3) (("2" (grind-reals) nil nil)) nil))
nil))
nil))
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)
(AND const-decl "[bool, 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)
(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_div_nzreal_is_real application-judgement "real" 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)
(atan_sub_swap formula-decl nil atan nil)
(atan2 const-decl "real" atan2 nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(pos_times_gt formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil))
shostak))
(atan2_swap_neg_TCC1 0
(atan2_swap_neg_TCC1-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(/= const-decl "boolean" notequal nil))
nil))
(atan2_swap_neg_TCC2 0
(atan2_swap_neg_TCC2-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(atan2_swap_neg_TCC3 0
(atan2_swap_neg_TCC3-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(atan2_swap_neg_TCC4 0
(atan2_swap_neg_TCC4-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(atan2_swap_neg 0
(atan2_swap_neg-1 nil 3514307142
("" (skeep)
(("" (case "x > 0 AND y < 0")
(("1" (hide -2)
(("1" (flatten)
(("1" (expand "atan2")
(("1" (assert)
(("1" (expand "sign")
(("1" (lemma "atan_sub_swap")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "x < 0 AND y > 0")
(("1" (hide -2 1)
(("1" (flatten)
(("1" (expand "sign")
(("1" (assert)
(("1" (expand "atan2")
(("1" (lemma "atan_sub_swap")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3) (("2" (grind-reals) nil nil)) nil))
nil))
nil))
nil)
((< const-decl "bool" reals 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)
(AND const-decl "[bool, 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)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(atan_sub_swap formula-decl nil atan nil)
(sign const-decl "Sign" sign "reals/")
(atan2 const-decl "real" atan2 nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(neg_times_lt formula-decl nil real_props nil)
(nil application-judgement "nnreal_lt_2pi" atan2 nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
shostak))
(atan2_swap_zero_TCC1 0
(atan2_swap_zero_TCC1-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil))
nil))
(atan2_swap_zero_TCC2 0
(atan2_swap_zero_TCC2-1 nil 3514306973 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(Integral const-decl "real" integral_def "analysis/")
(atan_value const-decl "real" atan nil)
(pi const-decl "posreal" atan nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nil application-judgement "nnreal_lt_2pi" atan2 nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(atan2_swap_zero 0
(atan2_swap_zero-1 nil 3514307173
("" (skeep)
(("" (lemma "atan_0")
(("" (split)
(("1" (flatten)
(("1" (replaces -1)
(("1" (case "y > 0")
(("1" (expand "atan2") (("1" (assert) nil nil)) nil)
("2" (expand "atan2") (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replaces -1)
(("2" (case "x > 0")
(("1" (expand "atan2") (("1" (assert) nil nil)) nil)
("2" (expand "atan2") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((atan_0 formula-decl nil atan nil)
(real_minus_real_is_real application-judgement "real" 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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(atan2 const-decl "real" atan2 nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(nil application-judgement "nnreal_lt_2pi" atan2 nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
shostak))
(atan2_cos_sin_TCC1 0
(atan2_cos_sin_TCC1-1 nil 3269553823
("" (skosimp*)
(("" (typepred "a!1")
(("" (lemma "sin_eq_0_2pi" ("a" "a!1"))
(("" (lemma "cos_eq_0_2pi" ("a" "a!1"))
(("" (assert)
(("" (split -1)
(("1" (split -2)
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (split -2)
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(cos_eq_0_2pi formula-decl nil trig_basic nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types 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)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sin_eq_0_2pi formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
shostak))
(atan2_cos_sin 0
(atan2_cos_sin-2 nil 3279154016
("" (case "FORALL (x:posreal): x < pi => sin(x) > 0")
(("1"
(case "FORALL (x: nnreal): x < pi => atan2(cos(x), sin(x)) = x")
(("1" (skolem 1 ("a"))
(("1" (case "a < pi")
(("1" (inst -2 "a") (("1" (assert) nil nil)) nil)
("2" (inst -1 "a-pi")
(("1" (assert)
(("1" (rewrite "cos_minus")
(("1" (rewrite "sin_minus")
(("1" (rewrite "sin_pi")
(("1" (rewrite "cos_pi")
(("1" (assert)
(("1"
(lemma "atan2_cancel_neg"
("x" "cos(a)" "y" "sin(a)" "nz" "-1"))
(("1" (case-replace "a=pi")
(("1" (rewrite "sin_pi")
(("1"
(rewrite "cos_pi")
(("1" (assert) nil nil))
nil))
nil)
("2" (lemma "sin_eq_0_2pi" ("a" "a"))
(("2"
(assert)
(("2"
(inst - "a-pi")
(("2"
(assert)
(("2"
(rewrite "sin_minus" -3)
(("2"
(rewrite "cos_pi")
(("2"
(rewrite "sin_pi")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skolem 1 ("a"))
(("2" (flatten)
(("2" (inst - "a")
(("1" (assert)
(("1" (expand "atan2")
(("1" (lemma "trichotomy" ("x" "cos(a)"))
(("1" (split)
(("1" (assert)
(("1" (case "a)
(("1" (rewrite "tan_rew")
(("1" (rewrite "atan_tan")
(("1"
(expand "abs")
(("1" (propax) nil nil))
nil))
nil)
("2" (expand "Tan?")
(("2" (assert) nil nil)) nil))
nil)
("2" (lemma "cos_value_strict_decreasing")
(("2" (case-replace "a=pi/2")
(("1"
(rewrite "cos_pi2")
(("1" (assert) nil nil))
nil)
("2"
(expand "strict_decreasing?")
(("2"
(inst - "pi/2" "a")
(("2"
(rewrite "cos_value_pi2")
(("2"
(assert)
(("2"
(lemma
"cos_cos_value"
("a" "a"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (lemma "cos_eq_0_2pi" ("a" "a"))
(("2" (assert) nil nil)) nil))
nil)
("3" (assert)
(("3" (lemma "cos_value_strict_decreasing")
(("3" (expand "strict_decreasing?")
(("3"
(lemma "trich_lt" ("x" "a" "y" "pi/2"))
(("3"
(split)
(("1"
(inst - "a" "pi/2")
(("1"
(rewrite "cos_value_pi2")
(("1"
(assert)
(("1"
(rewrite "cos_cos_value" -3)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(rewrite "cos_pi2")
(("2" (assert) nil nil))
nil))
nil)
("3"
(hide -2)
(("3"
(name "b" "a-pi/2")
(("3"
(lemma "sin_plus")
(("3"
(lemma "cos_plus")
(("3"
(inst - "b" "pi/2")
(("3"
(inst - "b" "pi/2")
(("3"
(rewrite "cos_pi2")
(("3"
(rewrite "sin_pi2")
(("3"
(assert)
(("3"
(replace -3 -1 rl)
(("3"
(replace
-3
-2
rl)
(("3"
(assert)
(("3"
(replace -3)
(("3"
(replace
-1)
(("3"
(replace
-2)
(("3"
(hide
-1
-2)
(("3"
(lemma
"atan_neg"
("x"
"cos(b)/sin(b)"))
(("3"
(replace
-1
1)
(("3"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"cos(b)"
"py"
"sin(b)"))
(("3"
(lemma
"atan_inv"
("px"
"cos(b) / sin(b)"))
(("1"
(rewrite
"div_div1"
-1)
(("1"
(assert)
(("1"
(case-replace
"((1 * sin(b)) / cos(b))=tan(b)")
(("1"
(rewrite
"atan_tan"
-2)
(("1"
(assert)
nil
nil)
("2"
(expand
"abs")
(("2"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"tan")
(("2"
(assert)
nil
nil))
nil)
("3"
(expand
"Tan?")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case-replace "a=0")
(("1" (rewrite "cos_0")
(("1" (rewrite "sin_0")
(("1" (expand "atan2")
(("1" (rewrite "atan_0") nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp)
(("3" (lemma "sin2_cos2" ("a" "x!1"))
(("3" (replace -3)
(("3" (replace -4)
(("3" (expand "sq") (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (case "x!1<=pi/2")
(("1" (rewrite "sin_sin_value")
(("1" (lemma "sin_value_strict_increasing")
(("1" (expand "strict_increasing?")
(("1" (inst - "0" "x!1")
(("1" (rewrite "sin_value_0")
(("1" (assert) nil nil)) nil)
("2" (expand "abs") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sin_sin_phase")
(("2" (expand "sin_phase")
(("2" (lemma "floor_div" ("x" "2*x!1" "py" "pi" "i" "1"))
(("2" (assert)
(("2" (lemma "sin_value_strict_increasing")
(("2" (expand "strict_increasing?")
(("2" (inst - "0" "pi-x!1")
(("1" (rewrite "sin_value_0")
(("1" (assert) nil nil)) nil)
("2" (expand "abs") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sin_value_strict_increasing formula-decl nil sincos_quad nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
(sin_value_0 formula-decl nil sincos_quad nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(sin_sin_value formula-decl nil sincos_def nil)
(sin_phase const-decl "real_abs_le1" sincos_phase nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(floor_div formula-decl nil floor_ceil nil)
(sin_sin_phase formula-decl nil sincos_def nil)
(cos const-decl "real" sincos_def nil)
(atan2 const-decl "real" atan2 nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.117 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
|
|
|
|
|
