| products/Sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
|
(quad_minmax
(quad_minmaxpt_delta 0 (quad_minmaxpt_delta-1 nil 3431167126 ("" (skosimp*) (("" (assert) (("" (grind) nil nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic nil) (sq const-decl "nonneg_real" sq nil)) shostak)) (quad_minmaxpt_midpt 0 (quad_minmaxpt_midpt-1 nil 3431169310 ("" (skosimp*) (("" (assert) (("" (expand "quadratic") (("" (ground) (("" (expand "sq") (("" (move-terms -1 r 2) (("" (move-terms -1 l 1) (("" (factor -1 l) (("" (isolate-mult -1 l 1) (("" (replace -2) (("" (cross-mult 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (times_div2 formula-decl nil real_props nil) (div_cancel4 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (both_sides_div1 formula-decl nil real_props nil) (sq const-decl "nonneg_real" sq nil) (quadratic const-decl "real" quadratic nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (quad_min 0 (quad_min-3 "" 3431087055 ("" (skosimp*) (("" (assert) (("" (expand "is_minimum?") (("" (skosimp*) (("" (expand "quadratic") (("" (claim "%1 = %2 + a!1 * sq(y!1+b!1/(2*a!1))" t (! 1 r) (! 1 l)) (("" (replace -1 :hide? t) (("" (move-terms 1 l *) (("" (assert) (("" (mult-cases 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq 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) (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pos_times_le formula-decl nil real_props nil) (quadratic const-decl "real" quadratic nil) (is_minimum? const-decl "bool" quad_minmax nil)) shostak) (quad_min-2 nil 3419262257 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (lemma "quadratic_min") (("" (inst?) (("" (inst - " quadratic(a!1, b!1, c!1)" "-b!1 / (2 * a!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq const-decl "nonneg_real" sq nil) (sq_pos formula-decl nil sq nil) (sign const-decl "Sign" sign nil) (sign_mult_pos formula-decl nil sign nil) (quadratic const-decl "real" quadratic nil)) nil) (quad_min-1 nil 3402151759 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (lemma "quadratic_min") (("" (inst - "a!1" "b!1" "c!1" "quadratic(a!1,b!1,c!1)" "-b!1/(2*a!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((quadratic const-decl "real" quadratic nil)) shostak)) (quad_min_val 0 (quad_min_val-2 "" 3431087665 ("" (skosimp*) (("" (assert) (("" (use "quad_min") (("" (ground) (("" (expand "is_minimum?") (("" (inst?) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) 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_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic nil) (sq const-decl "nonneg_real" sq nil) (is_minimum? const-decl "bool" quad_minmax nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (quad_min formula-decl nil quad_minmax nil)) shostak) (quad_min_val-1 nil 3402151883 ("" (skosimp*) (("" (lemma "quadratic_min_val") (("" (inst - "a!1" "b!1" "c!1" "quadratic(a!1,b!1,c!1)" "-b!1/(2*a!1)" "x!1") (("" (assert) nil nil)) nil)) nil)) nil) ((quadratic const-decl "real" quadratic nil) (sq const-decl "nonneg_real" sq nil)) shostak)) (quad_min_mono_inc 0 (quad_min_mono_inc-2 "" 3431091514 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (expand "quadratic") (("" (rewrite "canonical_sq") (("" (rewrite "canonical_sq") (("" (field :cancel? t) (("" (rewrite "sq_gt") (("" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic nil) (sq_gt formula-decl nil sq nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (CBD_3 skolem-const-decl "nzreal" quad_minmax nil) (nzreal nonempty-type-eq-decl nil reals nil) (both_sides_plus_gt1 formula-decl nil real_props nil) (both_sides_minus_ge1 formula-decl nil real_props nil) (both_sides_minus_gt1 formula-decl nil real_props nil) (both_sides_times_pos_ge2 formula-decl nil real_props nil) (both_sides_times_pos_gt2 formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (FDX_2 skolem-const-decl "nonzero_real" quad_minmax nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (> const-decl "bool" reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq 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, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (canonical_sq formula-decl nil quadratic nil)) shostak) (quad_min_mono_inc-1 nil 3402151913 ("" (skosimp*) (("" (lemma "quadratic_min_mono_inc") (("" (inst - "a!1" "b!1" "c!1" "quadratic(a!1,b!1,c!1)" "-b!1/(2*a!1)" "x!1" "y!1") (("" (assert) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((quadratic const-decl "real" quadratic nil) (sq_gt formula-decl nil sq nil) (canonical_sq formula-decl nil quadratic nil)) shostak)) (quad_min_mono_dec 0 (quad_min_mono_dec-2 "" 3431091966 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (expand "quadratic") (("" (rewrite "canonical_sq") (("" (rewrite "canonical_sq") (("" (field :cancel? t) (("" (lemma "sq_gt") (("" (invoke (inst - "-(%! 1 l 1%)" "-(%! 1 r 1%)")) (("1" (assert) (("1" (rewrite "sq_neg") (("1" (rewrite "sq_neg") nil nil)) nil)) nil) ("2" (grind-reals) nil nil) ("3" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_le_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) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic nil) (sq_gt formula-decl nil sq nil) (sq_neg formula-decl nil sq nil) (- const-decl "[numfield -> numfield]" number_fields nil) (b!1 skolem-const-decl "real" quad_minmax nil) (a!1 skolem-const-decl "nonzero_real" quad_minmax nil) (x!1 skolem-const-decl "real" quad_minmax nil) (y!1 skolem-const-decl "real" quad_minmax nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (CBD_5 skolem-const-decl "nzreal" quad_minmax nil) (nzreal nonempty-type-eq-decl nil reals nil) (both_sides_plus_gt1 formula-decl nil real_props nil) (both_sides_minus_ge1 formula-decl nil real_props nil) (both_sides_minus_gt1 formula-decl nil real_props nil) (both_sides_times_pos_ge2 formula-decl nil real_props nil) (both_sides_times_pos_gt2 formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (FDX_4 skolem-const-decl "nonzero_real" quad_minmax nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (> const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans 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 "[numfield, numfield -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (canonical_sq formula-decl nil quadratic nil)) shostak) (quad_min_mono_dec-1 nil 3402151950 ("" (skosimp*) (("" (lemma "quadratic_min_mono_dec") (("" (inst - "a!1" "b!1" "c!1" "quadratic(a!1,b!1,c!1)" "-b!1/(2*a!1)" "x!1" "y!1") (("" (assert) nil nil)) nil)) nil)) nil) ((quadratic const-decl "real" quadratic nil) (sq_gt formula-decl nil sq nil) (sq_neg formula-decl nil sq nil) (canonical_sq formula-decl nil quadratic nil)) shostak)) (quad_min_eq_intv 0 (quad_min_eq_intv-1 nil 3402152204 ("" (skosimp*) (("" (case "t!1 > - b!1/(2*a!1)") (("1" (lemma "quad_min_mono_inc") (("1" (inst - "a!1" "b!1" "c!1" "xu!1" "t!1") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "quad_min_mono_dec") (("2" (inst - "a!1" "b!1" "c!1" "xl!1" "t!1") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (quad_min_mono_inc formula-decl nil quad_minmax nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (quad_min_mono_dec formula-decl nil quad_minmax nil)) nil)) (quad_min_eq_is_in 0 (quad_min_eq_is_in-3 "" 3431163518 ("" (skosimp*) (("" (lemma "quad_min_mono_inc") (("" (inst - "a!1" "b!1" "c!1" "t!1" "xu!1") (("" (lemma "quad_min_mono_dec") (("" (inst - "a!1" "b!1" "c!1" "t!1" "xl!1") (("" (assert) (("" (assert) (("" (lemma "quad_minmaxpt_midpt") (("" (inst - "a!1" "b!1" "c!1" "xl!1" "xu!1") (("" (assert) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((quad_min_mono_inc formula-decl nil quad_minmax nil) (quad_min_mono_dec formula-decl nil quad_minmax nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (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_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (quad_minmaxpt_midpt formula-decl nil quad_minmax nil) (real_plus_real_is_real application-judgement "real" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak) (quad_min_eq_is_in-2 "" 3431105996 ("" (skosimp*) (("" (lemma "canonical_sq") (("" (inst - "a!1" "b!1" "c!1" "_") (("" (copy -1) (("" (copy -1) (("" (inst - "xl!1") (("" (inst - "xu!1") (("" (inst - "t!1") (("" (expand "quadratic") (("" (both-sides "+" "c!1" -5) (("" (replace -1 :hide? t) (("" (replace -1 :hide? t) (("" (replace -1 :hide? t) (("" (field -2) (("" (field -3) (("" (cancel -5) (("" (cancel -5) (("" (cancel-by -4 "a!1") (("" (use "sq_lt_abs") (("" (assert) (("" (replace -2 :dir rl) (("" (use "sq_lt_abs") (("" (assert) (("" (use "sq_eq_abs") (("" (assert) (("" (claim "xl!1 = -xu!1" t) (("1" (postpone) nil nil) ("2" (claim "(xl!1 + xu!1)/2 = -b!1/(2*a!1)" t) (("2" (flip-ineq 3) (("2" (lemma "quad_min_mono_inc") (("2" (inst - "a!1" "b!1" "c!1" "t!1" "xu!1") (("2" (assert) (("2" (lemma "quad_min_mono_dec") (("2" (inst - "a!1" "b!1" "c!1" "t!1" "xl!1") (("2" (assert) (("2" (split -3) (("1" (assert) (("1" (split -2) (("1" (hide -3) (("1" (expand "quadratic") (("1" (move-terms -1 r -1) (("1" (assert) (("1" (expand "sq") (("1" (assert) (("1" (cancel-terms -11 l) (("1" (assert) (("1" (move-terms -11 r 1) (("1" (factor -11 l (1 3)) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (quad_min_eq_is_in-1 nil 3402152282 ("" (skosimp*) (("" (lemma "canonical_sq") (("" (inst - "a!1" "b!1" "c!1" "_") (("" (copy -1) (("" (copy -1) (("" (inst - "xl!1") (("" (inst - "xu!1") (("" (inst - "t!1") (("" (expand "quadratic") (("" (assert) (("" (both-sides "+" "c!1" -5) (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (assert) (("" (div-by -2 "a!1") (("" (field -3) (("" (both-sides "-" "4*(a!1*c!1)" -5) (("" (assert) (("" (both-sides "+" "sq(b!1)" -5) (("" (case "sq(b!1 / (2 * a!1) + t!1) * sq(a!1) < sq(b!1 / (2 * a!1) + xu!1) * sq(a!1)") (("1" (div-by -1 "sq(a!1)") (("1" (hide -6) (("1" (lemma "sq_eq_abs") (("1" (inst?) (("1" (assert) (("1" (expand "abs") (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (replace -2 * rl) (("1" (rewrite "sq_neg") (("1" (lemma "sq_lt") (("1" (inst - "-(b!1 / (2 * a!1) + t!1)" "-(b!1 / (2 * a!1) + xl!1)") (("1" (rewrite "sq_neg") (("1" (rewrite "sq_neg") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_lt") (("2" (inst - "(b!1 / (2 * a!1) + t!1)" "-(b!1 / (2 * a!1) + xu!1)") (("1" (rewrite "sq_neg") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "sq_lt") (("2" (inst - "(b!1 / (2 * a!1) + t!1)" "(b!1 / (2 * a!1) + xu!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 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)) nil)) nil)) nil)) nil)) nil) ((quadratic const-decl "real" quadratic nil) (sq const-decl "nonneg_real" sq nil) (sq_nz_pos application-judgement "posreal" sq nil) (sq_eq_abs formula-decl nil sq nil) (sq_neg formula-decl nil sq nil) (sq_lt formula-decl nil sq nil) (canonical_sq formula-decl nil quadratic nil)) nil)) (quad_loc_min_is_glob_min 0 (quad_loc_min_is_glob_min-1 nil 3462526082 ("" (skosimp*) (("" (case "x!1 < -b!1/(2*a!1)") (("1" (name "h" "min(epsil!1/2,-b!1/(2*a!1) - x!1)") (("1" (label "hname" -1) (("1" (label "xcase" -2) (("1" (label "age" -3) (("1" (label "bp" -4) (("1" (label "finalone" 1) (("1" (inst - "x!1+h") (("1" (prop) (("1" (lemma "quad_min_mono_dec") (("1" (inst - "a!1" "b!1" "c!1" "x!1" "x!1 + h") (("1" (assert) (("1" (prop) (("1" (grind) nil nil) ("2" (both-sides "-" "x!1" "xcase") (("2" (assert) (("2" (grind) nil nil)) nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (lift-if) (("2" (assert) (("2" (prop) (("2" (both-sides "-" "x!1" "bp") (("2" (assert) (("2" (both-sides "-" "x!1" "xcase") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (both-sides "-" "x!1" "bp") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "h" "min(epsil!1/2,b!1/(2*a!1) + x!1)") (("2" (inst - "x!1-h") (("2" (assert) (("2" (prop) (("1" (label "quadr" -1) (("1" (label "hname" -2) (("1" (label "age" -3) (("1" (lemma "quad_min_mono_inc") (("1" (inst - "a!1" "b!1" "c!1" "x!1" "x!1-h") (("1" (case "x!1 > -b!1/(2*a!1)") (("1" (label "xcase" -1) (("1" (label "lem1" -2) (("1" (assert) (("1" (prop) (("1" (grind) nil nil) ("2" (both-sides "+" "b!1/(2*a!1)" "xcase") (("1" (case-replace "-b!1 / (2 * a!1) + b!1 / (2 * a!1) = 0") (("1" (expand "min") (("1" (lift-if) (("1" (prop) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "x!1 > -b!1/(2*a!1)") (("1" (label "xcase" -1) (("1" (both-sides "+" "b!1/(2*a!1)" "xcase") (("1" (case-replace "-b!1 / (2 * a!1) + b!1 / (2 * a!1) = 0") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic nil) (sq const-decl "nonneg_real" sq nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (pos_times_gt formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (neg_times_lt formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (quad_min_mono_dec formula-decl nil quad_minmax nil) (both_sides_plus_le1 formula-decl nil real_props nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (both_sides_plus_lt2 formula-decl nil real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (quad_min_mono_inc formula-decl nil quad_minmax nil) (div_distributes formula-decl nil real_props nil)) shostak)) (quad_max 0 (quad_max-2 "" 3431164981 ("" (skosimp*) (("" (assert) (("" (expand "is_maximum?") (("" (skosimp*) (("" (expand "quadratic") (("" (claim "%1 = %2 + a!1 * sq(y!1+b!1/(2*a!1))" t (! 1 r) (! 1 l)) (("" (replace -1 :hide? t) (("" (move-terms 1 l *) (("" (assert) (("" (mult-cases 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq 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) (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (neg_times_ge formula-decl nil real_props nil) (quadratic const-decl "real" quadratic nil) (is_maximum? const-decl "bool" quad_minmax nil)) shostak) (quad_max-1 nil 3402151971 ("" (skosimp*) (("" (lemma "quadratic_max") (("" (inst - "a!1" "b!1" "c!1" "quadratic(a!1,b!1,c!1)" "-b!1/(2*a!1)") (("" (assert) nil nil)) nil)) nil)) nil) ((sq const-decl "nonneg_real" sq nil) (sq_pos formula-decl nil sq nil) (quadratic const-decl "real" quadratic nil)) shostak)) (quad_max_val 0 (quad_max_val-2 "" 3431165161 ("" (skosimp*) (("" (assert) (("" (use "quad_max") (("" (ground) (("" (expand "is_maximum?") (("" (inst?) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_le_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_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic nil) (sq const-decl "nonneg_real" sq nil) (is_maximum? const-decl "bool" quad_minmax nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (quad_max formula-decl nil quad_minmax nil)) shostak) (quad_max_val-1 nil 3402151994 ("" (lemma "quadratic_max_val") (("" (skosimp*) (("" (assert) (("" (flatten) (("" (inst - "a!1" "b!1" "c!1" "quadratic(a!1,b!1,c!1)" "-b!1/(2*a!1)" "x!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sq const-decl "nonneg_real" sq nil) (quadratic const-decl "real" quadratic nil)) shostak)) (quad_max_mono_inc 0 (quad_max_mono_inc-2 "" 3431165712 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (expand "quadratic") (("" (rewrite "canonical_sq") (("" (rewrite "canonical_sq") (("" (field :cancel? t) (("" (lemma "sq_ge") (("" (invoke (inst - "-(%! 1 l 1%)" "-(%! 1 r 1%)")) (("1" (assert) (("1" (rewrite "sq_neg") (("1" (rewrite "sq_neg") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (grind-reals) nil nil) ("3" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_le_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) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic nil) (sq_ge formula-decl nil sq nil) (sq_neg formula-decl nil sq nil) (- const-decl "[numfield -> numfield]" number_fields nil) (b!1 skolem-const-decl "real" quad_minmax nil) (a!1 skolem-const-decl "nonzero_real" quad_minmax nil) (y!1 skolem-const-decl "real" quad_minmax nil) (x!1 skolem-const-decl "real" quad_minmax nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (CBD_7 skolem-const-decl "nzreal" quad_minmax nil) (nzreal nonempty-type-eq-decl nil reals nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (both_sides_minus_le1 formula-decl nil real_props nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (both_sides_times_pos_le2 formula-decl nil real_props nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (< const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (FDX_6 skolem-const-decl "nonzero_real" quad_minmax nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq 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, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (canonical_sq formula-decl nil quadratic nil)) shostak) (quad_max_mono_inc-1 nil 3402152023 ("" (skosimp*) (("" (lemma "quadratic_max_mono_inc") (("" (inst - "a!1" "b!1" "c!1" "quadratic(a!1,b!1,c!1)" "-b!1/(2*a!1)" "x!1" "y!1") (("" (assert) nil nil)) nil)) nil)) nil) ((quadratic const-decl "real" quadratic nil)) shostak)) (quad_max_mono_dec 0 (quad_max_mono_dec-2 "" 3431165830 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (expand "quadratic") (("" (rewrite "canonical_sq") (("" (rewrite "canonical_sq") (("" (field :cancel? t) (("" (rewrite "sq_lt") (("" (field 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic nil) (sq_lt formula-decl nil sq nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (CBD_9 skolem-const-decl "nzreal" quad_minmax nil) (nzreal nonempty-type-eq-decl nil reals nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (both_sides_minus_le1 formula-decl nil real_props nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (both_sides_times_pos_le2 formula-decl nil real_props nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (< const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (FDX_8 skolem-const-decl "nonzero_real" quad_minmax nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (> const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.57 Sekunden (vorverarbeitet) ¤ |
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchenDie farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
