| products/sources/formale sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: .project Sprache: LispUntersuchung PVS© |
|
||||||
|
(asinx
(cauchy_real_abs_le1_TCC1 0 (cauchy_real_abs_le1_TCC1-1 nil 3288581630 ("" (expand "cauchy_real_abs_le1?") (("" (inst + "0") (("1" (expand "cauchy_prop") (("1" (propax) nil nil)) nil) ("2" (grind) 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil) (cauchy_real_abs_le1? const-decl "bool" asinx nil)) shostak)) (subtype_TCC1 0 (subtype_TCC1-1 nil 3288581630 ("" (skosimp*) (("" (typepred "x!1") (("" (expand "cauchy_real_abs_le1?") (("" (expand "cauchy_real?") (("" (skosimp*) (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real_abs_le1 nonempty-type-eq-decl nil asinx nil) (cauchy_real_abs_le1? const-decl "bool" asinx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-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) (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) (cauchy_real? const-decl "bool" cauchy nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) shostak)) (cauchy_asin_TCC1 0 (cauchy_asin_TCC1-1 nil 3393224859 ("" (skosimp) (("" (typepred "cx!1") (("" (expand "cauchy_real_abs_le1?") (("" (skosimp) (("" (typepred "x!1") (("" (hide -4) (("" (lemma "mul_lemma" ("x" "x!1" "cx" "cx!1" "y" "x!1" "cy" "cx!1")) (("" (assert) (("" (rewrite "sq_rew") (("" (lemma "sub_lemma" ("x" "1" "y" "sq(x!1)" "cx" "cauchy_int(1)" "cy" "cauchy_mul(cx!1, cx!1)")) (("" (rewrite "int_lemma") (("" (assert) (("" (lemma "sq_le" ("nna" "abs(x!1)" "nnb" "1")) (("" (rewrite "sq_abs") (("" (assert) (("" (case "1-sq(x!1)>=0") (("1" (expand "cauchy_nnreal?") (("1" (inst + "1-sq(x!1)") nil nil)) nil) ("2" (assert) (("2" (hide-all-but (-3 -4 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real_abs_le1 nonempty-type-eq-decl nil asinx nil) (cauchy_real_abs_le1? const-decl "bool" asinx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-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) (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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (cauchy_mul const-decl "cauchy_real" mul nil) (cauchy_int const-decl "cauchy_real" int nil) (sub_lemma formula-decl nil sub nil) (sq_abs formula-decl nil sq "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal type-eq-decl nil real_types nil) (x!1 skolem-const-decl "real_abs_le1" asinx nil) (cauchy_nnreal? const-decl "bool" cauchy nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_1 formula-decl nil sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sq_le formula-decl nil sq "reals/") (int_lemma formula-decl nil int nil) (sq_rew formula-decl nil sq "reals/") (mul_lemma formula-decl nil mul nil) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil)) nil)) (cauchy_asin_TCC2 0 (cauchy_asin_TCC2-1 nil 3393224859 ("" (skosimp*) (("" (replace -3) (("" (hide -3 -4) (("" (typepred "cx!1") (("" (expand "cauchy_real_abs_le1?") (("" (skosimp) (("" (case "abs(x!1)<1") (("1" (hide -3) (("1" (lemma "mul_lemma" ("x" "x!1" "y" "x!1" "cx" "cx!1" "cy" "cx!1")) (("1" (assert) (("1" (rewrite "sq_rew") (("1" (lemma "sq_lt" ("nna" "abs(x!1)" "nnb" "1")) (("1" (rewrite "sq_abs") (("1" (assert) (("1" (lemma "sub_lemma" ("x" "1" "y" "sq(x!1)" "cx" "cauchy_int(1)" "cy" "cauchy_mul(cx!1, cx!1)")) (("1" (rewrite "int_lemma") (("1" (assert) (("1" (lemma "sqrt_lemma" ("nnx" "1-sq(x!1)" "nncx" "cauchy_sub(cauchy_int(1), cauchy_mul(cx!1, cx!1))")) (("1" (assert) (("1" (expand "cauchy_nzreal?") (("1" (inst + "sqrt(1 - sq(x!1))") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -3) (("2" (expand "cauchy_prop") (("2" (inst - "0") (("2" (rewrite "expt_x0") (("2" (flatten) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real_abs_le1 nonempty-type-eq-decl nil asinx nil) (cauchy_real_abs_le1? const-decl "bool" asinx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-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) (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) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt_x0 formula-decl nil exponentiation nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_lt formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_1 formula-decl nil sq "reals/") (int_lemma formula-decl nil int nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqrt_lemma formula-decl nil sqrtx nil) (cauchy_nnreal? const-decl "bool" cauchy nil) (cauchy_nnreal nonempty-type-eq-decl nil cauchy nil) (cauchy_sub const-decl "cauchy_real" sub nil) (nnreal type-eq-decl nil real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (nzreal nonempty-type-eq-decl nil reals nil) (x!1 skolem-const-decl "real_abs_le1" asinx 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) (/= const-decl "boolean" notequal nil) (sq const-decl "nonneg_real" sq "reals/") (cauchy_mul const-decl "cauchy_real" mul nil) (cauchy_int const-decl "cauchy_real" int nil) (sub_lemma formula-decl nil sub nil) (sq_abs formula-decl nil sq "reals/") (sq_rew formula-decl nil sq "reals/") (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (mul_lemma formula-decl nil mul nil) (< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (<= const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/")) nil)) (cauchy_asin_TCC3 0 (cauchy_asin_TCC3-1 nil 3508998293 ("" (skosimp*) (("" (typepred "cx!1") (("" (expand "cauchy_real_abs_le1?") (("" (skosimp) (("" (typepred "x!1") (("" (replace -4 *) (("" (hide -4 -5 -6) (("" (lemma "trichotomy" ("x" "cx!1(0)")) (("" (split) (("1" (hide 1) (("1" (copy -4) (("1" (expand "cauchy_prop" -1) (("1" (inst - "0") (("1" (rewrite "expt_x0") (("1" (flatten) (("1" (assert) (("1" (expand "cauchy_nzreal?") (("1" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (hide 1) (("3" (expand "cauchy_nzreal?") (("3" (inst + "x!1") (("3" (expand "cauchy_prop") (("3" (inst - "0") (("3" (rewrite "expt_x0") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real_abs_le1 nonempty-type-eq-decl nil asinx nil) (cauchy_real_abs_le1? const-decl "bool" asinx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-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) (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) (trichotomy formula-decl nil real_axioms nil) (x!1 skolem-const-decl "real_abs_le1" asinx nil) (posint_exp application-judgement "posint" exponentiation nil) (cauchy_prop const-decl "bool" cauchy nil) (expt_x0 formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil)) nil)) (asin_lemma 0 (asin_lemma-1 nil 3288581645 ("" (skosimp) (("" (expand "cauchy_asin") (("" (copy -1) (("" (expand "cauchy_prop" -1) (("" (inst - "0") (("" (rewrite "expt_x0") (("" (flatten -1) (("" (name-replace "TT" "cx!1(0)") (("" (lemma "mul_lemma" ("x" "x!1" "y" "x!1" "cx" "cx!1" "cy" "cx!1")) (("" (rewrite "sq_rew") (("" (assert) (("" (lemma "sub_lemma" ("x" "1" "y" "sq(x!1)" "cx" "cauchy_int(1)" "cy" "cauchy_mul(cx!1, cx!1)")) (("" (rewrite "int_lemma") (("" (assert) (("" (hide -2) (("" (case "1-sq(x!1)>=0") (("1" (lemma "sqrt_lemma" ("nnx" "1-sq(x!1)" "nncx" "cauchy_sub(cauchy_int(1), cauchy_mul(cx!1, cx!1))")) (("1" (assert) (("1" (name-replace "CY" "cauchy_sqrt(cauchy_sub(cauchy_int(1), cauchy_mul(cx!1, cx!1)))") (("1" (hide -3) (("1" (lemma "pi_lemma") (("1" (lemma "lemma_div2n" ("x" "pi" "cx" "cauchy_pi" "n" "1")) (("1" (assert) (("1" (name-replace "PI2" "cauchy_div2n(cauchy_pi, 1)") (("1" (expand "div2n") (("1" (rewrite "expt_x1") (("1" (hide -2) (("1" (case-replace "TT=0") (("1" (case "sq(x!1)<1") (("1" (lemma "sqrt_pos" ("px" "1-sq(x!1)")) (("1" (expand "asin") (("1" (assert) (("1" (rewrite "sq_rew") (("1" (lemma "div_lemma" ("x" "x!1" "cx" "cx!1" "nzy" "sqrt(1 - sq(x!1))" "nzcy" "CY")) (("1" (assert) (("1" (lemma "atan_lemma" ("x" "x!1 / sqrt(1 - sq(x!1))" "cx" "cauchy_div(cx!1, CY)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide-all-but (-5 -6 1)) (("2" (lemma "sq_lt" ("nna" "abs(x!1)" "nnb" "1")) (("2" (rewrite "sq_abs") (("2" (rewrite "sq_1") (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "x!1/=0") (("1" (case-replace "TT > 0") (("1" (case "x!1>0") (("1" (hide 1) (("1" (lemma "div_lemma" ("nzy" "x!1" "nzcy" "cx!1" "x" "sqrt(1 - sq(x!1))" "cx" "CY")) (("1" (assert) (("1" (lemma "atan_lemma" ("x" "sqrt(1 - sq(x!1)) / x!1" "cx" "cauchy_div(CY, cx!1)")) (("1" (assert) (("1" (lemma "sub_lemma" ("x" "pi/2" "cx" "PI2" "y" "atan(sqrt(1 - sq(x!1)) / x!1)" "cy" "cauchy_atan(cauchy_div(CY, cx!1))")) (("1" (assert) (("1" (rewrite "asin_pos_restrict") (("1" (rewrite "sq_rew") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace 1) (("2" (case "TT<0") (("1" (hide 1 2) (("1" (case "x!1<0") (("1" (lemma "div_lemma" ("nzy" "x!1" "nzcy" "cx!1" "x" "sqrt(1 - sq(x!1))" "cx" "CY")) (("1" (assert) (("1" (lemma "atan_lemma" ("x" "sqrt(1 - sq(x!1)) / x!1" "cx" "cauchy_div(CY, cx!1)")) (("1" (assert) (("1" (lemma "sub_lemma" ("x" "-pi/2" "cx" "cauchy_neg(PI2)" "y" "atan(sqrt(1 - sq(x!1)) / x!1)" "cy" "cauchy_atan(cauchy_div(CY, cx!1))")) (("1" (rewrite "neg_lemma" -7) (("1" (assert) (("1" (rewrite "asin_neg_restrict") (("1" (rewrite "sq_rew") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (hide 2) (("3" (expand "cauchy_nnreal?") (("3" (inst + "1-sq(x!1)") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "sq_lt" ("nna" "abs(x!1)" "nnb" "1")) (("2" (rewrite "sq_abs") (("2" (rewrite "sq_1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_asin const-decl "cauchy_real" asinx nil) (posint_exp application-judgement "posint" exponentiation nil) (cauchy_prop const-decl "bool" cauchy nil) (expt_x0 formula-decl nil exponentiation nil) (cauchy_real_abs_le1 nonempty-type-eq-decl nil asinx nil) (cauchy_real_abs_le1? const-decl "bool" asinx nil) (= const-decl "[T, T -> boolean]" equalities nil) (sq_rew formula-decl nil sq "reals/") (sub_lemma formula-decl nil sub nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_mul const-decl "cauchy_real" mul nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (x!1 skolem-const-decl "real_abs_le1" asinx nil) (lemma_div2n formula-decl nil shift nil) (cauchy_pi const-decl "cauchy_real" atanx nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan "trig_fnd/") (cauchy_div2n const-decl "cauchy_real" shift nil) (expt_x1 formula-decl nil exponentiation nil) (sq_abs formula-decl nil sq "reals/") (sq_1 formula-decl nil sq "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sq_lt formula-decl nil sq "reals/") (sqrt_pos judgement-tcc nil sqrt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (div_lemma formula-decl nil div nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (atan_lemma formula-decl nil atanx nil) (cauchy_div const-decl "cauchy_real" div nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (asin const-decl "real_abs_le_pi2" asin "trig_fnd/") (< const-decl "bool" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cauchy_neg const-decl "cauchy_real" neg nil) (asin_neg_restrict formula-decl nil asin "trig_fnd/") (neg_lemma formula-decl nil neg nil) (cauchy_atan const-decl "cauchy_real" atanx nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig_fnd/") (atan const-decl "real_abs_lt_pi2" atan "trig_fnd/") (asin_pos_restrict formula-decl nil asin "trig_fnd/") (div2n const-decl "real" shift nil) (pi_lemma formula-decl nil atanx nil) (cauchy_sqrt const-decl "cauchy_nnreal" sqrtx nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal type-eq-decl nil real_types nil) (cauchy_sub const-decl "cauchy_real" sub nil) (cauchy_nnreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nnreal? const-decl "bool" cauchy nil) (sqrt_lemma formula-decl nil sqrtx nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_lemma formula-decl nil int nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (mul_lemma formula-decl nil mul nil) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy 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 "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-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) (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)) shostak))) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.47Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
