| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Tarski/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 613 kB |
|
Quelle poly_systems.prfSprache: Lisp |
|||||||||||||||
|
(poly_systems (system_roots_enum 0 (system_roots_enum-1 nil 3618845198 ("" (skeep) (("" (case "FORALL (i): i<=k IMPLIES n(i)=0") (("1" (case "FORALL (i,x): i<=k IMPLIES polynomial(p(i),n(i))(x)/=0") (("1" (inst + "0" "LAMBDA (j:below(0)): 0") (("1" (split) (("1" (skosimp*) nil nil) ("2" (skosimp*) nil nil) ("3" (skosimp*) (("3" (inst - "j!1" "b!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (inst - "i") (("2" (inst - "i") (("2" (assert) (("2" (replace -3) (("2" (expand "polynomial") (("2" (expand "sigma") (("2" (expand "sigma") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "IGGY" "LAMBDA (b:real): ((EXISTS (j:nat): j<=k AND polynomial(p(j), n(j))(b) = 0))") (("2" (case "is_finite[real](IGGY)") (("1" (copy -1) (("1" (lemma "card_bij_inv[real]") (("1" (name "K" "card(IGGY)") (("1" (inst - "K" "IGGY") (("1" (assert) (("1" (label "fbij" -2) (("1" (skeep) (("1" (skeep -2) (("1" (name "newenum" "sort_array[K,real,<=].sort(f)") (("1" (inst + "K" "newenum") (("1" (case "NOT (FORALL (i, j: below(K)): i < j IMPLIES newenum(i) < newenum(j))") (("1" (hide 3) (("1" (skeep) (("1" (case "NOT newenum(i!1) = newenum(j)") (("1" (assert) (("1" (typepred "newenum") (("1" (expand "sorted?") (("1" (inst - "i!1" "j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "newenum") (("2" (expand "permutation_of?") (("2" (skosimp*) (("2" (expand "bijective?" -1) (("2" (flatten) (("2" (expand "surjective?") (("2" (inst-cp - "j") (("2" (inst - "i!1") (("2" (skosimp*) (("2" (inst-cp - "x!1") (("2" (inst - "x!2") (("2" (replace -2) (("2" (replace -3) (("2" (copy "fbij") (("2" (expand "bijective?" -1) (("2" (flatten) (("2" (expand "injective?" -1) (("2" (inst-cp - "x!1" "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (split) (("1" (skeep) (("1" (typepred "newenum") (("1" (expand "permutation_of?") (("1" (skosimp*) (("1" (expand "bijective?") (("1" (flatten) (("1" (expand "surjective?" -2) (("1" (inst - "i!1") (("1" (skolem - "j!1") (("1" (inst - "j!1") (("1" (assert) (("1" (typepred "f(j!1)") (("1" (replace -3) (("1" (replace -4 :dir rl) (("1" (expand "IGGY" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (typepred "newenum") (("2" (expand "permutation_of?") (("2" (skosimp*) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "surjective?" -11) (("2" (inst -11 "b") (("1" (skolem - "ii") (("1" (inst - "ii") (("1" (inst + "f!1(ii)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "IGGY" 1) (("2" (assert) (("2" (inst + "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (name "IGGYk" "LAMBDA (kp:nat): (LAMBDA (b: real):(EXISTS (j: nat): j <= kp AND polynomial(p(j), n(j))(b) = 0))") (("2" (case "FORALL (kp:nat): kp<=k IMPLIES is_finite[real](IGGYk(kp))") (("1" (inst - "k") (("1" (assert) (("1" (case "IGGYk(k) = IGGY") (("1" (assert) nil nil) ("2" (decompose-equality 1) (("2" (expand "IGGYk" 1) (("2" (expand "IGGY" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "IGGYthis" "LAMBDA (kp:nat): LAMBDA (b:real): polynomial(p(kp),n(kp))(b)=0") (("2" (case "FORALL (kp:nat): kp<=k IMPLIES is_finite[real](IGGYthis(kp))") (("1" (induct "kp") (("1" (assert) (("1" (inst - "0") (("1" (assert) (("1" (case "IGGYthis(0)=IGGYk(0)") (("1" (assert) nil nil) ("2" (decompose-equality 1) (("2" (expand "IGGYthis" 1) (("2" (expand "IGGYk" 1) (("2" (iff) (("2" (ground) (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (case "IGGYk(1+j) = union(IGGYk(j),IGGYthis(1+j))") (("1" (lemma "finite_union[real]") (("1" (inst - "IGGYk(j)" "IGGYthis(1+j)") (("1" (assert) nil nil) ("2" (inst - "1+j") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (expand "union" 1) (("2" (expand "member") (("2" (expand "IGGYk" 1) (("2" (expand "IGGYthis" 1) (("2" (iff) (("2" (ground) (("1" (skosimp*) (("1" (case "j!1 = 1+j") (("1" (assert) nil nil) ("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil) ("3" (inst + "1+j") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (kk:nat,a:[nat->real]): (EXISTS (i:nat):i<=kk AND a(i)/=0) IMPLIES is_finite (("1" (skeep) (("1" (inst - "n(kp)" "p(kp)") (("1" (split -) (("1" (assert) (("1" (expand "IGGYthis" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (inst + "n(kp)") (("2" (assert) (("2" (inst - "kp") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "kk") (("1" (skeep) (("1" (skeep -1) (("1" (case "i = 0") (("1" (replaces -1) (("1" (hide -) (("1" (assert) (("1" (lemma "finite_emptyset[real]") (("1" (invoke (case "%1 = %2") (! -1 1) (! 2 1)) (("1" (assert) nil nil) ("2" (hide (-1 3)) (("2" (decompose-equality 1) (("2" (expand "polynomial") (("2" (expand "sigma") (("2" (expand "sigma") (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (case "EXISTS (z:real): polynomial(a,j+1)(z)=0") (("1" (skeep -1) (("1" (lemma "polynomial_zero_factor") (("1" (inst?) (("1" (replace -2) (("1" (skosimp -1) (("1" (invoke (name "IP" "%1") (! 1 1)) (("1" (replace -1) (("1" (inst -4 "g!1") (("1" (split -4) (("1" (invoke (name "IG" "%1") (! -1 1)) (("1" (replace -1) (("1" (case "IP = union(IG,singleton(z))") (("1" (lemma "finite_union[real]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (iff) (("2" (expand "IP" +) (("2" (expand "IG" +) (("2" (expand "union" +) (("2" (expand "singleton" +) (("2" (expand "member" +) (("2" (ground) (("1" (inst-cp - "x!1") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "x!1") (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "polynomial_eq_coeff") (("2" (inst - "a" "LAMBDA (i:nat): 0" "j+1") (("2" (flatten) (("2" (hide -2) (("2" (split -1) (("1" (skosimp*) (("1" (inst - "i!1") (("1" (assert) nil nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (case "polynomial(LAMBDA (i: nat): 0, 1 + j)(x!1) = 0") (("1" (replaces -1) (("1" (assert) (("1" (inst - "x!1") (("1" (case "polynomial(g!1, j)(x!1) = 0") (("1" (assert) nil nil) ("2" (expand "polynomial" 1) (("2" (rewrite "sigma_restrict_eq_0") (("2" (hide 2) (("2" (skosimp*) (("2" (inst + "i!1") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "polynomial" 1) (("2" (rewrite "sigma_restrict_eq_0") (("2" (skosimp*) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_emptyset[real]") (("2" (invoke (case "%1 = %2") (! -1 1) (! 2 1)) (("1" (assert) nil nil) ("2" (decompose-equality 1) (("2" (iff) (("2" (expand "emptyset" 1) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities 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) (sigma def-decl "real" sigma "reals/") (FALSE const-decl "bool" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (/= const-decl "boolean" notequal nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (card_bij_inv formula-decl nil finite_sets nil) (IGGY skolem-const-decl "[real -> boolean]" poly_systems nil) (b skolem-const-decl "real" poly_systems nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (sort const-decl "{a | permutation_of?(A, a) AND sorted?(a)}" sort_array "structures/") (sorted? const-decl "bool" sort_array "structures/") (permutation_of? const-decl "bool" permutations "structures/") (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (emptyset const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset judgement-tcc nil finite_sets nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (IP skolem-const-decl "[real -> boolean]" poly_systems nil) (real_times_real_is_real application-judgement "real" reals nil) (IG skolem-const-decl "[real -> boolean]" poly_systems nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (nonempty_union2 application-judgement "(nonempty?)" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (subrange type-eq-decl nil integers nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (j skolem-const-decl "nat" poly_systems nil) (i!1 skolem-const-decl "nat" poly_systems nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (polynomial_eq_coeff formula-decl nil polynomials "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (polynomial_zero_factor formula-decl nil polynomials "reals/") (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (IGGYthis skolem-const-decl "[nat -> [real -> boolean]]" poly_systems nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" sets nil) (finite_union judgement-tcc nil finite_sets nil) (j skolem-const-decl "nat" poly_systems nil) (union const-decl "set" sets 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) (IGGYk skolem-const-decl "[nat -> [real -> boolean]]" poly_systems nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) nil)) (strict_poly_system_solvable_TCC1 0 (strict_poly_system_solvable_TCC1-1 nil 3618843949 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (strict_poly_system_solvable_TCC2 0 (strict_poly_system_solvable_TCC2-1 nil 3621242993 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (strict_poly_system_solvable 0 (strict_poly_system_solvable-4 nil 3618918694 ("" (lemma "system_roots_enum") (("" (skeep) (("" (inst - "k" "n" "p") (("" (assert) (("" (replace -2) (("" (skeep) (("" (label "fmz" -1) (("" (label "skz" -3) (("" (name "Q" "prod_polynomials (p, n, (LAMBDA (i: nat): 1), k)") (("" (replace -1) (("" (name "Qdeg" "sigma(0, k, n)") (("" (replace -1) (("" (case "NOT FORALL (x): polynomial(Q,Qdeg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i))") (("1" (hide 2) (("1" (skeep) (("1" (typepred "Q") (("1" (case "NOT n * (LAMBDA (i: nat): 1) = n") (("1" (decompose-equality 1) (("1" (expand "*" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (replace -1) (("2" (inst - "x") (("2" (replace -5) (("2" (replace -2) (("2" (ground) (("1" (lemma "product_eq_0[nat]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "^" -1) (("1" (expand "expt" -1) (("1" (expand "expt" -1) (("1" (inst "skz" "x" "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "^") (("2" (expand "expt") (("2" (expand "expt") (("2" (assert) (("2" (lemma "product_eq_zero[nat]") (("2" (inst?) (("2" (assert) (("2" (inst -8 "i!1") (("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split 1) (("1" (flatten) (("1" (skeep -1) (("1" (case "K = 0") (("1" (skeep 1) (("1" (inst - "i") (("1" (assert) (("1" (lemma "poly_sign_near_infinity") (("1" (inst - "p(i)" "n(i)") (("1" (assert) (("1" (inst-cp -11 "i") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (skeep -1) (("1" (expand "sign_ext" -1 2) (("1" (expand "sign_ext" -1) (("1" (assert) (("1" (inst-cp - "x") (("1" (assert) (("1" (inst - "M") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(i)" "0" "n(i)" "x" "M") (("1" (assert) (("1" (skosimp*) (("1" (inst -14 "cc!1" "i") (("1" (assert) (("1" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "x > enum(K-1)") (("1" (lemma "poly_sign_near_infinity") (("1" (case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): FORALL (x: real,j:nat): j<=jp AND x >= M IMPLIES sign_ext(polynomial(p(j),n(j))(x)) = sign_ext(p(j)(n(j))))") (("1" (inst - "k") (("1" (assert) (("1" (skeep -1) (("1" (hide -2) (("1" (skeep) (("1" (case "NOT FORALL (x: real): x >= M IMPLIES polynomial(p(i), n(i))(x)<=0") (("1" (skeep) (("1" (inst - "x!1" "i") (("1" (assert) (("1" (expand "sign_ext" -2) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "MM" "max(M,x+1)") (("2" (inst - "MM") (("2" (inst -5 "i") (("2" (assert) (("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(i)" "0" "n(i)" "x" "MM") (("2" (assert) (("2" (skosimp*) (("2" (inst -16 "cc!1" "i") (("2" (assert) (("2" (skosimp*) (("2" (inst -14 "i!2" "K-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "jp") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -9 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (skeep -) (("2" (inst -3 "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M,M!1)") (("1" (skeep) (("1" (case "j = 1+j!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (inst -2 "x!1" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -13 "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "x < enum(0)") (("1" (hide 3) (("1" (skeep) (("1" (lemma "poly_sign_near_negative_infinity") (("1" (case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): FORALL (x: real,j:nat): j<=jp AND x<=-M IMPLIES sign_ext(polynomial(p(j),n(j))(x)) = sign_ext((IF odd?(n(j)) THEN -1 ELSE 1 E (("1" (inst - "k") (("1" (assert) (("1" (skeep -1) (("1" (hide -2) (("1" (name "MM" "min(-M,x-1)") (("1" (case "NOT EXISTS (cc:real): MM<=cc AND cc<=x AND polynomial(p(i),n(i))(cc)=0") (("1" (inst -4 "i") (("1" (assert) (("1" (inst-cp - "MM" "i") (("1" (assert) (("1" (case "NOT sign_ext((IF odd?(n(i)) THEN -1 ELSE 1 ENDIF) * p(i)(n(i))) = -1") (("1" (inst -13 "i") (("1" (assert) (("1" (flatten) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "sign_ext" -4) (("2" (lift-if -4) (("2" (ground) (("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(i)" "0" "n(i)" "MM" "x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst -14 "cc" "i") (("2" (assert) (("2" (skosimp*) (("2" (inst -12 "0" "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "jp") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "even_or_odd") (("1" (inst - "n(0)") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -10 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (skeep -) (("2" (inst -3 "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M,M!1)") (("1" (skeep) (("1" (case "j = 1+j!1") (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "even_or_odd") (("1" (inst?) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -2 "x!1" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -12 "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT EXISTS (i:nat): i+1<K AND enum(i)<x AND x<enum(i+1)") (("1" (name "Nset" "{nm:nat | nm+1<K aNd enum(nm)<x}") (("1" (lemma "lub_nat") (("1" (inst - "Nset" "K+1") (("1" (assert) (("1" (split -1) (("1" (skolem -1 "i") (("1" (inst + "i") (("1" (typepred "i") (("1" (expand "Nset" -1) (("1" (flatten) (("1" (assert) (("1" (case "enum(1+i)=x") (("1" (inst -11 "1+i") (("1" (skeep -11) (("1" (assert) (("1" (inst -6 "j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?" -3) (("2" (inst - "1+i") (("1" (assert) nil nil) ("2" (expand "extend" 1) (("2" (expand "Nset" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_bound?" 1) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (expand "extend" -1) (("2" (split -) (("1" (flatten) (("1" (expand "Nset" -4) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?" 1) (("2" (inst + "0") (("2" (assert) (("2" (case "NOT K>1") (("1" (case "NOT x = enum(0)") (("1" (assert) nil nil) ("2" (inst -9 "0") (("2" (skeep -9) (("2" (inst - "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "x = enum(0)") (("1" (inst -10 "0") (("1" (skeep -10) (("1" (inst - "j") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (expand "empty?") (("2" (inst - "0") (("2" (expand "member") (("2" (expand "Nset" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skeep -1) (("2" (lemma "poly_Rolle") (("2" (inst - "Q" "Qdeg" "enum(i)" "enum(i+1)") (("2" (assert) (("2" (assert) (("2" (case "NOT Qdeg > 0") (("1" (assert) (("1" (hide -1) (("1" (typepred "Q") (("1" (case "FORALL (j): j<=k IMPLIES n(j)=0") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst -8 "i!1") (("1" (assert) (("1" (replace -1) (("1" (expand "polynomial" -8) (("1" (expand "sigma" -8) (("1" (expand "sigma" -8) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (pz:nat): pz<=k AND sigma[nat](0, pz, LAMBDA (j): n(j)) = 0 IMPLIES FORALL (j): j <= pz IMP (("1" (inst - "k") (("1" (assert) (("1" (replace 1) (("1" (case "NOT n = n*(LAMBDA (i:nat): 1)") (("1" (decompose-equality 1) (("1" (expand "*") (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (replaces -1 :dir rl) (("2" (assert) (("2" (lemma "sigma_tolambda") (("2" (inst - "n" "k" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "pz") (("1" (assert) (("1" (flatten) (("1" (skeep) (("1" (expand "sigma" -1) (("1" (expand "sigma" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp 1) (("2" (label "izp" 1) (("2" (assert) (("2" (split -1) (("1" (skeep) (("1" (case "NOT j = j!1+1") (("1" (inst - "j") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "sigma" -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sigma" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split -2) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (assert) (("1" (skolem 6 "iii") (("1" (flatten) (("1" (inst - "iii") (("1" (assert) (("1" (case "x < c!1") (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(iii)" "0" "n(iii)" "x" "c!1") (("1" (assert) (("1" (skosimp*) (("1" (copy "skz") (("1" (inst - "cc!1" "iii") (("1" (assert) (("1" (skosimp*) (("1" (copy "fmz") (("1" (inst-cp - "i!3" "i") (("1" (inst - "1+i" "i!3") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(iii)" "0" "n(iii)" "c!1" "x") (("2" (assert) (("2" (skosimp*) (("2" (copy "skz") (("2" (inst - "cc!1" "iii") (("2" (assert) (("2" (skosimp -1) (("2" (copy "fmz") (("2" (inst-cp - "i!3" "i") (("2" (inst - "1+i" "i!3") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst-cp -6 "enum(i)") (("2" (inst -6 "enum(1+i)") (("2" (assert) (("2" (flatten) (("2" (hide -6) (("2" (hide -7) (("2" (split -) (("1" (split -) (("1" (assert) nil nil) ("2" (inst + "i") nil nil)) nil) ("2" (inst + "1+i") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (lemma "poly_sign_near_infinity") (("1" (case "FORALL (j): j<=k IMPLIES EXISTS (M:posnat): FORALL (i): i<=j IMPLIES FORALL (x:real):x >= M IMPL (("1" (inst - "k") (("1" (assert) (("1" (skeep) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "i") (("1" (assert) (("1" (inst - "M") (("1" (assert) (("1" (inst - "i") (("1" (assert) (("1" (expand "sign_ext" -1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "j") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -1) (("1" (skeep) (("1" (inst + "M") (("1" (skeep) (("1" (skeep) (("1" (inst - "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (skeep -1) (("2" (inst - "p(1+j!1)" "n(1+j!1)") (("2" (split -) (("1" (skeep -1) (("1" (inst + "max(M!1,M)") (("1" (skeep) (("1" (case "i = 1+j!1") (("1" (skeep) (("1" (inst - "x") (("1" (assert) nil nil)) nil)) nil) ("2" (inst -2 "i") (("2" (assert) (("2" (skeep) (("2" (inst -2 "x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "1+j!1") (("2" (inst - "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (j): j<=k IMPLIES EXISTS (M:posnat): FORALL (i): i<=j IMPLIES FORALL (x:real):x <= -M IMP (("1" (inst - "k") (("1" (assert) (("1" (skeep) (("1" (inst + "-M") (("1" (skeep) (("1" (inst - "i") (("1" (assert) (("1" (inst - "-M") (("1" (assert) (("1" (inst - "i") (("1" (lemma "even_or_odd") (("1" (inst - "n(i)") (("1" (lift-if) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "j") (("1" (assert) (("1" (lemma "poly_sign_near_negative_infinity") (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -1) (("1" (skeep) (("1" (inst + "M") (("1" (skeep) (("1" (skeep) (("1" (inst - "x") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "0") (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "poly_sign_near_negative_infinity") (("2" (inst - "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M!1,M!2)") (("1" (skeep) (("1" (case " i = 1+j!1") (("1" (skeep) (("1" (inst - "x") (("1" (assert) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -2 "i") (("2" (assert) (("2" (skeep) (("2" (inst -2 "x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -3 "1+j!1") (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (inst + "x") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (even? const-decl "bool" integers nil) (poly_sign_near_infinity formula-decl nil more_polynomial_props "reals/") (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (poly_intermediate_value_dec formula-decl nil polynomials "reals/") (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (odd? const-decl "bool" integers nil) (minus_real_is_real application-judgement "real" reals nil) (poly_intermediate_value_inc formula-decl nil polynomials "reals/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (real_minus_real_is_real application-judgement "real" reals nil) (even_or_odd formula-decl nil naturalnumbers nil) (minus_int_is_int application-judgement "int" integers nil) (poly_sign_near_negative_infinity formula-decl nil more_polynomial_props "reals/") (n skolem-const-decl "[nat -> nat]" poly_systems nil) (sigma_tolambda formula-decl nil sigma_nat "reals/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (poly_Rolle formula-decl nil polynomials "reals/") (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (Nset skolem-const-decl "[nat -> boolean]" poly_systems nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (i skolem-const-decl "(Nset)" poly_systems nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (lub_nat formula-decl nil integer_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posrat_max application-judgement "{s: posrat | s >= q AND s >= r}" real_defs nil) (posint_max application-judgement "{k: posint | i <= k AND j <= k}" real_defs nil) (real_plus_real_is_real application-judgement "real" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (expt def-decl "real" exponentiation nil) (product_eq_0 formula-decl nil product "reals/") (j!1 skolem-const-decl "nat" poly_systems nil) (k skolem-const-decl "nat" poly_systems nil) (product_eq_zero formula-decl nil product "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (prod_polynomials def-decl "{a | (FORALL (x): polynomial(a, sigma(0, k, KF * GP))(x) = product(0, k, LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j))) AND ((FORALL (i): i <= k AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0) IMPLIES a(sigma(0, k, KF * GP)) /= 0) AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" poly_families 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) (system_roots_enum formula-decl nil poly_systems nil)) nil) (strict_poly_system_solvable-3 nil 3618918595 ("" (lemma "system_roots_enum") (("" (skeep) (("" (inst - "k" "n" "p") (("" (assert) (("" (replace -2) (("" (skeep) (("" (label "skz" -3) (("" (name "Q" "prod_upto(p, n, k)") (("" (replace -1) (("" (case "NOT FORALL (x): polynomial(Q`poly,Q`deg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i) (("1" (hide 2) (("1" (skeep) (("1" (typepred "Q") (("1" (inst - "x") (("1" (replace -2) (("1" (ground) (("1" (lemma "product_eq_0[nat]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst -8 "x" "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (lemma "product_eq_zero[nat]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst -6 "i!1") (("1" (skosimp*) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split 1) (("1" (flatten) (("1" (skeep -1) (("1" (case "K = 0") (("1" (skeep 1) (("1" (inst - "i") (("1" (assert) (("1" (lemma "poly_sign_near_infinity") (("1" (inst - "p(i)" "n(i)") (("1" (assert) (("1" (inst -10 "i") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (skeep -1) (("1" (expand "sign_ext" -1 2) (("1" (expand "sign_ext" -1) (("1" (assert) (("1" (inst-cp - "x") (("1" (assert) (("1" (inst - "M") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(i)" "0" "n(i)" "x" "M") (("1" (assert) (("1" (skosimp*) (("1" (inst -13 "cc!1" "i") (("1" (assert) (("1" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "x > enum(K-1)") (("1" (lemma "poly_sign_near_infinity") (("1" (case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): FORALL (x: real,j:nat): j<=jp AND x >= M IMPLIES sign_ext(polynomial(p(j),n(j))(x)) = sign_ext(p(j)(n(j))))") (("1" (inst - "k") (("1" (assert) (("1" (skeep -1) (("1" (hide -2) (("1" (skeep) (("1" (case "NOT FORALL (x: real): x >= M IMPLIES polynomial(p(i), n(i))(x)<=0") (("1" (skeep) (("1" (inst - "x!1" "i") (("1" (assert) (("1" (expand "sign_ext" -2) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "MM" "max(M,x+1)") (("2" (inst - "MM") (("2" (inst -5 "i") (("2" (assert) (("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(i)" "0" "n(i)" "x" "MM") (("2" (assert) (("2" (skosimp*) (("2" (inst -15 "cc!1" "i") (("2" (assert) (("2" (skosimp*) (("2" (inst -13 "i!2" "K-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "jp") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -8 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (skeep -) (("2" (inst -3 "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M,M!1)") (("1" (skeep) (("1" (case "j = 1+j!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (inst -2 "x!1" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -12 "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "x < enum(0)") (("1" (hide 3) (("1" (skeep) (("1" (lemma "poly_sign_near_negative_infinity") (("1" (case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): FORALL (x: real,j:nat): j<=jp AND x<=-M IMPLIES sign_ext(polynomial(p(j),n(j))(x)) = sign_ext((IF odd?(n(j)) THEN -1 ELSE 1 E (("1" (inst - "k") (("1" (assert) (("1" (skeep -1) (("1" (hide -2) (("1" (name "MM" "min(-M,x-1)") (("1" (case "NOT EXISTS (cc:real): MM<=cc AND cc<=x AND polynomial(p(i),n(i))(cc)=0") (("1" (inst -4 "i") (("1" (assert) (("1" (inst-cp - "MM" "i") (("1" (assert) (("1" (case "NOT sign_ext((IF odd?(n(i)) THEN -1 ELSE 1 ENDIF) * p(i)(n(i))) = -1") (("1" (inst -12 "i") (("1" (assert) (("1" (flatten) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "sign_ext" -4) (("2" (lift-if -4) (("2" (ground) (("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(i)" "0" "n(i)" "MM" "x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst -13 "cc" "i") (("2" (assert) (("2" (skosimp*) (("2" (inst -11 "0" "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "jp") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "even_or_odd") (("1" (inst - "n(0)") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -9 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (skeep -) (("2" (inst -3 "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M,M!1)") (("1" (skeep) (("1" (case "j = 1+j!1") (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "even_or_odd") (("1" (inst?) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -2 "x!1" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -11 "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT EXISTS (i:nat): i+1<K AND enum(i)<x AND x<enum(i+1)") (("1" (name "Nset" "{nm:nat | nm+1<K aNd enum(nm)<x}") (("1" (lemma "lub_nat") (("1" (inst - "Nset" "K+1") (("1" (assert) (("1" (split -1) (("1" (skolem -1 "i") (("1" (inst + "i") (("1" (typepred "i") (("1" (expand "Nset" -1) (("1" (flatten) (("1" (assert) (("1" (case "enum(1+i)=x") (("1" (inst -10 "1+i") (("1" (skeep -10) (("1" (assert) (("1" (inst -6 "j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?" -3) (("2" (inst - "1+i") (("1" (assert) nil nil) ("2" (expand "extend" 1) (("2" (expand "Nset" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_bound?" 1) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (expand "extend" -1) (("2" (split -) (("1" (flatten) (("1" (expand "Nset" -4) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?" 1) (("2" (inst + "0") (("2" (assert) (("2" (case "NOT K>1") (("1" (case "NOT x = enum(0)") (("1" (assert) nil nil) ("2" (inst -8 "0") (("2" (skeep -8) (("2" (inst - "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "x = enum(0)") (("1" (inst -9 "0") (("1" (skeep -9) (("1" (inst - "j") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (expand "empty?") (("2" (inst - "0") (("2" (expand "member") (("2" (expand "Nset" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skeep -1) (("2" (lemma "poly_Rolle") (("2" (inst - "Q`poly" "Q`deg" "enum(i)" "enum(i+1)") (("2" (assert) (("2" (assert) (("2" (case "NOT Q`deg > 0") (("1" (assert) (("1" (hide -1) (("1" (typepred "Q") (("1" (case "FORALL (j): j<=k IMPLIES n(j)=0") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst -8 "i!1") (("1" (assert) (("1" (replace -1) (("1" (expand "polynomial" -8) (("1" (expand "sigma" -8) (("1" (expand "sigma" -8) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (pz:nat): pz<=k AND sigma[nat](0, pz, LAMBDA (j): n(j)) = 0 IMPLIES FORALL (j): j <= pz IMP (("1" (inst - "k") (("1" (assert) nil nil)) nil) ("2" (induct "pz") (("1" (assert) (("1" (flatten) (("1" (skeep) (("1" (expand "sigma" -1) (("1" (expand "sigma" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp 1) (("2" (label "izp" 1) (("2" (assert) (("2" (split -1) (("1" (skeep) (("1" (case "NOT j = j!1+1") (("1" (inst - "j") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "sigma" -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sigma" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split -2) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (assert) (("1" (skolem 6 "iii") (("1" (flatten) (("1" (inst - "iii") (("1" (assert) (("1" (case "x < c!1") (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(iii)" "0" "n(iii)" "x" "c!1") (("1" (assert) (("1" (skosimp*) (("1" (copy "skz") (("1" (inst - "cc!1" "iii") (("1" (assert) (("1" (skosimp*) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil) ("3" (postpone) nil nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil) (strict_poly_system_solvable-2 nil 3618918536 ("" (lemma "system_roots_enum") (("" (skeep) (("" (inst - "k" "n" "p") (("" (assert) (("" (replace -2) (("" (skeep) (("" (label "skz" -4) (("" (name "Q" "prod_upto(p, n, k)") (("" (replace -1) (("" (case "NOT FORALL (x): polynomial(Q`poly,Q`deg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i) (("1" (hide 2) (("1" (skeep) (("1" (typepred "Q") (("1" (inst - "x") (("1" (replace -2) (("1" (ground) (("1" (lemma "product_eq_0[nat]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst -8 "x" "n!1") (("1" (assert) nil))))))))) ("2" (skosimp*) (("2" (assert) nil))))) ("2" (lemma "product_eq_zero[nat]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst -6 "i!1") (("1" (skosimp*) (("1" (inst + "j!1") (("1" (assert) nil))))))))))))) ("2" (skosimp*) (("2" (assert) nil))))))))))))))))) ("2" (split 1) (("1" (flatten) (("1" (skeep -1) (("1" (case "K = 0") (("1" (skeep 1) (("1" (inst - "i") (("1" (assert) (("1" (lemma "poly_sign_near_infinity") (("1" (inst - "p(i)" "n(i)") (("1" (assert) (("1" (inst -10 "i") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (skeep -1) (("1" (expand "sign_ext" -1 2) (("1" (expand "sign_ext" -1) (("1" (assert) (("1" (inst-cp - "x") (("1" (assert) (("1" (inst - "M") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(i)" "0" "n(i)" "x" "M") (("1" (assert) (("1" (skosimp*) (("1" (inst -13 "cc!1" "i") (("1" (assert) (("1" (skosimp*) nil))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (case "x > enum(K-1)") (("1" (lemma "poly_sign_near_infinity") (("1" (case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): FORALL (x: real,j:nat): j<=jp AND x >= M IMPLIES sign_ext(polynomial(p(j),n(j))(x)) = sign_ext(p(j)(n(j))))") (("1" (inst - "k") (("1" (assert) (("1" (skeep -1) (("1" (hide -2) (("1" (skeep) (("1" (case "NOT FORALL (x: real): x >= M IMPLIES polynomial(p(i), n(i))(x)<=0") (("1" (skeep) (("1" (inst - "x!1" "i") (("1" (assert) (("1" (expand "sign_ext" -2) (("1" (lift-if) (("1" (ground) nil))))))))))) ("2" (name "MM" "max(M,x+1)") (("2" (inst - "MM") (("2" (inst -5 "i") (("2" (assert) (("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(i)" "0" "n(i)" "x" "MM") (("2" (assert) (("2" (skosimp*) (("2" (inst -15 "cc!1" "i") (("2" (assert) (("2" (skosimp*) (("2" (inst -13 "i!2" "K-1") (("2" (assert) nil))))))))))))))))))))))))))))))))))))) ("2" (induct "jp") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "x!1") (("1" (assert) nil))))))))) ("2" (inst -8 "0") (("2" (assert) nil))))))))))) ("2" (skosimp*) (("2" (assert) (("2" (skeep -) (("2" (inst -3 "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M,M!1)") (("1" (skeep) (("1" (case "j = 1+j!1") (("1" (inst - "x!1") (("1" (assert) nil))) ("2" (inst -2 "x!1" "j") (("2" (assert) nil))))))))))) ("2" (inst -12 "1+j!1") (("2" (assert) nil))))))))))))))))))))) ("2" (case "x < enum(0)") (("1" (hide 3) (("1" (skeep) (("1" (lemma "poly_sign_near_negative_infinity") (("1" (case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): FORALL (x: real,j:nat): j<=jp AND x<=-M IMPLIES sign_ext(polynomial(p(j),n(j))(x)) = sign_ext((IF odd?(n(j)) THEN -1 ELSE 1 E (("1" (inst - "k") (("1" (assert) (("1" (skeep -1) (("1" (hide -2) (("1" (name "MM" "min(-M,x-1)") (("1" (case "NOT EXISTS (cc:real): MM<=cc AND cc<=x AND polynomial(p(i),n(i))(cc)=0") (("1" (inst -4 "i") (("1" (assert) (("1" (inst-cp - "MM" "i") (("1" (assert) (("1" (case "NOT sign_ext((IF odd?(n(i)) THEN -1 ELSE 1 ENDIF) * p(i)(n(i))) = -1") (("1" (inst -12 "i") (("1" (assert) (("1" (flatten) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) nil))))))))))))))))) ("2" (replace -1) (("2" (expand "sign_ext" -4) (("2" (lift-if -4) (("2" (ground) (("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(i)" "0" "n(i)" "MM" "x") (("2" (assert) nil))))))))))))))))))))))) ("2" (skeep -1) (("2" (inst -13 "cc" "i") (("2" (assert) (("2" (skosimp*) (("2" (inst -11 "0" "i!1") (("2" (assert) nil))))))))))))))))))))))) ("2" (induct "jp") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "even_or_odd") (("1" (inst - "n(0)") (("1" (lift-if) (("1" (ground) nil))))))))))))))))) ("2" (inst -9 "0") (("2" (assert) nil))))))))))) ("2" (skosimp*) (("2" (assert) (("2" (skeep -) (("2" (inst -3 "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M,M!1)") (("1" (skeep) (("1" (case "j = 1+j!1") (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "even_or_odd") (("1" (inst?) (("1" (lift-if) (("1" (ground) nil))))))))))) ("2" (inst -2 "x!1" "j") (("2" (assert) nil))))))))))) ("2" (inst -11 "1+j!1") (("2" (assert) nil))))))))))))))))))))))))) ("2" (case "NOT EXISTS (i:nat): i+1<K AND enum(i)<x AND x<enum(i+1)") (("1" (name "Nset" "{nm:nat | nm+1<K aNd enum(nm)<x}") (("1" (lemma "lub_nat") (("1" (inst - "Nset" "K+1") (("1" (assert) (("1" (split -1) (("1" (skolem -1 "i") (("1" (inst + "i") (("1" (typepred "i") (("1" (expand "Nset" -1) (("1" (flatten) (("1" (assert) (("1" (case "enum(1+i)=x") (("1" (inst -10 "1+i") (("1" (skeep -10) (("1" (assert) (("1" (inst -6 "j") (("1" (assert) nil))))))))) ("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?" -3) (("2" (inst - "1+i") (("1" (assert) nil) ("2" (expand "extend" 1) (("2" (expand "Nset" 1) (("2" (assert) nil))))))))))))))))))))))))))) ("2" (expand "upper_bound?" 1) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (expand "extend" -1) (("2" (split -) (("1" (flatten) (("1" (expand "Nset" -4) (("1" (flatten) (("1" (assert) nil))))))) ("2" (propax) nil))))))))))))))) ("2" (expand "nonempty?" 1) (("2" (inst + "0") (("2" (assert) (("2" (case "NOT K>1") (("1" (case "NOT x = enum(0)") (("1" (assert) nil) ("2" (inst -8 "0") (("2" (skeep -8) (("2" (inst - "j") (("2" (assert) nil))))))))) ("2" (assert) (("2" (case "x = enum(0)") (("1" (inst -9 "0") (("1" (skeep -9) (("1" (inst - "j") (("1" (assert) nil))))))) ("2" (assert) (("2" (assert) (("2" (expand "empty?") (("2" (inst - "0") (("2" (expand "member") (("2" (expand "Nset" 2) (("2" (propax) nil))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (assert) nil))))) ("2" (skeep -1) (("2" (lemma "poly_Rolle") (("2" (inst - "Q`poly" "Q`deg" "enum(i)" "enum(i+1)") (("2" (assert) (("2" (assert) (("2" (case "NOT Q`deg > 0") (("1" (assert) (("1" (hide -1) (("1" (typepred "Q") (("1" (case "FORALL (j): j<=k IMPLIES n(j)=0") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst -8 "i!1") (("1" (assert) (("1" (replace -1) (("1" (expand "polynomial" -8) (("1" (expand "sigma" -8) (("1" (expand "sigma" -8) (("1" (propax) nil))))))))))))))))) ("2" (case "FORALL (pz:nat): pz<=k AND sigma[nat](0, pz, LAMBDA (j): n(j)) = 0 IMPLIES FORALL (j): j <= pz IMP (("1" (inst - "k") (("1" (assert) nil))) ("2" (induct "pz") (("1" (assert) (("1" (flatten) (("1" (skeep) (("1" (expand "sigma" -1) (("1" (expand "sigma" -1) (("1" (assert) nil))))))))))) ("2" (skosimp 1) (("2" (label "izp" 1) (("2" (assert) (("2" (split -1) (("1" (skeep) (("1" (case "NOT j = j!1+1") (("1" (inst - "j") (("1" (assert) nil))) ("2" (replace -1) (("2" (assert) (("2" (expand "sigma" -4) (("2" (assert) nil))))))))))) ("2" (expand "sigma" -2) (("2" (assert) nil))))))))))))))))))))))) ("2" (assert) (("2" (split -2) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (assert) (("1" (skolem 6 "iii") (("1" (flatten) (("1" (inst - "iii") (("1" (assert) (("1" (case "x < c!1") (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(iii)" "0" "n(iii)" "x" "c!1") (("1" (assert) (("1" (skosimp*) (("1" (postpone) nil))))))))) ("2" (postpone) nil))))))))))))))))) ("2" (postpone) nil))))))))))))))))) ("3" (postpone) nil))) ("3" (postpone) nil))) ("3" (postpone) nil))))))))) ("2" (postpone) nil)))))))))))))))))))))) nil) nil nil) (strict_poly_system_solvable-1 nil 3618842027 ("" (lemma "system_roots_enum") (("" (skeep) (("" (inst - "k" "n" "p") (("" (assert) (("" (replace -2) (("" (skeep) (("" (name "Q" "prod_upto(p, n, k)") (("" (replace -1) (("" (case "NOT FORALL (x): polynomial(Q`poly,Q`deg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i) (("1" (hide 2) (("1" (skeep) (("1" (typepred "Q") (("1" (inst - "x") (("1" (replace -2) (("1" (ground) (("1" (lemma "product_eq_0[nat]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst -8 "x" "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (lemma "product_eq_zero[nat]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst -6 "i!1") (("1" (skosimp*) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split 1) (("1" (flatten) (("1" (skeep -1) (("1" (case "K = 0") (("1" (skeep 1) (("1" (inst - "i") (("1" (assert) (("1" (lemma "poly_sign_near_infinity") (("1" (inst - "p(i)" "n(i)") (("1" (assert) (("1" (inst -10 "i") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (skeep -1) (("1" (expand "sign_ext" -1 2) (("1" (expand "sign_ext" -1) (("1" (assert) (("1" (inst-cp - "x") (("1" (assert) (("1" (inst - "M") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(i)" "0" "n(i)" "x" "M") (("1" (assert) (("1" (skosimp*) (("1" (inst -13 "cc!1" "i") (("1" (assert) (("1" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "x > enum(K-1)") (("1" (lemma "poly_sign_near_infinity") (("1" (case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): FORALL (x: real,j:nat): j<=jp AND x >= M IMPLIES sign_ext(polynomial(p(j),n(j))(x)) = sign_ext(p(j)(n(j))))") (("1" (inst - "k") (("1" (assert) (("1" (skeep -1) (("1" (hide -2) (("1" (skeep) (("1" (case "NOT FORALL (x: real): x >= M IMPLIES polynomial(p(i), n(i))(x)<=0") (("1" (skeep) (("1" (inst - "x!1" "i") (("1" (assert) (("1" (expand "sign_ext" -2) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "MM" "max(M,x+1)") (("2" (inst - "MM") (("2" (inst -5 "i") (("2" (assert) (("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(i)" "0" "n(i)" "x" "MM") (("2" (assert) (("2" (skosimp*) (("2" (inst -15 "cc!1" "i") (("2" (assert) (("2" (skosimp*) (("2" (inst -13 "i!2" "K-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "jp") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -8 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (skeep -) (("2" (inst -3 "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M,M!1)") (("1" (skeep) (("1" (case "j = 1+j!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil) ("2" (inst -2 "x!1" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -12 "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "x < enum(0)") (("1" (hide 3) (("1" (skeep) (("1" (lemma "poly_sign_near_negative_infinity") (("1" (case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): FORALL (x: real,j:nat): j<=jp AND x<=-M IMPLIES sign_ext(polynomial(p(j),n(j))(x)) = sign_ext((IF odd?(n(j)) THEN -1 ELSE 1 E (("1" (inst - "k") (("1" (assert) (("1" (skeep -1) (("1" (hide -2) (("1" (name "MM" "min(-M,x-1)") (("1" (case "NOT EXISTS (cc:real): MM<=cc AND cc<=x AND polynomial(p(i),n(i))(cc)=0") (("1" (inst -4 "i") (("1" (assert) (("1" (inst-cp - "MM" "i") (("1" (assert) (("1" (case "NOT sign_ext((IF odd?(n(i)) THEN -1 ELSE 1 ENDIF) * p(i)(n(i))) = -1") (("1" (inst -12 "i") (("1" (assert) (("1" (flatten) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "sign_ext" -4) (("2" (lift-if -4) (("2" (ground) (("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(i)" "0" "n(i)" "MM" "x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (inst -13 "cc" "i") (("2" (assert) (("2" (skosimp*) (("2" (inst -11 "0" "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (induct "jp") (("1" (assert) (("1" (inst - "p(0)" "n(0)") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst + "M") (("1" (skeep) (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "even_or_odd") (("1" (inst - "n(0)") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -9 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (skeep -) (("2" (inst -3 "p(1+j!1)" "n(1+j!1)") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst + "max(M,M!1)") (("1" (skeep) (("1" (case "j = 1+j!1") (("1" (inst - "x!1") (("1" (assert) (("1" (lemma "even_or_odd") (("1" (inst?) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -2 "x!1" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -11 "1+j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT EXISTS (i:nat): i+1<K AND enum(i)<x AND x<enum(i+1)") (("1" (name "Nset" "{nm:nat | nm+1<K aNd enum(nm)<x}") (("1" (lemma "lub_nat") (("1" (inst - "Nset" "K+1") (("1" (assert) (("1" (split -1) (("1" (skolem -1 "i") (("1" (inst + "i") (("1" (typepred "i") (("1" (expand "Nset" -1) (("1" (flatten) (("1" (assert) (("1" (case "enum(1+i)=x") (("1" (inst -10 "1+i") (("1" (skeep -10) (("1" (assert) (("1" (inst -6 "j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?" -3) (("2" (inst - "1+i") (("1" (assert) nil nil) ("2" (expand "extend" 1) (("2" (expand "Nset" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_bound?" 1) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (expand "extend" -1) (("2" (split -) (("1" (flatten) (("1" (expand "Nset" -4) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?" 1) (("2" (inst + "0") (("2" (assert) (("2" (case "NOT K>1") (("1" (case "NOT x = enum(0)") (("1" (assert) nil nil) ("2" (inst -8 "0") (("2" (skeep -8) (("2" (inst - "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "x = enum(0)") (("1" (inst -9 "0") (("1" (skeep -9) (("1" (inst - "j") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (expand "empty?") (("2" (inst - "0") (("2" (expand "member") (("2" (expand "Nset" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (skeep -1) (("2" (lemma "poly_Rolle") (("2" (inst - "Q`poly" "Q`deg" "enum(i)" "enum(i+1)") (("2" (assert) (("2" (assert) (("2" (case "NOT Q`deg > 0") (("1" (assert) (("1" (hide -1) (("1" (typepred "Q") (("1" (case "FORALL (j): j<=k IMPLIES n(j)=0") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst -8 "i!1") (("1" (assert) (("1" (replace -1) (("1" (expand "polynomial" -8) (("1" (expand "sigma" -8) (("1" (expand "sigma" -8) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (pz:nat): pz<=k AND sigma[nat](0, pz, LAMBDA (j): n(j)) = 0 IMPLIES FORALL (j): j <= pz IMP (("1" (inst - "k") (("1" (assert) nil nil)) nil) ("2" (induct "pz") (("1" (assert) (("1" (flatten) (("1" (skeep) (("1" (expand "sigma" -1) (("1" (expand "sigma" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp 1) (("2" (label "izp" 1) (("2" (assert) (("2" (split -1) (("1" (skeep) (("1" (case "NOT j = j!1+1") (("1" (inst - "j") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "sigma" -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sigma" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split -2) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (assert) (("1" (skolem 6 "iii") (("1" (flatten) (("1" (inst - "iii") (("1" (assert) (("1" (case "x < c!1") (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(iii)" "0" "n(iii)" "x" "c!1") (("1" (assert) (("1" (skosimp*) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil) ("3" (postpone) nil nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (A63_tensor_power_mat_row_TCC1 0 (A63_tensor_power_mat_row_TCC1-1 nil 3621258003 ("" (skeep) (("" (rewrite "length_row") (("" (assert) nil nil)) nil)) nil) ((length_row formula-decl nil matrix_props "matrices/") (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices "matrices/") (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices "matrices/") (> const-decl "bool" reals nil) (rows const-decl "nat" matrices "matrices/") (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices "matrices/") (PosFullMatrix type-eq-decl nil matrices "matrices/") (A63 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" tarski_query_matrix nil) (subrange type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (A63_tensor_power_mat_row_TCC2 0 (A63_tensor_power_mat_row_TCC2-1 nil 3621258003 ("" (skeep) (("" (assert) (("" (typepred "vect2matrix(row(A63)(RelF6(0)))") (("" (assert) (("" (replace -6) (("" (rewrite "length_row" 1) (("" (assert) (("" (replace -7) (("" (expand "^" + 1) (("" (expand "expt") (("" (expand "expt") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (length_row formula-decl nil matrix_props "matrices/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Vector type-eq-decl nil matrices "matrices/") (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (Matrix type-eq-decl nil matrices "matrices/") (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices "matrices/") (rows const-decl "nat" matrices "matrices/") (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices "matrices/") (PosFullMatrix type-eq-decl nil matrices "matrices/") (vect2matrix const-decl "{PFM | rows(PFM) = 1 AND columns(PFM) = length(v)}" matrices "matrices/") (row const-decl "Vector" matrices "matrices/") (A63 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" tarski_query_matrix nil) (subrange type-eq-decl nil integers nil)) nil)) (A63_tensor_power_mat_row_TCC3 0 (A63_tensor_power_mat_row_TCC3-1 nil 3621258003 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers 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) (gt_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (A63_tensor_power_mat_row_TCC4 0 (A63_tensor_power_mat_row_TCC4-1 nil 3621258003 ("" (skeep) (("" (assert) nil nil)) 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) (lt_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (A63_tensor_power_mat_row_TCC5 0 (A63_tensor_power_mat_row_TCC5-1 nil 3621258003 ("" (skeep) (("" (rewrite "length_row") (("" (assert) nil nil)) nil)) nil) ((length_row formula-decl nil matrix_props "matrices/") (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices "matrices/") (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices "matrices/") (> const-decl "bool" reals nil) (rows const-decl "nat" matrices "matrices/") (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices "matrices/") (PosFullMatrix type-eq-decl nil matrices "matrices/") (A63 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" tarski_query_matrix nil) (subrange type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (A63_tensor_power_mat_row_TCC6 0 (A63_tensor_power_mat_row_TCC6-1 nil 3621258003 ("" (skeep) (("" (rewrite "tensor_rows") (("" (assert) (("" (expand "tensor_prod") (("" (lemma "columns_form_matrix") (("" (inst?) (("" (assert) (("" (replaces -1) (("" (expand "vect2matrix") (("" (lemma "columns_form_matrix") (("" (inst?) (("" (assert) (("" (replaces -1) (("" (rewrite "length_row") (("" (assert) (("" (typepred "v(m - 1)(LAMBDA (d): RelF6(1 + d))") (("" (replaces -6 +) (("" (hide -) (("" (expand "^") (("" (expand "expt" + 2) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (tensor_rows formula-decl nil tensor_product "matrices/") (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices "matrices/") (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices "matrices/") (> const-decl "bool" reals nil) (rows const-decl "nat" matrices "matrices/") (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices "matrices/") (PosFullMatrix type-eq-decl nil matrices "matrices/") (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (subrange type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation 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) (Vector type-eq-decl nil matrices "matrices/") (vect2matrix const-decl "{PFM | rows(PFM) = 1 AND columns(PFM) = length(v)}" matrices "matrices/") (row const-decl "Vector" matrices "matrices/") (A63 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" tarski_query_matrix nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (tensor_prod const-decl "PosFullMatrix" tensor_product "matrices/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (tensor_fun const-decl "[[nat, nat] -> real]" tensor_product "matrices/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (length_row formula-decl nil matrix_props "matrices/") (NOT const-decl "[bool -> bool]" booleans nil) (expt def-decl "real" exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (access const-decl "real" matrices "matrices/") (form_matrix_square application-judgement "FullMatrix" matrices "matrices/") (posint_exp application-judgement "posint" exponentiation nil) (columns_form_matrix formula-decl nil matrices "matrices/")) nil)) (A63_tensor_power_mat_row_def_TCC1 0 (A63_tensor_power_mat_row_def_TCC1-1 nil 3621269302 ("" (skeep) (("" (rewrite "length_row") (("" (lift-if) (("" (ground) (("" (lemma "tensor_power_rows_alt") (("" (inst?) (("" (assert) (("" (lemma "base_n_to_nat_lt") (("" (inst?) (("" (split -) (("1" (assert) nil nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length_row formula-decl nil matrix_props "matrices/") (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices "matrices/") (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices "matrices/") (> const-decl "bool" reals nil) (rows const-decl "nat" matrices "matrices/") (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices "matrices/") (PosFullMatrix type-eq-decl nil matrices "matrices/") (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (tensor_power_alt def-decl "PosFullMatrix" tensor_product "matrices/") (A63 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" tarski_query_matrix nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (base_n_to_nat_lt formula-decl nil base_repr "reals/") (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_exp application-judgement "posint" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (subrange type-eq-decl nil integers nil) (nat_exp application-judgement "nat" exponentiation nil) (tensor_power_rows_alt formula-decl nil tensor_product "matrices/")) nil)) (A63_tensor_power_mat_row_def 0 (A63_tensor_power_mat_row_def-1 nil 3621269303 ("" (induct "k") (("1" (assert) nil nil) ("2" (skeep) (("2" (rewrite "full_matrix_eq") (("2" (split) (("1" (expand "vect2matrix") (("1" (rewrite "rows_form_matrix") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "vect2matrix") (("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) (("2" (replaces -1) (("2" (rewrite "length_row") (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lemma "tensor_power_rows_alt") (("1" (inst?) (("1" (assert) (("1" (rewrite "expt_x1") (("1" (lemma "base_n_to_nat_lt") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "tensor_power_columns_alt") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (expand "A63_tensor_power_mat_row") (("3" (expand "vect2matrix") (("3" (rewrite "entry_form_matrix") (("3" (rewrite "entry_form_matrix") (("3" (assert) (("3" (lift-if) (("3" (lift-if) (("3" (lift-if) (("3" (ground) (("1" (rewrite "access_row") (("1" (rewrite "access_row") (("1" (expand "tensor_power_alt") (("1" (expand "base_n_to_nat") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (rewrite "expt_x0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_row") (("2" (rewrite "length_row") (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (expand "base_n_to_nat") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (rewrite "expt_x0") (("1" (lemma "tensor_power_rows_alt") (("1" (inst?) (("1" (assert) (("1" (rewrite "expt_x1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "tensor_power_columns_alt") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "length_row") (("3" (lift-if) (("3" (ground) (("3" (rewrite "length_row") (("3" (lemma "tensor_power_columns_alt") (("3" (inst?) (("3" (assert) (("3" (rewrite "expt_x1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem 1 "k") (("3" (flatten) (("3" (skeep) (("3" (assert) (("3" (rewrite "full_matrix_eq" +) (("3" (split) (("1" (expand "vect2matrix" +) (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (rewrite "length_row") (("1" (lift-if) (("1" (ground) (("1" (lemma "base_n_to_nat_lt") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (lemma "tensor_power_rows_alt") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "tensor_power_columns_alt") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (case "NOT i = 0") (("1" (typepred "i") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (case "NOT j < 3^(2+k)") (("1" (assert) nil nil) ("2" (expand "vect2matrix" +) (("2" (rewrite "entry_form_matrix") (("2" (lift-if) (("2" (ground) (("1" (rewrite "access_row") (("1" (expand "A63_tensor_power_mat_row" +) (("1" (expand "tensor_prod") (("1" (rewrite "entry_form_matrix") (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "tensor_fun") (("1" (inst? -5) (("1" (replace -5 +) (("1" (expand "vect2matrix" + 1) (("1" (rewrite "entry_form_matrix") (("1" (lift-if) (("1" (ground) (("1" (rewrite "access_row") (("1" (expand "vect2matrix" + 1) (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (split -) (("1" (assert) nil nil) ("2" (replaces -1) (("2" (expand "vect2matrix" + 1) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) (("2" (replaces -1) (("2" (assert) (("2" (expand "vect2matrix" + 1) (("2" (rewrite "entry_form_matrix") (("1" (lift-if) (("1" (ground) (("1" (rewrite "access_row") (("1" (expand "vect2matrix" + 1) (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (split -) (("1" (assert) nil nil) ("2" (replaces -1) (("2" (assert) (("2" (rewrite "length_row") (("2" (case "NOT columns(A63)=3") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (expand "tensor_power_alt" + 2) (("2" (expand "tensor_prod" +) (("2" (rewrite "entry_form_matrix" +) (("2" (lift-if) (("2" (ground) (("1" (expand "tensor_fun" +) (("1" (assert) (("1" (case "NOT rows(A63)=6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (case "base_n_to_nat(6, LAMBDA (d): RelF6(1 + d), k) = (base_n_to_nat(6, RelF6, 1 + k) - mod(base_n_to_nat(6, RelF6, 1 + k), 6)) / 6") (("1" (replace -1 :dir rl) (("1" (case "mod(base_n_to_nat(6, RelF6, 1 + k), 6) = RelF6(0)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "FORALL (dd:nat): mod(base_n_to_nat(6, RelF6, dd), 6) = RelF6(0)") (("1" (inst?) nil nil) ("2" (induct "dd") (("1" (expand "base_n_to_nat" 1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (rewrite "expt_x0") (("1" (assert) (("1" (expand "mod" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "dd") (("2" (flatten) (("2" (assert) (("2" (expand "base_n_to_nat" (-1 1)) (("2" (expand "sigma" + 1) (("2" (case "6^(1+dd) = 6*6^dd") (("1" (replace -1) (("1" (assert) (("1" (lemma "mod_sum") (("1" (inst - "sigma(0, dd, LAMBDA (s: nat): 6 ^ s * RelF6(s))" "6" "(RelF6(1 + dd) * 6 ^ dd)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "^") (("2" (expand "expt" + 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (case "FORALL (dd:nat): mod(base_n_to_nat(6, RelF6, dd), 6) = RelF6(0)") (("1" (inst - "1+k") (("1" (replace -1) (("1" (assert) (("1" (expand "base_n_to_nat" +) (("1" (lemma "sigma_split") (("1" (inst - _ "1+k" _ _) (("1" (inst - _ _ "0") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "sigma" + 2) (("1" (expand "sigma" + 2) (("1" (rewrite "expt_x0") (("1" (assert) (("1" (cross-mult 1) (("1" (rewrite "sigma_scal" :dir rl) (("1" (lemma "sigma_shift_to_zero") (("1" (inst - _ "1+k" "1") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (rewrite "sigma_eq" 1) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "^" +) (("1" (expand "expt" + 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "dd") (("1" (expand "base_n_to_nat") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (rewrite "expt_x0") (("1" (assert) (("1" (expand "mod") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "dd") (("2" (flatten) (("2" (expand "base_n_to_nat" (-1 1)) (("2" (expand "sigma" +) (("2" (case "6^(1+dd) = 6*6^dd") (("1" (replaces -1) (("1" (lemma "mod_sum") (("1" (inst - "sigma(0, dd, LAMBDA (s: nat): 6 ^ s * RelF6(s))" "6" "(RelF6(1 + dd) * 6 ^ dd)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "^" 1) (("2" (expand "expt" + 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "base_n_to_nat_lt") (("2" (inst?) (("2" (split -) (("1" (lemma "tensor_power_rows_alt") (("1" (inst?) (("1" (assert) (("1" (replaces -1 :dir rl) (("1" (expand "^") (("1" (expand "expt" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "tensor_power_columns_alt") (("3" (inst?) (("3" (assert) (("3" (typepred "j") (("3" (replace -2 :dir rl) (("3" (case "3^(2+k) = 3^(1+k)* 3") (("1" (assert) nil nil) ("2" (expand "^" 1) (("2" (expand "expt" + 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "vect2matrix" + 1) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) (("2" (lemma "mod_pos") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "length_row") (("2" (expand "vect2matrix" 1) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (split -) (("1" (assert) nil nil) ("2" (replaces -1) (("2" --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.918 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26