|
(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]): /=(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)
((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
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.102Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
