| products/sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: SMLOriginal von: PVS© |
|
||||||
|
(sqrt_approx
(sq_sq_aux 0 (sq_sq_aux-1 nil 3320768920 ("" (grind) nil nil) ((nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq nil)) shostak)) (sqrt_newton_aux_TCC1 0 (sqrt_newton_aux_TCC1-1 nil 3320768919 ("" (grind-reals) 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 "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types 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) (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) (div_mult_pos_ge1 formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (sqrt_newton_aux_TCC2 0 (sqrt_newton_aux_TCC2-1 nil 3320768919 ("" (grind-reals) nil nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (sqrt_newton_aux_TCC3 0 (sqrt_newton_aux_TCC3-1 nil 3320768919 ("" (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 "bool" reals nil) (nnreal 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 nonempty-type-eq-decl nil 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (sqrt_newton_aux_TCC4 0 (sqrt_newton_aux_TCC4-1 nil 3320768919 ("" (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 "bool" reals nil) (nnreal 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 nonempty-type-eq-decl nil 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) (sq const-decl "nonneg_real" sq nil) (/= const-decl "boolean" notequal nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil)) (sqrt_newton_aux_TCC5 0 (sqrt_newton_aux_TCC5-2 nil 3320769110 ("" (skosimp* :preds? t) (("" (case "y!1 > 0") (("1" (split) (("1" (cross-mult 1) (("1" (field) nil nil)) nil) ("2" (move-terms 1 l) (("2" (rewrite "sq_sq_aux") (("2" (rewrite "sq_div") (("2" (grind-reals) (("1" (rewrite "sq_times") (("1" (assert) nil nil)) nil) ("2" (name-replace "AA" "sq(y!1) - x!1") (("2" (expand "sq") (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "sq(y!1) > 0") (("1" (expand "sq" -1) (("1" (grind-reals) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq_div formula-decl nil sq nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_times formula-decl nil sq nil) (sq_nz_pos application-judgement "posreal" sq nil) (pos_times_lt formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pos_div_lt formula-decl nil real_props nil) (sq_sq_aux formula-decl nil sqrt_approx nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(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) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (FDX_87 skolem-const-decl "{y | x!1 < sq(y)}" sqrt_approx nil) (x!1 skolem-const-decl "nnreal" sqrt_approx nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil)) (sqrt_newton_aux_TCC6 0 (sqrt_newton_aux_TCC6-2 nil 3320772107 ("" (skosimp :preds? t) (("" (assert) (("" (lift-if) (("" (split 2) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (case "y!1 > 0") (("1" (lemma "sq_sq_aux") (("1" (inst -1 "x!1" "y!1") (("1" (replaces -1) (("1" (rewrite "sq_div") (("1" (rewrite "sq_times") (("1" (case-replace "sq(2) = 4") (("1" (lemma "log_nat_incr") (("1" (inst?) (("1" (inst -1 "(sq(y!1)-x!1)/eps!1") (("1" (assert) (("1" (hide 3) (("1" (field 1) (("1" (factor 1 r) (("1" (name-replace "AA" "sq(y!1)-x!1" :hide? nil) (("1" (expand "sq" 1 1) (("1" (cancel-by 1 "AA") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sq" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (wrap-formula 1 "sq") (("1" (rewrite "sq_0") (("1" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!1 skolem-const-decl "nnreal" sqrt_approx nil) (y!1 skolem-const-decl "{y | x!1 < sq(y)}" sqrt_approx nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sq_div formula-decl nil sq nil) (= const-decl "[T, T -> boolean]" equalities nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (above nonempty-type-eq-decl nil integers 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_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonzero_times3 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (pos_times_gt formula-decl nil real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (FDX_89 skolem-const-decl "posreal" sqrt_approx nil) (FDX_88 skolem-const-decl "nonneg_real" sqrt_approx nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (zero_times1 formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (pos_div_gt formula-decl nil real_props nil) (CBD_90 skolem-const-decl "real" sqrt_approx nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (log_nat_incr formula-decl nil log_nat nil) (sq_nz_pos application-judgement "posreal" sq nil) (sq_times formula-decl nil sq nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_sq_aux formula-decl nil sqrt_approx nil) (sq_0 formula-decl nil sq nil) (posint_exp application-judgement "posint" exponentiation 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) (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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil)) (sqrt_newton_aux_NOT_increasing 0 (sqrt_newton_aux_NOT_increasing-1 nil 3557592665 ("" (eval-expr "sq(2.9)") (("" (eval-expr "sq(2.91)") (("" (inst + "8.32" "8.31681" "2.9" "2.91" "0.1") (("1" (assert) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil) ((nnreal type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities 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) (sq const-decl "nonneg_real" sq 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) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (sqrt_newton_TCC1 0 (sqrt_newton_TCC1-1 nil 3320768919 ("" (subtype-tcc) nil nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq const-decl "nonneg_real" sq nil)) nil)) (sqrt_newton_is_NOT_increasing 0 (sqrt_newton_is_NOT_increasing-1 nil 3557676691 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (sq_sqrt_newton 0 (sq_sqrt_newton-1 nil 3321016010 ("" (skeep) (("" (typepred "sqrt_newton(x, eps)") (("" (assert) nil nil)) nil)) nil) ((sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}" sqrt_approx nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sq const-decl "nonneg_real" sq nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_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) (real_minus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq nil)) shostak)) (sqrt_newton_gt 0 (sqrt_newton_gt-1 nil 3321016041 ("" (skeep) (("" (lemma "sq_sqrt_newton") (("" (inst -1 "eps" "x") (("" (wrap-formula -1 "sqrt") (("1" (rewrite "sqrt_sq") nil nil) ("2" (hide 2) (("2" (rewrite "sqrt_gt") nil nil)) nil)) nil)) nil)) nil)) nil) ((sq_sqrt_newton formula-decl nil sqrt_approx 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 nil) (sq const-decl "nonneg_real" sq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}" sqrt_approx nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (sqrt_sq formula-decl nil sqrt 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) (sqrt_gt formula-decl nil sqrt nil) (nnreal type-eq-decl nil real_types 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) (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) (sq_nz_pos application-judgement "posreal" sq nil)) shostak)) (sqrt_newton_lt 0 (sqrt_newton_lt-1 nil 3321016482 ("" (skeep) (("" (cross-mult 2) (("" (lemma "sqrt_newton_gt") (("" (inst -1 "eps" "x") (("" (mult-by -1 "sqrt(x)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}" sqrt_approx nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sq const-decl "nonneg_real" sq nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types 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) (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) (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) (x skolem-const-decl "nnreal" sqrt_approx nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (sqrt_newton_gt formula-decl nil sqrt_approx nil) (sq_nz_pos application-judgement "posreal" sq nil)) shostak)) (sqrt_newton_le 0 (sqrt_newton_le-1 nil 3321016611 ("" (skeep) (("" (lemma "sqrt_newton_lt") (("" (inst -1 "eps" "x") (("" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((sqrt_newton_lt formula-decl nil sqrt_approx nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal type-eq-decl nil real_types 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) (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) (sq_nz_pos application-judgement "posreal" sq nil)) shostak)) (sqrt_approx_TCC1 0 (sqrt_approx_TCC1-2 nil 3557832683 ("" (skosimp*) (("" (assert) (("" (replaces -4) (("" (cross-mult 1) (("" (ground) (("1" (case "x!1*N!1>=0") (("1" (assert) nil) ("2" (assert) (("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst?) nil))))))) ("2" (case "2*10^n!1>=1") (("1" (assert) nil) ("2" (case "FORALL (nn:nat): 2*10^nn >=1") (("1" (inst?) nil) ("2" (hide-all-but 1) (("2" (induct "nn") (("1" (grind) nil) ("2" (skeep) (("2" (expand "^") (("2" (expand "expt" +) (("2" (assert) nil)))))))))))))))))))))))) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posint_exp application-judgement "posint" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (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) (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)) nil) (sqrt_approx_TCC1-1 nil 3557745411 ("" (skeep) (("" (skeep) (("" (skosimp*) (("" (assert) (("" (typepred "floor(2*10^n)") (("" (assert) (("" (typepred "floor(1)") (("" (assert) (("" (case "2*10^n >= 1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (case "FORALL (nn:nat): 2*10^nn >=1") (("1" (inst?) nil nil) ("2" (induct "nn") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "^") (("2" (expand "expt" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (sqrt_approx_TCC2 0 (sqrt_approx_TCC2-2 nil 3557832760 ("" (skeep) (("" (skeep) (("" (skeep) (("" (skeep) (("" (name "qq" "sqrt_newton(xx, 10 ^ (-n)/2)") (("1" (replaces -1) (("1" (typepred "qq") (("1" (hide (-1 -2)) (("1" (case "x >= xx AND abs(x-xx)<10^(-n)/2") (("1" (flatten) (("1" (grind :exclude ("sq" "floor" "^")) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (mult-by 1 "N") (("1" (assert) nil nil)) nil) ("2" (case "1/N = 10^(-n)/2") (("1" (case "abs(x-xx)<1/N") (("1" (assert) (("1" (replaces -2) nil nil)) nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (ground) (("2" (lemma "abs_mult") (("2" (inst - "x-xx" "N") (("2" (assert) (("2" (expand "abs" - 3) (("2" (replaces -1 :dir rl) (("2" (assert) (("2" (case "N*xx = k") (("1" (replace -1) (("1" (assert) (("1" (replace -7) (("1" (hide-all-but 1) (("1" (grind :exclude ("sq" "floor" "^")) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult -7) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (assert) (("2" (replace -4) (("2" (assert) (("2" (lemma "expt_plus") (("2" (inst - "n" "-n" "10") (("2" (assert) (("2" (replace -1 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (posint_exp application-judgement "posint" exponentiation nil) (div_cancel4 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (abs_mult formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt def-decl "real" exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt_plus formula-decl nil exponentiation nil) (int_times_even_is_even application-judgement "even_int" integers nil) (times_div2 formula-decl nil real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (div_cancel3 formula-decl nil real_props nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (nnreal type-eq-decl nil real_types 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}" sqrt_approx nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sq_nz_pos application-judgement "posreal" sq nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (sqrt_approx_TCC2-1 nil 3557745411 ("" (skosimp*) (("" (assert) (("" (replaces -4) (("" (cross-mult 1) (("" (ground) (("1" (case "x!1*N!1>=0") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst?) nil nil)) nil)) nil)) nil) ("2" (case "2*10^n!1>=1") (("1" (assert) nil nil) ("2" (case "FORALL (nn:nat): 2*10^nn >=1") (("1" (inst?) nil nil) ("2" (hide-all-but 1) (("2" (induct "nn") (("1" (grind) nil nil) ("2" (skeep) (("2" (expand "^") (("2" (expand "expt" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (sqrt_approx_increasing 0 (sqrt_approx_increasing-1 nil 3557827887 ("" (skeep) (("" (name "qx" "sqrt_approx(x, n)") (("" (name "qy" "sqrt_approx(y, n)") (("" (replace -1) (("" (replace -2) (("" (expand "sqrt_approx") (("" (invoke (name "yy" "%1") (! -1 1 1)) (("" (replace -1) (("" (invoke (name "xx" "%1") (! -3 1 1)) (("" (replace -1) (("" (case "xx<=yy") (("1" (name "qxx" "sqrt_newton(xx, 10 ^ (-n) / 2)") (("1" (name "qyy" "sqrt_newton(yy, 10 ^ (-n) / 2)") (("1" (assert) (("1" (case "xx = yy") (("1" (assert) nil nil) ("2" (case "NOT xx (("1" (assert) nil nil) ("2" (hide 1) (("2" (name "N" "2*10^n") (("2" (replace -1) (("2" (case "yy-xx>=1/N") (("1" (assert) (("1" (typepred "qxx") (("1" (typepred "qyy") (("1" (assert) (("1" (case "1/N = 10^(-n)/2") (("1" (assert) (("1" (replace -1) (("1" (name "epsi" "10^(-n)/2") (("1" (replace -1) (("1" (case "qxx<=qyy") (("1" (assert) nil nil) ("2" (hide-all-but (-5 -6 -9 -10 -11 1)) (("2" (case "NOT sq(qxx)<=sq(qyy)") (("1" (assert) nil nil) ("2" (lemma "sq_le") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "N" 1) (("2" (cross-mult 1) (("2" (lemma "expt_plus") (("2" (inst - "n" "-n" "10") (("2" (assert) (("2" (replace -1 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but (-2 1)) (("2" (expand "xx") (("2" (expand "yy") (("2" (expand "N") (("2" (case "floor(2 * (10 ^ n * x)) <= floor(2 * (10 ^ n * y))-1") (("1" (mult-by -1 "1/(2*10^n)") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (case "floor(2 * (10 ^ n * x)) < floor(2 * (10 ^ n * y))") (("1" (assert) nil nil) ("2" (mult-by 1 "1/(2*10^n)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "floor(2 * (10 ^ n * x)) <= floor(2 * (10 ^ n * y))") (("1" (mult-by -1 "1/(2*10^n)") (("1" (assert) nil nil)) nil) ("2" (mult-by -5 "2*10^n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sqrt_approx const-decl "{z | abs(sq(z) - x) < 10 ^ (-n) / 2}" sqrt_approx nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (sq const-decl "nonneg_real" sq nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (posint_exp application-judgement "posint" exponentiation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}" sqrt_approx nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (times_div2 formula-decl nil real_props nil) (div_cancel4 formula-decl nil real_props nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt def-decl "real" exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt_plus formula-decl nil exponentiation nil) (N skolem-const-decl "posint" sqrt_approx nil) (posrat nonempty-type-eq-decl nil rationals nil) (sq_le formula-decl nil sq nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (yy skolem-const-decl "nonneg_rat" sqrt_approx nil) (int_minus_int_is_int application-judgement "int" integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (xx skolem-const-decl "nonneg_rat" sqrt_approx nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (sq_nz_pos application-judgement "posreal" sq nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil)) shostak)) (sqrt_old_bounds 0 (sqrt_old_bounds-1 nil 3576862732 ("" (skeep) (("" (split) (("1" (expand "sqrt_lb_old") (("1" (name "q" "sqrt_approx(x,2*n)") (("1" (replaces -1) (("1" (typepred "q") (("1" (hide -1) (("1" (case "NOT x > sq(q)-10 ^ (-(2 * n)) / 2") (("1" (hide 2) (("1" (grind :exclude "^") nil nil)) nil) ("2" (lemma "sqrt_gt") (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("2" (inst - "x" "sq(q)-10 ^ (-(2 * n)) / 2") (("1" (assert) (("1" (case "sqrt(sq(q)-10 ^ (-(2 * n)) / 2)>=q-10 ^ (-n)") (("1" (assert) nil nil) ("2" (lemma "sq_ge") (("2" (inst?) (("2" (assert) (("2" (rewrite "sq_minus") (("2" (assert) (("2" (case "2 * (10 ^ (-n) * q) >= 10 ^ (-(2 * n)) / 2 + sq(10 ^ (-n))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "2 * 10 ^ (-n) >= 10 ^ (-n) / 2 + 10 ^ (-n)") (("1" (case "q>=10^(-n)") (("1" (mult-ineq -1 -2) (("1" (assert) (("1" (expand "sq") (("1" (lemma "expt_plus") (("1" (inst - "-n" "-n" "10") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_ge") (("2" (inst - "q" "10^(-n)") (("2" (assert) (("2" (expand "sq") (("2" (rewrite "expt_plus" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sqrt_ub_old") (("2" (name "q" "sqrt_approx(x,2*n)") (("2" (replaces -1) (("2" (typepred "q") (("2" (hide -1) (("2" (case "NOT x < sq(q)+10 ^ (-(2 * n)) / 2") (("1" (hide 2) (("1" (grind :exclude "^") nil nil)) nil) ("2" (lemma "sqrt_lt") (("2" (inst - "x" "sq(q)+10 ^ (-(2 * n)) / 2") (("2" (assert) (("2" (case "sqrt(sq(q)+10 ^ (-(2 * n)) / 2)<=q+10 ^ (-n)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "sq_le") (("2" (inst?) (("2" (assert) (("2" (rewrite "sq_plus") (("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.87Angebot 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 |
