Quelle tarski_query_matrix.prf
Sprache: Lisp
(tarski_query_matrixnil 3620050327"" (skeep)"" (skosimp*)"" (replaces -1)"" (assert )"" (lemma "base_n_lt_n" )"" (lemma "columns_form_matrix" )"" (inst?)"" (assert )"" (lemma "base_n_lt_n" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"posint" nil )"posint" exponentiation nil )"(total_order?[real])" nil )nil matrices "matrices/" )"posint" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"(strict_total_order?[real])" real_props 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 )nil base_repr "reals/" ))nil ))nil 3621088362"" (skeep)"" (skeep)"" (rewrite "rows_form_matrix" )"" (lemma "columns_form_matrix" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil matrices "matrices/" )"FullMatrix" matrices"matrices/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR 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 )nil matrices "matrices/" )"posint" exponentiation nil )"posint" nil ))nil ))nil 3620494852"" (skeep)"" (skeep)"" (skeep)"" (case "x1<=k" )"1" (inst + "x1" )"1" (replace -2 +)"1" (assert ) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (assert )"2" (case "GPFun(i1,j1)(x1)=0" )"1" (assert ) nil nil )"2" (replaces -1)"2" (assert )"2" (assert )"2" (lemma "base_n_0" )"2" (inst?)"2" (assert )"2" (lemma "both_sides_expt_gt1_le_aux" )"2" (inst - "6" "k" "x1-1" )"2" expand "^" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals 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 )"posint" nil )"(total_order?[real])" nil )"posint" exponentiation nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"nat" tarski_query_matrix nil )"nat" tarski_query_matrix nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )nil base_repr "reals/" )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )nil real_types nil )"int" integers nil )"posnat" exponentiation nil )"real" exponentiation nil )nil exponentiation nil )"bool" reals nil ))nil ))nil 3620494852"" (skeep)"" (skeep)"" (rewrite "rows_form_matrix" )"" (assert )"" (lemma "columns_form_matrix" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"FullMatrix" matrices"matrices/" )"posint" nil )nil matrices "matrices/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR 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 )nil matrices "matrices/" )"posint" exponentiation nil )"posint" nil ))nil ))nil 3620051889"" (skosimp*)"" (lemma "base_n_lt_n" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil base_repr "reals/" )"(total_order?[real])" nil )"posint" nil )"posint" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals 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 )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621088362"" (skeep)"" (rewrite "rows_form_matrix" )"" (lemma "columns_form_matrix" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posint" nil )"posint" exponentiation nil )nil matrices "matrices/" )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"FullMatrix" matrices"matrices/" )nil matrices "matrices/" ))nil ))nil 3620139071"" (skosimp*)"" (lemma "base_n_lt_n" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil base_repr "reals/" )"(total_order?[real])" nil )"posint" nil )"posint" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals 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 )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621088362"" (skeep)"" (rewrite "rows_form_matrix" )"" (assert )"" (lemma "columns_form_matrix" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"posint" nil )"posint" exponentiation nil )nil matrices "matrices/" )nil numbers nil )nil booleans 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 )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil matrices "matrices/" )"posint" nil )"FullMatrix" matrices"matrices/" ))nil ))nil 3620408236 ("" (grind) nil nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"boolean" list_adt nil ))nil ))nil 3620408236 ("" (grind) nil nil )"odd_int" integers nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"boolean" list_adt nil ))nil ))nil 3620408236 ("" (eval-formula) nil nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil ))nil 3621152270"" (skeep) (("" (eval-formula) nil nil )) nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil ))nil ))nil 3621152270 ("" (grind) nil nil )"odd_int" integers nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"boolean" list_adt nil ))nil ))nil 3621152270 ("" (grind) nil nil )"posrat" nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"nzrat" rationalsnil )"odd_int" integers nil )"boolean" list_adt nil ))nil ))nil 3621152270 ("" (eval-formula) nil nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil ))nil 3620495242"" (skeep)"" (case "2<3^(1+k) AND 3^(1+k)<6^(1+k)" )"1" (label "2lem" -1)"1" (hide "2lem" )"1" (rewrite "full_matrix_eq" +)"1" (invoke (case "NOT %1" ) (! 2 1))"1" (hide 3)"1" (rewrite "rows_mult" )"1" (assert )"1" (lemma "tensor_power_rows_alt" )"1" (inst?)"1" (replaces -1 :dir rl)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (invoke (case "NOT %1" ) (! 2 1))"1" (hide (-1 3))"1" (rewrite "columns_mult" )"1" (assert ) nil nil )"2" (lemma "tensor_power_rows_alt" )"2" (inst?)"2" (expand "rows" -1 2)"2" (expand "length" -1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (skeep)"2" (typepred "j" )"2" (typepred "i" )"2" (case "NOT i < 6^(k+1)" )"1" (assert ) nil nil )"2" (case "NOT j = 0" )"1" (assert ) nil nil )"2" replace -1)"2" assert )"2" rewrite "entry_mult" )"2" assert )"2" "tensor_power_rows_alt" )"2" "2" assert )"2" "dot_eq_sigma" )"2" expand "*" + 1)"2" rewrite -1 +)"2" expand "TQ_vect6k" "2" rewrite "entry_form_matrix" )"1" case "EXISTS (p: upto(k)): base_n(6, i)(p) > 2" )"1" replace -1)"1" rewrite "length_row" "1" rewrite "length_col" "1" assert )"1" "tensor_power_columns_alt" )"1" "1" assert )"1" replace "1" expand "min" "1" case "NOT columns(A66_inv) = 6" )"1" assert )nil nil )"2" replace "2" assert )"2" "mult_tarski_query_simple_6_above_2" )"2" "GF" "KF" "base_n(6,i)" "a" "k" "n" )"1" assert )"1" replace "1" replace "1" case "%1 = %2" )"1" assert )nil nil )"2" "2" rewrite "sigma_eq" )"1" "1" "1" case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIES a1*a2 = b1*b2" )"1" rewrite "1" "1" rewrite "access_row" )"1" "tensor_entry" )"1" "1" assert )"1" "1" expand "sign_coeff6_zero" )"1" rewrite "product_eq" )"1" "1" "1" case "NOT rows(A66_inv)=6" )"1" assert )nil nil )"2" replace "2" assert )"2" replace "2" expand "entry_pick" "2" case "NOT FORALL (ii1,jj2:upto(5)): IF ii1 = 0 IF jj2 >= 3 THEN 0 ELSE 1 ENDIF)IF jj2 = 1 THEN 1IF 1 <= jj2 AND jj2 <= 2IF 1 <= jj2 AND jj2 <= 2IF jj2 <= 1 THEN -1IF jj2 = 0 OR jj2 = 2 THEN -1") "1" "1" nil nil ))nil )"2" expand "sign_coeff6_zero_entry" "2" "base_n(6,i)(n!2)" "base_n(6,n!1)(n!2)" )"1" assert )"1" "1" "base_n_lt_n" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "access_col" )"2" expand "NSol_vect6k" "2" rewrite "entry_form_matrix" )"2" "2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" "3" "base_n_lt_n" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "base_n_lt_n" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" "base_n_lt_n" )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tensor_power_rows_alt" )"2" "2" expand "rows" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "mult_tarski_query_simple_6_0_to_3" )"2" "GF" "base_n(6,i)" "KF" "a" "k" "n" )"2" assert )"2" replace "2" replace "2" rewrite "length_row" "1" rewrite "length_col" "1" assert )"1" "tensor_power_columns_alt" )"1" "1" assert )"1" replace "1" expand "min" "1" case "NOT columns(A66_inv) = 6" )"1" assert )nil nil )"2" replace "2" assert )"2" rewrite "sigma_eq" )"2" "2" "2" expand "sign_prod_coeff6" "2" case "EXISTS (p: upto(k)): base_n(6, n!1)(p) >= 3" )"1" replace "1" case "access(row(tensor_power_alt(A66_inv, 1 + k))(i))(n!1) = 0" )"1" replace "1" assert )nil nil ))nil )"2" "2" rewrite "access_row" )"2" "tensor_entry" )"2" "2" assert )"2" "2" expand "sign_prod_coeff6" )"2" case "NOT rows(A66_inv)=6" )"1" assert )nil nil )"2" replace "2" replace "2" assert )"2" "product_eq_zero[nat]" )"2" "2" assert )"2" "2" "2" "p" )"2" expand "entry_pick" "2" case "FORALL (ii1,ii2:upto(5)): ii1<=2 AND ii2>=3 IMPLIES entry(A66_inv)(ii1,ii2)=0" )"1" "p" )"1" "base_n(6,i)(p)" "base_n(6,n!1)(p)" )"1" assert )nil nil )"2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "base_n_lt_n" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )"2" replace "2" case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIES a1*a2 = b1*b2" )"1" rewrite "1" "1" rewrite "access_row" )"1" "tensor_entry" )"1" "1" assert )"1" "1" case "NOT rows(A66_inv)=6" )"1" assert )nil nil )"2" replace "2" replace "2" assert )"2" expand "sign_prod" "2" rewrite "product_eq" )"1" "1" "1" "1" expand "entry_pick" "1" "n!2" )"1" "n!2" )"1" assert )"1" expand "sig_seq" )"1" case "FORALL (ii1,ii2:upto(2)): entry(A66_inv)(ii1,ii2) = sig(ii2)^ii1" )"1" "base_n(6,i)(n!2)" "base_n(6,n!1)(n!2)" )"1" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" "x1" )"1" assert )nil nil )"2" assert )"2" "upper_is_bound" )"2" "2" assert )"2" "1" assert )nil nil )"2" expand "upper_index" )"2" "2" "2" "log_nat_bounds" )"2" "2" assert )"2" "2" case "log_nat(n!1,6)`1<=k" )"1" assert )nil nil )"2" "both_sides_expt_gt1_le_aux" )"2" "6" "k" "log_nat(n!1,6)`1-1" )"2" "n!1" )"2" expand "^" )"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 )"2" "2" rewrite "access_col" )"2" expand "NSol_vect6k" "2" rewrite "entry_form_matrix" )"1" expand "NSol_seq6" "1" replace "1" expand "NSol_all" )"1" expand "NSol" )"1" case "Sol(k, a, n, GF, KF, sig_seq(base_n(6, n!1))) = ") "1" assert )nil nil )"2" "2" "2" "2" expand "Sol" "2" expand "Sol_all" "2" "1" "1" "i!1" )"1" "i!1" )"1" assert )"1" expand "sig_seq" )"1" expand "sig" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" expand "sig_seq" )"2" expand "sig" )"2" "2" assert )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"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 "rows" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"2" "6" "i!1" "x1!1" )"2" assert )"2" "x1!1" )"1" assert )nil nil )"2" assert )"2" "upper_is_bound" )"2" "2" assert )"2" expand "upper_index" )"2" "2" "2" case "log_nat(i!1,6)`1<=k" )"1" assert )nil nil )"2" case "NOT i!1 <=expt(6,1+k)-1" )"1" assert )"1" expand "^" "1" assert )"1" case "NOT FORALL (i1,i2:int): i1<i2 IMPLIES i1<=i2-1" )"1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "log_nat_bounds" )"2" "2" assert )"2" "2" expand "^" )"2" assert )"2" "both_sides_expt_gt1_le_aux" )"2" "6" "k" "log_nat(i!1,6)`1-1" )"2" "i!1" )"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 )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" case "FORALL (dd:nat): 2 < 3 ^ (1 + dd) AND 3 ^ (1 + dd) < 6 ^ (1 + dd)" )"1" (inst - "k" ) nil nil )"2" (hide 2)"2" (induct "dd" )"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (skeep)"3" (expand "^" )"3" (expand "expt" +) (("3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"bool" reals nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrices "matrices/" )nil tensor_product "matrices/" )"nat" exponentiation nil )nil matrices "matrices/" )nil matrices "matrices/" )"{k: int | k <= i AND k <= j}" nil )"int" integers nil )"real" reals nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )"int" poly_families nil )nil integers nil )"nat" base_repr "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil matrices "matrices/" )"FullMatrix" matrices"matrices/" )"(total_order?[real])" nil )"subrange(-1, 1)" poly_families nil )"subrange(-1, 1)" poly_families nil )"int" exponentiation nil )"subrange(-1, 1)" poly_families nil )"nat" tarski_query_matrix nil )nil base_repr "reals/" )"nat" base_repr "reals/" )nil integers nil )nil exponentiation nil )"posnat" exponentiation nil )"int" exponentiation nil )"int" integers nil )nil real_types nil )nil real_types nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat"reals/" )nil log_nat "reals/" )"nat" poly_families nil )"nat" tarski_query_matrix nil )"finite_set[real]" poly_families nil )"finite_set[real]" poly_families nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )"upto(k)" tarski_query_matrix nil )"subrange(0, 6 ^ (1 + k) - 1)" nil )nil product "reals/" )"nonneg_int" nil )"even_int" integersnil )"subrange(-1, 1)" poly_families nil )"nat" poly_families nil )nil poly_familiesnil )nil matrices "matrices/" )nil tensor_product"matrices/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil poly_familiesnil )"(divides(m))" divides nil )"(divides(n))" divides nil )"odd_int" integers nil )nil matrices "matrices/" )nil tensor_product "matrices/" )nil base_repr "reals/" )"subrange(0, 6 ^ (1 + k) - 1)" nil )"subrange(0, k)" tarski_query_matrix nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil product "reals/" )"subrange(-1, 1)" poly_familiesnil )"real" tensor_product "matrices/" )nil product "reals/" )nil product "reals/" )nil matrices "matrices/" )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"subrange(-1, 1)" poly_families nil )"nat" poly_families nil )"real" matrices "matrices/" )"below(rows(TQ_vect6k(k, a, n, GF, KF)))" nil )"[nat -> nat]" tarski_query_matrix nil )"[nat -> [nat -> int]]" tarski_query_matrixnil )"posnat" tarski_query_matrix nil )"[nat -> int]" tarski_query_matrix nil )"nat" tarski_query_matrix nil )nil matrices "matrices/" )"nat" tarski_query_matrix nil )"nat" exponentiation nil )"real" exponentiation nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )nil matrices "matrices/" )"posint" exponentiation nil )"(strict_total_order?[real])" real_props nil )"{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" nil )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6}" nil )"PosFullMatrix" tensor_product"matrices/" )"{A: MatrixMN(rows(M), columns(N)) | " "matrices/" )"VectorN(rows(M))" matrices "matrices/" )nil matrices "matrices/" )"Vector" matrices "matrices/" )"real" matrices "matrices/" )nil matrices "matrices/" )"real" matrices "matrices/" )nil matrices "matrices/" )"{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" nil )nil matrices "matrices/" )"{c: nat | AND AND c = 0 OR " "matrices/" )"nat" matrices "matrices/" )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil matrices "matrices/" )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"[list -> boolean]" list_adt nil )nil matrices "matrices/" )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil matrices "matrices/" )"FullMatrix" matrices "matrices/" )"posint" nil )nil defined_types nil )nil naturalnumbers nil )"odd_int" integers nil )"posrat" nil )"posint" nil ))nil ))nil 3621152436"" (skeep)"" (lemma "multi_sturm_tarski_6by6" )"" (inst?)"" (assert )"" (replace -2)"" case "NOT tensor_power_alt(A66, 1 + k)*TQ_vect6k(k, a, n, GF, KF) = ))") "1" (assert ) nil nil )"2" (rewrite "matrix_mult_assoc" :dir rl)"1" (rewrite "power_assoc" :dir rl)"1" (rewrite "power_assoc" :dir rl)"1" (lemma "invertible_tensor_power" )"1" (inst - "A66_inv" "1+k" )"1" (split -)"1" (flatten)"1" (typepred "A66" )"1" replace -7 :dir rl)"1" replace -9 :dir rl)"1" rewrite "mult_inverse_left" )"1" rewrite "mult_Id_left" )"1" (assert ) nil nil )"2" "tensor_power_rows" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "invertible?" )"2" (inst + "A66" )"2" "2" (eval-formula) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but -1)"2" (lemma "tensor_power_rows_alt" )"2" (inst?)"2" (assert )"2" (expand "rows" -1 2)"2" (expand "length" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil tarski_query_matrix nil )"posint" nil )"FullMatrix" matrices "matrices/" )"{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" nil )"{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" nil )"real" exponentiation nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6 AND M = inverse(A66_inv)}" nil )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6}" nil )"{IQ | AND AND SQ * IQ = Id(rows(SQ))}" "matrices/" )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " "matrices/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil matrices "matrices/" )"bool" matrix_inv "matrices/" )"real" matrix_props "matrices/" )"boolean" notequal nil )nil matrices "matrices/" )"PosFullMatrix" tensor_product"matrices/" )nil matrices "matrices/" )nil matrices "matrices/" )"{A: MatrixMN(rows(M), columns(N)) | " "matrices/" )"VectorN(rows(M))" matrices "matrices/" )nil matrices "matrices/" )"Vector" matrices "matrices/" )"real" matrices "matrices/" )nil matrices "matrices/" )"real" matrices "matrices/" )nil matrices "matrices/" )"{c: nat | AND AND c = 0 OR " "matrices/" )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (nth def-decl "T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )"nat" matrices "matrices/" )"nat" list_props nil )nil matrices "matrices/" )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )nil tensor_product "matrices/" )nil tensor_product "matrices/" )nil tensor_product"matrices/" )nil matrices "matrices/" )"(strict_total_order?[real])" real_props nil )"nat" exponentiation nil )nil tensor_product "matrices/" )nil matrix_inv "matrices/" )"PosFullMatrix" tensor_product "matrices/" )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil matrices "matrices/" )nil integers nil )"bool" reals nil )nil integers 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 ))nil 3621167024"" (skeep)"" (split)"1" (eval-formula) nil nil )"2" (flatten) (("2" (eval-formula -1) nil nil )) nil ))nil ))nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil ))nil 3621167024 ("" (eval-formula) nil nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil ))nil 3621167024 ("" (eval-formula) nil nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil ))nil 3621167232 ("" (eval-formula) nil nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil 3621168373"" (skeep)"" (lemma "multi_sturm_tarski_NSol" )"" (inst?)"" (assert )"" (replace -2)"" (replaces -1)"" (rewrite "full_matrix_eq" )"" (invoke (case "NOT %1" ) (! 2 1))"1" (hide 3)"1" (rewrite "rows_mult" )"1" (rewrite "rows_mult" )"1" (assert )"1" (lemma "tensor_power_rows_alt" )"1" (inst?)"1" "1" "tensor_power_rows_alt" )"1" "A63" "1+k" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (invoke (case "NOT %1" ) (! 2 1))"1" (hide 3)"1" (lemma "columns_mult" )"1" (inst?)"1" (assert )"1" "1" replace -1)"1" "1" "columns_mult" )"1" "1" "1" "1" (assert ) nil nil ))nil )"2" "tensor_power_rows_alt" )"2" "2" expand "rows" -1 2)"2" expand "length" -1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tensor_power_rows_alt" )"2" "2" expand "rows" -1 2)"2" expand "length" -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skeep)"2" (typepred "i" )"2" case "NOT rows(tensor_power_alt(A66, 1 + k) * TQ_vect6k(k, a, n, GF, KF)) = 6^(1+k)" )"1" assert )"1" rewrite "rows_mult" )"1" "tensor_power_rows_alt" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "j" )"2" case "NOT columns(tensor_power_alt(A66, 1 + k) * TQ_vect6k(k, a, n, GF, KF)) = 1" )"1" "columns_mult" )"1" "1" assert )"1" "tensor_power_rows_alt" )"1" "1" expand "rows" -1 2)"1" expand "length" -1)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT j = 0" )"1" (assert ) nil nil )"2" replace -1)"2" assert )"2" rewrite "entry_mult" )"2" rewrite "entry_mult" )"2" assert )"2" "tensor_power_rows_alt" )"2" "A66" "1+k" )"2" "tensor_power_rows_alt" )"2" "A63" "1+k" )"2" assert )"2" "dot_eq_sigma" )"2" expand "*" "2" rewrite "2" rewrite "2" rewrite "length_row" )"1" rewrite "length_row" )"1" rewrite "length_col" )"1" rewrite "length_col" )"1" "tensor_power_columns_alt" )"1" "A63" "1+k" )"1" "tensor_power_columns_alt" )"1" "A66" "1+k" )"1" assert )"1" replace "1" replace "1" expand "min" "1" case "NOT columns(A66) = 6" )"1" assert )nil nil )"2" replace "2" case "NOT columns(A63) = 3" )"1" assert )nil nil )"2" replace "2" assert )"2" "siggy" "LAMBDA (i:nat): base_n_to_nat(6,base_n(3,i),k)" )"2" "F" "%1" )"2" "2" "G" "%1" )"2" "2" "sigma_inj" )"2" "F" "G" "3^(1+k)-1" "6^(1+k)-1" "0" "0" "siggy" )"2" assert )"2" "2" "1" "1" expand "siggy" "1" assert )"1" "1" assert )nil nil )"2" "base_n_to_nat_lt" )"2" "2" assert )"2" "1" assert )"1" case "FORALL (i1,i2:int): i1<i2 IMPLIES i1<=i2-1" )"1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "siggy" "2" "base_n_to_nat_unique" )"2" "2" assert )"2" "k" )"2" "1" "base_n_is_n_alt" )"1" "3" "i!1" "k" )"1" "base_n_is_n_alt" )"1" "3" "j!1" "k" )"1" assert )"1" "1" "1" "base_n_to_nat_eq" )"1" "1" assert )"1" "k" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"2" "2" assert )"2" "base_n_lt_n" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "G" "3" case "access(col(TQ_vect6k(k, a, n, GF, KF))(0))(i!1) = 0" )"1" assert )nil nil )"2" "2" rewrite "access_col" )"2" expand "TQ_vect6k" "2" rewrite "entry_form_matrix" )"1" "1" "1" "jj" "base_n_to_nat(3,base_n(6,i!1),k)" )"1" "jj" )"1" expand "siggy" "1" expand "jj" "1" "base_n_base_n_to_nat" )"1" "1" assert )"1" "1" "base_n_to_nat_eq" )"1" "6" "k" "k" "base_n(3, base_n_to_nat(3, base_n(6, i!1), k))" "base_n(6,i!1)" )"1" replace "1" "1" "base_n_is_n_alt" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "jj" "2" "base_n_to_nat_lt" )"2" "2" assert )"2" "1" case "FORALL (i1,i2:int): i1<i2 IMPLIES i1<=i2-1" )"1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" "i!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" assert )"2" "x1!1" )"1" assert )nil nil )"2" assert )"2" "base_n_0" )"2" "2" assert )"2" "both_sides_expt_gt1_le_aux" )"2" "6" "k" "x1!1-1" )"2" assert )"2" expand "^" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "F" "4" expand "G" "4" rewrite "access_row" )"4" rewrite "access_row" )"4" rewrite "access_col" )"4" rewrite "access_col" )"4" case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIES a1*a2=b1*b2" )"1" rewrite "1" "1" "tensor_entry_alt" )"1" "1" assert )"1" "1" "tensor_entry_alt" )"1" "1" assert )"1" "1" rewrite "product_eq" )"1" "1" "1" case "NOT rows(A66)=6" )"1" assert )nil nil )"2" replace "2" replace "2" replace "2" case "NOT rows(A63) = 6" )"1" assert )nil nil )"2" replace "2" assert )"2" expand "entry_pick" "2" case "base_n(6, siggy(i!1)) = base_n(3, i!1)" )"1" "1" rewrite "A63_def" "1" "base_n_lt_n" )"1" "1" assert )nil nil ))nil ))nil )"2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "siggy" "2" "base_n_base_n_to_nat" )"2" "2" "1" "1" case "x!1<=k" )"1" "x!1" )nil nil )"2" assert )"2" "base_n_0" )"2" "2" assert )"2" "1" "base_n_0" )"1" replace "1" "3" "i!1" "x!1" )"1" assert )"1" "i!1" )"1" "both_sides_expt_gt1_le_aux" )"1" "3" "k" "x!1-1" )"1" expand "^" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "base_n_to_nat_lt" )"2" "2" assert )"2" "1" "both_sides_expt_gt1_le_aux" )"1" "6" "k" "x!1-1" )"1" expand "^" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "base_n_lt_n" )"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 )"2" "2" expand "siggy" "2" "base_n_to_nat_lt" )"2" "2" assert )"2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "TQ_vect6k" "2" expand "TQ_vect3k" "2" rewrite "entry_form_matrix" )"1" rewrite "entry_form_matrix" )"1" assert )"1" "1" "1" "1" "1" "1" "1" expand "siggy" "1" "base_n_base_n_to_nat" )"1" "1" "1" rewrite "1" "base_n_lt_n" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "base_n(3, i!1)=base_n(6, siggy(i!1))" )"1" assert )nil nil )"2" "2" "2" expand "siggy" "2" "base_n_base_n_to_nat" )"2" "2" "1" "1" case "x!1<=k" )"1" rewrite nil nil )"2" "base_n_0" )"2" "2" assert )"2" "1" replace "1" "base_n_0" )"1" "6" "1" "1" assert )"1" "base_n_to_nat_lt" )"1" "1" assert )"1" "1" "both_sides_expt_gt1_le_aux" )"1" "6" "k" "x!1-1" )"1" expand "^" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "both_sides_expt_gt1_le_aux" )"2" "3" "k" "x!1-1" )"2" expand "^" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "siggy" "2" "base_n_to_nat_lt" )"2" "2" assert )"2" "2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" assert )"2" "base_n_lt_n" )"2" "2" assert )"2" "x1!1" )"1" assert )nil nil )"2" assert )"2" "base_n_0" )"2" "2" assert )"2" "both_sides_expt_gt1_le_aux" )"2" "6" "k" "x1!1-1" )"2" expand "^" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" assert )"2" "base_n_lt_n" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )"2" "2" "tensor_power_rows_alt" )"2" "2" expand "rows" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "rows" "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 tarski_query_matrix nil )"posint" nil )"FullMatrix" matrices "matrices/" )NOT const-decl "[bool -> bool]" booleans nil )nil matrices "matrices/" )"nat" exponentiation nil )nil tensor_product "matrices/" )nil matrices "matrices/" )"posint" exponentiation nil )"(strict_total_order?[real])" real_props nil )nil matrices "matrices/" )nil matrices "matrices/" )"{k: int | k <= i AND k <= j}" nil )"int" integers nil )"real" reals nil )"(total_order?[real])" nil )nil matrices "matrices/" )nil matrices "matrices/" )nil tensor_product"matrices/" )"real" matrices "matrices/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma_nat "reals/" )"[nat -> nat]" tarski_query_matrix nil )"(total_order?[real])" nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil base_repr "reals/" )nil base_repr "reals/" )"(strict_total_order?[real])" real_props nil )nil base_repr "reals/" )nil base_repr "reals/" )nil base_repr "reals/" )"[nat -> real]" tarski_query_matrix nil )"nat" tarski_query_matrix nil )nil base_repr "reals/" )nil real_types nil )nil real_types nil )"posnat" exponentiation nil )"int" integers nil )nil exponentiation nil )"nat" tarski_query_matrix nil )nil base_repr "reals/" )"nat" tarski_query_matrix nil )"nat" tarski_query_matrix nil )"FullMatrix" matrices"matrices/" )nil matrices "matrices/" )"int" poly_families nil )nil matrices "matrices/" )"[nat -> real]" tarski_query_matrix nil )nil matrices "matrices/" )"nat" exponentiation nil )"nat" tarski_query_matrix nil )"nat" tarski_query_matrix nil )"subrange(0, 3 ^ (1 + k) - 1)" nil )nil tarski_query_matrix nil )"nat" tarski_query_matrix nil )nil product "reals/" )"real" tensor_product "matrices/" )nil product "reals/" )nil product "reals/" )nil tensor_product "matrices/" )"[numfield, numfield -> numfield]" number_fields nil )"nat" base_repr "reals/" )"nat" base_repr "reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"{v: PosFullMatrix | rows(v) = 3 ^ (k + 1) AND columns(v) = 1}" nil )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" nil )"{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" nil )"real" exponentiation nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6 AND M = inverse(A66_inv)}" nil )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6}" nil )"{IQ | AND AND SQ * IQ = Id(rows(SQ))}" "matrices/" )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " "matrices/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil matrices "matrices/" )"bool" matrix_inv "matrices/" )"real" matrix_props "matrices/" )"boolean" notequal nil )nil matrices "matrices/" )"PosFullMatrix" tensor_product"matrices/" )nil matrices "matrices/" )"{A: MatrixMN(rows(M), columns(N)) | " "matrices/" )"VectorN(rows(M))" matrices "matrices/" )nil matrices "matrices/" )"Vector" matrices "matrices/" )"real" matrices "matrices/" )nil matrices "matrices/" )"real" matrices "matrices/" )nil matrices "matrices/" )"{c: nat | AND AND c = 0 OR " "matrices/" )"bool" reals nil )"nat" matrices "matrices/" )nil matrices "matrices/" )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices "matrices/" )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil matrices "matrices/" )"posint" nil )nil integers nil )"bool" reals nil )nil integers 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 ))nil )nil 3621167258"" (skeep)"" (lemma "multi_sturm_tarski_NSol" )"" (inst?)"" (assert )"" (replace -2)"" (replaces -1)"" (rewrite "full_matrix_eq" )"" (invoke (case "NOT %1" ) (! 2 1))"1" (hide 3)"1" (rewrite "rows_mult" )"1" (rewrite "rows_mult" )"1" (assert )"1" (lemma "tensor_power_rows_alt" )"1" (inst?)"1" "1" "tensor_power_rows_alt" )"1" "A63" "1+k" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (invoke (case "NOT %1" ) (! 2 1))"1" (hide 3)"1" (lemma "columns_mult" )"1" (inst?)"1" (assert )"1" "1" replace -1)"1" "1" "columns_mult" )"1" "1" "1" "1" (assert ) nil nil ))nil )"2" "tensor_power_rows_alt" )"2" "2" expand "rows" -1 2)"2" expand "length" -1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tensor_power_rows_alt" )"2" "2" expand "rows" -1 2)"2" expand "length" -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skeep)"2" (typepred "i" )"2" case "NOT rows(tensor_power_alt(A66, 1 + k) * TQ_vect6k(k, a, n, GF, KF)) = 6^(1+k)" )"1" assert )"1" rewrite "rows_mult" )"1" "tensor_power_rows_alt" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "j" )"2" case "NOT columns(tensor_power_alt(A66, 1 + k) * TQ_vect6k(k, a, n, GF, KF)) = 1" )"1" "columns_mult" )"1" "1" assert )"1" "tensor_power_rows_alt" )"1" "1" expand "rows" -1 2)"1" expand "length" -1)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT j = 0" )"1" (assert ) nil nil )"2" replace -1)"2" assert )"2" rewrite "entry_mult" )"2" rewrite "entry_mult" )"2" assert )"2" "tensor_power_rows_alt" )"2" "A66" "1+k" )"2" "tensor_power_rows_alt" )"2" "A63" "1+k" )"2" assert )"2" "dot_eq_sigma" )"2" expand "*" "2" rewrite "2" rewrite "2" rewrite "length_row" )"1" rewrite "length_row" )"1" rewrite "length_col" )"1" rewrite "length_col" )"1" "tensor_power_columns_alt" )"1" "A63" "1+k" )"1" "tensor_power_columns_alt" )"1" "A66" "1+k" )"1" assert )"1" replace "1" replace "1" expand "min" "1" case "NOT columns(A66) = 6" )"1" assert )nil nil )"2" replace "2" case "NOT columns(A63) = 3" )"1" assert )nil nil )"2" replace "2" assert )"2" "siggy" "LAMBDA (i:nat): base_n_to_nat(6,base_n(3,i),k+1)" )"2" "F" "%1" )"2" "2" "G" "%1" )"2" "2" "sigma_inj" )"2" "F" "G" "3^(1+k)-1" "6^(1+k)-1" "0" "0" "siggy" )"2" assert )"2" "2" "1" "1" expand "siggy" "1" assert )"1" "1" assert )nil nil )"2" "base_n_to_nat_lt" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" nil nil ))nil ))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 )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak)))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.387Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
