| products/sources/formale Sprachen/PVS/trig_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: tan_quad.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(tan_quad
(tan_value_def_TCC1 0 (tan_value_def_TCC1-1 nil 3264857198 ("" (skosimp*) (("" (typepred "x!1") (("" (assert) nil nil)) nil)) nil) ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (tan_value_def_TCC2 0 (tan_value_def_TCC2-1 nil 3264857222 ("" (skosimp*) (("" (typepred "x!1") (("" (assert) (("" (expand "abs") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (tan_value_def_TCC3 0 (tan_value_def_TCC3-1 nil 3264857251 ("" (skosimp*) (("" (typepred "x!1") (("" (lemma "cos_value_strict_decreasing") (("" (expand "strict_decreasing?") (("" (inst - "abs(x!1)" "pi/2") (("" (rewrite "cos_value_pi2") (("" (assert) (("" (expand "abs") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (cos_value_pi2 formula-decl nil sincos_quad nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (cos_value_strict_decreasing formula-decl nil sincos_quad nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (tan_value_def 0 (tan_value_def-3 nil 3408979579 ("" (skosimp*) (("" (typepred "x!1") (("" (lemma "atan_bij") (("" (expand "tan_value") (("" (lemma "comp_inverse_right[real, real_abs_lt_pi2]" ("f" "atan" "y" "x!1")) (("1" (expand "bijective?") (("1" (expand "injective?") (("1" (flatten) (("1" (hide -3) (("1" (inst - "inverse(atan)(x!1)" "sin_value(x!1) / cos_value(abs(x!1))") (("1" (split -2) (("1" (propax) nil nil) ("2" (lemma "cos_eqv_sqrt_sin_value" ("q1" "abs(x!1)")) (("1" (case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))") (("1" (replace -1) (("1" (replace -3 1) (("1" (replace -2 1 rl) (("1" (hide -1 -2 -3 2) (("1" (lemma "asin_sin_value" ("xs" "x!1")) (("1" (expand "asin") (("1" (lemma "sin_value_strict_increasing") (("1" (expand "strict_increasing?") (("1" (inst-cp - "-pi/2" "x!1") (("1" (inst - "x!1" "pi/2") (("1" (rewrite "sin_value_pi2") (("1" (rewrite "sin_value_minus_pi2") (("1" (case "x!1<0") (("1" (assert) (("1" (case "-pi / 2 < x!1") (("1" (rewrite "sq_rew" -5) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "sq_rew" -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (case "x!1<0") (("1" (lemma "sin_value_neg" ("xs" "x!1")) (("1" (assert) (("1" (replace -1 1) (("1" (rewrite "sq_neg" 1) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (hide 2 3) (("2" (ground) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (tan_value const-decl "[real_abs_lt_pi2 -> real]" tan_quad nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (inverse const-decl "D" function_inverse nil) (<= const-decl "bool" reals nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (nnreal type-eq-decl nil real_types nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil) (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (sq_neg formula-decl nil sq "reals/") (sin_value_neg formula-decl nil sincos_quad nil) (asin_sin_value formula-decl nil sincos_quad nil) (sin_value_strict_increasing formula-decl nil sincos_quad nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sin_value_pi2 formula-decl nil sincos_quad nil) (sq_rew formula-decl nil sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_value_minus_pi2 formula-decl nil sincos_quad nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (asin const-decl "real_abs_le_pi2" asin nil) (real_times_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (injective? const-decl "bool" functions nil) (atan const-decl "real_abs_lt_pi2" atan nil) (bijective? const-decl "bool" functions nil) (comp_inverse_right formula-decl nil function_inverse nil) (atan_bij formula-decl nil atan nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil) (tan_value_def-2 nil 3408966564 ("" (skosimp*) (("" (typepred "x!1") (("" (lemma "atan_bij") (("" (expand "tan_value") (("" (lemma "comp_inverse_right[real, real_abs_lt_pi]" ("f" "atan" "y" "x!1")) (("1" (expand "bijective?") (("1" (expand "injective?") (("1" (flatten) (("1" (hide -3) (("1" (inst - "inverse(atan)(x!1)" "sin_value(x!1) / cos_value(abs(x!1))") (("1" (split -2) (("1" (propax) nil nil) ("2" (lemma "cos_eqv_sqrt_sin_value" ("q1" "abs(x!1)")) (("1" (case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))") (("1" (replace -1) (("1" (replace -3 1) (("1" (replace -2 1 rl) (("1" (hide -1 -2 -3 2) (("1" (lemma "asin_sin_value" ("xs" "x!1")) (("1" (expand "asin") (("1" (lemma "sin_value_strict_increasing") (("1" (expand "strict_increasing?") (("1" (inst-cp - "-pi/2" "x!1") (("1" (inst - "x!1" "pi/2") (("1" (rewrite "sin_value_pi2") (("1" (rewrite "sin_value_minus_pi2") (("1" (case "x!1<0") (("1" (assert) (("1" (case "-pi / 2 < x!1") (("1" (rewrite "sq_rew" -5) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "sq_rew" -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (case "x!1<0") (("1" (lemma "sin_value_neg" ("xs" "x!1")) (("1" (assert) (("1" (replace -1 1) (("1" (rewrite "sq_neg" 1) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (hide 2 3) (("2" (ground) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((atan_bij formula-decl nil atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (sq const-decl "nonneg_real" sq "reals/") (asin const-decl "real_abs_le_pi2" asin nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (sin_value_minus_pi2 formula-decl nil sincos_quad nil) (sq_rew formula-decl nil sq "reals/") (sin_value_pi2 formula-decl nil sincos_quad nil) (sin_value_strict_increasing formula-decl nil sincos_quad nil) (asin_sin_value formula-decl nil sincos_quad nil) (sin_value_neg formula-decl nil sincos_quad nil) (sq_neg formula-decl nil sq "reals/") (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil) (cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (pi const-decl "posreal" atan nil)) nil) (tan_value_def-1 nil 3264857402 ("" (skosimp*) (("" (typepred "x!1") (("" (lemma "atan_bij") (("" (expand "tan_value") (("" (lemma "comp_inverse_right[real, real_mpi_ppi]" ("f" "atan" "y" "x!1")) (("1" (expand "bijective?") (("1" (expand "injective?") (("1" (flatten) (("1" (hide -3) (("1" (inst - "inverse(atan)(x!1)" "sin_value(x!1) / cos_value(abs(x!1))") (("1" (split -2) (("1" (propax) nil nil) ("2" (lemma "cos_eqv_sqrt_sin_value" ("q1" "abs(x!1)")) (("1" (case "sq(sin_value(abs(x!1))) = sq(sin_value(x!1))") (("1" (replace -1) (("1" (replace -3 1) (("1" (replace -2 1 rl) (("1" (hide -1 -2 -3 2) (("1" (lemma "asin_sin_value" ("xs" "x!1")) (("1" (expand "asin") (("1" (lemma "sin_value_strict_increasing") (("1" (expand "strict_increasing?") (("1" (inst-cp - "-pi/2" "x!1") (("1" (inst - "x!1" "pi/2") (("1" (rewrite "sin_value_pi2") (("1" (rewrite "sin_value_minus_pi2") (("1" (case "x!1<0") (("1" (assert) (("1" (case "-pi / 2 < x!1") (("1" (rewrite "sq_rew" -5) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "sq_rew" -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (case "x!1<0") (("1" (lemma "sin_value_neg" ("xs" "x!1")) (("1" (assert) (("1" (replace -1 1) (("1" (rewrite "sq_neg" 1) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (hide 2 3) (("2" (ground) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((atan_bij formula-decl nil atan nil) (atan_value const-decl "real" atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (sq const-decl "nonneg_real" sq "reals/") (asin const-decl "real_abs_le_pi2" asin nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (sin_value_minus_pi2 formula-decl nil sincos_quad nil) (sq_rew formula-decl nil sq "reals/") (sin_value_pi2 formula-decl nil sincos_quad nil) (sin_value_strict_increasing formula-decl nil sincos_quad nil) (asin_sin_value formula-decl nil sincos_quad nil) (sin_value_neg formula-decl nil sincos_quad nil) (sq_neg formula-decl nil sq "reals/") (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil) (cos_eqv_sqrt_sin_value formula-decl nil sincos_quad nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (pi const-decl "posreal" atan nil)) shostak)) (tan_value_0_TCC1 0 (tan_value_0_TCC1-1 nil 3264857350 ("" (assert) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (tan_value_0 0 (tan_value_0-1 nil 3264858476 ("" (lemma "tan_value_def" ("x" "0")) (("1" (rewrite "sin_value_0") (("1" (expand "abs") (("1" (rewrite "cos_value_0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil) ((sin_value_0 formula-decl nil sincos_quad nil) (cos_value_0 formula-decl nil sincos_quad nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (tan_value_def formula-decl nil tan_quad nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)) shostak)) (tan_value_pi4_TCC1 0 (tan_value_pi4_TCC1-1 nil 3264857364 ("" (expand "abs") (("" (typepred "pi") (("" (assert) nil nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil)) shostak)) (tan_value_pi4 0 (tan_value_pi4-1 nil 3264858541 ("" (lemma "tan_value_def" ("x" "pi/4")) (("1" (rewrite "sin_value_pi4") (("1" (expand "abs") (("1" (assert) (("1" (rewrite "cos_value_pi4") (("1" (rewrite "div_simp" -1) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (typepred "pi") (("2" (assert) nil nil)) nil)) nil)) nil) ((sin_value_pi4 formula-decl nil sincos_quad nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_simp formula-decl nil real_props nil) (cos_value_pi4 formula-decl nil sincos_quad nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (tan_value_def formula-decl nil tan_quad nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)) shostak))) ¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
