| products/Sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
|
(polynomials
(IMP_sigma_swap_TCC1 0 (IMP_sigma_swap_TCC1-1 nil 3618849661 ("" (assuming-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (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) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (expt_plus2_TCC1 0 (expt_plus2_TCC1-1 nil 3618056032 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (expt_plus2_TCC2 0 (expt_plus2_TCC2-1 nil 3618056032 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (expt_plus2 0 (expt_plus2-1 nil 3618056034 ("" (induct "i") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (expand "^") (("2" (expand "expt" + 1) (("2" (expand "expt" + 2) (("2" (inst - "j!2" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (expt def-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers 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) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (polynomial_TCC1 0 (polynomial_TCC1-1 nil 3259331390 ("" (grind) nil nil) nil shostak)) (polynomial_n0 0 (polynomial_n0-1 nil 3260328144 ("" (skolem 1 ("a")) (("" (expand "polynomial") (("" (expand "sigma") (("" (expand "sigma") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (sigma def-decl "real" sigma nil)) shostak)) (polynomial_x0 0 (polynomial_x0-1 nil 3260328178 ("" (skolem 1 ("a" "n")) (("" (case "n=0") (("1" (replace -1) (("1" (rewrite "polynomial_n0") (("1" (simplify 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "n>0") (("1" (hide 1) (("1" (expand "polynomial") (("1" (lemma "sigma_first[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE 0 ^ i ENDIF)")) (("1" (lemma "sigma_eq[nat]" ("low" "1" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE 0 ^ i ENDIF)" "G" "LAMBDA (i:nat): 0")) (("1" (split -1) (("1" (lemma "sigma_zero[nat]" ("low" "1" "high" "n")) (("1" (replace -1) (("1" (simplify 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (skosimp*) (("2" (typepred "n!1") (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) 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) (polynomial_n0 formula-decl nil polynomials nil) (sequence type-eq-decl nil sequences nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_first formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (nat_exp application-judgement "nat" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_zero formula-decl nil sigma nil) (expt def-decl "real" exponentiation nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_eq formula-decl nil sigma nil) (polynomial const-decl "[real -> real]" polynomials nil) (> const-decl "bool" reals nil)) shostak)) (polynomial_x1 0 (polynomial_x1-1 nil 3260328670 ("" (expand "polynomial") (("" (skolem 1 ("a" "n")) (("" (lemma "extensionality" ("f" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE 1 ^ i ENDIF)" "g" "a")) (("" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (skolem 1 ("i")) (("2" (case "i=0") (("1" (assert) nil nil) ("2" (assert) (("2" (rewrite "expt_1i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((expt_1i formula-decl nil exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (posint_exp application-judgement "posint" exponentiation nil) (extensionality formula-decl nil functions nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (polynomial const-decl "[real -> real]" polynomials nil)) shostak)) (polynomial_eq_a0_plus_TCC1 0 (polynomial_eq_a0_plus_TCC1-1 nil 3569327711 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (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) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (polynomial_eq_a0_plus 0 (polynomial_eq_a0_plus-1 nil 3569327715 ("" (skeep) (("" (expand "polynomial" + 1) (("" (lemma "sigma_split") (("" (inst?) (("" (inst - "0") (("" (assert) (("" (replaces -1) (("" (case "FORALL (aa,bb,cc,dd:real): aa = cc AND bb=dd IMPLIES aa+bb=cc+dd") (("1" (rewrite -1) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "polynomial") (("2" (rewrite "sigma_scal" :dir rl) (("2" (rewrite "sigma_shift_fun_eq") (("2" (hide 2) (("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (real_times_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_scal formula-decl nil sigma nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_shift_fun_eq formula-decl nil sigma nil) (expt def-decl "real" exponentiation nil) (sigma def-decl "real" sigma nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_split formula-decl nil sigma 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)) nil)) (polynomial_rec 0 (polynomial_rec-1 nil 3570368182 ("" (skeep) (("" (expand "polynomial") (("" (expand "sigma" + 1) (("" (assert) nil nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" sigma nil)) shostak)) (extend_polynomial 0 (extend_polynomial-1 nil 3259336754 ("" (skolem 1 ("a" "_" "n")) (("" (induct "m") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (skolem 1 ("j")) (("2" (flatten) (("2" (replace -2 -1) (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "polynomial") (("2" (expand "sigma" 1 2) (("2" (inst - "1+j") (("2" (replace -1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (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) (sequence type-eq-decl nil sequences nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polynomial const-decl "[real -> real]" polynomials nil) (nat_induction formula-decl nil naturalnumbers nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (sum_polynomial 0 (sum_polynomial-1 nil 3259337167 ("" (skolem 1 ("a" "b" "m" "n")) (("" (flatten) (("" (expand "max") (("" (case "n (("1" (assert) (("1" (lemma "extend_polynomial" ("a" "a" "n" "n" "m" "m-n")) (("1" (replace -3 -1) (("1" (replace -1 1) (("1" (simplify 1) (("1" (expand "polynomial" 1) (("1" (expand "+" 1) (("1" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): sigma(0, m, LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)) + sigma(0, m, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)))" "g" "(LAMBDA (x: real): sigma(0, m, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF) + b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_sum[nat]" ("low" "0" "high" "m" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "G" "LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("2" (simplify -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "extend_polynomial" ("a" "b" "n" "m" "m" "n-m")) (("2" (replace -3 -1) (("2" (replace -1 2) (("2" (simplify 2) (("2" (hide-all-but 2) (("2" (expand "polynomial") (("2" (expand "+") (("2" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): sigma(0, n, LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)) + sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)))" "g" "(LAMBDA (x: real): sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF) + b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_sum[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "G" "LAMBDA (i: nat): b(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("2" (simplify -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 "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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sequence type-eq-decl nil sequences nil) (extend_polynomial formula-decl nil polynomials nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (polynomial const-decl "[real -> real]" polynomials nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (extensionality formula-decl nil functions nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_sum formula-decl nil sigma nil) (+ const-decl "[T -> real]" real_fun_ops nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) shostak)) (sum_polynomial_eq_degree 0 (sum_polynomial_eq_degree-1 nil 3564509725 ("" (skeep) (("" (expand "polynomial") (("" (decompose-equality) (("" (expand "+") (("" (rewrite "sigma_sum") (("" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_eq formula-decl nil sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_sum formula-decl nil sigma nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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 "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma def-decl "real" sigma nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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 "[T -> real]" real_fun_ops nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sum_polynomial_eq_degree_eval 0 (sum_polynomial_eq_degree_eval-1 nil 3569164790 ("" (skeep) (("" (rewrite "sum_polynomial_eq_degree" :dir rl) (("" (expand "+") (("" (propax) nil nil)) nil)) nil)) nil) ((sum_polynomial_eq_degree formula-decl nil 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) (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) (sequence type-eq-decl nil sequences nil) (+ const-decl "[T -> real]" real_fun_ops nil)) shostak)) (neg_polynomial 0 (neg_polynomial-1 nil 3259339078 ("" (skolem 1 ("a" "n")) (("" (expand "polynomial") (("" (expand "-") (("" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): -sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)))" "g" "(LAMBDA (x: real): sigma(0, n, LAMBDA (i: nat): -a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_scal[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "a" "-1")) (("2" (assert) (("2" (replace -1 1 rl) (("2" (assert) (("2" (lemma "extensionality" ("f" "LAMBDA (i_1: nat): -1 * (a(i_1) * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF))" "g" "LAMBDA (i: nat): -a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)")) (("2" (split -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (skolem 1 ("i")) (("2" (assert) (("2" (name-replace "X" "(IF i = 0 THEN 1 ELSE x ^ i ENDIF)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials nil) (numfield nonempty-type-eq-decl nil number_fields 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) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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]" number_fields nil) (extensionality formula-decl nil functions nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_scal formula-decl nil sigma nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops nil)) shostak)) (diff_polynomial 0 (diff_polynomial-1 nil 3259339692 ("" (skolem 1 ("a" "b" "m" "n")) (("" (flatten) (("" (lemma "sum_polynomial" ("a" "a" "n" "n" "b" "-b" "m" "m")) (("" (replace -2 -1) (("" (split -1) (("1" (lemma "neg_polynomial" ("a" "b" "n" "m")) (("1" (replace -1 -2 rl) (("1" (assert) (("1" (case "a+ -b = a-b") (("1" (replace -1 -3) (("1" (replace -3 1 rl) (("1" (assert) (("1" (name-replace "AN" "polynomial(a,n)") (("1" (name-replace "BM" "polynomial(b,m)") (("1" (assert) (("1" (expand "-" 1) (("1" (expand "+" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (expand "+" 1) (("2" (expand "-" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (skosimp*) (("2" (inst - "i!1") (("2" (assert) (("2" (name-replace "IM" "i!1+m") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (neg_polynomial formula-decl nil polynomials nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (polynomial const-decl "[real -> real]" polynomials nil) (- const-decl "[T -> real]" real_fun_ops nil) (+ const-decl "[T -> real]" real_fun_ops nil) (= const-decl "[T, T -> boolean]" equalities nil) (sum_polynomial formula-decl nil 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) (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) (sequence type-eq-decl nil sequences nil) (- const-decl "[T -> real]" real_fun_ops nil)) shostak)) (polynomial_sub 0 (polynomial_sub-1 nil 3569091477 ("" (skeep) (("" (decompose-equality) (("" (expand "-") (("" (expand "polynomial") (("" (rewrite "sigma_minus") nil nil)) nil)) nil)) nil)) 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) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials nil) (- const-decl "[T -> real]" real_fun_ops 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) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_minus formula-decl nil sigma nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (mul_x_to_n_polynomial_TCC1 0 (mul_x_to_n_polynomial_TCC1-1 nil 3259344411 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil)) shostak)) (mul_x_to_n_polynomial_TCC2 0 (mul_x_to_n_polynomial_TCC2-1 nil 3259344425 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (mul_x_to_n_polynomial 0 (mul_x_to_n_polynomial-1 nil 3259342637 ("" (skolem 1 ("a" "n" "pn")) (("" (expand "*") (("" (expand "polynomial") (("" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)) * x_1 ^ pn)" "g" "(LAMBDA (x: real): sigma(0, n + pn, LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_scal[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "a" "x^pn")) (("2" (replace -1 1 rl) (("2" (simplify 1) (("2" (hide -1) (("2" (lemma "sigma_split[nat]") (("2" (inst - "LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)" "n+pn" "0" "pn-1") (("1" (assert) (("1" (assert) (("1" (case "sigma(0, pn - 1, LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)) = 0") (("1" (replace -1 -2) (("1" (replace -2 1) (("1" (hide -1 -2) (("1" (lemma "sigma_shift_T[nat]" ("low" "0" "high" "n" "z" "pn" "F" "LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)")) (("1" (split -1) (("1" (replace -1 1) (("1" (lemma "extensionality" ("f" "LAMBDA (i_1: nat): x ^ pn * (a(i_1) * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF))" "g" "LAMBDA (i: nat): (LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)) (i + pn)")) (("1" (split -1) (("1" (replace -1 1 rl) (("1" (propax) nil nil)) nil) ("2" (hide 2 -1) (("2" (skolem 1 ("i")) (("2" (typepred "i") (("2" (expand ">=" -1) (("2" (expand "<=" -1) (("2" (split -1) (("1" (assert) (("1" (case "x = 0") (("1" (replace -1) (("1" (expand "^" 1) (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "expt_plus" ("n0x" "x" "i" "i" "j" "pn")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1 1 rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "sigma_eq[nat]" ("low" "0" "high" "pn-1" "F" "LAMBDA (i_1: nat): IF i_1 < pn THEN 0 ELSE a(i_1 - pn) ENDIF * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF)" "G" "LAMBDA (i:nat): 0")) (("2" (split -1) (("1" (lemma "sigma_zero[nat]" ("low" "0" "high" "pn-1")) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skolem 1 ("j")) (("2" (assert) (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "[T -> real]" real_fun_ops nil) (numfield nonempty-type-eq-decl nil number_fields 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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 "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sequence type-eq-decl nil sequences nil) (sigma def-decl "real" sigma nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (extensionality formula-decl nil functions nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_scal formula-decl nil sigma nil) (sigma_split formula-decl nil sigma nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_shift_T formula-decl nil sigma nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt def-decl "real" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_plus formula-decl nil exponentiation nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sigma_eq formula-decl nil sigma nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_zero formula-decl nil sigma nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_nat application-judgement "nat" sigma_nat nil) (real_plus_real_is_real application-judgement "real" reals nil) (pn skolem-const-decl "posnat" polynomials nil) (polynomial const-decl "[real -> real]" polynomials nil)) shostak)) (first_polynomial_TCC1 0 (first_polynomial_TCC1-1 nil 3260329723 ("" (grind) nil nil) nil shostak)) (first_polynomial 0 (first_polynomial-1 nil 3260329193 ("" (skolem 1 ("a" "_" "x")) (("" (induct "pn") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skolem 1 ("j")) (("3" (flatten) (("3" (lemma "trichotomy" ("x" "j")) (("3" (split -1) (("1" (assert) (("1" (expand "polynomial") (("1" (expand "sigma" 1) (("1" (replace -2 1) (("1" (simplify 1) (("1" (hide -2) (("1" (case "x=0") (("1" (replace -1) (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "expt_plus" ("n0x" "x" "i" "1" "j" "j")) (("1" (rewrite "expt_x1" -1) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -3 -2) (("2" (grind) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat_induction formula-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (expt_plus formula-decl nil exponentiation nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_x1 formula-decl nil exponentiation nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (nat_exp application-judgement "nat" exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma def-decl "real" sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (trichotomy formula-decl nil real_axioms nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (scal_polynomial 0 (scal_polynomial-1 nil 3259344618 ("" (skolem 1 ("a" "n" "y")) (("" (expand "const_fun") (("" (expand "*") (("" (expand "polynomial") (("" (lemma "extensionality" ("f" "(LAMBDA (x_1: real): y * sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x_1 ^ i ENDIF)))" "g" "(LAMBDA (x: real): sigma(0, n, LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF) * y))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "sigma_scal[nat]" ("low" "0" "high" "n" "F" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF)" "a" "y")) (("2" (replace -1 1 rl) (("2" (simplify 1) (("2" (lemma "extensionality" ("f" "LAMBDA (i_1: nat): y * (a(i_1) * (IF i_1 = 0 THEN 1 ELSE x ^ i_1 ENDIF))" "g" "LAMBDA (i: nat): a(i) * (IF i = 0 THEN 1 ELSE x ^ i ENDIF) * y")) (("2" (split -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.93 Sekunden (vorverarbeitet) ¤ |
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchenDie farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
