| products/Sources/formale Sprachen/PVS/vectors/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: vect_trig_2D.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(atan2_props
(atan2_is_0 0 (atan2_is_0-1 nil 3295014402 ("" (skolem 1 ("a" "b")) (("" (split 1) (("1" (flatten) (("1" (lemma "trichotomy" ("x" "a")) (("1" (split -1) (("1" (expand "atan2") (("1" (assert) (("1" (lemma "trichotomy" ("x" "b")) (("1" (split -1) (("1" (assert) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "b" "py" "a")) (("1" (lemma "atan_strict_increasing") (("1" (expand "strict_increasing?") (("1" (inst - "0" "b/a") (("1" (rewrite "atan_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (assert) (("3" (hide 1) (("3" (typepred "atan(b/a)") (("3" (hide -1) (("3" (expand "abs") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "atan2") (("2" (case-replace "b>0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 1) (("3" (expand "atan2") (("3" (assert) (("3" (typepred "atan(b/a)") (("3" (hide -1) (("3" (expand "abs") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -2) (("2" (expand "atan2") (("2" (assert) (("2" (rewrite "atan_0") 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) (posreal_div_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) (atan2 const-decl "real" atan2 nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (atan_strict_increasing formula-decl nil atan nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (atan_0 formula-decl nil atan nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (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) (posreal_div_posreal_is_posreal judgement-tcc nil real_types 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)) shostak)) (atan2_is_pi2 0 (atan2_is_pi2-1 nil 3295016283 ("" (skolem 1 ("a" "b")) (("" (typepred "b") (("" (split 1) (("1" (flatten) (("1" (lemma "trichotomy" ("x" "a")) (("1" (split -1) (("1" (expand "atan2") (("1" (assert) (("1" (typepred "atan(b/a)") (("1" (case-replace "b>=0") (("1" (assert) nil nil) ("2" (assert) (("2" (hide (-1 -5 2)) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (expand "atan2") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide -3 1) (("3" (expand "atan2") (("3" (typepred "atan(b/a)") (("3" (hide -1) (("3" (expand "abs") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (replace -1) (("2" (expand "atan2") (("2" (propax) nil nil)) nil)) nil)) 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) (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_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) (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_div_nzreal_is_real application-judgement "real" reals nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (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) (atan2 const-decl "real" atan2 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) (trichotomy formula-decl nil real_axioms nil)) shostak)) (atan2_is_pi 0 (atan2_is_pi-1 nil 3295015762 ("" (skolem 1 ("a" "b")) (("" (typepred "b") (("" (lemma "trichotomy" ("x" "a")) (("" (split -1) (("1" (expand "atan2") (("1" (assert) (("1" (hide -2) (("1" (typepred "atan(b/a)") (("1" (case-replace "b>=0") (("1" (assert) nil nil) ("2" (assert) (("2" (hide -1) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (expand "atan2") (("2" (case-replace "b>0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide -2) (("3" (expand "atan2") (("3" (split 1) (("1" (flatten) (("1" (lemma "atan_bij") (("1" (expand "bijective?") (("1" (flatten) (("1" (expand "injective?") (("1" (inst - "0" "b/a") (("1" (rewrite "atan_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (rewrite "atan_0") nil nil)) nil)) nil)) nil)) nil)) nil)) 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_lt_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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (atan const-decl "real_abs_lt_pi2" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals 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) (atan2 const-decl "real" atan2 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) (atan_bij formula-decl nil atan nil) (atan_0 formula-decl nil atan nil) (injective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (trichotomy formula-decl nil real_axioms nil)) shostak)) (atan2_is_3pi2 0 (atan2_is_3pi2-1 nil 3295016463 ("" (skolem 1 ("a" "b")) (("" (typepred "b") (("" (expand "atan2") (("" (split 1) (("1" (flatten) (("1" (lemma "trichotomy" ("x" "a")) (("1" (split -1) (("1" (assert) (("1" (typepred "atan(b / a)") (("1" (case-replace "b >= 0") (("1" (assert) nil nil) ("2" (assert) (("2" (hide -1 -5 2) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "b>=0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("3" (assert) (("3" (hide -3 1) (("3" (typepred "atan(b / a)") (("3" (hide -1) (("3" (expand "abs") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) 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) (trichotomy formula-decl nil real_axioms nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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_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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (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) (atan2 const-decl "real" atan2 nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil)) shostak)) (atan2_quad1 0 (atan2_quad1-1 nil 3295016960 ("" (skolem 1 ("a" "b")) (("" (typepred "b") (("" (expand "atan2") (("" (split 1) (("1" (flatten) (("1" (lemma "trichotomy" ("x" "a")) (("1" (split -1) (("1" (typepred "atan(b/a)") (("1" (assert) (("1" (case-replace "b=0") (("1" (rewrite "atan_0") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (hide -1 -6) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) (("3" (hide -4 1) (("3" (typepred "atan(b/a)") (("3" (hide -1) (("3" (expand "abs") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide -3) (("2" (typepred "atan(b/a)") (("2" (hide -1) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "b" "py" "a")) (("2" (lemma "atan_strict_increasing") (("2" (expand "strict_increasing?") (("2" (inst - "0" "b/a") (("2" (rewrite "atan_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (trichotomy formula-decl nil real_axioms nil) (atan const-decl "real_abs_lt_pi2" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (atan_0 formula-decl nil atan nil) (real_plus_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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (atan_strict_increasing 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)) shostak)) (atan2_quad2 0 (atan2_quad2-1 nil 3295016986 ("" (skolem 1 ("a" "b")) (("" (typepred "b") (("" (lemma "trichotomy" ("x" "a")) (("" (split -1) (("1" (expand "atan2") (("1" (assert) (("1" (typepred "atan(b/a)") (("1" (case-replace "b>=0") (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (hide -1 -4) (("2" (assert) (("2" (expand "abs" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "atan2") (("2" (case-replace "b>0") (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "atan2") (("3" (assert) (("3" (typepred "atan(b / a)") (("3" (hide -1 -4) (("3" (assert) (("3" (lemma "atan_strict_increasing") (("3" (expand "strict_increasing?") (("3" (lemma "trichotomy" ("x" "b")) (("3" (split -1) (("1" (lemma "both_sides_div_neg_lt1" ("nz" "a" "y" "0" "x" "b")) (("1" (inst - "b/a" "0") (("1" (rewrite "atan_0") (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "atan_0") (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "both_sides_div_neg_lt1" ("nz" "a" "y" "b" "x" "0")) (("3" (inst - "0" "b/a") (("3" (rewrite "atan_0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (real_gt_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) (real_plus_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) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (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) (atan2 const-decl "real" atan2 nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (atan_strict_increasing formula-decl nil atan nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_div_neg_lt1 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (atan_0 formula-decl nil atan nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (trichotomy formula-decl nil real_axioms nil)) shostak)) (atan2_quad3 0 (atan2_quad3-1 nil 3295016997 ("" (skolem 1 ("a" "b")) (("" (typepred "b") (("" (lemma "trichotomy" ("x" "a")) (("" (split -1) (("1" (expand "atan2") (("1" (typepred "atan(b / a)") (("1" (case-replace "b >= 0") (("1" (assert) nil nil) ("2" (assert) (("2" (hide -1 -4) (("2" (flatten) (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (expand "atan2") (("2" (flatten) (("2" (case-replace "b>0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "atan2") (("3" (typepred "atan(b / a)") (("1" (assert) (("1" (lemma "atan_strict_increasing") (("1" (expand "strict_increasing?") (("1" (lemma "atan_0") (("1" (lemma "trichotomy" ("x" "b")) (("1" (split -1) (("1" (lemma "both_sides_div_neg_lt1" ("nz" "a" "y" "0" "x" "b")) (("1" (inst - "b/a" "0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (lemma "both_sides_div_neg_lt1" ("nz" "a" "x" "0" "y" "b")) (("3" (inst - "0" "b/a") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) 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) (atan const-decl "real_abs_lt_pi2" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (atan2 const-decl "real" atan2 nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (atan_strict_increasing formula-decl nil atan nil) (atan_0 formula-decl nil atan nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (both_sides_div_neg_lt1 formula-decl nil real_props nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (trichotomy formula-decl nil real_axioms nil)) shostak)) (atan2_quad4 0 (atan2_quad4-1 nil 3295017008 ("" (skolem 1 ("a" "b")) (("" (typepred "b") (("" (lemma "trichotomy" ("x" "a")) (("" (expand "atan2") (("" (split -1) (("1" (typepred "atan(b / a)") (("1" (case-replace "b>=0") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "atan_strict_increasing") (("2" (expand "strict_increasing?") (("2" (lemma "both_sides_div_pos_lt1" ("pz" "a" "x" "b" "y" "0")) (("2" (inst - "b/a" "0") (("2" (rewrite "atan_0") (("2" (assert) (("2" (hide -3) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (flatten) (("2" (case-replace "b>0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (typepred "atan(b/a)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) 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) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (atan2 const-decl "real" atan2 nil) (atan const-decl "real_abs_lt_pi2" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (atan_0 formula-decl nil atan nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (atan_strict_increasing formula-decl nil atan 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) (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (trichotomy formula-decl nil real_axioms nil)) shostak)) (atan2_0x 0 (atan2_0x-1 nil 3422013511 ("" (skosimp*) (("" (grind) nil nil)) nil) ((nil application-judgement "nnreal_lt_2pi" atan2 nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (atan2 const-decl "real" atan2 nil) (pi const-decl "posreal" atan nil) (atan_value const-decl "real" atan nil) (Integral const-decl "real" integral_def "analysis/")) shostak)) (atan2_x0_TCC1 0 (atan2_x0_TCC1-1 nil 3422014592 ("" (subtype-tcc) nil nil) nil nil)) (atan2_x0 0 (atan2_x0-1 nil 3422013280 ("" (skosimp*) (("" (expand "atan2") (("" (lift-if) (("" (rewrite "atan_0") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((atan2 const-decl "real" atan2 nil) (atan_0 formula-decl nil atan nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (atan2_11 0 (atan2_11-1 nil 3422012447 ("" (lemma "atan_tan") (("" (inst - "pi/4") (("1" (expand "tan") (("1" (assert) (("1" (rewrite "sin_pi4") (("1" (rewrite "cos_pi4") (("1" (assert) (("1" (case-replace "1 / sqrt(2) / (1 / sqrt(2)) = 1") (("1" (expand "atan2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (field 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (nil application-judgement "nnreal_lt_2pi" atan2 nil) (cos_range application-judgement "trig_range" sincos_def nil) (sin_range application-judgement "trig_range" sincos_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_pi4 formula-decl nil trig_values 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) (= const-decl "[T, T -> boolean]" equalities nil) (atan2 const-decl "real" atan2 nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (sin_pi4 formula-decl nil trig_values nil) (tan const-decl "real" sincos_def nil) (atan_tan formula-decl nil sincos_def nil)) nil)) (atan2_m11 0 (atan2_m11-1 nil 3422012483 ("" (expand "atan2") (("" (lemma "atan_tan") (("" (inst - "-pi/4") (("1" (expand "tan") (("1" (move-terms 1 l 2) (("1" (assert) (("1" (case-replace "-pi / 4 = -(pi/4)") (("1" (hide -1) (("1" (rewrite "sin_neg") (("1" (rewrite "cos_neg") (("1" (rewrite "sin_pi4") (("1" (rewrite "cos_pi4") (("1" (case-replace "1 / sqrt(2) / (-1 / sqrt(2)) = -1") (("1" (field 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((atan_tan formula-decl nil sincos_def nil) (tan const-decl "real" sincos_def nil) (cos_range application-judgement "trig_range" sincos_def nil) (sin_range application-judgement "trig_range" sincos_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_neg formula-decl nil trig_basic nil) (cos_pi4 formula-decl nil trig_values nil) (nnreal type-eq-decl nil real_types nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sin_pi4 formula-decl nil trig_values nil) (minus_real_is_real application-judgement "real" reals nil) (sin_neg formula-decl nil trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (atan const-decl "real_abs_lt_pi2" atan nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, 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 "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) (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_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (atan2 const-decl "real" atan2 nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (atan2_1m1 0 (atan2_1m1-1 nil 3422012528 ("" (expand "atan2") (("" (lemma "atan_tan") (("" (inst - "-pi/4") (("1" (expand "tan") (("1" (move-terms 1 l 2) (("1" (assert) (("1" (case-replace "-pi / 4 = -(pi/4)") (("1" (hide -1) (("1" (rewrite "sin_neg") (("1" (rewrite "cos_neg") (("1" (rewrite "sin_pi4") (("1" (rewrite "cos_pi4") (("1" (case-replace "-(1 / sqrt(2)) / (1 / sqrt(2)) = -1") (("1" (field 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((atan_tan formula-decl nil sincos_def nil) (tan const-decl "real" sincos_def nil) (cos_range application-judgement "trig_range" sincos_def nil) (sin_range application-judgement "trig_range" sincos_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_neg formula-decl nil trig_basic nil) (cos_pi4 formula-decl nil trig_values nil) (nnreal type-eq-decl nil real_types nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sin_pi4 formula-decl nil trig_values nil) (minus_real_is_real application-judgement "real" reals nil) (sin_neg formula-decl nil trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (atan const-decl "real_abs_lt_pi2" atan nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, 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 "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) (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_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" 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) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (atan2_m1m1 0 (atan2_m1m1-1 nil 3422013036 ("" (lemma "atan_tan") (("" (inst - "pi/4") (("1" (expand "tan") (("1" (assert) (("1" (rewrite "sin_pi4") (("1" (rewrite "cos_pi4") (("1" (assert) (("1" (case-replace "1 / sqrt(2) / (1 / sqrt(2)) = 1") (("1" (expand "atan2") (("1" (assert) nil nil)) nil) ("2" (field 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nil application-judgement "nnreal_lt_2pi" atan2 nil) (cos_range application-judgement "trig_range" sincos_def nil) (sin_range application-judgement "trig_range" sincos_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_pi4 formula-decl nil trig_values 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) (= const-decl "[T, T -> boolean]" equalities nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (atan2 const-decl "real" atan2 nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (sin_pi4 formula-decl nil trig_values nil) (tan const-decl "real" sincos_def nil) (atan_tan formula-decl nil sincos_def nil)) shostak)) (atan2_1sqrt3 0 (atan2_1sqrt3-1 nil 3422014623 ("" (expand "atan2") (("" (case "sqrt(3) >= 0") (("1" (assert) (("1" (rewrite "atan_sqrt3") nil nil)) nil) ("2" (hide 2) (("2" (lemma "sqrt_gt") (("2" (inst - "3" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) 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) (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) (atan_sqrt3 formula-decl nil atan_values 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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sqrt_gt formula-decl nil sqrt "reals/") (atan2 const-decl "real" atan2 nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (sqrt_pos application-judgement "posreal" sqrt "reals/")) shostak)) (atan2_sqrt3_TCC1 0 (atan2_sqrt3_TCC1-1 nil 3422013789 ("" (subtype-tcc) nil nil) ((sqrt_pos application-judgement "posreal" sqrt "reals/")) nil)) (atan2_sqrt3 0 (atan2_sqrt3-1 nil 3422013793 ("" (expand "atan2") (("" (case-replace "sqrt(3) > 0") (("1" (assert) (("1" (rewrite "atan_1sqrt3") nil nil)) nil) ("2" (hide 2) (("2" (lemma "sqrt_gt") (("2" (inst - "3" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) 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) (>= 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/") (atan_1sqrt3 formula-decl nil atan_values 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) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sqrt_gt formula-decl nil sqrt "reals/") (atan2 const-decl "real" atan2 nil) (sqrt_pos application-judgement "posreal" sqrt "reals/")) shostak)) (atan2_m1sqrt3 0 (atan2_m1sqrt3-1 nil 3422177809 ("" (expand "atan2") (("" (lemma "atan_neg") (("" (inst - "sqrt(3)") (("" (rewrite "atan_sqrt3") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((atan_neg formula-decl nil atan nil) (atan_sqrt3 formula-decl nil atan_values 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals 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) (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) (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) (atan2 const-decl "real" atan2 nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sqrt_pos application-judgement "posreal" sqrt "reals/")) nil)) (atan2_sqrt3m1_TCC1 0 (atan2_sqrt3m1_TCC1-1 nil 3422178073 ("" (subtype-tcc) nil nil) ((sqrt_pos application-judgement "posreal" sqrt "reals/")) nil)) (atan2_sqrt3m1 0 (atan2_sqrt3m1-1 nil 3422178093 ("" (expand "atan2") (("" (lemma "atan_neg") (("" (inst - "1/sqrt(3)") (("" (case-replace "sqrt(3) > 0") (("1" (assert) (("1" (rewrite "atan_1sqrt3") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((atan_neg formula-decl nil atan nil) (> const-decl "bool" reals nil) (atan_1sqrt3 formula-decl nil atan_values nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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) (posreal_div_posreal_is_posreal application-judgement "posreal" 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) (sqrt_pos application-judgement "posreal" sqrt "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak))) ¤ Dauer der Verarbeitung: 0.132 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.Bot Zugriff |
