| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Tarski/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 370 kB |
|
Quelle tarski_query.prfSprache: Lisp |
|||||||||||||||
|
(tarski_query (NSol_squared_gt 0 (NSol_squared_gt-1 nil 3619522848 ("" (skeep) (("" (expand "restrict") (("" (expand "NSol") (("" (case "Sol(a, n, polynomial_prod(g, k, g, k), 2 * k, >)=Sol(a, n, g, k, LAMBDA (s: [real, real]): / (("1" (assert) nil nil) ("2" (hide 3) (("2" (decompose-equality) (("2" (expand "Sol") (("2" (rewrite "polynomial_prod_def" :dir rl) (("2" (iff) (("2" (typepred "sq(polynomial(g,k)(x!1))") (("2" (lemma "sq_eq_0") (("2" (inst?) (("2" (expand "sq") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((restrict const-decl "R" restrict nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (polynomial_prod const-decl "real" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (/= const-decl "boolean" notequal 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (polynomial_prod_def formula-decl nil polynomials "reals/") (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sq_eq_0 formula-decl nil sq "reals/") (NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski nil)) shostak)) (NSol_squared_lt 0 (NSol_squared_lt-1 nil 3619522969 ("" (skeep) (("" (expand "NSol") (("" (lemma "empty_card[real]") (("" (inst?) (("" (assert) (("" (hide 3) (("" (expand "empty?") (("" (expand "member") (("" (skosimp*) (("" (expand "Sol") (("" (rewrite "polynomial_prod_def" :dir rl) (("" (flatten) (("" (typepred "sq(polynomial(g,k)(x!1))") (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski 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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (/= const-decl "boolean" notequal nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (sequence type-eq-decl nil sequences nil) (polynomial_prod const-decl "real" polynomials "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (member const-decl "bool" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (polynomial_prod_def formula-decl nil polynomials "reals/") (empty? const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty_card formula-decl nil finite_sets 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)) nil)) (NSol_poly1_lt 0 (NSol_poly1_lt-1 nil 3619523064 ("" (skeep) (("" (expand "NSol") (("" (lemma "empty_card[real]") (("" (inst?) (("" (assert) (("" (hide 3) (("" (expand "empty?") (("" (expand "member") (("" (skosimp*) (("" (expand "Sol") (("" (flatten) (("" (expand "polynomial" -2) (("" (expand "sigma") (("" (expand "sigma") (("" (expand "poly1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (/= const-decl "boolean" notequal nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (poly1 const-decl "nat" poly_families nil) (< const-decl "bool" reals nil) (member const-decl "bool" sets nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (empty? const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty_card formula-decl nil finite_sets 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)) shostak)) (A3_TCC1 0 (A3_TCC1-1 nil 3619454656 ("" (grind) nil nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (every adt-def-decl "boolean" list_adt nil)) nil)) (A3_TCC2 0 (A3_TCC2-1 nil 3619454656 ("" (grind) nil nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (every adt-def-decl "boolean" list_adt nil)) nil)) (A3_TCC3 0 (A3_TCC3-1 nil 3619454656 ("" (deftactic jingle (then (replaces -1) (replaces -1) (repeat (expand "nth")) (repeat (expand "length")))) (("" (split) (("1" (flatten) (("1" (skosimp*) (("1" (case "i!1 = 0 OR i!1 = 1 OR i!1 = 2") (("1" (case "j!1 = 0 OR j!1 = 1 OR j!1 = 2") (("1" (ground) (("1" (jingle) nil nil) ("2" (jingle) nil nil) ("3" (jingle) nil nil) ("4" (jingle) nil nil) ("5" (jingle) nil nil) ("6" (jingle) nil nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (typepred "j!1") (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide 2) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil)) nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (nth def-decl "T" list_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, 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) (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) (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) (length def-decl "nat" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices "matrices/") (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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/") (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (A3_inv_TCC1 0 (A3_inv_TCC1-1 nil 3619779062 ("" (skeep) (("" (assert) nil nil)) nil) nil nil)) (A3_inv_TCC2 0 (A3_inv_TCC2-1 nil 3619779062 ("" (grind) nil nil) ((listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (every adt-def-decl "boolean" list_adt nil)) nil)) (A3_inv_TCC3 0 (A3_inv_TCC3-1 nil 3619779062 ("" (grind) nil nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (every adt-def-decl "boolean" list_adt nil)) nil)) (A3_inv_TCC4 0 (A3_inv_TCC4-1 nil 3619779062 ("" (split) (("1" (flatten) (("1" (hide 1) (("1" (skosimp*) (("1" (case "NOT (i!1 = 0 OR i!1 = 1 OR i!1 = 2)") (("1" (ground) (("1" (hide 4) (("1" (typepred "i!1") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (case "NOT (j!1 = 0 OR j!1 = 1 OR j!1 = 2)") (("1" (hide -1) (("1" (hide 2) (("1" (flatten) (("1" (typepred "j!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (deftactic izp (then (ground) (repeat (replaces -1)) (grind))) (("2" (izp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil) ("7" (eval-formula 1) nil nil)) nil) ((bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (^ const-decl "real" exponentiation nil) (row const-decl "Vector" matrices "matrices/") (access const-decl "real" matrices "matrices/") (entry const-decl "real" matrices "matrices/") (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices "matrices/") (remove const-decl "{N | (rows(M) > 1 AND columns(M) > 1 IMPLIES (rows(N) = rows(M) - 1 AND columns(N) = columns(M) - 1)) AND (FORALL (m, n): LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF, newn = IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF IN entry(N)(m, n) = entry(M)(newm, newn))}" matrix_props "matrices/") (det def-decl "real" matrix_props "matrices/") (expt def-decl "real" exponentiation nil) (sigma def-decl "real" sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (int_expt application-judgement "int" exponentiation nil) (real_times_real_is_real application-judgement "real" 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/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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) (rows const-decl "nat" matrices "matrices/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nth def-decl "T" list_props nil) (TRUE const-decl "bool" booleans nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (length def-decl "nat" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil)) nil)) (TQ_vect3_TCC1 0 (TQ_vect3_TCC1-1 nil 3619454656 ("" (subtype-tcc) nil nil) ((poly1 const-decl "nat" poly_families nil)) nil)) (TQ_vect3_TCC2 0 (TQ_vect3_TCC2-1 nil 3619454656 ("" (expand "polynomial_prod") (("" (skeep) (("" (skeep) (("" (case "FORALL (GB:[nat->int],jj,kk:nat): rational_pred(sigma(jj,kk, GB)) AND integer_pred(sigma(jj,kk, GB)) ") (("1" (inst?) (("1" (assert) nil nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "kk") (("1" (skeep) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "GB" "jj") (("2" (expand "sigma" +) (("2" (flatten) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (case "FORALL (rd:int): rational_pred(GB(1+j)+rd)") (("1" (rewrite -1) nil nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil) ("2" (case "FORALL (rd:int): integer_pred(GB(1+j)+rd)") (("1" (rewrite -1) nil nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (k skolem-const-decl "{k | g(k) /= 0}" tarski_query nil) (g skolem-const-decl "[nat -> int]" tarski_query nil) (x1 skolem-const-decl "nat" tarski_query nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs 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) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (real_plus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (polynomial_prod const-decl "real" polynomials "reals/")) nil)) (TQ_vect3_TCC3 0 (TQ_vect3_TCC3-1 nil 3619454656 ("" (skeep) (("" (expand "polynomial_prod") (("" (expand "max") (("" (expand "sigma") (("" (expand "sigma") (("" (typepred "k") (("" (real-props) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial_prod const-decl "real" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (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) (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 "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nonzero_times3 formula-decl nil real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) nil)) (TQ_vect3_TCC4 0 (TQ_vect3_TCC4-1 nil 3619454656 ("" (skeep) (("" (deftactic jiffy (then (replaces -1) (replaces -1) (repeat (expand "nth")) (repeat (expand "length")) (ground))) (("" (split) (("1" (flatten) (("1" (skosimp*) (("1" (case "i!1 = 0 OR i!1 = 1 OR i!1 = 2") (("1" (case "j!1 = 0 OR j!1 = 1 OR j!1 =2") (("1" (ground) (("1" (jiffy) nil nil) ("2" (jiffy) nil nil) ("3" (jiffy) nil nil) ("4" (jiffy) nil nil) ("5" (jiffy) nil nil) ("6" (jiffy) nil nil)) nil) ("2" (hide (2 3)) (("2" (typepred "j!1") (("2" (jiffy) nil nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (typepred "i!1") (("2" (jiffy) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind :exclude ("TQ" "polynomial_prod")) nil nil) ("3" (grind :exclude ("TQ" "polynomial_prod")) nil nil) ("4" (grind :exclude ("TQ" "polynomial_prod")) nil nil) ("5" (grind :exclude ("TQ" "polynomial_prod")) nil nil)) nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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/") (posint_plus_nnint_is_posint application-judgement "posint" 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (rows const-decl "nat" matrices "matrices/") (below type-eq-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (polynomial_prod const-decl "real" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (poly1 const-decl "nat" poly_families nil) (TQ const-decl "int" compute_sturm_tarski nil) (/= const-decl "boolean" notequal nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (length def-decl "nat" list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (< const-decl "bool" reals 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (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) (nth def-decl "T" list_props nil)) nil)) (NSol_vect3_TCC1 0 (NSol_vect3_TCC1-1 nil 3619454656 ("" (skeep) (("" (deftactic jiffy (then (replaces -1) (replaces -1) (repeat (expand "nth")) (repeat (expand "length")) (ground))) (("" (split) (("1" (flatten) (("1" (skosimp*) (("1" (case "i!1 = 0 OR i!1 = 1 OR i!1 = 2") (("1" (case "j!1 = 0 OR j!1 = 1 OR j!1 =2") (("1" (ground) (("1" (jiffy) nil nil) ("2" (jiffy) nil nil) ("3" (jiffy) nil nil) ("4" (jiffy) nil nil) ("5" (jiffy) nil nil) ("6" (jiffy) nil nil)) nil) ("2" (hide (2 3)) (("2" (typepred "j!1") (("2" (jiffy) nil nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (typepred "i!1") (("2" (jiffy) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil)) nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans 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/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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) (rows const-decl "nat" matrices "matrices/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (restrict const-decl "R" restrict nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski nil) (bijective? const-decl "bool" functions nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (length def-decl "nat" list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (< const-decl "bool" reals 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nth def-decl "T" list_props nil)) nil)) (tarski_query_system_basic_3 0 (tarski_query_system_basic_3-1 nil 3619454894 ("" (skeep) (("" (rewrite "full_matrix_eq") (("" (invoke (case "NOT %1") (! 3 1)) (("1" (hide 4) (("1" (rewrite "rows_mult") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (invoke (case "NOT %1") (! 3 1)) (("1" (assert) (("1" (hide 4) (("1" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (hide-all-but -1) (("2" (expand "A3") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (typepred "i") (("2" (rewrite "rows_mult") (("2" (typepred "j") (("2" (rewrite "columns_mult") (("1" (assert) (("1" (case "NOT j = 0") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (case "NOT (i = 0 OR i = 1 OR i = 2)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (split) (("1" (replace -1) (("1" (assert) (("1" (rewrite "entry_mult" +) (("1" (expand "row" + 1) (("1" (assert) (("1" (expand "A3" +) (("1" (assert) (("1" (expand "length" + 1) (("1" (assert) (("1" (expand "length" + 1) (("1" (expand "length" + 1) (("1" (expand "length" + 1) (("1" (expand "nth" + 1) (("1" (expand "*" +) (("1" (rewrite "dot_eq_sigma") (("1" (rewrite "length_col") (("1" (expand "length" + 1) (("1" (expand "length" + 1) (("1" (expand "length" + 1) (("1" (expand "length" + 1) (("1" (expand "min") (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (rewrite "access_col") (("1" (rewrite "access_col") (("1" (rewrite "access_col") (("1" (expand "access" + 1) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "nth" +) (("1" (expand "access" + 2) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "nth" +) (("1" (expand "nth" +) (("1" (expand "access" + 2) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "nth" +) (("1" (expand "nth" +) (("1" (expand "nth" +) (("1" (assert) (("1" (expand "access") (("1" (rewrite "length_row") (("1" (rewrite "length_row") (("1" (assert) (("1" (expand "row") (("1" (assert) (("1" (typepred "TQ_vect3(a,n,g,k)") (("1" (expand "rows" -5) (("1" (assert) (("1" (expand "TQ_vect3" +) (("1" (expand "nth" + 2) (("1" (expand "nth" + 1) (("1" (expand "nth" + 2) (("1" (expand "nth" + 2) (("1" (expand "nth" + 2) (("1" (expand "nth" + 1) (("1" (expand "entry" +) (("1" (expand "access" +) (("1" (rewrite "length_row" +) (("1" (assert) (("1" (expand "NSol_vect3" +) (("1" (expand "row" +) (("1" (assert) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "length" +) (("1" (expand "nth" + 2) (("1" (expand "nth" + 1) (("1" (expand "restrict") (("1" (lemma "TQ_def") (("1" (inst - "a" "poly1" "0" "n") (("1" (assert) (("1" (split -1) (("1" (replaces -1) (("1" (lemma "TQ_def") (("1" (inst?) (("1" (assert) (("1" (split -1) (("1" (replace -1) (("1" (assert) (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (rewrite "NSol_squared_lt") (("1" (assert) (("1" (rewrite "NSol_poly1_lt") (("1" (assert) (("1" (invoke (both-sides "+" "%1" 3) (! 3 1 2)) (("1" (assert) (("1" (lemma "card_disj_union[real]") (("1" (expand "NSol" +) (("1" (rewrite -1 + :dir rl) (("1" (hide -1) (("1" (case "Sol(a, n, poly1, 0, >) =union(Sol(a, n, g, k, LAMBDA (s: [real, real]): =(s)), Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s)))") (("1" (assert) nil nil) ("2" (hide 4) (("2" (decompose-equality 1) (("2" (expand "Sol" +) (("2" (expand "union") (("2" (expand "member" +) (("2" (case "polynomial(poly1,0)(x!1)>0") (("1" (assert) (("1" (iff) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "poly1" 1) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (skeep) (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "Sol") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "polynomial_prod" 1) (("2" (expand "max") (("2" (expand "sigma") (("2" (expand "sigma") (("2" (assert) (("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "poly1") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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" (rewrite "entry_mult" +) (("2" (expand "row" + 1) (("2" (assert) (("2" (expand "A3" +) (("2" (assert) (("2" (expand "length" + 1) (("2" (assert) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "nth" + 1) (("2" (expand "nth" + 1) (("2" (expand "*" +) (("2" (rewrite "dot_eq_sigma") (("2" (rewrite "length_col") (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "min") (("2" (assert) (("2" (expand "sigma") (("2" (expand "sigma") (("2" (expand "sigma") (("2" (expand "sigma") (("2" (rewrite "access_col") (("2" (rewrite "access_col") (("2" (rewrite "access_col") (("2" (expand "access" + 1) (("2" (expand "length" +) (("2" (expand "length" +) (("2" (expand "length" +) (("2" (expand "nth" +) (("2" (expand "access" + 2) (("2" (rewrite "length_row") (("2" (assert) (("2" (expand "access" + 1) (("2" (expand "length" +) (("2" (expand "length" +) (("2" (expand "length" +) (("2" (expand "access" + 1) (("2" (expand "length" +) (("2" (expand "length" +) (("2" (expand "length" +) (("2" (expand "TQ_vect3" +) (("2" (expand "row") (("2" (expand "access") (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (assert) (("2" (expand "nth" + 1) (("2" (expand "nth" + 1) (("2" (expand "nth" + 2) (("2" (expand "nth" + 2) (("2" (expand "nth" + 2) (("2" (expand "nth" + 2) (("2" (expand "nth" + 2) (("2" (assert) (("2" (expand "nth" + 1) (("2" (expand "nth" + 1) (("2" (expand "nth" + 1) (("2" (expand "nth" + 1) (("2" (expand "length" + 1) (("2" (expand "nth" + 2) (("2" (expand "nth" + 2) (("2" (expand "nth" + 2) (("2" (expand "nth" + 1) (("2" (expand "NSol_vect3" +) (("2" (expand "restrict") (("2" (expand "entry") (("2" (expand "row") (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "length" + 1) (("2" (expand "nth" +) (("2" (expand "nth" +) (("2" (expand "access") (("2" (expand "length" + 1) (("2" (expand "nth") (("2" (lemma "TQ_def") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (replaces -1) (("1" (lemma "TQ_def") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (assert) (("1" (rewrite "NSol_squared_lt") (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (assert) (("1" (expand "NSol") (("1" (case "Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s)) = union(Sol(a, n, g, k, >),Sol(a, n, g, k, <))") (("1" (lemma "card_disj_union[real]") (("1" (inst?) (("1" (split -1) (("1" (replace -2 :dir rl) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 4) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (expand "intersection") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "Sol") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (decompose-equality 1) (("2" (expand "union") (("2" (expand "member") (("2" (expand "Sol") (("2" (iff) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "polynomial_prod") (("2" (expand "max") (("2" (expand "sigma") (("2" (expand "sigma") (("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst?) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -1) (("3" (assert) (("3" (rewrite "entry_mult" +) (("3" (expand "row" + 1) (("3" (assert) (("3" (expand "A3" +) (("3" (assert) (("3" (expand "length" + 1) (("3" (assert) (("3" (expand "length" + 1) (("3" (expand "length" + 1) (("3" (expand "length" + 1) (("3" (expand "nth" + 1) (("3" (expand "nth" + 1) (("3" (expand "*" +) (("3" (rewrite "dot_eq_sigma") (("3" (rewrite "length_col") (("3" (expand "nth" + 1) (("3" (expand "length" + 1) (("3" (expand "length" + 1) (("3" (expand "length" + 1) (("3" (expand "length" + 1) (("3" (expand "min") (("3" (expand "sigma") (("3" (expand "sigma") (("3" (expand "sigma") (("3" (expand "sigma") (("3" (rewrite "access_col") (("3" (rewrite "access_col") (("3" (rewrite "access_col") (("3" (expand "access" + 1) (("3" (expand "nth" + 1) (("3" (expand "length" +) (("3" (expand "length" +) (("3" (expand "length" +) (("3" (expand "nth" + 1) (("3" (expand "NSol_vect3") (("3" (hide -) (("3" (grind :exclude ("TQ" "NSol")) (("3" (rewrite "TQ_def") (("1" (rewrite "TQ_def") (("1" (assert) (("1" (rewrite "NSol_squared_lt") (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (expand "NSol") (("1" (case "Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s)) = union(Sol(a, n, g, k,>),Sol(a,n,g,k,<))") (("1" (lemma "card_disj_union[real]") (("1" (inst?) (("1" (assert) (("1" (expand "disjoint?" 1) (("1" (expand "empty?") (("1" (expand "intersection") (("1" (expand "member") (("1" (skosimp*) (("1" (expand "Sol" (-1 -2)) (("1" (flatten) (("1" (name "ZZP" "polynomial(g,k)(x!1)") (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "Sol") (("2" (expand "union") (("2" (expand "member") (("2" (name "RD" "polynomial(a,n)") (("2" (replaces -1) (("2" (name "D65" "polynomial(g,k)") (("2" (replaces -1) (("2" (decompose-equality 1) (("2" (iff) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nzreal_times_nzreal_is_nzreal") (("2" (inst?) (("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)) 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-all-but -1) (("2" (typepred "A3") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil) ((mult_full application-judgement "FullMatrix" matrices "matrices/") (full_matrix_eq formula-decl nil matrices "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/") (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/") (MatrixMN type-eq-decl nil matrices "matrices/") (entry const-decl "real" matrices "matrices/") (Vector type-eq-decl nil matrices "matrices/") (* const-decl "real" matrices "matrices/") (row const-decl "Vector" matrices "matrices/") (VectorN type-eq-decl nil matrices "matrices/") (col def-decl "VectorN(rows(M))" matrices "matrices/") (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices "matrices/") (> const-decl "bool" reals nil) (PosFullMatrix type-eq-decl nil matrices "matrices/") (A3 const-decl "{M: PosFullMatrix | rows(M) = 3 AND columns(M) = 3}" tarski_query nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (TQ_vect3 const-decl "{v: PosFullMatrix | rows(v) = 3 AND columns(v) = 1}" tarski_query nil) (NSol_vect3 const-decl "{v: PosFullMatrix | rows(v) = 3 AND columns(v) = 1}" tarski_query nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (entry_mult formula-decl nil matrices "matrices/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (null adt-constructor-decl "(null?)" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (dot_eq_sigma formula-decl nil matrices "matrices/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (sigma def-decl "real" sigma "reals/") (access_col formula-decl nil matrix_props "matrices/") (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (TQ_def formula-decl nil compute_sturm_tarski nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (polynomial_prod const-decl "real" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (member const-decl "bool" sets nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (union const-decl "set" sets nil) (finite_union application-judgement "finite_set" finite_sets nil) (card_disj_union formula-decl nil finite_sets nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (bijective? const-decl "bool" functions nil) (NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NSol_poly1_lt formula-decl nil tarski_query nil) (NSol_squared_lt formula-decl nil tarski_query nil) (NSol_squared_gt formula-decl nil tarski_query nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil) (nzreal nonempty-type-eq-decl nil reals nil) (poly1 const-decl "nat" poly_families nil) (restrict const-decl "R" restrict 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) (length_row formula-decl nil matrix_props "matrices/") (real_minus_real_is_real application-judgement "real" reals nil) (access const-decl "real" matrices "matrices/") (length_col formula-decl nil matrices "matrices/") (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) (columns_mult formula-decl nil matrices "matrices/") (rows_mult formula-decl nil matrices "matrices/") (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (A6_TCC1 0 (A6_TCC1-1 nil 3619526340 ("" (grind) nil nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (every adt-def-decl "boolean" list_adt nil)) nil)) (A6_TCC2 0 (A6_TCC2-1 nil 3619526340 ("" (deftactic flipper (then (replaces -1) (replaces -1) (repeat (expand "nth")) (repeat (expand "length")) (assert))) (("" (split) (("1" (flatten) (("1" (skeep) (("1" (case "i = 0 OR i = 1 OR i = 2 OR i = 3 OR i = 4 OR i = 5") (("1" (case "j = 0 OR j = 1 OR j = 2 OR j = 3 OR j = 4 OR j = 5") (("1" (hide 1) (("1" (deftactic skipper (then (split -) (split -) (flipper))) (("1" (skipper) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "j") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil)) nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (nth def-decl "T" list_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (OR const-decl "[bool, 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) (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) (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) (length def-decl "nat" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices "matrices/") (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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/") (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (NSol_vect6_TCC1 0 (NSol_vect6_TCC1-1 nil 3619526340 ("" (skeep) (("" (split) (("1" (flatten) (("1" (hide 1) (("1" (deftactic flipper (then (replaces -1) (replaces -1) (repeat (expand "nth")) (repeat (expand "length")) (assert))) (("1" (skeep) (("1" (case "i = 0 OR i = 1 OR i = 2 OR i = 3 OR i = 4 OR i = 5") (("1" (case "j = 0 OR j = 1 OR j = 2 OR j = 3 OR j = 4 OR j = 5") (("1" (deftactic skipper (then (split -) (split -) (flipper))) (("1" (skipper) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "j") (("2" (grind :exclude "NSol") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "i") (("2" (grind :exclude "NSol") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind :exclude "NSol") nil nil) ("3" (grind :exclude "NSol") nil nil) ("4" (grind :exclude "NSol") nil nil) ("5" (grind :exclude "NSol") nil nil)) nil)) nil) ((nth def-decl "T" list_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (OR const-decl "[bool, 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) (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) (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) (length def-decl "nat" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (/= const-decl "boolean" notequal nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (bijective? const-decl "bool" functions nil) (NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (restrict const-decl "R" restrict nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (<= const-decl "bool" reals nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (rows const-decl "nat" matrices "matrices/") (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/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)) nil)) (tarski_query_system_basic_6 0 (tarski_query_system_basic_6-1 nil 3619526348 ("" (skeep) (("" (rewrite "full_matrix_eq") (("" (invoke (case "NOT %1") (! 3 1)) (("1" (hide 2) (("1" (rewrite "rows_mult") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (invoke (case "NOT %1") (! 3 1)) (("1" (hide 2) (("1" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (hide-all-but -1) (("2" (expand "A6") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (typepred "i") (("2" (rewrite "rows_mult") (("2" (typepred "j") (("2" (rewrite "columns_mult") (("1" (assert) (("1" (case "NOT j = 0") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (case "NOT (i = 0 OR i = 1 OR i = 2 OR i = 3 OR i = 4 OR i = 5)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (split) (("1" (replace -1) (("1" (hide -) (("1" (grind :exclude ("TQ" "NSol")) (("1" (expand "restrict") (("1" (rewrite "TQ_def") (("1" (rewrite "TQ_def") (("1" (assert) (("1" (rewrite "NSol_squared_lt") (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (rewrite "NSol_poly1_lt") (("1" (assert) (("1" (expand "NSol") (("1" (case "Sol(a, n, poly1, 0, >) =union(Sol(a, n, g, k, LAMBDA (s: [real, real]): =(s)), Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s)))") (("1" (assert) (("1" (lemma "card_disj_union[real]") (("1" (inst?) (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (skeep) (("1" (expand "member") (("1" (expand "intersection") (("1" (expand "member") (("1" (expand "Sol") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "union") (("2" (expand "member") (("2" (name "AB" "Sol(a, n, poly1, 0, >)") (("2" (replaces -1) (("2" (name "ABC" "Sol(a, n, g, k, LAMBDA (s: [real, real]): =(s))") (("2" (replaces -1) (("2" (name "ABCD" "Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s))") (("2" (replaces -1) (("2" (decompose-equality 1) (("2" (iff) (("2" (expand "ABC") (("2" (expand "ABCD") (("2" (expand "AB") (("2" (expand "Sol") (("2" (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) ("2" (real-props) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -) (("2" (grind :exclude ("TQ" "NSol")) (("2" (rewrite "TQ_def") (("1" (rewrite "TQ_def") (("1" (assert) (("1" (rewrite "NSol_squared_lt") (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (case "Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s)) = union(Sol(a, n, g, k, >) ,Sol(a, n, g, k, <))") (("1" (expand "NSol") (("1" (assert) (("1" (lemma "card_disj_union[real]") (("1" (inst?) (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (skeep) (("1" (expand "member") (("1" (expand "intersection") (("1" (expand "member") (("1" (expand "Sol") (("1" (flatten) (("1" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "union") (("2" (expand "member") (("2" (grind :exclude "polynomial") (("2" (decompose-equality 1) (("2" (iff) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (real-props) nil nil)) nil)) nil)) nil)) nil) ("3" (replace -1) (("3" (hide -) (("3" (grind :exclude ("TQ" "NSol")) (("3" (rewrite "TQ_def") (("1" (rewrite "TQ_def") (("1" (assert) (("1" (rewrite "NSol_squared_lt") (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (case "Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s)) = union(Sol(a, n, g, k, >) ,Sol(a, n, g, k, <))") (("1" (lemma "card_disj_union[real]") (("1" (expand "NSol") (("1" (inst?) (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (skeep) (("1" (expand "member") (("1" (expand "intersection") (("1" (expand "member") (("1" (expand "Sol") (("1" (flatten) (("1" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "union") (("2" (expand "member") (("2" (grind :exclude "polynomial") (("2" (decompose-equality 1) (("2" (iff) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (real-props) nil nil)) nil)) nil)) nil)) nil) ("4" (replace -1) (("4" (hide -) (("4" (grind :exclude ("TQ" "NSol")) (("4" (expand "restrict") (("4" (rewrite "TQ_def") (("1" (rewrite "NSol_squared_lt") (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (real-props) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (replace -1) (("5" (hide -) (("5" (grind :exclude ("TQ" "NSol")) (("5" (rewrite "TQ_def") (("5" (rewrite "TQ_def") (("5" (rewrite "TQ_def") (("1" (assert) (("1" (rewrite "NSol_squared_lt") (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (rewrite "NSol_poly1_lt") (("1" (assert) (("1" (expand "NSol") (("1" (case "Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s)) = union(Sol(a, n, g, k, >) ,Sol(a, n, g, k, <))") (("1" (lemma "card_disj_union[real]") (("1" (inst?) (("1" (assert) (("1" (split -1) (("1" (replace -2) (("1" (replace -1) (("1" (assert) (("1" (case "card(Sol(a, n, poly1, 0, >)) - card(Sol(a, n, g, k, <))=card(Sol(a, n, g, k, >=))") (("1" (assert) nil nil) ("2" (hide 4) (("2" (hide -) (("2" (case "Sol(a, n, poly1, 0, >) = union(Sol(a, n, g, k, <),Sol(a, n, g, k, >=))") (("1" (lemma "card_disj_union[real]") (("1" (inst?) (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (skeep) (("1" (expand "member") (("1" (expand "intersection") (("1" (expand "member") (("1" (expand "Sol") (("1" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind :exclude "polynomial") (("2" (decompose-equality 1) (("2" (iff) (("2" (case "polynomial(poly1,0)(x!1) > 0") (("1" (ground) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (skeep) (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "Sol") (("2" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "union") (("2" (expand "member") (("2" (grind :exclude "polynomial") (("2" (decompose-equality 1) (("2" (iff) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (real-props) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (replace -1) (("6" (hide -) (("6" (grind :exclude ("TQ" "NSol")) (("6" (rewrite "TQ_def") (("6" (rewrite "TQ_def") (("1" (rewrite "TQ_def") (("1" (assert) (("1" (rewrite "NSol_squared_lt") (("1" (rewrite "NSol_squared_gt") (("1" (expand "restrict") (("1" (assert) (("1" (rewrite "NSol_poly1_lt") (("1" (assert) (("1" (case "Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s)) = union(Sol(a, n, g, k, >) ,Sol(a, n, g, k, <))") (("1" (lemma "card_disj_union[real]") (("1" (inst?) (("1" (expand "NSol") (("1" (assert) (("1" (split -1) (("1" (replaces -2) (("1" (replaces -1) (("1" (assert) (("1" (case "Sol(a, n, poly1, 0, >) = union(Sol(a, n, g, k, >),Sol(a, n, g, k, <=))") (("1" (lemma "card_disj_union[real]") (("1" (inst?) (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (skeep) (("1" (expand "member") (("1" (expand "intersection") (("1" (expand "member") (("1" (expand "Sol") (("1" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "union") (("2" (expand "member") (("2" (grind :exclude "polynomial") (("2" (decompose-equality 1) (("2" (iff) (("2" (ground) (("1" (hide -) (("1" (grind) nil nil)) nil) ("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (skeep) (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "Sol") (("2" (grind :exclude "polynomial") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "union") (("2" (expand "member") (("2" (grind :exclude "polynomial") (("2" (decompose-equality 1) (("2" (iff) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (real-props) nil nil)) nil)) nil)) 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) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil) ((mult_full application-judgement "FullMatrix" matrices "matrices/") (full_matrix_eq formula-decl nil matrices "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/") (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/") (MatrixMN type-eq-decl nil matrices "matrices/") (entry const-decl "real" matrices "matrices/") (Vector type-eq-decl nil matrices "matrices/") (* const-decl "real" matrices "matrices/") (row const-decl "Vector" matrices "matrices/") (VectorN type-eq-decl nil matrices "matrices/") (col def-decl "VectorN(rows(M))" matrices "matrices/") (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices "matrices/") (> const-decl "bool" reals nil) (PosFullMatrix type-eq-decl nil matrices "matrices/") (A6 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" tarski_query nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (TQ_vect3 const-decl "{v: PosFullMatrix | rows(v) = 3 AND columns(v) = 1}" tarski_query nil) (NSol_vect6 const-decl "{v: PosFullMatrix | rows(v) = 6 AND columns(v) = 1}" tarski_query nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices "matrices/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices "matrices/") (dot def-decl "real" matrices "matrices/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (access const-decl "real" matrices "matrices/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals 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) (form_matrix_square application-judgement "FullMatrix" matrices "matrices/") (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_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) (poly1 const-decl "nat" poly_families nil) (TQ_def formula-decl nil compute_sturm_tarski nil) (nonzero_times3 formula-decl nil real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (NSol_squared_gt formula-decl nil tarski_query nil) (NSol_poly1_lt formula-decl nil tarski_query nil) (NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski nil) (ABCD skolem-const-decl "finite_set[real]" tarski_query nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (AB skolem-const-decl "finite_set[real]" tarski_query nil) (ABC skolem-const-decl "finite_set[real]" tarski_query nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (card_disj_union formula-decl nil finite_sets nil) (union const-decl "set" sets nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (finite_union application-judgement "finite_set" finite_sets nil) (NSol_squared_lt formula-decl nil tarski_query nil) (sigma def-decl "real" sigma "reals/") (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (sequence type-eq-decl nil sequences nil) (polynomial_prod const-decl "real" polynomials "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (restrict const-decl "R" restrict nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (columns_mult formula-decl nil matrices "matrices/") (rows_mult formula-decl nil matrices "matrices/") (NOT const-decl "[bool -> bool]" booleans nil)) nil)))
¤ Dauer der Verarbeitung: 0.358 Sekunden (vorverarbeitet am 2026-05-05) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26