Impressum tarski_query.prf
Sprache: Lisp
(tarski_querynil 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]): /=(s))" )"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 )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" polynomials "reals/" )nil sequences nil )nil integers nil )"bool" reals nil )nil integers nil )"finite_set[real]" sturmtarski nil )nil finite_sets nil )"bool" finite_sets nil )"boolean" notequal nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )nil polynomials "reals/" )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_types nil )"nonneg_real" sq "reals/" )"[real -> real]" polynomials "reals/" )nil sq "reals/" )"{d: nat | " sturmtarski nil)) 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 )"{d: nat | " sturmtarski nil) "(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )nil naturalnumbers nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"boolean" notequal nil )"finite_set[real]" sturmtarski nil )nil integers nil )"bool" reals nil )nil integers nil )nil sequences nil )"real" polynomials "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil ) (member const-decl "bool" sets nil )"(total_order?[real])" nil )"[real -> real]" polynomials "reals/" )"nonneg_real" sq "reals/" )nil real_types nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )nil polynomials "reals/" )"bool" sets nil )"(strict_total_order?[real])" real_props nil )nil finite_sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil ))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 )"{d: nat | " sturmtarski nil) nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )nil naturalnumbers nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"boolean" notequal nil )"finite_set[real]" sturmtarski nil )nil integers nil )"bool" reals nil )nil integers nil )"nat" poly_families nil )"bool" reals nil ) (member const-decl "bool" sets nil )"[real -> real]" polynomials "reals/" )"real" sigma "reals/" )"bool" sets nil )"(strict_total_order?[real])" real_props nil )nil finite_sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3619454656 ("" (grind) nil nil )"odd_int" integers nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"boolean" list_adt nil ))nil ))nil 3619454656 ("" (grind) nil nil )"posrat" nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"nzrat" rationalsnil )"odd_int" integers nil )"boolean" list_adt nil ))nil ))nil 3619454656"" expand "nth" ))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 )"odd_int" integers nil )"T" list_props nil )"nzrat" rationalsnil )"posrat" nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"posint" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"nat" matrices "matrices/" )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{c: nat | AND AND c = 0 OR " "matrices/" )"bool" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil ))nil ))nil 3619779062"" (skeep) (("" (assert ) nil nil )) nil ) nil nil ))nil 3619779062 ("" (grind) nil nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"boolean" list_adt nil ))nil ))nil 3619779062 ("" (grind) nil nil )"odd_int" integers nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"boolean" list_adt nil ))nil ))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" "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 )"bool" functions nil )"(bijective?[T, T])" identity nil )"real" exponentiation nil )"Vector" matrices "matrices/" )"real" matrices "matrices/" )"real" matrices "matrices/" )"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" "structures/" )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"{M: MatrixMN(m, n) | " "matrices/" )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" "matrices/" )"real" matrix_props "matrices/" )"real" exponentiation nil )"real" sigma "reals/" )"(total_order?[real])" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"real" reals nil )"real" reals nil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" reals nil )"{c: nat | AND AND c = 0 OR " "matrices/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"nat" matrices "matrices/" )"(strict_total_order?[real])" real_props nil )"T" list_props nil )"bool" booleans nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"int" integers nil )"posint" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )nil number_fields nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[numfield -> numfield]" number_fields nil )nil naturalnumbers nil ))nil ))nil 3619454656 ("" (subtype-tcc) nil nil )"nat" poly_families nil )) nil ))nil 3619454656"" (expand "polynomial_prod" )"" (skeep)"" (skeep)"" case "FORALL (GB:[nat->int],jj,kk:nat): AND ") "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" "1" case "FORALL (rd:int): rational_pred(GB(1+j)+rd)" )"1" (rewrite -1) nil nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" case "FORALL (rd:int): integer_pred(GB(1+j)+rd)" )"1" (rewrite -1) nil nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"[bool, bool -> bool]" booleans nil )"{k | g(k) /= 0}" tarski_query nil )"[nat -> int]" tarski_query nil )"nat" tarski_query nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"boolean" notequal nil )"int" integers nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil defined_types nil )nil naturalnumbers nil )"real" reals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" polynomials "reals/" ))nil ))nil 3619454656"" (skeep)"" (expand "polynomial_prod" )"" (expand "max" )"" (expand "sigma" )"" (expand "sigma" )"" (typepred "k" ) (("" (real-props) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" polynomials "reals/" )"real" sigma "reals/" )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(divides(n))" divides nil )nil real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil ))nil ))nil 3619454656"" (skeep)"" expand "nth" ))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 )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"bool" booleans nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{c: nat | AND AND c = 0 OR " "matrices/" )"posint" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"nat" matrices "matrices/" )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" polynomials "reals/" )nil sequences nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"nat" poly_families nil )"int" compute_sturm_tarski nil )"boolean" notequal nil )nil integers nil )"bool" reals nil )nil integers nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"nat" list_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"T" list_props nil ))nil ))nil 3619454656"" (skeep)"" expand "nth" ))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 )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"bool" booleans nil )"{c: nat | AND AND c = 0 OR " "matrices/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"nat" matrices "matrices/" )"posint" nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"R" restrict nil )nil integers nil )"bool" reals nil )nil integers nil )"{d: nat | " sturmtarski nil) "bool" functions nil )"finite_set[real]" sturmtarski nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"boolean" notequal nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"nat" list_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"T" list_props nil ))nil ))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" "1" (assert ) nil nil ))nil )"2" "1" replace -1)"1" assert )"1" rewrite "entry_mult" +)"1" expand "row" + 1)"1" assert )"1" expand "A3" +)"1" assert )"1" expand "length" "1" assert )"1" expand "length" "1" expand "length" "1" expand "length" "1" expand "nth" "1" expand "*" "1" rewrite "dot_eq_sigma" )"1" rewrite "length_col" )"1" expand "length" "1" expand "length" "1" expand "length" "1" expand "length" "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" expand "length" "1" expand "length" "1" expand "length" "1" expand "nth" "1" expand "access" "1" expand "length" "1" expand "length" "1" expand "length" "1" expand "nth" "1" expand "nth" "1" expand "access" "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" "TQ_vect3(a,n,g,k)" )"1" expand "rows" "1" assert )"1" expand "TQ_vect3" "1" expand "nth" "1" expand "nth" "1" expand "nth" "1" expand "nth" "1" expand "nth" "1" expand "nth" "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" "1" expand "nth" "1" expand "restrict" )"1" "TQ_def" )"1" "a" "poly1" "0" "n" )"1" assert )"1" "1" "1" "TQ_def" )"1" "1" assert )"1" "1" replace "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" "+" "%1" "1" assert )"1" "card_disj_union[real]" )"1" expand "NSol" "1" rewrite "1" "1" case "Sol(a, n, poly1, 0, >) =union(Sol(a, n, g, k, LAMBDA (s: [real, real]): =(s)), LAMBDA (s: [real, real]): /=(s)))") "1" assert )nil nil )"2" "2" "2" expand "Sol" "2" expand "union" )"2" expand "member" "2" case "polynomial(poly1,0)(x!1)>0" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" expand "poly1" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" expand "empty?" )"2" "2" expand "member" )"2" expand "intersection" )"2" expand "member" )"2" expand "Sol" )"2" 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" "2" expand "max" )"2" expand "sigma" )"2" expand "sigma" )"2" assert )"2" "nzreal_times_nzreal_is_nzreal" )"2" "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" "2" assert )"2" expand "length" "2" expand "length" "2" expand "length" "2" expand "nth" "2" expand "nth" "2" expand "*" "2" rewrite "dot_eq_sigma" )"2" rewrite "length_col" )"2" expand "length" "2" expand "length" "2" expand "length" "2" expand "length" "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" "2" expand "length" "2" expand "length" "2" expand "length" "2" expand "nth" "2" expand "access" "2" rewrite "length_row" )"2" assert )"2" expand "access" "2" expand "length" "2" expand "length" "2" expand "length" "2" expand "access" "2" expand "length" "2" expand "length" "2" expand "length" "2" expand "TQ_vect3" "2" expand "row" )"2" expand "access" )"2" expand "length" "2" expand "length" "2" expand "length" "2" expand "length" "2" expand "length" "2" expand "length" "2" expand "length" "2" expand "length" "2" assert )"2" expand "nth" "2" expand "nth" "2" expand "nth" "2" expand "nth" "2" expand "nth" "2" expand "nth" "2" expand "nth" "2" assert )"2" expand "nth" "2" expand "nth" "2" expand "nth" "2" expand "nth" "2" expand "length" "2" expand "nth" "2" expand "nth" "2" expand "nth" "2" expand "nth" "2" expand "NSol_vect3" "2" expand "restrict" )"2" expand "entry" )"2" expand "row" )"2" expand "length" "2" expand "length" "2" expand "length" "2" expand "length" "2" expand "nth" "2" expand "nth" "2" expand "access" )"2" expand "length" "2" expand "nth" )"2" "TQ_def" )"2" "2" assert )"2" "1" "1" "TQ_def" )"1" "1" assert )"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" "card_disj_union[real]" )"1" "1" "1" replace "1" replace "1" assert )nil nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" expand "empty?" )"2" expand "intersection" )"2" expand "member" )"2" "2" expand "Sol" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "union" )"2" expand "member" )"2" expand "Sol" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "polynomial_prod" )"2" expand "max" )"2" expand "sigma" )"2" expand "sigma" )"2" "nzreal_times_nzreal_is_nzreal" )"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 ))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" "3" assert )"3" expand "length" "3" expand "length" "3" expand "length" "3" expand "nth" "3" expand "nth" "3" expand "*" "3" rewrite "dot_eq_sigma" )"3" rewrite "length_col" )"3" expand "nth" "3" expand "length" "3" expand "length" "3" expand "length" "3" expand "length" "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" "3" expand "nth" "3" expand "length" "3" expand "length" "3" expand "length" "3" expand "nth" "3" expand "NSol_vect3" )"3" "3" "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" "card_disj_union[real]" )"1" "1" assert )"1" expand "disjoint?" "1" expand "empty?" )"1" expand "intersection" )"1" expand "member" )"1" "1" expand "Sol" "1" "1" "ZZP" "polynomial(g,k)(x!1)" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Sol" )"2" expand "union" )"2" expand "member" )"2" "RD" "polynomial(a,n)" )"2" "2" "D65" "polynomial(g,k)" )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "nzreal_times_nzreal_is_nzreal" )"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 ))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 )"FullMatrix" matrices "matrices/" )nil matrices "matrices/" )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices "matrices/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices "matrices/" )"nat" matrices "matrices/" )"bool" reals nil )"{c: nat | AND AND c = 0 OR " "matrices/" )nil matrices "matrices/" )"real" matrices "matrices/" )nil matrices "matrices/" )"real" matrices "matrices/" )"Vector" matrices "matrices/" )nil matrices "matrices/" )"VectorN(rows(M))" matrices "matrices/" )"{A: MatrixMN(rows(M), columns(N)) | " "matrices/" )"bool" reals nil )nil matrices "matrices/" )"{M: PosFullMatrix | rows(M) = 3 AND columns(M) = 3}" nil )nil integers nil )nil integers nil )"boolean" notequal nil )"{v: PosFullMatrix | rows(v) = 3 AND columns(v) = 1}" tarski_querynil )"{v: PosFullMatrix | rows(v) = 3 AND columns(v) = 1}" tarski_querynil )"posint" nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"rat" rationals nil )"rat" rationals nil )"posrat" nil )"nonneg_rat" nil )"rat" rationals nil )nil matrices "matrices/" )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"(total_order?[real])" nil )"nzrat" rationalsnil )"posint" nil )"(null?)" list_adt nil )"[numfield -> numfield]" number_fields nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )nil number_fields nil )nil matrices "matrices/" )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" sigma "reals/" )nil matrix_props "matrices/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil compute_sturm_tarski nil )"[numfield, numfield -> numfield]" number_fields nil )"real" polynomials "reals/" )nil sequences nil )"nonneg_int" nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"finite_set" nil )"bool" sets nil )"real" exponentiation nil )"real" exponentiation nil )"[real -> real]" polynomials "reals/" )"set" sets nil )"finite_set" finite_sets nil )nil finite_sets nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"finite_set[real]" sturmtarski nil )"bool" functions nil )"{d: nat | " sturmtarski nil) "[numfield, numfield -> numfield]" number_fields nil )nil tarski_query nil )nil tarski_query nil )nil tarski_query nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil real_types nil )nil reals nil )"nat" poly_families nil )"R" restrict nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil matrix_props "matrices/" )"real" reals nil )"real" matrices "matrices/" )nil matrices "matrices/" )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil matrices "matrices/" )nil matrices "matrices/" )NOT const-decl "[bool -> bool]" booleans nil ))nil 3619526340 ("" (grind) nil nil )"posrat" nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"nzrat" rationalsnil )"odd_int" integers nil )"boolean" list_adt nil ))nil ))nil 3619526340"" expand "nth" ))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" "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 )"odd_int" integers nil )"T" list_props nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"nzrat" rationalsnil )"posrat" nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"(strict_total_order?[real])" real_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"nat" matrices "matrices/" )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{c: nat | AND AND c = 0 OR " "matrices/" )"bool" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil ))nil ))nil 3619526340"" (skeep)"" (split)"1" (flatten)"1" (hide 1)"1" expand "nth" ))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" "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 )"T" list_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posint" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"boolean" notequal nil )nil naturalnumbers nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"finite_set[real]" sturmtarski nil )"bool" functions nil )"{d: nat | " sturmtarski nil) nil integers nil )"bool" reals nil )nil integers nil )"R" restrict nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"bool" reals nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil )"nat" matrices "matrices/" )"{c: nat | AND AND c = 0 OR " "matrices/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil ))nil ))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" "1" (assert ) nil nil ))nil )"2" "1" replace -1)"1" "1" "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)), LAMBDA (s: [real, real]): /=(s)))") "1" assert )"1" "card_disj_union[real]" )"1" "1" assert )"1" "1" expand "disjoint?" )"1" expand "empty?" )"1" "1" expand "member" )"1" expand "intersection" )"1" expand "member" )"1" expand "Sol" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "union" )"2" expand "member" )"2" "AB" "Sol(a, n, poly1, 0, >)" )"2" "2" "ABC" "Sol(a, n, g, k, LAMBDA (s: [real, real]): =(s))" )"2" "2" "ABCD" "Sol(a, n, g, k, LAMBDA (s: [real, real]): /=(s))" )"2" "2" "2" "2" expand "ABC" )"2" expand "ABCD" )"2" expand "AB" )"2" expand "Sol" )"2" 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" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "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" "card_disj_union[real]" )"1" "1" assert )"1" "1" expand "disjoint?" )"1" expand "empty?" )"1" "1" expand "member" )"1" expand "intersection" )"1" expand "member" )"1" expand "Sol" )"1" "1" "polynomial" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "union" )"2" expand "member" )"2" "polynomial" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"3" replace -1)"3" "3" "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" "card_disj_union[real]" )"1" expand "NSol" )"1" "1" assert )"1" "1" expand "disjoint?" )"1" expand "empty?" )"1" "1" expand "member" )"1" expand "intersection" )"1" expand "member" )"1" expand "Sol" )"1" "1" "polynomial" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "union" )"2" expand "member" )"2" "polynomial" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"4" replace -1)"4" "4" "TQ" "NSol" ))"4" expand "restrict" )"4" rewrite "TQ_def" )"1" rewrite "NSol_squared_lt" )"1" rewrite "NSol_squared_gt" )"1" expand "restrict" )"1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"5" replace -1)"5" "5" "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" "card_disj_union[real]" )"1" "1" assert )"1" "1" replace "1" replace "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" "2" "2" case "Sol(a, n, poly1, 0, >) = union(Sol(a, n, g, k, <),Sol(a, n, g, k, >=))" )"1" "card_disj_union[real]" )"1" "1" assert )"1" "1" expand "disjoint?" )"1" expand "empty?" )"1" "1" expand "member" )"1" expand "intersection" )"1" expand "member" )"1" expand "Sol" )"1" "polynomial" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "polynomial" )"2" "2" "2" case "polynomial(poly1,0)(x!1) > 0" )"1" nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" expand "empty?" )"2" "2" expand "member" )"2" expand "intersection" )"2" expand "member" )"2" expand "Sol" )"2" "polynomial" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "union" )"2" expand "member" )"2" "polynomial" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" replace -1)"6" "6" "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" "card_disj_union[real]" )"1" "1" expand "NSol" )"1" assert )"1" "1" "1" "1" assert )"1" case "Sol(a, n, poly1, 0, >) = union(Sol(a, n, g, k, >),Sol(a, n, g, k, <=))" )"1" "card_disj_union[real]" )"1" "1" assert )"1" "1" expand "disjoint?" )"1" expand "empty?" )"1" "1" expand "member" )"1" expand "intersection" )"1" expand "member" )"1" expand "Sol" )"1" "polynomial" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "union" )"2" expand "member" )"2" "polynomial" )"2" "2" "2" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" expand "empty?" )"2" "2" expand "member" )"2" expand "intersection" )"2" expand "member" )"2" expand "Sol" )"2" "polynomial" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "union" )"2" expand "member" )"2" "polynomial" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 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 )"FullMatrix" matrices "matrices/" )nil matrices "matrices/" )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices "matrices/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices "matrices/" )"nat" matrices "matrices/" )"bool" reals nil )"{c: nat | AND AND c = 0 OR " "matrices/" )nil matrices "matrices/" )"real" matrices "matrices/" )nil matrices "matrices/" )"real" matrices "matrices/" )"Vector" matrices "matrices/" )nil matrices "matrices/" )"VectorN(rows(M))" matrices "matrices/" )"{A: MatrixMN(rows(M), columns(N)) | " "matrices/" )"bool" reals nil )nil matrices "matrices/" )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" tarski_querynil )nil integers nil )nil integers nil )"boolean" notequal nil )"{v: PosFullMatrix | rows(v) = 3 AND columns(v) = 1}" tarski_querynil )"{v: PosFullMatrix | rows(v) = 6 AND columns(v) = 1}" tarski_querynil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_rat" nil )"rat" rationals nil )"int" integers nil )"posint" nil )"{A: MatrixMN(rows(M), columns(N)) | " "matrices/" )"{M: MatrixMN(m, n) | " "matrices/" )"real" matrices "matrices/" )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" "structures/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" matrices "matrices/" )"odd_int" integers nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"posrat" nil )"nzrat" rationalsnil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"FullMatrix" matrices"matrices/" )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"rat" rationals nil )"rat" rationals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nat" poly_families nil )nil compute_sturm_tarski nil )nil real_props nil )"nonneg_int" nil )nil tarski_query nil )nil tarski_query nil )"{d: nat | " sturmtarski nil) "finite_set[real]" tarski_query nil )"[real -> real]" polynomials "reals/" )"real" exponentiation nil )"real" exponentiation nil )"finite_set[real]" tarski_query nil )"finite_set[real]" tarski_query nil )"bool" sets nil )"bool" sets nil )"set" sets nil )"bool" sets nil )"finite_set" nil )nil finite_sets nil )"set" sets nil )"finite_set[real]" sturmtarski nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )"finite_set" finite_sets nil )nil tarski_query nil )"real" sigma "reals/" )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )nil sequences nil )"real" polynomials "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"(strict_total_order?[real])" real_props nil )nil matrices "matrices/" )nil matrices "matrices/" )NOT const-decl "[bool -> bool]" booleans nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.403 Sekunden
(vorverarbeitet am 2026-05-05)
¤ *© Formatika GbR, Deutschland
2026-05-26
