%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 13, 2003 4:25) $$$top.pvs top : THEORY BEGIN IMPORTING square_root, cauchy_schwartz, sqrt2_irrational END top $$$top.prf (|top|) $$$sqrt2_irrational.pvs sqrt2_irrational : THEORY BEGIN IMPORTING square_root m, n: VAR nat p: VAR posnat rational_square_root: LEMMA rational_pred(sqrt(n)) IFF EXISTS m, p: sqrt(n) = m / p %-------------------------------------------------- % Proof as in Freek Wiedijk's "15 Provers" paper %-------------------------------------------------- odd_square: LEMMA odd?(m) IMPLIES odd?(expt(m, 2)) aux: LEMMA expt(m, 2) = 2 * expt(n, 2) IMPLIES m = 0 sqrt2_irrational: PROPOSITION not rational_pred(sqrt(2)) %----------------------- % Generalization %----------------------- sqrt_of_nat_var: PROPOSITION rational_pred(sqrt(n)) IMPLIES EXISTS m: n = m * m sqrt_of_nat: PROPOSITION rational_pred(sqrt(n)) IFF EXISTS m: n = m * m sqrt2_irrational2: PROPOSITION not rational_pred(sqrt(2)) END sqrt2_irrational $$$sqrt2_irrational.prf (sqrt2_irrational (rational_square_root 0 (rational_square_root-1 nil 3245191585 3245592986 ("" (skolem!) (("" (reduce :if-match nil) (("" (use "rational_pred_ax2" ("r" "sqrt(n!1)")) (("" (skolem!) (("" (inst?) (("" (use "pos_div_le") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (>= 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) (pos_div_le formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (sqrt const-decl "nonneg_real" square_root nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rat nonempty-type-eq-decl nil rationals nil) (rational_pred_ax2 formula-decl nil rational_props nil)) 288 260 t shostak)) (odd_square 0 (odd_square-1 nil 3239041137 3245592987 ("" (grind :if-match nil) (("" (inst + "2 * j!1 * j!1 + 2 * j!1") (("" (assert) nil nil)) nil)) nil) unchecked ((* 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) (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) (rational_pred const-decl "[real -> boolean]" rationals 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (odd? const-decl "bool" integers nil)) 491 460 nil nil)) (aux 0 (aux-1 nil 3239041137 3245592988 ("" (induct "m" :name "NAT_induction") (("" (skosimp*) (("" (use "odd_square") (("" (ground) (("1" (replace*) (("1" (rewrite "odd_not_even") nil nil)) nil) ("2" (rewrite "odd_not_even") (("2" (inst - "n!1") (("2" (grind :if-match nil) (("1" (use "zero_times3" ("x" "j!2")) (("1" (inst - "j!2") (("1" (assert) nil nil)) nil)) nil) ("2" (use "both_sides_expt_nonneg_le" ("nny" "n!1" "nnx" "2 * j!2")) (("2" (use "zero_times3" ("x" "n!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((odd_not_even formula-decl nil parity nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_expt_nonneg_le formula-decl nil exponent_props nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (zero_times3 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (even? const-decl "bool" integers nil) (odd_square formula-decl nil sqrt2_irrational nil) (NAT_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (expt def-decl "real" exponentiation nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (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)) 1333 1230 nil nil)) (sqrt2_irrational 0 (sqrt2_irrational-1 nil 3239041137 3245592988 ("" (rewrite "rational_square_root") (("" (skolem!) (("" (use "square_sqrt2") (("" (auto-rewrite "expt_div" "div_cancel3" "even_expt_opposite") (("" (reduce) (("" (forward-chain "aux") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (aux formula-decl nil sqrt2_irrational nil) (expt_div formula-decl nil exponent_props nil) (div_cancel3 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (square_sqrt2 formula-decl nil square_root nil) (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) (rational_square_root formula-decl nil sqrt2_irrational nil)) 322 290 t nil)) (sqrt_of_nat_var 0 (sqrt_of_nat_var-2 nil 3246649171 3246649179 ("" (skosimp) (("" (assert) (("" (rewrite "rational_square_root") (("" (use "wf_nat") (("" (expand "well_founded?") (("" (inst - "{ b: nat | b > 0 AND EXISTS (a: int): sqrt(n!1) = a / b }") (("1" (ground) (("1" (delete -2) (("1" (skosimp* :preds? t) (("1" (use "euclid_int" ("n" "a!1" "b" "y!1")) (("1" (skolem!) (("1" (case "r!1 > 0") (("1" (assert) (("1" (delete -3 -4 1) (("1" (case-replace "a!1 / y!1 = (y!1 * n!1 - q!1 * a!1) / r!1") (("1" (inst - "r!1") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil) ("2" (delete -4) (("2" (rewrite "sqrt_def") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -2 -3 -5) (("2" (assert) (("2" (inst + "q!1") (("2" (auto-rewrite "sqrt_def" "expt") (("2" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skolem!) (("2" (inst + "p!1") (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((rational_square_root formula-decl nil sqrt2_irrational 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) (rational_pred const-decl "[real -> boolean]" rationals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (well_founded? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (r!1 skolem-const-decl "mod(y!1)" sqrt2_irrational nil) (y!1 skolem-const-decl "({b: nat | b > 0 AND (EXISTS (a: int): sqrt(n!1) = a / b)})" sqrt2_irrational nil) (n!1 skolem-const-decl "nat" sqrt2_irrational nil) (sqrt_def formula-decl nil square_root nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (< const-decl "bool" reals nil) (euclid_int formula-decl nil euclidean_division nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sqrt const-decl "nonneg_real" square_root nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (/= const-decl "boolean" notequal nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (wf_nat formula-decl nil naturalnumbers nil)) 6378 910 t nil) (sqrt_of_nat_var-1 nil 3246649114 3246649143 ("" (auto-rewrite "sqrt_square" "sqrt_def") (("" (reduce :if-match nil) (("" (rewrite "rational_square_root") (("" (use "wf_nat") (("" (expand "well_founded?") (("" (inst - "{ b: nat | b > 0 AND EXISTS (a: int): sqrt(n!1) = a / b }") (("1" (ground) (("1" (delete -2 -3) (("1" (skosimp* :preds? t) (("1" (use "euclid_int" ("n" "a!1" "b" "y!1")) (("1" (skolem!) (("1" (inst - "r!1") (("1" (assert) nil nil) ("2" (ground) (("1" (inst + "q!1") (("1" (assert) nil nil)) nil) ("2" (inst + "y!1 * n!1 - q!1 * a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 2) (("2" (skolem!) (("2" (inst + "p!1") (("2" (reduce) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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) (>= 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) (wf_nat formula-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqrt const-decl "nonneg_real" square_root nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (euclid_int formula-decl nil euclidean_division nil) (< const-decl "bool" reals nil) (n!1 skolem-const-decl "nat" sqrt2_irrational nil) (y!1 skolem-const-decl "({b: nat | b > 0 AND (EXISTS (a: int): sqrt(n!1) = a / b)})" sqrt2_irrational nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (r!1 skolem-const-decl "mod(y!1)" sqrt2_irrational nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (well_founded? const-decl "bool" orders nil) (sqrt_def formula-decl nil square_root nil) (rational_square_root formula-decl nil sqrt2_irrational nil)) 17268 5070 t nil)) (sqrt_of_nat 0 (sqrt_of_nat-4 "let PVS do the case split (r > 0), as a TCC" 3245594169 3245594169 ("" (auto-rewrite "sqrt_square" "sqrt_def") (("" (reduce :if-match nil) (("" (rewrite "rational_square_root") (("" (use "wf_nat") (("" (expand "well_founded?") (("" (inst - "{ b: nat | b > 0 AND EXISTS (a: int): sqrt(n!1) = a / b }") (("1" (ground) (("1" (delete -2 -3) (("1" (skosimp* :preds? t) (("1" (use "euclid_int" ("n" "a!1" "b" "y!1")) (("1" (skolem!) (("1" (inst - "r!1") (("1" (assert) nil nil) ("2" (ground) (("1" (inst + "q!1") (("1" (assert) nil nil)) nil) ("2" (inst + "y!1 * n!1 - q!1 * a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 2) (("2" (skolem!) (("2" (inst + "p!1") (("2" (reduce) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((rational_square_root formula-decl nil sqrt2_irrational 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) (rational_pred const-decl "[real -> boolean]" rationals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (well_founded? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (expt def-decl "real" exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt_def formula-decl nil square_root nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (< const-decl "bool" reals nil) (euclid_int formula-decl nil euclidean_division nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sqrt const-decl "nonneg_real" square_root nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (/= const-decl "boolean" notequal nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (wf_nat formula-decl nil naturalnumbers nil)) 92939 5280 t shostak) (sqrt_of_nat-3 "" 3245593713 3245593983 ("" (auto-rewrite "sqrt_square" "sqrt_def") (("" (reduce :if-match nil) (("" (rewrite "rational_square_root") (("" (use "wf_nat") (("" (expand "well_founded?") (("" (inst - "{ b: nat | b > 0 AND EXISTS (a: int): sqrt(n!1) = a / b }") (("1" (ground) (("1" (delete -2 -3) (("1" (skosimp* :preds? t) (("1" (use "euclid_int" ("n" "a!1" "b" "y!1")) (("1" (skolem!) (("1" (case "r!1 > 0") (("1" (assert) (("1" (delete -3 -4 1) (("1" (inst - "r!1") (("1" (assert) nil nil) ("2" (inst + "y!1 * n!1 - q!1 * a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (delete -2 -3 -5) (("2" (assert) (("2" (inst + "q!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -1 2) (("2" (skolem!) (("2" (inst + "p!1") (("2" (reduce) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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) (>= 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) (sqrt_square formula-decl nil square_root nil) (wf_nat formula-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqrt const-decl "nonneg_real" square_root nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (euclid_int formula-decl nil euclidean_division nil) (< const-decl "bool" reals nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (well_founded? const-decl "bool" orders nil) (sqrt_def formula-decl nil square_root nil) (rational_square_root formula-decl nil sqrt2_irrational nil)) 104340 6970 t shostak) (sqrt_of_nat-2 nil 3245513275 3245593602 ("" (auto-rewrite "sqrt_square") (("" (reduce :if-match nil) (("" (rewrite "rational_square_root") (("" (use "wf_nat") (("" (expand "well_founded?") (("" (inst - "{ b: nat | b > 0 AND EXISTS (a: int): sqrt(n!1) = a / b }") (("1" (ground) (("1" (delete -2 -3) (("1" (skosimp* :preds? t) (("1" (use "euclid_int" ("n" "a!1" "b" "y!1")) (("1" (skolem!) (("1" (case "r!1 > 0") (("1" (assert) (("1" (delete -3 -4 1) (("1" (inst - "r!1") (("1" (assert) nil nil) ("2" (inst + "y!1 * n!1 - q!1 * a!1") (("2" (assert) (("2" (auto-rewrite "sqrt_def") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -2 -3 -5) (("2" (assert) (("2" (inst + "q!1") (("2" (rewrite "sqrt_def") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skolem!) (("2" (inst + "p!1") (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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) (>= 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) (sqrt_square formula-decl nil square_root nil) (wf_nat formula-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqrt const-decl "nonneg_real" square_root nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (euclid_int formula-decl nil euclidean_division nil) (< const-decl "bool" reals nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (well_founded? const-decl "bool" orders nil) (sqrt_def formula-decl nil square_root nil) (rational_square_root formula-decl nil sqrt2_irrational nil)) 151472 8140 t nil) (sqrt_of_nat-1 nil 3245190233 3246648846 ("" (skosimp) (("" (assert) (("" (rewrite "rational_square_root") (("" (use "wf_nat") (("" (expand "well_founded?") (("" (inst - "{ b: nat | b > 0 AND EXISTS (a: int): sqrt(n!1) = a / b }") (("1" (ground) (("1" (delete -2) (("1" (skosimp* :preds? t) (("1" (use "euclid_int" ("n" "a!1" "b" "y!1")) (("1" (skolem!) (("1" (case "r!1 > 0") (("1" (assert) (("1" (delete -3 -4 1) (("1" (case-replace "a!1 / y!1 = (y!1 * n!1 - q!1 * a!1) / r!1") (("1" (inst - "r!1") (("1" (assert) nil nil) ("2" (inst?) nil nil)) nil) ("2" (delete -4) (("2" (rewrite "sqrt_def") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete -2 -3 -5) (("2" (assert) (("2" (inst + "q!1") (("2" (auto-rewrite "sqrt_def" "expt") (("2" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skolem!) (("2" (inst + "p!1") (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((wf_nat formula-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqrt const-decl "nonneg_real" square_root nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (euclid_int formula-decl nil euclidean_division nil) (< const-decl "bool" reals nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (sqrt_def formula-decl nil square_root nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation nil) (NOT const-decl "[bool -> bool]" booleans nil) (well_founded? const-decl "bool" orders nil) (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) (rational_square_root formula-decl nil sqrt2_irrational nil)) 11227 560 t nil)) (sqrt2_irrational2 0 (sqrt2_irrational2-1 nil 3245192267 3245592990 ("" (rewrite "sqrt_of_nat") (("" (skolem!) (("" (use "both_sides_expt_nonneg_lt" ("nnx" "m!1" "p" "2" "nny" "2")) (("" (auto-rewrite "expt") (("" (assert) (("" (case-replace "m!1 = 1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((= const-decl "[T, T -> boolean]" equalities nil) (expt def-decl "real" exponentiation nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_expt_nonneg_lt formula-decl nil exponent_props nil) (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) (sqrt_of_nat formula-decl nil sqrt2_irrational nil)) 321 310 t shostak))) $$$quadratic_polynomials.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Notations: % Q(a, b, c) = lambda x: a x^2 + b x + c % D(a, b, c) = discriminant = b^2 - 4 ac % % If D(a, b, c) >= 0 AND a /= 0, the two roots of Q(a, b, c) are % S1(a, b, c) = (- b + sqrt(b^2 - 4 ac)) /2a % S2(a, b, c) = (- b - sqrt(b^2 - 4 ac)) /2a % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% quadratic_polynomials : THEORY BEGIN IMPORTING square_root a, b, c: VAR real x, y, z: VAR real f, g: VAR [real -> real] nza: VAR nzreal pa: VAR posreal na: VAR negreal %-------------- % Identities %-------------- square_sum: LEMMA expt(a + b, 2) = expt(a, 2) + 2*a*b + expt(b, 2) square_diff: LEMMA expt(a - b, 2) = expt(a, 2) - 2*a*b + expt(b, 2) diff_squares: LEMMA expt(a, 2) - expt(b, 2) = (a + b) * (a - b) square_x_plus_1: LEMMA expt(x + 1, 2) = expt(x, 2) + 2 * x + 1 square_x_minus_1: LEMMA expt(x - 1, 2) = expt(x, 2) - 2 * x + 1 %------------------------- % quadratic polynomial %------------------------- Q(a, b, c)(x): real = a * expt(x, 2) + b * x + c quadra_equiv: LEMMA Q(a, b, c)(x) = a * x^2 + b * x + c %-------------------------------------------------- % a x^2 + b x + c = a (x + b/2a)^2 + c - b^2/4a %-------------------------------------------------- quadra_identity: LEMMA Q(nza, b, c)(x) = nza * expt(x + b/(2 * nza), 2) + c - expt(b, 2)/(4*nza) quadra_identity2: LEMMA Q(nza, b, c)(x) = Q(nza, 0, c - expt(b, 2)/(4*nza))(x + b/(2 * nza)) symmetry1: LEMMA Q(nza, b, c)(x) = Q(nza, b, c)(- b/nza - x) symmetry2: LEMMA x + y = -b/nza IMPLIES Q(nza, b, c)(y) = Q(nza, b, c)(x) %-------------------------------------------------------------- % intervals where the polynomial is increasing or decreasing % depending on wheter a is positive/negative %-------------------------------------------------------------- decreasing_pos_left: LEMMA x < y AND y <= -b/(2*pa) IMPLIES Q(pa, b, c)(x) > Q(pa, b, c)(y) increasing_pos_right: LEMMA -b/(2*pa) <= x AND x < y IMPLIES Q(pa, b, c)(x) < Q(pa, b, c)(y) increasing_neg_left: LEMMA x < y AND y <= -b/(2*na) IMPLIES Q(na, b, c)(x) < Q(na, b, c)(y) decreasing_neg_right: LEMMA -b/(2*na) <= x AND x < y IMPLIES Q(na, b, c)(x) > Q(na, b, c)(y) %----------------------------------------------------- % -b/2a is a minimum or a maximum of the polynomial %----------------------------------------------------- minimum_pos: LEMMA Q(pa, b, c)(-b/(2*pa)) <= Q(pa, b, c)(x) maximum_neg: LEMMA Q(na, b, c)(-b/(2*na)) >= Q(na, b, c)(x) %-------------------------------------------------- % the polynomial gets arbitrarily large or small % depending on whether a is positive/negative %-------------------------------------------------- infinity_pos: LEMMA FORALL y: EXISTS x: Q(pa, b, c)(x) > y infinity_neg: LEMMA FORALL y: EXISTS x: Q(na, b, c)(x) < y %--------------------------- % Zeros of the polynomial %--------------------------- D(a, b, c): real = expt(b, 2) - 4 * a * c quadra_zero_equiv: LEMMA Q(nza, b, c)(x) = 0 IFF expt(x + b/(2 * nza), 2) = D(nza, b, c)/expt(2 * nza, 2) %--------------------------------------------------- % Two solutions: S1(a, b, c) and S2(a, b, c) % defined provided D(a, b, c) is not negative %--------------------------------------------------- S1(nza, b, (c | D(nza, b, c) >= 0)): real = (- b + sqrt(D(nza, b, c))) / (2 * nza) S2(nza, b, (c | D(nza, b, c) >= 0)): real = (- b - sqrt(D(nza, b, c))) / (2 * nza) quadra_first_zero: LEMMA D(nza, b, c) >= 0 IMPLIES Q(nza, b, c)(S1(nza, b, c)) = 0 quadra_second_zero: LEMMA D(nza, b, c) >= 0 IMPLIES Q(nza, b, c)(S2(nza, b, c)) = 0 sum_zeros: LEMMA D(nza, b, c) >= 0 IMPLIES S1(nza, b, c) + S2(nza, b, c) = - b/nza prod_zeros: LEMMA D(nza, b, c) >= 0 IMPLIES S1(nza, b, c) * S2(nza, b, c) = c/nza quadra_factorization: LEMMA D(nza, b, c) >= 0 IMPLIES Q(nza, b, c) = lambda x: nza * (x - S1(nza, b, c)) * (x - S2(nza, b, c)) quadra_zeros: LEMMA D(nza, b, c) >= 0 IMPLIES (Q(nza, b, c)(x) = 0 IFF x = S1(nza, b, c) OR x = S2(nza, b, c)) unique_zero: LEMMA D(nza, b, c) = 0 IMPLIES (Q(nza, b, c)(x) = 0 IFF x = - b / (2 * nza)) quadra_factorization2: LEMMA D(nza, b, c) = 0 IMPLIES Q(nza, b, c) = lambda x: nza * expt(x + b/(2*nza), 2) %---------------------------------------------------------- % Constraints for a x^2 + bx + c to be positive/negative %---------------------------------------------------------- existence_of_zeros: LEMMA (EXISTS x: Q(nza, b, c)(x) = 0) IFF D(nza, b, c) >= 0 quadra_positive: LEMMA (FORALL x: Q(nza, b, c)(x) > 0) IFF (D(nza, b, c) < 0 AND nza > 0) quadra_negative: LEMMA (FORALL x: Q(nza, b, c)(x) < 0) IFF (D(nza, b, c) < 0 AND nza < 0) positive_discriminant1: LEMMA D(nza, b, c) > 0 IMPLIES (EXISTS x: Q(nza, b, c)(x) > 0) positive_discriminant2: LEMMA D(nza, b, c) > 0 IMPLIES (EXISTS x: Q(nza, b, c)(x) < 0) quadra_positive2: LEMMA (FORALL x: Q(nza, b, c)(x) >= 0) IMPLIES D(nza, b, c) <= 0 quadra_negative2: LEMMA (FORALL x: Q(nza, b, c)(x) <= 0) IMPLIES D(nza, b, c) <= 0 END quadratic_polynomials $$$quadratic_polynomials.prf (quadratic_polynomials (square_sum 0 (square_sum-1 nil 3243631995 3245096894 ("" (grind) nil nil) proved ((expt def-decl "real" exponentiation nil)) 223 190 nil nil)) (square_diff 0 (square_diff-1 nil 3243631995 3245096894 ("" (grind) nil nil) proved ((expt def-decl "real" exponentiation nil)) 199 190 nil nil)) (diff_squares 0 (diff_squares-1 nil 3243631995 3245096894 ("" (grind) nil nil) proved ((expt def-decl "real" exponentiation nil)) 138 120 nil nil)) (square_x_plus_1 0 (square_x_plus_1-1 nil 3243631995 3245096894 ("" (grind) nil nil) proved ((expt def-decl "real" exponentiation nil)) 136 120 nil nil)) (square_x_minus_1 0 (square_x_minus_1-1 nil 3243631995 3245096894 ("" (grind) nil nil) proved ((expt def-decl "real" exponentiation nil)) 143 130 nil nil)) (quadra_equiv_TCC1 0 (quadra_equiv_TCC1-1 nil 3243631995 3245096434 ("" (subtype-tcc) nil nil) proved-complete ((/= const-decl "boolean" notequal nil)) 15 20 nil nil)) (quadra_equiv 0 (quadra_equiv-1 nil 3243631995 3245096894 ("" (grind :exclude ("expt")) nil nil) proved ((^ const-decl "real" exponentiation nil) (Q const-decl "real" quadratic_polynomials nil)) 98 100 nil nil)) (quadra_identity 0 (quadra_identity-1 nil 3243631995 3245096895 ("" (grind) nil nil) proved ((expt def-decl "real" exponentiation nil) (Q const-decl "real" quadratic_polynomials nil)) 339 330 nil nil)) (quadra_identity2 0 (quadra_identity2-1 nil 3243631995 3245097203 ("" (skolem!) (("" (rewrite "quadra_identity") (("" (expand "Q") (("" (propax) nil nil)) nil)) nil)) nil) proved ((quadra_identity formula-decl nil quadratic_polynomials 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) (nzreal nonempty-type-eq-decl nil reals nil) (Q const-decl "real" quadratic_polynomials nil)) 10797 840 t nil)) (symmetry1 0 (symmetry1-1 nil 3243631995 3245096895 ("" (grind) nil nil) proved ((expt def-decl "real" exponentiation nil) (Q const-decl "real" quadratic_polynomials nil)) 278 280 nil nil)) (symmetry2 0 (symmetry2-1 nil 3243631995 3245096895 ("" (skosimp) (("" (rewrite "symmetry1") (("" (assert) nil nil)) nil)) nil) proved ((symmetry1 formula-decl nil quadratic_polynomials 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) (nzreal nonempty-type-eq-decl nil reals nil)) 120 110 nil nil)) (decreasing_pos_left 0 (decreasing_pos_left-1 nil 3243631995 3245096896 ("" (skosimp) (("" (auto-rewrite "quadra_identity") (("" (assert) (("" (case "pa!1 * expt(b!1 / (2 * pa!1) + x!1, 2) > pa!1 * expt(b!1 / (2 * pa!1) + y!1, 2)") (("1" (assert) nil nil) ("2" (auto-rewrite "both_sides_times_pos_gt2" "both_sides_expt_nonpos_even_gt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((/ 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) (expt def-decl "real" exponentiation 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) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (both_sides_expt_nonpos_even_gt formula-decl nil exponent_props nil) (both_sides_times_pos_gt2 formula-decl nil real_props nil) (quadra_identity formula-decl nil quadratic_polynomials nil)) 415 380 nil nil)) (increasing_pos_right 0 (increasing_pos_right-1 nil 3243631995 3245096896 ("" (skosimp) (("" (auto-rewrite "quadra_identity") (("" (assert) (("" (case "pa!1 * expt(b!1 / (2 * pa!1) + x!1, 2) < pa!1 * expt(b!1 / (2 * pa!1) + y!1, 2)") (("1" (assert) nil nil) ("2" (auto-rewrite "both_sides_times_pos_lt2" "both_sides_expt_nonneg_lt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((/ 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) (expt def-decl "real" exponentiation 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) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (both_sides_expt_nonneg_lt formula-decl nil exponent_props nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (quadra_identity formula-decl nil quadratic_polynomials nil)) 413 400 nil nil)) (increasing_neg_left 0 (increasing_neg_left-1 nil 3243631995 3245096897 ("" (skosimp) (("" (auto-rewrite "quadra_identity") (("" (assert) (("" (case "na!1 * expt(b!1 / (2 * na!1) + x!1, 2) < na!1 * expt(b!1 / (2 * na!1) + y!1, 2)") (("1" (assert) nil nil) ("2" (auto-rewrite "both_sides_times_neg_lt2" "both_sides_expt_nonpos_even_lt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((/ 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) (expt def-decl "real" exponentiation 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) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (both_sides_expt_nonpos_even_lt formula-decl nil exponent_props nil) (both_sides_times_neg_lt2 formula-decl nil real_props nil) (quadra_identity formula-decl nil quadratic_polynomials nil)) 393 380 nil nil)) (decreasing_neg_right 0 (decreasing_neg_right-1 nil 3243631995 3245096897 ("" (skosimp) (("" (auto-rewrite "quadra_identity") (("" (assert) (("" (case "na!1 * expt(b!1 / (2 * na!1) + x!1, 2) > na!1 * expt(b!1 / (2 * na!1) + y!1, 2)") (("1" (assert) nil nil) ("2" (auto-rewrite "both_sides_times_neg_gt2" "both_sides_expt_nonneg_gt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((/ 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) (expt def-decl "real" exponentiation 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) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (both_sides_expt_nonneg_gt formula-decl nil exponent_props nil) (both_sides_times_neg_gt2 formula-decl nil real_props nil) (quadra_identity formula-decl nil quadratic_polynomials nil)) 384 360 nil nil)) (minimum_pos 0 (minimum_pos-1 nil 3243631995 3245096897 ("" (skolem!) (("" (use "decreasing_pos_left" ("x" "x!1" "y" "-b!1 / (2 * pa!1)")) (("" (use "increasing_pos_right" ("x" "-b!1 / (2 * pa!1)" "y" "x!1")) (("" (smash) nil nil)) nil)) nil)) nil) proved ((decreasing_pos_left formula-decl nil quadratic_polynomials 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[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) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (increasing_pos_right formula-decl nil quadratic_polynomials nil)) 469 430 nil nil)) (maximum_neg 0 (maximum_neg-1 nil 3243631995 3245096898 ("" (skolem!) (("" (use "increasing_neg_left" ("x" "x!1" "y" "-b!1 / (2 * na!1)")) (("" (use "decreasing_neg_right" ("x" "-b!1 / (2 * na!1)" "y" "x!1")) (("" (assert) nil nil)) nil)) nil)) nil) proved ((increasing_neg_left formula-decl nil quadratic_polynomials 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) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (decreasing_neg_right formula-decl nil quadratic_polynomials nil)) 424 400 nil nil)) (infinity_pos 0 (infinity_pos-1 nil 3243631995 3245097248 ("" (case "FORALL pa, c, y: EXISTS x: Q(pa, 0, c)(x) >= y") (("1" (skolem!) (("1" (inst - "pa!1" "c!1 - expt(b!1, 2)/(4*pa!1)" "y!1+1") (("1" (skolem!) (("1" (inst + "x!1 - b!1/(2*pa!1)") (("1" (rewrite "quadra_identity2" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skolem!) (("2" (expand "Q") (("2" (auto-rewrite "expt_zero" "square_sqrt2" "div_cancel1" "div_cancel2") (("2" (case "(y!1 - c!1)/pa!1 >= 0") (("1" (assert) (("1" (inst + "sqrt((y!1 - c!1)/pa!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "pos_div_ge") (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((sqrt const-decl "nonneg_real" square_root nil) (div_cancel1 formula-decl nil real_props nil) (square_sqrt2 formula-decl nil square_root nil) (expt_zero formula-decl nil exponent_props nil) (pos_div_ge formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (quadra_identity2 formula-decl nil quadratic_polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation 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) (/ 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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (Q const-decl "real" quadratic_polynomials nil)) 27175 3910 t nil)) (infinity_neg 0 (infinity_neg-2 nil 3245097263 3245097269 ("" (case "FORALL na, c, y: EXISTS x: Q(na, 0, c)(x) <= y") (("1" (skolem!) (("1" (inst - "na!1" "c!1 - expt(b!1, 2)/(4*na!1)" "y!1-1") (("1" (skolem!) (("1" (inst + "x!1 - b!1/(2*na!1)") (("1" (rewrite "quadra_identity2" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skolem!) (("2" (expand "Q") (("2" (auto-rewrite "expt_zero" "square_sqrt2" "div_cancel1" "div_cancel2") (("2" (case "(y!1 - c!1)/na!1 >= 0") (("1" (assert) (("1" (inst + "sqrt((y!1 - c!1) / na!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "pos_div_ge") (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((Q const-decl "real" quadratic_polynomials nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" 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) (rational_pred const-decl "[real -> boolean]" rationals 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (quadra_identity2 formula-decl nil quadratic_polynomials nil) (nzreal nonempty-type-eq-decl nil reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (pos_div_ge formula-decl nil real_props nil) (expt_zero formula-decl nil exponent_props nil) (square_sqrt2 formula-decl nil square_root nil) (div_cancel1 formula-decl nil real_props nil) (sqrt const-decl "nonneg_real" square_root nil) (nonneg_real nonempty-type-eq-decl nil real_types nil)) 5115 520 t nil) (infinity_neg-1 nil 3243631995 3245096898 ("" (case "FORALL na, c, y: EXISTS x: q(na, 0, c)(x) <= y") (("1" (skolem!) (("1" (inst - "na!1" "c!1 - expt(b!1, 2)/(4*na!1)" "y!1-1") (("1" (skolem!) (("1" (inst + "x!1 - b!1/(2*na!1)") (("1" (rewrite "quadra_identity2" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skolem!) (("2" (expand "q") (("2" (auto-rewrite "expt_zero" "square_sqrt2" "div_cancel1" "div_cancel2") (("2" (case "(y!1 - c!1)/na!1 >= 0") (("1" (assert) (("1" (inst + "sqrt((y!1 - c!1) / na!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "pos_div_ge") (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((nonneg_real nonempty-type-eq-decl nil real_types nil) (sqrt const-decl "nonneg_real" square_root nil) (div_cancel1 formula-decl nil real_props nil) (square_sqrt2 formula-decl nil square_root nil) (expt_zero formula-decl nil exponent_props nil) (pos_div_ge formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (quadra_identity2 formula-decl nil quadratic_polynomials nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation 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) (/ 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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) nil) 9 0 t nil)) (quadra_zero_equiv 0 (quadra_zero_equiv-1 nil 3243631995 3245096899 ("" (skolem!) (("" (case-replace "D(nza!1, b!1, c!1) / expt(2 * nza!1, 2) = (D(nza!1, b!1, c!1) / (4 * nza!1)) / nza!1") (("1" (delete -) (("1" (rewrite "div_cancel4") (("1" (rewrite "quadra_identity") (("1" (expand "D") (("1" (rewrite "div_distributes_minus" :dir rl) (("1" (smash) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (auto-rewrite "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((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) (number_field nonempty-type-from-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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (D const-decl "real" quadratic_polynomials nil) (nzreal nonempty-type-eq-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (div_distributes_minus formula-decl nil real_props nil) (quadra_identity formula-decl nil quadratic_polynomials nil)) 677 650 t nil)) (S1_TCC1 0 (S1_TCC1-1 nil 3243631995 3245096439 ("" (subtype-tcc) nil nil) proved-complete ((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 "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (>= const-decl "bool" reals nil) (D const-decl "real" quadratic_polynomials nil)) 371 350 nil nil)) (quadra_first_zero 0 (quadra_first_zero-2 nil 3245096791 3245096899 ("" (expand "S1") (("" (skosimp) (("" (assert) (("" (rewrite "quadra_zero_equiv") (("" (assert) (("" (auto-rewrite "expt_div" "square_sqrt2") (("" (case-replace "(sqrt(D(nza!1, b!1, c!1)) + -b!1) / (2 * nza!1) + b!1 / (2 * nza!1) = sqrt(D(nza!1, b!1, c!1)) / (2 * nza!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((quadra_zero_equiv formula-decl nil quadratic_polynomials 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) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> 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) (sqrt const-decl "nonneg_real" square_root nil) (D const-decl "real" quadratic_polynomials nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (square_sqrt2 formula-decl nil square_root nil) (expt_div formula-decl nil exponent_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (S1 const-decl "real" quadratic_polynomials nil)) 412 380 t nil) (quadra_first_zero-1 nil 3243631995 3245096440 ("" (expand "S1") (("" (skosimp) (("" (assert) (("" (rewrite "quadra_zero_equiv") (("" (assert) (("" (auto-rewrite "expt_div" "square_sqrt2") (("" (case-replace "(sqrt(Delta(nza!1, b!1, c!1)) + -b!1) / (2 * nza!1) + b!1 / (2 * nza!1) = sqrt(Delta(nza!1, b!1, c!1)) / (2 * nza!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((quadra_zero_equiv formula-decl nil quadratic_polynomials 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) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> 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) (sqrt const-decl "nonneg_real" square_root nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (square_sqrt2 formula-decl nil square_root nil) (expt_div formula-decl nil exponent_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (S1 const-decl "real" quadratic_polynomials nil)) 308 270 nil nil)) (quadra_second_zero 0 (quadra_second_zero-1 nil 3243631995 3245096899 ("" (skosimp) (("" (forward-chain "quadra_first_zero") (("" (auto-rewrite "S1" "S2") (("" (rewrite "symmetry1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((quadra_first_zero formula-decl nil quadratic_polynomials 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) (nzreal nonempty-type-eq-decl nil reals nil) (symmetry1 formula-decl nil quadratic_polynomials nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (D const-decl "real" quadratic_polynomials nil) (S1 const-decl "real" quadratic_polynomials nil) (S2 const-decl "real" quadratic_polynomials nil)) 247 230 nil nil)) (sum_zeros 0 (sum_zeros-1 nil 3243631995 3245096899 ("" (grind :exclude ("Delta" "sqrt")) nil nil) proved ((S2 const-decl "real" quadratic_polynomials nil) (S1 const-decl "real" quadratic_polynomials nil) (D const-decl "real" quadratic_polynomials nil) (expt def-decl "real" exponentiation nil)) 245 230 nil nil)) (prod_zeros 0 (prod_zeros-1 nil 3243631995 3245096900 ("" (skosimp) (("" (expand* "S1" "S2") (("" (assert) (("" (rewrite "div_times") (("" (auto-rewrite "square_sqrt" "expt" "D") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((S2 const-decl "real" quadratic_polynomials nil) (S1 const-decl "real" quadratic_polynomials nil) (div_times formula-decl nil real_props 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals 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) (sqrt const-decl "nonneg_real" square_root nil) (D const-decl "real" quadratic_polynomials nil) (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation nil) (square_sqrt formula-decl nil square_root nil)) 659 630 t nil)) (quadra_factorization 0 (quadra_factorization-2 nil 3245097298 3245097306 ("" (skosimp) (("" (auto-rewrite "Q" "expt") (("" (apply-extensionality :hide? t) (("" (rewrite "prod_zeros") (("" (case "(S1(nza!1, b!1, c!1) + S2(nza!1, b!1, c!1)) * nza!1 * x!1 = -b!1 * x!1") (("1" (assert) nil nil) ("2" (rewrite "sum_zeros") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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) (S2 const-decl "real" quadratic_polynomials nil) (S1 const-decl "real" quadratic_polynomials 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) (Q const-decl "real" quadratic_polynomials nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (D const-decl "real" quadratic_polynomials nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (nza!1 skolem-const-decl "nzreal" quadratic_polynomials nil) (b!1 skolem-const-decl "real" quadratic_polynomials nil) (c!1 skolem-const-decl "real" quadratic_polynomials nil) (expt def-decl "real" exponentiation nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sum_zeros formula-decl nil quadratic_polynomials nil) (prod_zeros formula-decl nil quadratic_polynomials nil)) 5630 840 t nil) (quadra_factorization-1 nil 3243631995 3245096901 ("" (skosimp) (("" (auto-rewrite "q" "expt") (("" (apply-extensionality :hide? t) (("" (rewrite "prod_zeros") (("" (case "(S1(nza!1, b!1, c!1) + S2(nza!1, b!1, c!1)) * nza!1 * x!1 = -b!1 * x!1") (("1" (assert) nil nil) ("2" (rewrite "sum_zeros") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((prod_zeros formula-decl nil quadratic_polynomials nil) (sum_zeros formula-decl nil quadratic_polynomials nil) (- const-decl "[numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (expt def-decl "real" exponentiation nil) nil nil nil (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (D const-decl "real" quadratic_polynomials nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) 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) (S1 const-decl "real" quadratic_polynomials nil) (S2 const-decl "real" quadratic_polynomials 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)) 658 590 t nil)) (quadra_zeros 0 (quadra_zeros-1 nil 3243631995 3245096902 ("" (auto-rewrite "quadra_first_zero" "quadra_second_zero") (("" (reduce) (("" (forward-chain "quadra_factorization") (("" (replace*) (("" (beta) (("" (auto-rewrite "zero_times3") (("" (name-replace "aux!1" "x!1 - S1(nza!1, b!1, c!1)" :hide? nil) (("" (name-replace "aux!2" "x!1 - S2(nza!1, b!1, c!1)" :hide? nil) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((nzreal 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) (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) (quadra_second_zero formula-decl nil quadratic_polynomials nil) (quadra_first_zero formula-decl nil quadratic_polynomials nil) (S2 const-decl "real" quadratic_polynomials nil) (zero_times3 formula-decl nil real_props nil) (S1 const-decl "real" quadratic_polynomials nil) (D const-decl "real" quadratic_polynomials nil) (>= const-decl "bool" reals 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) (quadra_factorization formula-decl nil quadratic_polynomials nil)) 713 670 nil nil)) (unique_zero 0 (unique_zero-1 nil 3243631995 3245096902 ("" (skosimp) (("" (assert) (("" (auto-rewrite "quadra_zeros" "S1" "S2" "sqrt_zero") (("" (reduce) nil nil)) nil)) nil)) nil) proved ((sqrt_zero formula-decl nil square_root nil) (S1 const-decl "real" quadratic_polynomials nil) (S2 const-decl "real" quadratic_polynomials nil) (quadra_zeros formula-decl nil quadratic_polynomials nil)) 340 330 nil nil)) (quadra_factorization2 0 (quadra_factorization2-1 nil 3243631995 3245096903 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (rewrite "quadra_factorization") (("" (case "S1(nza!1, b!1, c!1) = - b!1 /(2*nza!1) AND S2(nza!1, b!1, c!1) = -b!1/(2*nza!1)") (("1" (auto-rewrite "expt") (("1" (ground) nil nil)) nil) ("2" (delete 2) (("2" (use* "quadra_first_zero" "quadra_second_zero") (("2" (auto-rewrite "unique_zero") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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 "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation nil) (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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (Q const-decl "real" quadratic_polynomials nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (D const-decl "real" quadratic_polynomials nil) (S1 const-decl "real" quadratic_polynomials nil) (- const-decl "[numfield -> numfield]" number_fields nil) (S2 const-decl "real" quadratic_polynomials nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (quadra_first_zero formula-decl nil quadratic_polynomials nil) (quadra_second_zero formula-decl nil quadratic_polynomials nil) (unique_zero formula-decl nil quadratic_polynomials nil) (quadra_factorization formula-decl nil quadratic_polynomials nil)) 954 900 nil nil)) (existence_of_zeros 0 (existence_of_zeros-1 nil 3243631995 3245096903 ("" (skolem!) (("" (ground) (("1" (skolem!) (("1" (rewrite "quadra_zero_equiv") (("1" (rewrite "div_cancel4") (("1" (replace -1 + rl) (("1" (auto-rewrite "pos_times_ge" "expt_even_is_nonneg") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (forward-chain "quadra_first_zero") (("2" (inst?) nil nil)) nil)) nil)) nil) proved ((quadra_zero_equiv formula-decl nil quadratic_polynomials 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) (nzreal nonempty-type-eq-decl nil 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) (D const-decl "real" quadratic_polynomials nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (expt def-decl "real" exponentiation nil) (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) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel4 formula-decl nil real_props nil) (S1 const-decl "real" quadratic_polynomials nil) (quadra_first_zero formula-decl nil quadratic_polynomials nil)) 315 280 nil nil)) (quadra_positive 0 (quadra_positive-1 nil 3243631995 3245097429 ("" (skolem!) (("" (smash) (("1" (use "infinity_neg" ("y" "0")) (("1" (skolem!) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (use "existence_of_zeros") (("2" (assert) (("2" (skolem!) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skolem!) (("3" (rewrite "quadra_identity") (("3" (case "expt(b!1, 2) / (4 * nza!1) < c!1 AND nza!1 * expt(b!1 / (2 * nza!1) + x!1, 2) >= 0") (("1" (ground) nil nil) ("2" (delete 2) (("2" (auto-rewrite "pos_times_ge" "expt_even_is_nonneg" "div_mult_pos_lt1" "D") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (infinity_neg formula-decl nil quadratic_polynomials nil) (existence_of_zeros formula-decl nil quadratic_polynomials nil) (quadra_identity formula-decl nil quadratic_polynomials nil) (D const-decl "real" quadratic_polynomials nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) 102032 3920 t nil)) (quadra_negative 0 (quadra_negative-2 nil 3245097443 3245097449 ("" (skolem!) (("" (smash) (("1" (use "infinity_pos" ("y" "0")) (("1" (skolem!) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (use "existence_of_zeros") (("2" (assert) (("2" (skolem!) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skolem!) (("3" (rewrite "quadra_identity") (("3" (case "expt(b!1, 2) / (4 * nza!1) > c!1 AND nza!1 * expt(b!1 / (2 * nza!1) + x!1, 2) <= 0") (("1" (ground) nil nil) ("2" (delete 2) (("2" (auto-rewrite "neg_times_le" "div_mult_neg_gt2" "D") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (neg_times_le formula-decl nil real_props nil) (div_mult_neg_gt2 formula-decl nil real_props nil) (D const-decl "real" quadratic_polynomials nil) (quadra_identity formula-decl nil quadratic_polynomials nil) (existence_of_zeros formula-decl nil quadratic_polynomials nil) (infinity_pos formula-decl nil quadratic_polynomials 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) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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)) 4396 500 t nil) (quadra_negative-1 nil 3243631995 3245096904 ("" (skolem!) (("" (smash) (("1" (use "infinity_pos" ("y" "0")) (("1" (skolem!) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (use "existence_of_zeros") (("2" (assert) (("2" (skolem!) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skolem!) (("3" (rewrite "quadra_identity") (("3" (case "expt(b!1, 2) / (4 * nza!1) > c!1 AND nza!1 * expt(b!1 / (2 * nza!1) + x!1, 2) <= 0") (("1" (ground) nil nil) ("2" (delete 2) (("2" (auto-rewrite "neg_times_le" "div_mult_neg_gt2" "Delta") (("2" (assert) (("2" (delete -1) (("2" (use "expt_even_is_nonneg") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((bool nonempty-type-eq-decl nil booleans 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 "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (infinity_pos formula-decl nil quadratic_polynomials nil) (existence_of_zeros formula-decl nil quadratic_polynomials nil) (quadra_identity formula-decl nil quadratic_polynomials nil) (div_mult_neg_gt2 formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) 556 500 nil nil)) (positive_discriminant1 0 (positive_discriminant1-1 nil 3245079501 3245097492 ("" (skosimp) (("" (assert) (("" (case "nza!1 > 0") (("1" (rewrite "infinity_pos") nil nil) ("2" (assert) (("2" (inst + "-b!1/(2*nza!1)") (("2" (auto-rewrite "quadra_first_zero") (("2" (use "quadra_zeros") (("2" (use "null_sqrt" ("x" "D(nza!1, b!1, c!1)")) (("2" (assert) (("2" (expand* "S1" "S2") (("2" (use "maximum_neg" ("x" "S1(nza!1, b!1, c!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((D const-decl "real" quadratic_polynomials nil) (null_sqrt formula-decl nil square_root nil) (S2 const-decl "real" quadratic_polynomials nil) (S1 const-decl "real" quadratic_polynomials nil) (quadra_first_zero formula-decl nil quadratic_polynomials nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (maximum_neg formula-decl nil quadratic_polynomials nil) (quadra_zeros formula-decl nil quadratic_polynomials 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) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (infinity_pos formula-decl nil quadratic_polynomials nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) 24105 2900 t shostak)) (positive_discriminant2 0 (positive_discriminant2-1 nil 3245092652 3245097515 ("" (skosimp) (("" (assert) (("" (case "nza!1 < 0") (("1" (rewrite "infinity_neg") nil nil) ("2" (assert) (("2" (inst + "-b!1/(2*nza!1)") (("2" (auto-rewrite "quadra_first_zero") (("2" (use "quadra_zeros") (("2" (use "null_sqrt" ("x" "D(nza!1, b!1, c!1)")) (("2" (assert) (("2" (expand* "S1" "S2") (("2" (use "minimum_pos" ("x" "S1(nza!1, b!1, c!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((D const-decl "real" quadratic_polynomials nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (null_sqrt formula-decl nil square_root nil) (S2 const-decl "real" quadratic_polynomials nil) (S1 const-decl "real" quadratic_polynomials nil) (quadra_first_zero formula-decl nil quadratic_polynomials nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (minimum_pos formula-decl nil quadratic_polynomials nil) (quadra_zeros formula-decl nil quadratic_polynomials 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) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (infinity_neg formula-decl nil quadratic_polynomials nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) 19664 2880 t nil)) (quadra_positive2 0 (quadra_positive2-1 nil 3245092714 3245096905 ("" (skosimp) (("" (use "positive_discriminant2") (("" (assert) (("" (skolem!) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((positive_discriminant2 formula-decl nil quadratic_polynomials nil) (nzreal 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)) 73 60 t shostak)) (quadra_negative2 0 (quadra_negative2-1 nil 3245092834 3245096905 ("" (skosimp) (("" (use "positive_discriminant1") (("" (assert) (("" (skolem!) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((positive_discriminant1 formula-decl nil quadratic_polynomials nil) (nzreal 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)) 72 60 t nil))) $$$cauchy_schwartz.pvs cauchy_schwartz : THEORY BEGIN IMPORTING quadratic_polynomials u, v: VAR [nat -> real] i, j, n: VAR nat x, y, z: VAR real %----------------------------------- % sum(n, u) = u(0) + ... + u(n-1) %----------------------------------- sum(n, u): RECURSIVE real = IF n=0 THEN 0 ELSE sum(n-1, u) + u(n-1) ENDIF MEASURE n w: VAR [nat -> nonneg_real] nonneg_sum: JUDGEMENT sum(n, w) HAS_TYPE nonneg_real %------------------------------------- % sum of squares and sum of products %------------------------------------- sum_sq(n, u): nonneg_real = sum(n, lambda i: expt(u(i), 2)) sum_p(n, u, v): real = sum(n, lambda i: u(i) * v(i)) sum_square_zero: LEMMA sum_sq(n, u) = 0 IMPLIES FORALL (i: below(n)): u(i) = 0 sum_product_zero: LEMMA (FORALL (i: below(n)): u(i) = 0) IMPLIES sum_p(n, u, v) = 0 %--------------------------------- % Polynomial used in the proof %-------------------------------- P(n, u, v)(x): nonneg_real = sum(n, lambda i: expt(u(i) * x + v(i), 2)) equiv_P: LEMMA P(n, u, v)(x) = Q(sum_sq(n, u), 2 * sum_p(n, u, v), sum_sq(n, v))(x) %------------------------------ % Cauchy-Schwartz inequality %------------------------------ CauchySchwartz1: PROPOSITION expt(sum_p(n, u, v), 2) <= sum_sq(n, u) * sum_sq(n, v) CauchySchwartz: PROPOSITION sum_p(n, u, v) <= sqrt(sum_sq(n, u)) * sqrt(sum_sq(n, v)) END cauchy_schwartz $$$cauchy_schwartz.prf (cauchy_schwartz (sum_TCC1 0 (sum_TCC1-1 nil 3245101691 3245101698 ("" (skosimp) (("" (assert) nil nil)) nil) proved-complete nil 6252 380 t shostak)) (sum_TCC2 0 (sum_TCC2-1 nil 3245101700 3245101704 ("" (skosimp) (("" (assert) nil nil)) nil) proved-complete nil 4053 400 t shostak)) (nonneg_sum 0 (nonneg_sum-1 nil 3245100877 3245100885 ("" (induct-and-simplify "n") nil nil) proved-complete ((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) (rational_pred const-decl "[real -> boolean]" rationals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sum def-decl "real" cauchy_schwartz nil) (nat_induction formula-decl nil naturalnumbers nil)) 7814 460 t shostak)) (sum_square_zero 0 (sum_square_zero-1 nil 3245101712 3245103165 ("" (induct-and-rewrite "n" 1 "sum_sq" "sum" "null_expt") (("" (case-replace "sum(j!1, LAMBDA i: expt(u!1(i), 2)) = 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) proved-complete ((expt def-decl "real" exponentiation nil) (null_expt formula-decl nil exponent_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sum def-decl "real" cauchy_schwartz 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) (rational_pred const-decl "[real -> boolean]" rationals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sum_sq const-decl "nonneg_real" cauchy_schwartz nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (nat_induction formula-decl nil naturalnumbers nil)) 19241 1260 t shostak)) (sum_product_zero 0 (sum_product_zero-1 nil 3245103174 3245103193 ("" (induct-and-simplify "n") nil nil) proved-complete ((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) (rational_pred const-decl "[real -> boolean]" rationals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (sum_p const-decl "real" cauchy_schwartz nil) (nat_induction formula-decl nil naturalnumbers nil) (sum def-decl "real" cauchy_schwartz nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil)) 18207 690 t shostak)) (equiv_P 0 (equiv_P-1 nil 3245100895 3245101099 ("" (skolem + (_ "u!1" "v!1" "x!1")) (("" (induct-and-simplify "n") nil nil)) nil) proved-complete ((expt def-decl "real" exponentiation nil) (sum def-decl "real" cauchy_schwartz nil) (nat_induction formula-decl nil naturalnumbers nil) (sum_p const-decl "real" cauchy_schwartz nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sum_sq const-decl "nonneg_real" cauchy_schwartz nil) (Q const-decl "real" quadratic_polynomials nil) (P const-decl "nonneg_real" cauchy_schwartz nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (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)) 48143 1670 t shostak)) (CauchySchwartz1 0 (CauchySchwartz1-1 nil 3245101116 3245103568 ("" (skolem!) (("" (case "sum_sq(n!1, u!1) = 0") (("1" (auto-rewrite "sum_product_zero" "expt_zero" "sum_square_zero") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (auto-rewrite "expt" "D") (("2" (use "quadra_positive2" ("nza" "sum_sq(n!1, u!1)" "b" "2 * sum_p(n!1, u!1, v!1)" "c" "sum_sq(n!1, v!1)")) (("2" (ground) (("2" (skolem!) (("2" (rewrite "equiv_P" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((sum_sq const-decl "nonneg_real" cauchy_schwartz nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sum_square_zero formula-decl nil cauchy_schwartz nil) (sum_product_zero formula-decl nil cauchy_schwartz nil) (expt_zero formula-decl nil exponent_props nil) (D const-decl "real" quadratic_polynomials nil) (expt def-decl "real" exponentiation nil) (equiv_P formula-decl nil cauchy_schwartz nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (sum_p const-decl "real" cauchy_schwartz nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (quadra_positive2 formula-decl nil quadratic_polynomials nil)) 91181 2620 t shostak)) (CauchySchwartz 0 (CauchySchwartz-1 nil 3245104176 3245105537 ("" (skolem!) (("" (assert) (("" (use "CauchySchwartz1") (("" (auto-rewrite "sqrt_mult") (("" (rewrite "sqrt_expt_le2" :dir rl) nil nil)) nil)) nil)) nil)) nil) proved ((sum_sq const-decl "nonneg_real" cauchy_schwartz nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sum_p const-decl "real" cauchy_schwartz nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqrt_expt_le2 formula-decl nil square_root nil) (sqrt_mult formula-decl nil square_root 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) (rational_pred const-decl "[real -> boolean]" rationals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (CauchySchwartz1 formula-decl nil cauchy_schwartz nil)) 49480 1160 t nil))) $$$extra_props.pvs extra_props : THEORY BEGIN IMPORTING absolute_value x1, x2, y1, y2 : VAR real e, e1, e2, d: VAR posreal n : VAR nat prod_bound : LEMMA abs(x1 - y1) < e1 AND abs(x2 - y2) < e2 IMPLIES abs(x1 * x2 - y1 * y2) < e1 * e2 + abs(y1) * e2 + abs(y2) * e1 prod_epsilon : LEMMA EXISTS e1, e2 : e1 * e2 + abs(y1) * e2 + abs(y2) * e1 < e expt_continuous : LEMMA FORALL x1, e, n : EXISTS d : FORALL y1 : abs(y1 - x1) < d IMPLIES abs(expt(y1, n) - expt(x1, n)) < e END extra_props $$$extra_props.prf (|extra_props| (|prod_bound| "" (SKOSIMP) (("" (LEMMA "sum_abs" ("x" "(x1!1 - y1!1) * x2!1" "y" "(x2!1 - y2!1) * y1!1")) (("" (REWRITE "prod_abs") (("" (REWRITE "prod_abs") (("" (ASSERT) (("" (CASE "abs(x2!1 - y2!1) * abs(y1!1) <= e2!1 * abs(y1!1) AND abs(x1!1 - y1!1) * abs(x2!1) < e1!1 * (abs(y2!1) + e2!1)") (("1" (GROUND) NIL NIL) ("2" (DELETE -1 2) (("2" (SPLIT) (("1" (REWRITE "le_times_le_pos") NIL NIL) ("2" (REWRITE "lt_times_lt_pos1") (("2" (LEMMA "diff_abs" ("x" "x2!1" "y" "y2!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_epsilon| "" (SKOLEM!) (("" (CASE "EXISTS (u, v, w : posreal) : u * v <= e!1/3 and abs(y1!1) * v < e!1/3 and abs(y2!1) * w < e!1/3") (("1" (SKOSIMP) (("1" (INST + "min(u!1, w!1)" "v!1") (("1" (ASSERT) (("1" (CASE "min(u!1, w!1) * v!1 <= u!1 * v!1 and abs(y2!1) * min(u!1, w!1) <= abs(y2!1) * w!1") (("1" (GROUND) NIL NIL) ("2" (AUTO-REWRITE "both_sides_times_pos_le1" "le_times_le_pos") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (NAME-REPLACE "f" "e!1/3") (("2" (CASE "FORALL (x : nonneg_real) : x * (f / (x+1)) < f") (("1" (INST-CP - "abs(y1!1)") (("1" (INST - "abs(y2!1)") (("1" (ASSERT) (("1" (INST + "abs(y1!1) + 1" "f / (abs(y1!1) + 1)" "f / (abs(y2!1) + 1)") (("1" (REWRITE "div_cancel1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REWRITE "times_div1") (("2" (REWRITE "div_mult_pos_lt1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|expt_continuous| "" (AUTO-REWRITE "expt" "null_abs2") (("" (INDUCT "n") (("1" (SKOLEM!) (("1" (INST + "1") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (USE "prod_epsilon" ("e" "e!1" "y1" "x1!1" "y2" "expt(x1!1, j!1)")) (("2" (SKOSIMP) (("2" (INST - "x1!1" "e2!1") (("2" (SKOLEM!) (("2" (INST + "min(d!1, e1!1)") (("2" (SKOSIMP) (("2" (INST - "y1!1") (("2" (ASSERT) (("2" (USE "prod_bound") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$parity.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % A few lemmas about odd or even numbers % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% parity : THEORY BEGIN i : VAR int incr_odd : LEMMA odd?(i + 1) IFF even?(i) incr_even : LEMMA even?(i + 1) IFF odd?(i) opposite_odd : LEMMA odd?(- i) IFF odd?(i) opposite_even : LEMMA even?(- i) IFF even?(i) parity1 : LEMMA odd?(i) OR odd?(i + 1) parity2 : LEMMA even?(i) OR even?(i + 1) odd_not_even : LEMMA odd?(i) IFF not even?(i) even_not_odd : LEMMA even?(i) IFF not odd?(i) even_2i : LEMMA even?(2 * i) odd_2i_plus1 : LEMMA odd?(2 * i + 1) odd_2i_minus1 : LEMMA odd?(2 * i - 1) %------------------------------------- % Rewrite rules for small constants %------------------------------------- parity_zero: LEMMA even?(0) parity_one: LEMMA odd?(1) parity_two: LEMMA even?(2) parity_three: LEMMA odd?(3) parity_minus_one: LEMMA odd?(-1) parity_minus_two: LEMMA even?(-2) parity_minus_three: LEMMA odd?(-3) END parity $$$parity.prf (|parity| (|incr_odd| "" (GRIND :IF-MATCH NIL) NIL NIL) (|incr_even| "" (GRIND :IF-MATCH NIL) (("1" (INST + "j!1 - 1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "j!1 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|opposite_odd| "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1-1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "- j!1 -1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|opposite_even| "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "-j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|parity1| "" (CASE "FORALL (n : nat) : odd?(n) OR odd?(n + 1)") (("1" (SKOSIMP) (("1" (CASE "i!1 >= 0") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (INST - "- (1 + i!1)") (("2" (REWRITE "opposite_odd" 2 :DIR RL) (("2" (REWRITE "opposite_odd" 3 :DIR RL) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (GROUND) NIL NIL) ("2" (SKOLEM!) (("2" (GROUND) (("2" (DELETE 1) (("2" (EXPAND "odd?") (("2" (SKOLEM!) (("2" (INST + "j!2 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|parity2| "" (AUTO-REWRITE "incr_even") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "parity1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|odd_not_even| "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_not_odd| "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_2i| "" (GRIND) NIL NIL) (|odd_2i_plus1| "" (GRIND) NIL NIL) (|odd_2i_minus1| "" (SKOLEM!) (("" (REWRITE "incr_even" :DIR RL) NIL NIL)) NIL) (|parity_zero| "" (GRIND) NIL NIL) (|parity_one| "" (REWRITE "incr_odd") NIL NIL) (|parity_two| "" (REWRITE "incr_even") NIL NIL) (|parity_three| "" (REWRITE "incr_odd") NIL NIL) (|parity_minus_one| "" (REWRITE "opposite_odd") NIL NIL) (|parity_minus_two| "" (REWRITE "opposite_even") NIL NIL) (|parity_minus_three| "" (REWRITE "opposite_odd") NIL NIL)) $$$absolute_value.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properites of absolute value %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% absolute_value : THEORY BEGIN x, y : VAR real z : VAR nzreal null_abs : PROPOSITION abs(x) = 0 IFF x = 0 null_abs2 : PROPOSITION abs(0) = 0 positive_abs : PROPOSITION abs(z) > 0 diff_abs : PROPOSITION abs(x) - abs(y) <= abs(x - y) % sum_abs is triangle in prelude % sum_abs : PROPOSITION abs(x + y) <= abs(x) + abs(y) neg_abs : PROPOSITION abs(- x) = abs(x) % prod_abs is abs_mult in prelude % prod_abs : PROPOSITION abs(x * y) = abs(x) * abs(y) inverse_abs : PROPOSITION abs(1/z) = 1/abs(z) divide_abs : PROPOSITION abs(x/z) = abs(x)/abs(z) abs_abs : PROPOSITION abs(abs(x)) = abs(x) abs_square : PROPOSITION abs(x * x) = x * x %--- abs(x - y) as distance between x and y ---% t, a, b : VAR real diff_abs_commute : PROPOSITION abs(x - y) = abs(y - x) null_distance : PROPOSITION x = y IFF abs(x - y) = 0 triangle2 : PROPOSITION abs(x - t) < a AND abs(x - y) < b IMPLIES abs(t - y) < a + b END absolute_value $$$absolute_value.prf (|absolute_value| (|null_abs| "" (GRIND) NIL NIL) (|null_abs2| "" (GRIND) NIL NIL) (|positive_abs| "" (GRIND) NIL NIL) (|diff_abs| "" (GRIND) NIL NIL) (|sum_abs| "" (GRIND) NIL NIL) (|neg_abs| "" (GRIND) NIL NIL) (|prod_abs| "" (LEMMA "abs_mult") (("" (PROPAX) NIL NIL)) NIL) (|inverse_abs| "" (GRIND :REWRITES ("quotient_neg_lt")) NIL NIL) (|divide_abs| "" (GRIND :REWRITES ("neg_div_lt")) NIL NIL) (|abs_abs| "" (GRIND) NIL NIL) (|abs_square| "" (SKOLEM!) (("" (REWRITE "prod_abs") (("" (GRIND) NIL NIL)) NIL)) NIL) (|diff_abs_commute| "" (GRIND) NIL NIL) (|null_distance| "" (GRIND) NIL NIL) (|triangle2| "" (GRIND) NIL NIL)) $$$exponent_props.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properties of expt % %%%%%%%%%%%%%%%%%%%%%%%%%%%%% exponent_props : THEORY BEGIN IMPORTING absolute_value, parity n, m : VAR nat p : VAR posnat x, y : VAR real z : VAR nzreal nnx, nny : VAR nonneg_real npx, npy : VAR nonpos_real px, py: VAR posreal nx, ny: VAR negreal a, b : VAR posreal lt1x : VAR { a | a < 1} gt1x : VAR { a | 1 < a } evn : VAR { n | even?(n) } evp : VAR { p | even?(p) } odn : VAR { n | odd?(n) } %% Judgements missing in prelude oddnat_positive : JUDGEMENT { n | odd?(n)} SUBTYPE_OF posnat %% Not anymore %% expt_nonzero_is_nonzero: JUDGEMENT expt(z, n) HAS_TYPE nzreal %------------------------------------ % Powers of product, inverse, etc. %------------------------------------ expt_x0 : LEMMA expt(x, 0) = 1 expt_x1 : LEMMA expt(x, 1) = x expt_x2 : LEMMA expt(x, 2) = x * x expt_1n : LEMMA expt(1, n) = 1 expt_mult : LEMMA expt(x * y, n) = expt(x, n) * expt(y, n) expt_div : LEMMA expt(x / z, n) = expt(x, n) / expt(z, n) expt_inv : LEMMA expt(1 / z, n) = 1 / expt(z, n) abs_expt : LEMMA abs(expt(x, n)) = expt(abs(x), n) %------------------------------------------------------- % Same properties as in the prelude % (not restricted to non-zero reals unless necessary) %------------------------------------------------------- expt_plus : LEMMA expt(x, n + m) = expt(x, n) * expt(x, m) expt_minus : LEMMA n <= m IMPLIES expt(z, m - n) = expt(z, m) / expt(z, n) expt_times : LEMMA expt(x, n * m) = expt(expt(x, n), m) expt_divide : LEMMA 1 / expt(z, m * n) = expt(1/expt(z, m), n) expt_zero : LEMMA expt(0, p) = 0 null_expt : LEMMA expt(x, n) = 0 IFF x = 0 AND n > 0 %---------------- % Powers of -1 %---------------- expt_minus_one : LEMMA expt(-1, n) = IF even?(n) THEN 1 ELSE -1 ENDIF odd_expt_m1 : LEMMA expt(-1, odn) = -1 even_expt_m1 : LEMMA expt(-1, evn) = 1 expt_m1_2n : LEMMA expt(-1, 2 * n) = 1 expt_m1_2n1 : LEMMA expt(-1, 2 * n + 1) = -1 %---------------- % Powers of -x %---------------- expt_opp_aux : LEMMA expt(- x, n) = expt(-1, n) * expt(x, n) expt_opposite : LEMMA expt(- x, n) = IF even?(n) THEN expt(x, n) ELSE - expt(x, n) ENDIF odd_expt_opposite : LEMMA expt(- x, odn) = - expt(x, odn) even_expt_opposite : LEMMA expt(-x, evn) = expt(x, evn) expt_opp_2n : LEMMA expt(-x, 2 * n) = expt(x, 2 * n) expt_opp_2n1 : LEMMA expt(-x, 2 * n + 1) = - expt(x, 2 * n + 1) %---------------------------------------------- % Relations between x^n and |x|^n for n even %---------------------------------------------- even_expt_abs: LEMMA expt(x, evn) = expt(abs(x), evn) expt_abs_2n: LEMMA expt(x, 2 * n) = expt(abs(x), 2 * n) %--------------------------------- % Sign of x^n for n odd or even %--------------------------------- odd_expt_negative : LEMMA expt(x, odn) < 0 IFF x < 0 odd_expt_positive : LEMMA expt(x, odn) > 0 IFF x > 0 even_expt_positive : LEMMA expt(x, evn) > 0 IFF x /= 0 OR evn = 0 even_expt_negative : LEMMA NOT expt(x, evn) < 0 %------------------------------------------- % Same properties in judgement form % (judgement expt(px, n) HAS_TYPE posreal % is in the prelude) %------------------------------------------- expt_even_is_nonneg: JUDGEMENT expt(x, evn) HAS_TYPE nonneg_real expt_even_negreal_is_posreal: JUDGEMENT expt(nx, evn) HAS_TYPE posreal expt_odd_negreal_is_negreal: JUDGEMENT expt(nx, odn) HAS_TYPE negreal %-------------------------------------------------------------- % Monotonicity for non-negative arguments, positive exponent %-------------------------------------------------------------- both_sides_expt_nonneg_lt : LEMMA expt(nnx, p) < expt(nny, p) IFF nnx < nny both_sides_expt_nonneg_le : LEMMA expt(nnx, p) <= expt(nny, p) IFF nnx <= nny both_sides_expt_nonneg_gt : LEMMA expt(nnx, p) > expt(nny, p) IFF nnx > nny both_sides_expt_nonneg_ge : LEMMA expt(nnx, p) >= expt(nny, p) IFF nnx >= nny both_sides_expt_nonneg : LEMMA expt(nnx, p) = expt(nny, p) IFF nnx = nny %--------------------------------- % Monotonicity for odd exponent %--------------------------------- both_sides_expt_odd_lt : LEMMA expt(x, odn) < expt(y, odn) IFF x < y both_sides_expt_odd_le : LEMMA expt(x, odn) <= expt(y, odn) IFF x <= y both_sides_expt_odd_gt : LEMMA expt(x, odn) > expt(y, odn) IFF x > y both_sides_expt_odd_ge : LEMMA expt(x, odn) >= expt(y, odn) IFF x >= y both_sides_expt_odd : LEMMA expt(x, odn) = expt(y, odn) IFF x = y %------------------------------------------------- % Monotonicity for positive, even exponent % and non-positive arguments %------------------------------------------------- both_sides_expt_nonpos_even_lt : LEMMA expt(npx, evp) < expt(npy, evp) IFF npy < npx both_sides_expt_nonpos_even_le : LEMMA expt(npx, evp) <= expt(npy, evp) IFF npy <= npx both_sides_expt_nonpos_even_gt : LEMMA expt(npx, evp) > expt(npy, evp) IFF npy > npx both_sides_expt_nonpos_even_ge : LEMMA expt(npx, evp) >= expt(npy, evp) IFF npy >= npx both_sides_expt_nonpos_even : LEMMA expt(npx, evp) = expt(npy, evp) IFF npx = npy %--------------------------------------------------- % Rules for even exponent and arbitrary arguments %--------------------------------------------------- both_sides_expt_even: LEMMA expt(x, evp) = expt(y, evp) IFF x=y OR x=-y both_sides_expt_even_lt: LEMMA expt(x, evp) < expt(y, evp) IFF abs(x) < abs(y) both_sides_expt_even_le: LEMMA expt(x, evp) <= expt(y, evp) IFF abs(x) <= abs(y) both_sides_expt_even_gt: LEMMA expt(x, evp) > expt(y, evp) IFF abs(x) > abs(y) both_sides_expt_even_ge: LEMMA expt(x, evp) >= expt(y, evp) IFF abs(x) >= abs(y) both_sides_expt_even1: LEMMA expt(x, evp) = expt(y, evp) IFF abs(x) = abs(y) both_sides_expt_even2: LEMMA expt(x, evn) = expt(y, evn) IFF evn=0 OR x=y OR x=-y same_square1 : LEMMA x * x = y * y IFF abs(x) = abs(y) same_square2 : LEMMA x * x = y * y IFF x = y OR x = -y %---------------------------------------------- % Bounds of powers x for 0 < x < 1 OR x > 1 %---------------------------------------------- expt_lt1_bound1 : LEMMA expt(lt1x, n) <= 1 expt_lt1_bound2 : LEMMA expt(lt1x, p) < 1 expt_lt1_bound3 : LEMMA expt(lt1x, p) <= lt1x expt_gt1_bound1 : LEMMA 1 <= expt(gt1x, n) expt_gt1_bound2 : LEMMA 1 < expt(gt1x, p) expt_gt1_bound3 : LEMMA gt1x <= expt(gt1x, p) expt_lt_one : LEMMA expt(nnx, p) < 1 IFF nnx < 1 expt_le_one : LEMMA expt(nnx, p) <= 1 IFF nnx <= 1 expt_gt_one : LEMMA expt(nnx, p) > 1 IFF nnx > 1 expt_ge_one : LEMMA expt(nnx, p) >= 1 IFF nnx >= 1 expt_eq_one : LEMMA expt(nnx, p) = 1 IFF nnx = 1 %---------------------------------- % Order relations for 0 < x < 1 %---------------------------------- both_sides_expt_lt1_lt : LEMMA expt(lt1x, n) < expt(lt1x, m) IFF m < n both_sides_expt_lt1_le : LEMMA expt(lt1x, n) <= expt(lt1x, m) IFF m <= n both_sides_expt_lt1_gt : LEMMA expt(lt1x, n) > expt(lt1x, m) IFF m > n both_sides_expt_lt1_ge : LEMMA expt(lt1x, n) >= expt(lt1x, m) IFF m >= n %----------------------------- % Order relations for x > 1 %----------------------------- both_sides_expt_gt1_lt : LEMMA expt(gt1x, n) < expt(gt1x, m) IFF n < m both_sides_expt_gt1_le : LEMMA expt(gt1x, n) <= expt(gt1x, m) IFF n <= m both_sides_expt_gt1_gt : LEMMA expt(gt1x, n) > expt(gt1x, m) IFF n > m both_sides_expt_gt1_ge : LEMMA expt(gt1x, n) >= expt(gt1x, m) IFF n >= m %--------------------------------------- % Equal powers for a /= 1 %--------------------------------------- both_sides_expt_pos : LEMMA FORALL (a | a /= 1) : expt(a, n) = expt(a, m) IFF n = m %---------------------------------- % No upper bound on a^n if 1 < a % Lower bound = 0 if 0 < a < 1 %---------------------------------- large_expt : LEMMA 1 < a IMPLIES (FORALL b : EXISTS n : b < expt(a, n)) small_expt : LEMMA a < 1 IMPLIES (FORALL b : EXISTS n : expt(a, n) < b) END exponent_props $$$exponent_props.prf (|exponent_props| (|oddnat_positive| "" (GRIND) NIL NIL) (|expt_x0| "" (GRIND) NIL NIL) (|expt_x1| "" (GRIND) NIL NIL) (|expt_x2| "" (GRIND) NIL NIL) (|expt_1n| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL) (|expt_mult| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL) (|expt_div| "" (INDUCT-AND-SIMPLIFY "n") (("" (REPLACE*) (("" (REWRITE "div_times") NIL NIL)) NIL)) NIL) (|expt_inv| "" (SKOLEM!) (("" (REWRITE "expt_div") (("" (REWRITE "expt_1n") NIL NIL)) NIL)) NIL) (|abs_expt| "" (INDUCT-AND-SIMPLIFY "n" :REWRITES "prod_abs") NIL NIL) (|expt_plus| "" (SKOLEM 1 ("m!1" _ "x!1")) (("" (INDUCT-AND-SIMPLIFY "n") NIL NIL)) NIL) (|expt_minus_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL) (|expt_minus| "" (SKOSIMP) (("" (ASSERT) (("" (USE "expt_plus" ("n" "m!1 - n!1" "m" "n!1")) (("" (REWRITE "div_cancel3" :DIR RL) NIL NIL)) NIL)) NIL)) NIL) (|expt_times| "" (SKOLEM 1 (_ "n!1" "x!1")) (("" (INDUCT-AND-SIMPLIFY "m" :REWRITES ("expt_plus")) NIL NIL)) NIL) (|expt_divide| "" (SKOLEM!) (("" (REWRITE "expt_inv") (("" (REWRITE "expt_times") NIL NIL)) NIL)) NIL) (|expt_zero| "" (GRIND) NIL NIL) (|null_expt| "" (CASE "FORALL n, x : expt(x, n) = 0 IMPLIES x=0 AND n>0") (("1" (SKOLEM!) (("1" (INST?) (("1" (CASE "expt(x!1, n!1) = 0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOLEM 1 (_ "x!1")) (("2" (INDUCT-AND-REWRITE "n" 1 "expt" "zero_times3") NIL NIL)) NIL)) NIL)) NIL) (|expt_minus_one| "" (INDUCT "n") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (AUTO-REWRITE "expt") (("2" (ASSERT) (("2" (REWRITE "incr_even" +) (("2" (REWRITE "odd_not_even") (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|odd_expt_m1| "" (SKOLEM-TYPEPRED) (("" (AUTO-REWRITE "expt_minus_one" "even_not_odd") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|even_expt_m1| "" (SKOLEM!) (("" (REWRITE "expt_minus_one") NIL NIL)) NIL) (|expt_m1_2n| "" (AUTO-REWRITE "expt_minus_one" "even_2i") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_m1_2n1| "" (AUTO-REWRITE "expt_minus_one" "even_not_odd" "odd_2i_plus1") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_opp_aux| "" (SKOLEM!) (("" (REWRITE "expt_mult" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_opposite| "" (AUTO-REWRITE "expt_minus_one") (("" (SKOLEM!) (("" (REWRITE "expt_opp_aux") (("" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|odd_expt_opposite| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "expt_opp_aux") (("" (REWRITE "odd_expt_m1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_expt_opposite| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "expt_opp_aux") (("" (REWRITE "even_expt_m1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_opp_2n| "" (SKOSIMP) (("" (AUTO-REWRITE "expt_m1_2n") (("" (REWRITE "expt_opp_aux") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|expt_opp_2n1| "" (SKOSIMP) (("" (AUTO-REWRITE "expt_m1_2n1") (("" (REWRITE "expt_opp_aux") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|even_expt_abs| "" (AUTO-REWRITE ("abs") "even_expt_opposite") (("" (REDUCE) NIL NIL)) NIL) (|expt_abs_2n| "" (SKOLEM!) (("" (REWRITE "even_expt_abs") NIL NIL)) NIL) (|odd_expt_abs| "" (SKOLEM!) (("" (POSTPONE) NIL NIL)) NIL) (|odd_expt_negative| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_pos_aux") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "expt") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "expt_pos_aux" ("px" "- x!1" "n" "odn!1")) (("2" (REWRITE "odd_expt_opposite") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|odd_expt_positive| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_pos_aux" ("px" "- x!1")) (("1" (REWRITE "odd_expt_opposite") (("1" (ASSERT) NIL NIL)) NIL) ("2" (AUTO-REWRITE "expt") (("2" (USE "oddnat_positive") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "expt_pos_aux") NIL NIL)) NIL)) NIL) (|even_expt_positive| "" (SKOLEM!) (("" (AUTO-REWRITE "expt" "even_expt_opposite") (("" (GROUND) (("1" (EXPAND "expt") (("1" (ASSERT) NIL NIL)) NIL) ("2" (CASE "x!1 < 0") (("1" (ASSERT) (("1" (USE "expt_pos_aux" ("px" "-x!1" "n" "evn!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "expt_pos_aux") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_expt_negative| "" (SKOLEM!) (("" (USE "even_expt_positive") (("" (AUTO-REWRITE "expt") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|expt_even_is_nonneg| "" (SKOLEM!) (("" (USE "even_expt_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_even_negreal_is_posreal| "" (SKOLEM!) (("" (REWRITE "even_expt_positive") NIL NIL)) NIL) (|expt_odd_negreal_is_negreal| "" (SKOLEM!) (("" (USE "odd_expt_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonneg_lt| "" (AUTO-REWRITE "expt_x1" "expt_zero") (("" (SKOLEM 1 ("x!1" "y!1" _)) (("" (CASE "FORALL n : expt(x!1, n+1) < expt(y!1, n+1) IFF x!1 < y!1") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL) ("3" (SKOSIMP) (("3" (EXPAND "expt" +) (("3" (GROUND) (("1" (CASE-REPLACE "x!1 = 0") (("1" (ASSERT) (("1" (REWRITE "pos_times_lt") NIL NIL)) NIL) ("2" (ASSERT) (("2" (REWRITE "lt_times_lt_pos1") NIL NIL)) NIL)) NIL) ("2" (USE "le_times_le_pos" ("nnx" "y!1" "y" "x!1" "nnz" "expt(y!1, 1 + j!1)" "w" "expt(x!1, 1 + j!1)")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_nonneg_le| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_lt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonneg_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_lt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonneg_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_gt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonneg| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_lt" ("nny" "nny!1")) (("" (USE "both_sides_expt_nonneg_gt" ("nny" "nny!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|both_sides_expt_odd_lt| "" (SKOLEM!) (("" (AUTO-REWRITE "odd_expt_opposite" "oddnat_positive") (("" (USE "odd_expt_negative") (("" (USE "odd_expt_negative" ("x" "y!1")) (("" (CASE "x!1 < 0") (("1" (CASE "y!1 < 0") (("1" (ASSERT) (("1" (USE "both_sides_expt_nonneg_lt" ("nnx" "-y!1" "nny" "-x!1" "p" "odn!1")) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (CASE "y!1 < 0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (REWRITE "both_sides_expt_nonneg_lt") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_odd_le| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_lt" ("x" "y!1" "y" "x!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_odd_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_lt" ("x" "y!1" "y" "x!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_odd_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_gt" ("x" "y!1" "y" "x!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_odd| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_lt" ("y" "y!1")) (("" (USE "both_sides_expt_odd_gt" ("y" "y!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even_lt| "" (SKOLEM!) (("" (USE "even_expt_opposite" ("x" "npx!1")) (("" (USE "even_expt_opposite" ("x" "npy!1")) (("" (USE "both_sides_expt_nonneg_lt" ("nnx" "-npx!1" "nny" "-npy!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even_le| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_lt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_lt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_gt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_gt" ("npy" "npy!1")) (("" (USE "both_sides_expt_nonpos_even_lt" ("npy" "npy!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|both_sides_expt_even| "" (SKOLEM!) (("" (AUTO-REWRITE "even_expt_opposite") (("" (REDUCE) (("" (LEMMA "both_sides_expt_nonneg" ("p" "evp!1")) (("" (CASE* "x!1 >= 0" "y!1 >= 0") (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (INST - "x!1" "-y!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (ASSERT) (("3" (INST - "-x!1" "y!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("4" (ASSERT) (("4" (INST - "- x!1" "- y!1") (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_even_lt| "" (SKOSIMP) (("" (REWRITE "even_expt_abs") (("" (USE "even_expt_abs" ("x" "y!1")) (("" (REPLACE*) (("" (DELETE -) (("" (REWRITE "both_sides_expt_nonneg_lt") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_even_le| "" (SKOSIMP) (("" (USE "both_sides_expt_even_lt" ("x" "y!1" "y" "x!1")) (("" (SMASH) NIL NIL)) NIL)) NIL) (|both_sides_expt_even_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_even_lt" ("x" "y!1" "x" "x!1")) (("" (SMASH) NIL NIL)) NIL)) NIL) (|both_sides_expt_even_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_even_le" ("x" "y!1" "x" "x!1")) (("" (SMASH) NIL NIL)) NIL)) NIL) (|both_sides_expt_even1| "" (SKOLEM!) (("" (REWRITE "both_sides_expt_even") (("" (EXPAND "abs") (("" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|both_sides_expt_even2| "" (SKOLEM!) (("" (AUTO-REWRITE "both_sides_expt_even" "expt_x0") (("" (CASE-REPLACE "evn!1 = 0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|same_square1| "" (SKOLEM!) (("" (USE "both_sides_expt_even1" ("evp" "2")) (("" (AUTO-REWRITE "expt") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|same_square2| "" (SKOLEM!) (("" (REWRITE "same_square1") (("" (EXPAND "abs") (("" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|expt_lt1_bound1| "" (INDUCT-AND-SIMPLIFY "n") (("" (USE "both_sides_times_pos_le2" ("pz" "lt1x!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_lt1_bound2| "" (SKOLEM!) (("" (USE "expt_lt1_bound1" ("n" "p!1 - 1")) (("" (AUTO-REWRITE "expt") (("" (EXPAND "expt" +) (("" (USE "both_sides_times_pos_le1" ("pz" "lt1x!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|expt_lt1_bound3| "" (SKOLEM!) (("" (AUTO-REWRITE "expt" "expt_lt1_bound1") (("" (ASSERT) (("" (LEMMA "both_sides_times_pos_le2" ("pz" "lt1x!1" "x" "expt(lt1x!1, p!1 - 1)" "y" "1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_gt1_bound1| "" (SKOLEM 1 ("a!1" _)) (("" (INDUCT-AND-SIMPLIFY "n") (("" (LEMMA "both_sides_times_pos_le2") (("" (INST -1 "expt(a!1, j!1)" "1" "a!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_gt1_bound2| "" (SKOLEM!) (("" (USE "expt_gt1_bound1" ("n" "p!1 - 1")) (("" (EXPAND "expt" +) (("" (USE "both_sides_times_pos_le1" ("pz" "gt1x!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_gt1_bound3| "" (SKOLEM!) (("" (AUTO-REWRITE "expt" "expt_gt1_bound1") (("" (ASSERT) (("" (LEMMA "both_sides_times_pos_le2" ("pz" "gt1x!1" "x" "1" "y" "expt(gt1x!1, p!1 - 1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_lt_one| "" (SKOLEM!) (("" (AUTO-REWRITE "expt_1n" "expt_zero" "expt_lt1_bound2") (("" (GROUND) (("1" (CASE-REPLACE "nnx!1 = 1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (USE "expt_gt1_bound1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "nnx!1=0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_le_one| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_gt1_bound2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (AUTO-REWRITE "expt_zero" "expt_1n" "expt_lt1_bound1") (("2" (CASE-REPLACE "nnx!1=0") (("1" (ASSERT) NIL NIL) ("2" (CASE-REPLACE "nnx!1=1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|expt_gt_one| "" (SKOLEM!) (("" (USE "expt_le_one") (("" (GROUND) NIL NIL)) NIL)) NIL) (|expt_ge_one| "" (SKOLEM!) (("" (USE "expt_lt_one") (("" (GROUND) NIL NIL)) NIL)) NIL) (|expt_eq_one| "" (SKOLEM!) (("" (USE* "expt_lt_one" "expt_gt_one") (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_lt1_lt| "" (SKOLEM!) (("" (CASE "FORALL (n, m : nat) : m < n IMPLIES expt(lt1x!1, n) < expt(lt1x!1, m)") (("1" (PROP) (("1" (INST -2 "m!1" "n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (USE "expt_plus" ("n" "m!2" "m" "n!2 - m!2")) (("2" (ASSERT) (("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST - "expt(lt1x!1, m!2)" "expt(lt1x!1, n!2 - m!2)" "1") (("2" (AUTO-REWRITE "expt_lt1_bound2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_lt1_le| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_lt1_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_lt1_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_le" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_gt1_lt| "" (SKOLEM!) (("" (CASE "FORALL (n, m : nat) : n < m IMPLIES expt(gt1x!1, n) < expt(gt1x!1, m)") (("1" (PROP) (("1" (INST -2 "m!1" "n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (USE "expt_plus" ("n" "n!2" "m" "m!2 - n!2")) (("2" (ASSERT) (("2" (LEMMA "both_sides_times_pos_lt2") (("2" (INST - "expt(gt1x!1, n!2)" "1" "expt(gt1x!1, m!2 - n!2)") (("2" (AUTO-REWRITE "expt_gt1_bound2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_gt1_le| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_gt1_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_gt1_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_le" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_pos| "" (SKOLEM!) (("" (CASE "a!1 < 1") (("1" (USE "both_sides_expt_lt1_lt" ("m" "m!1")) (("1" (USE "both_sides_expt_lt1_gt" ("m" "m!1")) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (USE "both_sides_expt_gt1_lt" ("m" "m!1")) (("2" (USE "both_sides_expt_gt1_gt" ("m" "m!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|large_expt| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[real]") (("" (LEMMA "real_complete" ("S" "{x:real | EXISTS (n : nat) : x = expt(a!1, n)}")) (("1" (GROUND) (("1" (DELETE 1) (("1" (GRIND :IF-MATCH NIL) (("1" (INST -3 "y!1 / a!1") (("1" (CASE "y!1 > 0") (("1" (GROUND) (("1" (LEMMA "both_sides_div_pos_le2" ("px" "1" "py" "a!1" "pz" "y!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (INST - "s!1 * a!1") (("1" (REWRITE "div_mult_pos_le2") NIL NIL) ("2" (INST + "n!1+1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -3) (("2" (INST - "1") (("1" (ASSERT) NIL NIL) ("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST + "b!1") (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "1") (("2" (INST + "0") (("2" (EXPAND "expt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|small_expt| "" (SKOSIMP*) (("" (LEMMA "large_expt" ("a" "1/a!1")) (("" (REWRITE "div_mult_pos_lt2") (("" (ASSERT) (("" (INST - "1/b!1") (("" (SKOLEM!) (("" (INST + "n!1") (("" (REWRITE "expt_inv") (("" (REWRITE "both_sides_div_pos_lt2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$roots.pvs roots : THEORY BEGIN IMPORTING exponent_props, extra_props x, y, z : VAR nonneg_real px, py : VAR posreal m, p : VAR posnat e : VAR posreal lt1x : VAR { px | px < 1 } gt1x : VAR { x | 1 < x } %--------------------- % Existence of root %--------------------- root_aux1 : LEMMA expt(x, m) < y IMPLIES EXISTS z : x < z AND expt(z, m) < y root_aux2 : LEMMA y < expt(x, m) IMPLIES EXISTS z : z < x AND y < expt(z, m) root_exists : LEMMA FORALL x, m : EXISTS y : expt(y, m) = x %-------------- % Definition %-------------- root(x, m) : { y | expt(y, m) = x } expt_root : LEMMA expt(root(x, m), m) = x root_def : LEMMA root(x, m) = y IFF expt(y, m) = x root_expt : LEMMA root(expt(x, m), m) = x posreal_root_is_positive: JUDGEMENT root(px, m) HAS_TYPE posreal %-------------- % Properties %-------------- root_zero : LEMMA root(0, m) = 0 root_one : LEMMA root(1, m) = 1 root_x1 : LEMMA root(x, 1) = x null_root : LEMMA root(x, m) = 0 IFF x = 0 root_mult : LEMMA root(x * y, m) = root(x, m) * root(y, m) root_inv : LEMMA root(1/px, m) = 1 / root(px, m) root_div : LEMMA root(x/py, m) = root(x, m) / root(py, m) root_times : LEMMA root(x, m * p) = root(root(x, m), p) %--------------------- % Monotonicity, etc. %--------------------- both_sides_root : LEMMA root(x, m) = root(y, m) IFF x = y both_sides_root_lt : LEMMA root(x, m) < root(y, m) IFF x < y both_sides_root_le : LEMMA root(x, m) <= root(y, m) IFF x <= y both_sides_root_gt : LEMMA root(x, m) > root(y, m) IFF x > y both_sides_root_ge : LEMMA root(x, m) >= root(y, m) IFF x >= y root_expt_lt1: LEMMA root(x, m) < y IFF x < expt(y, m) root_expt_lt2: LEMMA x < root(y, m) IFF expt(x, m) < y root_expt_le1: LEMMA root(x, m) <= y IFF x <= expt(y, m) root_expt_le2: LEMMA x <= root(y, m) IFF expt(x, m) <= y root_expt_gt1: LEMMA root(x, m) > y IFF x > expt(y, m) root_expt_gt2: LEMMA x > root(y, m) IFF expt(x, m) > y root_expt_ge1: LEMMA root(x, m) >= y IFF x >= expt(y, m) root_expt_ge2: LEMMA x >= root(y, m) IFF expt(x, m) >= y %---------- % Bounds %---------- root_lt1_bound : LEMMA root(lt1x, m) < 1 root_gt1_bound : LEMMA root(gt1x, m) > 1 root_lt1_bound2 : LEMMA root(x, m) < 1 IFF x < 1 root_gt1_bound2 : LEMMA root(x, m) > 1 IFF x > 1 root_le1_bound : LEMMA root(x, m) <= 1 IFF x <= 1 root_ge1_bound : LEMMA root(x, m) >= 1 IFF x >= 1 %-------------------- % Order properties %-------------------- both_sides_root_lt1_lt : LEMMA root(lt1x, m) < root(lt1x, p) IFF m < p both_sides_root_lt1_le : LEMMA root(lt1x, m) <= root(lt1x, p) IFF m <= p both_sides_root_lt1_gt : LEMMA root(lt1x, m) > root(lt1x, p) IFF m > p both_sides_root_lt1_ge : LEMMA root(lt1x, m) >= root(lt1x, p) IFF m >= p both_sides_root_gt1_lt : LEMMA root(gt1x, m) < root(gt1x, p) IFF p < m both_sides_root_gt1_le : LEMMA root(gt1x, m) <= root(gt1x, p) IFF p <= m both_sides_root_gt1_gt : LEMMA root(gt1x, m) > root(gt1x, p) IFF p > m both_sides_root_gt1_ge : LEMMA root(gt1x, m) >= root(gt1x, p) IFF p >= m equal_roots : LEMMA x /= 0 AND x /= 1 AND root(x, m) = root(x, p) IMPLIES m = p %---------------------------------------------- % Limit of root(x, m) as m tends to infinity %---------------------------------------------- limit_root_gt1x: LEMMA FORALL e: EXISTS m: root(gt1x, m) - 1 < e limit_root_lt1x: LEMMA FORALL e: EXISTS m: 1 - root(lt1x, m) < e limit_root_posreal: LEMMA FORALL e: EXISTS m: abs(root(px, m) - 1) < e limit_root_posreal2: LEMMA FORALL e: EXISTS m: FORALL p: m <= p IMPLIES abs(root(px, p) - 1) < e END roots $$$roots.prf (roots (root_aux1 0 (root_aux1-1 nil 3245104739 nil ("" (skosimp) (("" (assert) (("" (auto-rewrite "abs") (("" (use "expt_continuous" ("e" "y!1 - expt(x!1, m!1)" "x1" "x!1")) (("" (skosimp) (("" (inst + "x!1 + d!1/2") (("" (assert) (("" (inst - "d!1 / 2 + x!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (+ const-decl "[numfield, numfield -> numfield]" 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) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (expt def-decl "real" exponentiation 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (expt_continuous formula-decl nil extra_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) nil nil nil nil)) (root_aux2 0 (root_aux2-1 nil 3245104739 nil ("" (skosimp) (("" (assert) (("" (use "expt_continuous" ("e" "expt(x!1, m!1) - y!1" "x1" "x!1")) (("" (skosimp) (("" (inst + "x!1 - d!1/2") (("1" (assert) (("1" (inst - "x!1 - d!1/2") (("1" (auto-rewrite "abs") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "0") (("2" (name-replace "x!2" "expt(x!1, m!1)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((AND const-decl "[bool, bool -> bool]" booleans nil) (expt_continuous formula-decl nil extra_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil)) nil nil nil nil)) (root_exists 0 (root_exists-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "least_upper_bound?" "upper_bound?" "expt_zero" "expt_x1") (("" (lemma "real_complete" ("S" "{ u:real | u >= 0 AND expt(u, m!1) <= x!1 }")) (("1" (ground) (("1" (skosimp) (("1" (inst-cp - "0") (("1" (assert) (("1" (inst? +) (("1" (use "root_aux1" ("y" "x!1")) (("1" (ground) (("1" (skosimp) (("1" (assert) (("1" (inst - "z!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (use "root_aux2" ("y" "x!1")) (("2" (ground) (("2" (skosimp) (("2" (delete -3) (("2" (inst - "z!1") (("2" (assert) (("2" (skolem-typepred) (("2" (use "both_sides_expt_nonneg_lt" ("nnx" "s!1" "nny" "z!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (case "x!1 <= 1") (("1" (inst + "1") (("1" (skolem-typepred) (("1" (assert) (("1" (use "expt_gt1_bound2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst + "x!1") (("2" (skolem-typepred) (("2" (use "both_sides_expt_nonneg_le" ("nny" "x!1")) (("2" (use "both_sides_expt_gt1_le" ("gt1x" "x!1" "n" "1" "m" "m!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (grind :if-match nil :exclude ("expt")) (("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (expt def-decl "real" exponentiation 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) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets 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_complete formula-decl nil bounded_real_defs nil) (both_sides_expt_gt1_le formula-decl nil exponent_props nil) (expt_x1 formula-decl nil exponent_props nil) (both_sides_expt_nonneg_le formula-decl nil exponent_props nil) (< const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (expt_gt1_bound2 formula-decl nil exponent_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (root_aux1 formula-decl nil roots nil) (expt_zero formula-decl nil exponent_props nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil)) nil nil nil nil)) (root_TCC1 0 (root_TCC1-1 nil 3245104739 nil ("" (inst + "lambda x, m: epsilon! y: expt(y, m) = x") (("" (skolem!) (("" (use "epsilon_ax[nonneg_real]") (("" (ground) (("" (use "root_exists") nil nil)) nil)) nil)) nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (pred type-eq-decl nil defined_types nil) (epsilon const-decl "T" epsilons nil) (epsilon_ax formula-decl nil epsilons nil) (root_exists formula-decl nil roots nil)) nil nil nil nil)) (expt_root 0 (expt_root-1 nil 3245104739 nil ("" (skolem!) (("" (assert) nil nil)) nil) unchecked nil nil nil nil nil)) (root_def 0 (root_def-1 nil 3245104739 nil ("" (skolem!) (("" (ground) (("" (use "both_sides_expt_nonneg" ("nny" "root(x!1, m!1)")) (("" (assert) nil nil)) nil)) nil)) nil) unchecked ((both_sides_expt_nonneg formula-decl nil exponent_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil)) nil nil nil nil)) (root_expt 0 (root_expt-1 nil 3245104739 nil ("" (skolem!) (("" (rewrite "root_def") nil nil)) nil) unchecked ((expt def-decl "real" exponentiation nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (root_def formula-decl nil roots nil)) nil nil nil nil)) (posreal_root_is_positive 0 (posreal_root_is_positive-1 nil 3245104739 nil ("" (skolem!) (("" (name-replace "xxx" "root(px!1, m!1)" :hide? nil) (("" (case "expt(xxx, m!1) = px!1") (("1" (delete -2) (("1" (grind) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) proved-incomplete ((posreal nonempty-type-eq-decl nil real_types nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (expt def-decl "real" exponentiation nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil nil nil nil)) (root_zero 0 (root_zero-1 nil 3245104739 nil ("" (skolem!) (("" (rewrite "root_def") (("" (rewrite "expt_zero") nil nil)) nil)) nil) unchecked ((expt_zero formula-decl nil exponent_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (root_def formula-decl nil roots nil)) nil nil nil nil)) (root_one 0 (root_one-1 nil 3245104739 nil ("" (auto-rewrite "root_def" "expt_1n") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((root_def formula-decl nil roots nil) (expt_1n formula-decl nil exponent_props nil)) nil nil nil nil)) (root_x1 0 (root_x1-1 nil 3245104739 nil ("" (auto-rewrite "root_def" "expt_x1") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((root_def formula-decl nil roots nil) (expt_x1 formula-decl nil exponent_props nil)) nil nil nil nil)) (null_root 0 (null_root-1 nil 3245104739 nil ("" (grind :defs nil :rewrites ("root_zero" "root_def" "expt")) nil nil) unchecked ((root_def formula-decl nil roots nil) (expt def-decl "real" exponentiation nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> 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)) nil nil nil nil)) (root_mult 0 (root_mult-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "root_def" "expt_mult") (("" (name-replace "xx1" "root(x!1, m!1)" :hide? nil) (("" (name-replace "yy1" "root(y!1, m!1)" :hide? nil) (("" (assert) nil nil)) nil)) nil)) nil)) nil) unchecked ((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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (root_def formula-decl nil roots nil) (expt_mult formula-decl nil exponent_props nil)) nil nil nil nil)) (root_inv 0 (root_inv-1 nil 3245104739 nil ("" (skolem!) (("" (name-replace "xxx" "root(px!1, m!1)" :hide? nil) (("" (assert) (("" (auto-rewrite "root_def" "expt_inv") (("" (assert) nil nil)) nil)) nil)) nil)) nil) unchecked ((root_def formula-decl nil roots nil) (expt_inv formula-decl nil exponent_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (expt def-decl "real" exponentiation nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil nil nil nil)) (root_div 0 (root_div-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "root_def" "expt_div") (("" (name-replace "xx1" "root(x!1, m!1)" :hide? nil) (("" (name-replace "yy1" "root(py!1, m!1)" :hide? nil) (("" (assert) nil nil)) nil)) nil)) nil)) nil) unchecked ((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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (root_def formula-decl nil roots nil) (expt_div formula-decl nil exponent_props nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil nil nil nil)) (root_times 0 (root_times-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "root_def") (("" (name-replace "xx1" "root(x!1, m!1)" :hide? nil) (("" (name-replace "xx2" "root(xx1, p!1)" :hide? nil) (("" (assert) (("" (use "expt_times" ("n" "p!1" "m" "m!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (root_def formula-decl nil roots nil) (expt_times formula-decl nil exponent_props nil)) nil nil nil nil)) (both_sides_root 0 (both_sides_root-1 nil 3245104739 nil ("" (auto-rewrite "root_def" "expt_root") (("" (skolem!) (("" (assert) (("" (ground) nil nil)) nil)) nil)) nil) unchecked ((root_def formula-decl nil roots nil) (expt_root formula-decl nil roots nil)) nil nil nil nil)) (both_sides_root_lt 0 (both_sides_root_lt-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "both_sides_expt_nonneg_lt") (("" (name-replace "xx1" "root(x!1, m!1)") (("" (name-replace "yy1" "root(y!1, m!1)") (("" (typepred "xx1" "yy1") (("" (replace -2 + rl) (("" (replace -4 + rl) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_expt_nonneg_lt formula-decl nil exponent_props nil)) nil nil nil nil)) (both_sides_root_le 0 (both_sides_root_le-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "both_sides_expt_nonneg_le") (("" (name-replace "xx1" "root(x!1, m!1)") (("" (name-replace "yy1" "root(y!1, m!1)") (("" (typepred "xx1" "yy1") (("" (replace -2 + rl) (("" (replace -4 + rl) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_expt_nonneg_le formula-decl nil exponent_props nil)) nil nil nil nil)) (both_sides_root_gt 0 (both_sides_root_gt-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "both_sides_expt_nonneg_gt") (("" (name-replace "xx1" "root(x!1, m!1)") (("" (name-replace "yy1" "root(y!1, m!1)") (("" (typepred "xx1" "yy1") (("" (replace -2 + rl) (("" (replace -4 + rl) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_expt_nonneg_gt formula-decl nil exponent_props nil)) nil nil nil nil)) (both_sides_root_ge 0 (both_sides_root_ge-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "both_sides_expt_nonneg_ge") (("" (name-replace "xx1" "root(x!1, m!1)") (("" (name-replace "yy1" "root(y!1, m!1)") (("" (typepred "xx1" "yy1") (("" (replace -2 + rl) (("" (replace -4 + rl) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_expt_nonneg_ge formula-decl nil exponent_props nil)) nil nil nil nil)) (root_expt_lt1 0 (root_expt_lt1-1 nil 3245104742 3245104897 ("" (skolem!) (("" (use "both_sides_root_lt" ("y" "expt(y!1, m!1)")) (("" (rewrite "root_expt") nil nil)) nil)) nil) unchecked ((both_sides_root_lt formula-decl nil roots nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (root_expt formula-decl nil roots nil)) 7914 700 t shostak)) (root_expt_lt2 0 (root_expt_lt2-1 nil 3245104906 3245104969 ("" (skolem!) (("" (use "both_sides_root_lt" ("x" "expt(x!1, m!1)")) (("" (rewrite "root_expt") nil nil)) nil)) nil) proved ((both_sides_root_lt formula-decl nil roots nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (root_expt formula-decl nil roots nil)) 28632 710 t shostak)) (root_expt_le1 0 (root_expt_le1-1 nil 3245104983 3245104988 ("" (skolem!) (("" (use "both_sides_root_le" ("y" "expt(y!1, m!1)")) (("" (rewrite "root_expt") nil nil)) nil)) nil) proved ((root_expt formula-decl nil roots nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (expt def-decl "real" exponentiation 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) (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) (both_sides_root_le formula-decl nil roots nil)) 3191 110 t nil)) (root_expt_le2 0 (root_expt_le2-1 nil 3245105036 nil ("" (skolem!) (("" (use "both_sides_root_le" ("x" "expt(x!1, m!1)")) (("" (rewrite "root_expt") nil)))) nil) unchecked nil nil nil nil nil)) (root_expt_gt1 0 (root_expt_gt1-1 nil 3245104998 nil ("" (skolem!) (("" (use "both_sides_root_gt" ("y" "expt(y!1, m!1)")) (("" (rewrite "root_expt") nil)))) nil) unchecked nil nil nil nil nil)) (root_expt_gt2 0 (root_expt_gt2-1 nil 3245105043 nil ("" (skolem!) (("" (use "both_sides_root_gt" ("x" "expt(x!1, m!1)")) (("" (rewrite "root_expt") nil)))) nil) unchecked nil nil nil nil nil)) (root_expt_ge1 0 (root_expt_ge1-1 nil 3245105016 nil ("" (skolem!) (("" (use "both_sides_root_ge" ("y" "expt(y!1, m!1)")) (("" (rewrite "root_expt") nil)))) nil) unchecked nil nil nil nil nil)) (root_expt_ge2 0 (root_expt_ge2-1 nil 3245105049 nil ("" (skolem!) (("" (use "both_sides_root_ge" ("x" "expt(x!1, m!1)")) (("" (rewrite "root_expt") nil)))) nil) unchecked nil nil nil nil nil)) (root_lt1_bound 0 (root_lt1_bound-1 nil 3245104739 nil ("" (skolem!) (("" (case-replace "1 = root(1, m!1)") (("1" (rewrite "both_sides_root_lt") nil nil) ("2" (rewrite "root_one") nil nil)) nil)) nil) unchecked ((root_one formula-decl nil roots nil) (< const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_root_lt formula-decl nil roots nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (expt def-decl "real" exponentiation nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil nil nil nil)) (root_gt1_bound 0 (root_gt1_bound-1 nil 3245104739 nil ("" (skolem!) (("" (case-replace "1 = root(1, m!1)") (("1" (rewrite "both_sides_root_gt") nil nil) ("2" (rewrite "root_one") nil nil)) nil)) nil) unchecked ((root_one formula-decl nil roots nil) (< const-decl "bool" reals nil) (both_sides_root_gt formula-decl nil roots nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (expt def-decl "real" exponentiation nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil nil nil nil)) (root_lt1_bound2 0 (root_lt1_bound2-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_lt" ("y" "1")) (("" (rewrite "root_one") nil nil)) nil)) nil) unchecked ((root_one formula-decl nil roots nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers 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) (both_sides_root_lt formula-decl nil roots nil)) nil nil nil nil)) (root_gt1_bound2 0 (root_gt1_bound2-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_gt" ("y" "1")) (("" (rewrite "root_one") nil nil)) nil)) nil) unchecked ((root_one formula-decl nil roots nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers 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) (both_sides_root_gt formula-decl nil roots nil)) nil nil nil nil)) (root_le1_bound 0 (root_le1_bound-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_le" ("y" "1")) (("" (rewrite "root_one") nil nil)) nil)) nil) unchecked ((root_one formula-decl nil roots nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers 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) (both_sides_root_le formula-decl nil roots nil)) nil nil nil nil)) (root_ge1_bound 0 (root_ge1_bound-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_ge" ("y" "1")) (("" (rewrite "root_one") nil nil)) nil)) nil) unchecked ((root_one formula-decl nil roots nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers 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) (both_sides_root_ge formula-decl nil roots nil)) nil nil nil nil)) (both_sides_root_lt1_lt 0 (both_sides_root_lt1_lt-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "root_def") (("" (name-replace "xx1" "root(lt1x!1, m!1)" :hide? nil) (("" (name-replace "yy1" "root(lt1x!1, p!1)" :hide? nil) (("" (assert) (("" (use "expt_lt_one" ("nnx" "yy1")) (("" (assert) (("" (ground) (("1" (use "both_sides_expt_lt1_ge" ("lt1x" "yy1" "m" "m!1" "n" "p!1")) (("1" (use "both_sides_expt_nonneg_lt" ("nnx" "xx1" "nny" "yy1" "p" "m!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (use "both_sides_expt_nonneg_ge" ("p" "m!1" "nnx" "xx1" "nny" "yy1")) (("2" (use "both_sides_expt_lt1_lt" ("lt1x" "yy1" "m" "m!1" "n" "p!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (posreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (root_def formula-decl nil roots nil) (both_sides_expt_nonneg_ge formula-decl nil exponent_props nil) (both_sides_expt_lt1_lt formula-decl nil exponent_props nil) (both_sides_expt_lt1_ge formula-decl nil exponent_props nil) (both_sides_expt_nonneg_lt formula-decl nil exponent_props nil) (expt_lt_one formula-decl nil exponent_props nil)) nil nil nil nil)) (both_sides_root_lt1_le 0 (both_sides_root_lt1_le-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_lt1_lt" ("m" "p!1" "p" "m!1")) (("" (ground) nil nil)) nil)) nil) unchecked ((< const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (both_sides_root_lt1_lt formula-decl nil roots nil)) nil nil nil nil)) (both_sides_root_lt1_gt 0 (both_sides_root_lt1_gt-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_lt1_lt" ("m" "p!1" "p" "m!1")) (("" (ground) nil nil)) nil)) nil) unchecked ((< const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (both_sides_root_lt1_lt formula-decl nil roots nil)) nil nil nil nil)) (both_sides_root_lt1_ge 0 (both_sides_root_lt1_ge-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_lt1_gt" ("m" "p!1" "p" "m!1")) (("" (ground) nil nil)) nil)) nil) unchecked ((< const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (both_sides_root_lt1_gt formula-decl nil roots nil)) nil nil nil nil)) (both_sides_root_gt1_lt 0 (both_sides_root_gt1_lt-1 nil 3245104739 nil ("" (skolem!) (("" (name-replace "xx1" "root(gt1x!1, m!1)") (("" (name-replace "yy1" "root(gt1x!1, p!1)") (("" (typepred "xx1" "yy1") (("" (assert) (("" (use "expt_gt_one" ("nnx" "xx1")) (("" (assert) (("" (ground) (("1" (use "both_sides_expt_gt1_ge" ("gt1x" "yy1" "m" "m!1" "n" "p!1")) (("1" (use "both_sides_expt_nonneg_lt" ("nnx" "xx1" "nny" "yy1" "p" "m!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (use "both_sides_expt_nonneg_ge" ("p" "p!1" "nnx" "xx1" "nny" "yy1")) (("2" (use "both_sides_expt_gt1_lt" ("gt1x" "xx1" "m" "m!1" "n" "p!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((both_sides_expt_nonneg_ge formula-decl nil exponent_props nil) (both_sides_expt_gt1_lt formula-decl nil exponent_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_expt_gt1_ge formula-decl nil exponent_props nil) (both_sides_expt_nonneg_lt formula-decl nil exponent_props nil) (expt_gt_one formula-decl nil exponent_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (root const-decl "{y | expt(y, m) = x}" roots nil) (expt def-decl "real" exponentiation nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil nil nil nil)) (both_sides_root_gt1_le 0 (both_sides_root_gt1_le-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_gt1_lt" ("m" "p!1" "p" "m!1")) (("" (ground) nil nil)) nil)) nil) unchecked ((< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (both_sides_root_gt1_lt formula-decl nil roots nil)) nil nil nil nil)) (both_sides_root_gt1_gt 0 (both_sides_root_gt1_gt-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_gt1_lt" ("m" "p!1" "p" "m!1")) (("" (ground) nil nil)) nil)) nil) unchecked ((< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (both_sides_root_gt1_lt formula-decl nil roots nil)) nil nil nil nil)) (both_sides_root_gt1_ge 0 (both_sides_root_gt1_ge-1 nil 3245104739 nil ("" (skolem!) (("" (use "both_sides_root_gt1_gt" ("m" "p!1" "p" "m!1")) (("" (ground) nil nil)) nil)) nil) unchecked ((< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (both_sides_root_gt1_gt formula-decl nil roots nil)) nil nil nil nil)) (equal_roots 0 (equal_roots-1 nil 3245104739 nil ("" (skosimp) (("" (case "x!1 < 1") (("1" (assert) (("1" (use "both_sides_root_lt1_lt" ("p" "p!1")) (("1" (use "both_sides_root_lt1_gt" ("p" "p!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (use "both_sides_root_gt1_lt" ("p" "p!1")) (("2" (use "both_sides_root_gt1_gt" ("p" "p!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((both_sides_root_gt1_gt formula-decl nil roots nil) (both_sides_root_gt1_lt formula-decl nil roots nil) (both_sides_root_lt1_gt formula-decl nil roots nil) (posreal nonempty-type-eq-decl nil real_types nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (both_sides_root_lt1_lt formula-decl nil roots nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil)) nil nil nil nil)) (limit_root_gt1x 0 (limit_root_gt1x-1 nil 3245104739 nil ("" (skosimp) (("" (assert) (("" (use "large_expt" ("a" "1 + e!1")) (("" (assert) (("" (inst - "gt1x!1") (("" (skolem!) (("" (auto-rewrite "expt_x0" "root_expt") (("" (case-replace "n!1 = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (inst + "n!1") (("2" (use "both_sides_root_lt" ("m" "n!1" "y" "expt(1 + e!1, n!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((large_expt formula-decl nil exponent_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (expt def-decl "real" exponentiation nil) (both_sides_root_lt formula-decl nil roots nil) (root_expt formula-decl nil roots nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (expt_x0 formula-decl nil exponent_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil nil nil nil)) (limit_root_lt1x 0 (limit_root_lt1x-1 nil 3245104739 nil ("" (skosimp) (("" (assert) (("" (auto-rewrite "root_x1" "expt_x0" "root_expt" "nnreal_expt") (("" (case "e!1 >= 1") (("1" (inst + "1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (use "small_expt" ("a" "1 - e!1")) (("2" (assert) (("2" (inst - "lt1x!1") (("2" (skolem!) (("2" (case-replace "n!1 = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (inst + "n!1") (("2" (use "both_sides_root_lt" ("m" "n!1" "x" "expt(1 - e!1, n!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((nnreal_expt subtype-tcc nil exponentiation nil) (expt def-decl "real" exponentiation nil) (both_sides_root_lt formula-decl nil roots nil) (root_expt formula-decl nil roots nil) (expt_x0 formula-decl nil exponent_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (small_expt formula-decl nil exponent_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (root_x1 formula-decl nil roots nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil nil nil nil)) (limit_root_posreal 0 (limit_root_posreal-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "abs" "root_one") (("" (case "px!1 < 1") (("1" (assert) (("1" (use "limit_root_lt1x" ("e" "e!1")) (("1" (skolem!) (("1" (use "root_lt1_bound") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "px!1 = 1") (("1" (inst + "1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (use "limit_root_gt1x" ("e" "e!1")) (("2" (skolem!) (("2" (use "root_gt1_bound") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (< const-decl "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) (limit_root_lt1x formula-decl nil roots nil) (root_lt1_bound formula-decl nil roots nil) (posnat 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) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (root_gt1_bound formula-decl nil roots nil) (limit_root_gt1x formula-decl nil roots nil) (root_one formula-decl nil roots nil) (= const-decl "[T, T -> boolean]" equalities nil)) nil nil nil nil)) (limit_root_posreal2 0 (limit_root_posreal2-1 nil 3245104739 nil ("" (skolem!) (("" (auto-rewrite "abs" "root_one") (("" (case "px!1 < 1") (("1" (assert) (("1" (use "limit_root_lt1x" ("e" "e!1")) (("1" (skolem!) (("1" (inst + "m!1") (("1" (skosimp) (("1" (use "root_lt1_bound" ("m" "p!1")) (("1" (use "both_sides_root_lt1_le") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "px!1 = 1") (("1" (inst + "1") (("1" (reduce) nil nil)) nil) ("2" (assert) (("2" (use "limit_root_gt1x" ("e" "e!1")) (("2" (skolem!) (("2" (inst + "m!1") (("2" (skosimp) (("2" (use "root_gt1_bound" ("m" "p!1")) (("2" (use "both_sides_root_gt1_le") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (< const-decl "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) (limit_root_lt1x formula-decl nil roots nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (root_lt1_bound formula-decl nil roots nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (both_sides_root_lt1_le formula-decl nil roots nil) (both_sides_root_gt1_le formula-decl nil roots nil) (root_gt1_bound formula-decl nil roots nil) (limit_root_gt1x formula-decl nil roots nil) (root_one formula-decl nil roots nil) (= const-decl "[T, T -> boolean]" equalities nil)) nil nil nil nil))) $$$square_root.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Defines square root % % Specializes the lemmas on roots % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% square_root : THEORY BEGIN IMPORTING roots x, y : VAR nonneg_real px, py : VAR posreal u, v : VAR real %-------------- % Definition %-------------- sqrt(x) : nonneg_real = root(x, 2) sqrt_def : LEMMA sqrt(x) = y IFF y * y = x square_sqrt : LEMMA sqrt(x) * sqrt(x) = x sqrt_square : LEMMA sqrt(x * x) = x square_sqrt2 : LEMMA expt(sqrt(x), 2) = x sqrt_square2 : LEMMA sqrt(expt(x, 2)) = x sqrt_square3 : LEMMA sqrt(u * u) = abs(u) sqrt_square4 : LEMMA sqrt(expt(u, 2)) = abs(u) posreal_sqrt_is_positive: JUDGEMENT sqrt(px) HAS_TYPE posreal %-------------- % Properties %-------------- sqrt_zero : LEMMA sqrt(0) = 0 sqrt_one : LEMMA sqrt(1) = 1 null_sqrt : LEMMA sqrt(x) = 0 IFF x = 0 sqrt_mult : LEMMA sqrt(x * y) = sqrt(x) * sqrt(y) sqrt_inv : LEMMA sqrt(1/px) = 1 / sqrt(px) sqrt_div : LEMMA sqrt(x/py) = sqrt(x) / sqrt(py) %---------------- % Monotonicity %---------------- both_sides_sqrt : LEMMA sqrt(x) = sqrt(y) IFF x = y both_sides_sqrt_lt : LEMMA sqrt(x) < sqrt(y) IFF x < y both_sides_sqrt_le : LEMMA sqrt(x) <= sqrt(y) IFF x <= y both_sides_sqrt_gt : LEMMA sqrt(x) > sqrt(y) IFF x > y both_sides_sqrt_ge : LEMMA sqrt(x) >= sqrt(y) IFF x >= y sqrt_expt_lt1: LEMMA sqrt(x) < y IFF x < expt(y, 2) sqrt_expt_lt2: LEMMA x < sqrt(y) IFF expt(x, 2) < y sqrt_expt_le1: LEMMA sqrt(x) <= y IFF x <= expt(y, 2) sqrt_expt_le2: LEMMA x <= sqrt(y) IFF expt(x, 2) <= y sqrt_expt_gt1: LEMMA sqrt(x) > y IFF x > expt(y, 2) sqrt_expt_gt2: LEMMA x > sqrt(y) IFF expt(x, 2) > y sqrt_expt_ge1: LEMMA sqrt(x) >= y IFF x >= expt(y, 2) sqrt_expt_ge2: LEMMA x >= sqrt(y) IFF expt(x, 2) >= y %---------- % Bounds %---------- sqrt_lt1_bound : LEMMA sqrt(x) < 1 IFF x < 1 sqrt_gt1_bound : LEMMA sqrt(x) > 1 IFF x > 1 sqrt_le1_bound : LEMMA sqrt(x) <= 1 IFF x <= 1 sqrt_ge1_bound : LEMMA sqrt(x) >= 1 IFF x >= 1 END square_root $$$square_root.prf (square_root (sqrt_def 0 (sqrt_def-1 nil 3245105261 nil ("" (auto-rewrite "expt_x2" "root_def" "sqrt") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((root_def formula-decl nil roots nil) (expt_x2 formula-decl nil exponent_props nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (square_sqrt 0 (square_sqrt-1 nil 3245105261 nil ("" (skolem!) (("" (rewrite "sqrt_def" :dir rl) nil nil)) nil) unchecked ((sqrt const-decl "nonneg_real" square_root 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) (sqrt_def formula-decl nil square_root nil)) nil nil nil nil)) (sqrt_square 0 (sqrt_square-1 nil 3245105261 nil ("" (skolem!) (("" (rewrite "sqrt_def") nil nil)) nil) unchecked ((* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (sqrt_def formula-decl nil square_root nil)) nil nil nil nil)) (square_sqrt2 0 (square_sqrt2-1 nil 3245105261 nil ("" (auto-rewrite "expt_root" "sqrt") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((expt_root formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (sqrt_square2 0 (sqrt_square2-1 nil 3245105261 nil ("" (auto-rewrite "root_expt" "sqrt") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((sqrt const-decl "nonneg_real" square_root nil) (root_expt formula-decl nil roots nil)) nil nil nil nil)) (sqrt_square3_TCC1 0 (sqrt_square3_TCC1-1 nil 3245105261 nil ("" (skolem!) (("" (rewrite "pos_times_ge") (("" (ground) nil nil)) nil)) nil) proved-complete ((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) (pos_times_ge formula-decl nil real_props nil)) nil nil nil nil)) (sqrt_square3 0 (sqrt_square3-1 nil 3245105261 nil ("" (skolem!) (("" (rewrite "sqrt_def") (("" (grind) nil nil)) nil)) nil) unchecked ((abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (sqrt_def formula-decl nil square_root nil)) nil nil nil nil)) (sqrt_square4 0 (sqrt_square4-1 nil 3245105261 nil ("" (grind :exclude ("sqrt") :rewrites ("sqrt_def")) nil nil) unchecked ((abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (expt def-decl "real" exponentiation nil) (sqrt_def formula-decl nil square_root 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)) nil nil nil nil)) (posreal_sqrt_is_positive 0 (posreal_sqrt_is_positive-1 nil 3245105261 nil ("" (subtype-tcc) nil nil) proved-complete ((sqrt const-decl "nonneg_real" square_root 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) (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)) nil nil nil nil)) (sqrt_zero 0 (sqrt_zero-1 nil 3245105261 nil ("" (rewrite "sqrt_def") nil nil) unchecked ((sqrt_def formula-decl nil square_root nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil)) nil nil nil nil)) (sqrt_one 0 (sqrt_one-1 nil 3245105261 nil ("" (rewrite "sqrt_def") nil nil) unchecked ((sqrt_def formula-decl nil square_root nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil)) nil nil nil nil)) (null_sqrt 0 (null_sqrt-1 nil 3245105261 nil ("" (auto-rewrite "sqrt" "null_root") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((null_root formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (sqrt_mult 0 (sqrt_mult-1 nil 3245105261 nil ("" (auto-rewrite "sqrt" "root_mult") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((sqrt const-decl "nonneg_real" square_root nil) (root_mult formula-decl nil roots nil)) nil nil nil nil)) (sqrt_inv 0 (sqrt_inv-1 nil 3245105261 nil ("" (auto-rewrite "sqrt" "root_inv") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((sqrt const-decl "nonneg_real" square_root nil) (root_inv formula-decl nil roots nil)) nil nil nil nil)) (sqrt_div 0 (sqrt_div-1 nil 3245105261 nil ("" (auto-rewrite "sqrt" "root_div") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((sqrt const-decl "nonneg_real" square_root nil) (root_div formula-decl nil roots nil)) nil nil nil nil)) (both_sides_sqrt 0 (both_sides_sqrt-1 nil 3245105261 nil ("" (auto-rewrite "both_sides_root" "sqrt") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((both_sides_root formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (both_sides_sqrt_lt 0 (both_sides_sqrt_lt-1 nil 3245105261 nil ("" (auto-rewrite "both_sides_root_lt" "sqrt") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((both_sides_root_lt formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (both_sides_sqrt_le 0 (both_sides_sqrt_le-1 nil 3245105261 nil ("" (auto-rewrite "both_sides_root_le" "sqrt") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((both_sides_root_le formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (both_sides_sqrt_gt 0 (both_sides_sqrt_gt-1 nil 3245105261 nil ("" (auto-rewrite "both_sides_root_gt" "sqrt") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((both_sides_root_gt formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (both_sides_sqrt_ge 0 (both_sides_sqrt_ge-1 nil 3245105261 nil ("" (auto-rewrite "both_sides_root_ge" "sqrt") (("" (skolem!) (("" (assert) nil nil)) nil)) nil) unchecked ((both_sides_root_ge formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (sqrt_expt_lt1 0 (sqrt_expt_lt1-1 nil 3245105262 3245105301 ("" (skolem!) (("" (use "both_sides_sqrt_lt" ("y" "expt(y!1, 2)")) (("" (rewrite "sqrt_square2") nil nil)) nil)) nil) proved ((both_sides_sqrt_lt formula-decl nil square_root nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (sqrt_square2 formula-decl nil square_root nil)) 39211 650 t shostak)) (sqrt_expt_lt2 0 (sqrt_expt_lt2-1 nil 3245105337 3245105368 ("" (skolem!) (("" (use "both_sides_sqrt_lt" ("x" "expt(x!1, 2)")) (("" (rewrite "sqrt_square2") nil nil)) nil)) nil) proved ((both_sides_sqrt_lt formula-decl nil square_root nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (sqrt_square2 formula-decl nil square_root nil)) 30809 660 t shostak)) (sqrt_expt_le1 0 (sqrt_expt_le1-1 nil 3245105318 nil ("" (skolem!) (("" (use "both_sides_sqrt_le" ("y" "expt(y!1, 2)")) (("" (rewrite "sqrt_square2") nil)))) nil) unchecked nil nil nil nil nil)) (sqrt_expt_le2 0 (sqrt_expt_le2-1 nil 3245105382 nil ("" (skolem!) (("" (use "both_sides_sqrt_le" ("x" "expt(x!1, 2)")) (("" (rewrite "sqrt_square2") nil)))) nil) unchecked nil nil nil nil nil)) (sqrt_expt_gt1 0 (sqrt_expt_gt1-1 nil 3245105327 nil ("" (skolem!) (("" (use "both_sides_sqrt_gt" ("y" "expt(y!1, 2)")) (("" (rewrite "sqrt_square2") nil)))) nil) unchecked nil nil nil nil nil)) (sqrt_expt_gt2 0 (sqrt_expt_gt2-1 nil 3245105392 nil ("" (skolem!) (("" (use "both_sides_sqrt_gt" ("x" "expt(x!1, 2)")) (("" (rewrite "sqrt_square2") nil)))) nil) unchecked nil nil nil nil nil)) (sqrt_expt_ge1 0 (sqrt_expt_ge1-1 nil 3245105333 nil ("" (skolem!) (("" (use "both_sides_sqrt_ge" ("y" "expt(y!1, 2)")) (("" (rewrite "sqrt_square2") nil)))) nil) unchecked nil nil nil nil nil)) (sqrt_expt_ge2 0 (sqrt_expt_ge2-1 nil 3245105398 nil ("" (skolem!) (("" (use "both_sides_sqrt_ge" ("x" "expt(x!1, 2)")) (("" (rewrite "sqrt_square2") nil)))) nil) unchecked nil nil nil nil nil)) (sqrt_lt1_bound 0 (sqrt_lt1_bound-1 nil 3245105261 nil ("" (auto-rewrite "root_lt1_bound2" "sqrt") (("" (skosimp) (("" (assert) nil nil)) nil)) nil) unchecked ((root_lt1_bound2 formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (sqrt_gt1_bound 0 (sqrt_gt1_bound-1 nil 3245105261 nil ("" (auto-rewrite "root_gt1_bound2" "sqrt") (("" (skosimp) (("" (assert) nil nil)) nil)) nil) unchecked ((root_gt1_bound2 formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (sqrt_le1_bound 0 (sqrt_le1_bound-1 nil 3245105261 nil ("" (auto-rewrite "root_le1_bound" "sqrt") (("" (skosimp) (("" (assert) nil nil)) nil)) nil) unchecked ((root_le1_bound formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)) (sqrt_ge1_bound 0 (sqrt_ge1_bound-1 nil 3245105261 nil ("" (auto-rewrite "root_ge1_bound" "sqrt") (("" (skosimp) (("" (assert) nil nil)) nil)) nil) unchecked ((root_ge1_bound formula-decl nil roots nil) (sqrt const-decl "nonneg_real" square_root nil)) nil nil nil nil)))