| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Tarski/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 436 kB |
|
Quelle tarski_query_matrix.prfSprache: Lisp |
|||||||||||||||
|
(tarski_query_matrix (TQ_vect3k_TCC1 0 (TQ_vect3k_TCC1-1 nil 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) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (columns_form_matrix formula-decl nil matrices "matrices/") (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) (> const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (base_n_lt_n formula-decl nil base_repr "reals/")) nil)) (TQ_vect3k_TCC2 0 (TQ_vect3k_TCC2-1 nil 3621088362 ("" (skeep) (("" (skeep) (("" (rewrite "rows_form_matrix") (("" (lemma "columns_form_matrix") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((columns_form_matrix formula-decl nil matrices "matrices/") (form_matrix_square application-judgement "FullMatrix" matrices "matrices/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR 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) (rows_form_matrix formula-decl nil matrices "matrices/") (posint_exp application-judgement "posint" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (TQ_vect6k_TCC1 0 (TQ_vect6k_TCC1-1 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) ((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) (<= const-decl "bool" reals 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_exp application-judgement "posint" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (x1 skolem-const-decl "nat" tarski_query_matrix nil) (k skolem-const-decl "nat" tarski_query_matrix nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (base_n_0 formula-decl nil base_repr "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (posnat_expt application-judgement "posnat" exponentiation nil) (^ const-decl "real" exponentiation nil) (both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil) (> const-decl "bool" reals nil)) nil)) (TQ_vect6k_TCC2 0 (TQ_vect6k_TCC2-1 nil 3620494852 ("" (skeep) (("" (skeep) (("" (rewrite "rows_form_matrix") (("" (assert) (("" (lemma "columns_form_matrix") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((form_matrix_square application-judgement "FullMatrix" matrices "matrices/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (columns_form_matrix formula-decl nil matrices "matrices/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR 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) (rows_form_matrix formula-decl nil matrices "matrices/") (posint_exp application-judgement "posint" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (NSol_vect3k_TCC1 0 (NSol_vect3k_TCC1-1 nil 3620051889 ("" (skosimp*) (("" (lemma "base_n_lt_n") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((base_n_lt_n formula-decl nil base_repr "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (NSol_vect3k_TCC2 0 (NSol_vect3k_TCC2-1 nil 3621088362 ("" (skeep) (("" (rewrite "rows_form_matrix") (("" (lemma "columns_form_matrix") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (rows_form_matrix formula-decl nil matrices "matrices/") (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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (form_matrix_square application-judgement "FullMatrix" matrices "matrices/") (columns_form_matrix formula-decl nil matrices "matrices/")) nil)) (NSol_vect6k_TCC1 0 (NSol_vect6k_TCC1-1 nil 3620139071 ("" (skosimp*) (("" (lemma "base_n_lt_n") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((base_n_lt_n formula-decl nil base_repr "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (NSol_vect6k_TCC2 0 (NSol_vect6k_TCC2-1 nil 3621088362 ("" (skeep) (("" (rewrite "rows_form_matrix") (("" (assert) (("" (lemma "columns_form_matrix") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (rows_form_matrix formula-decl nil matrices "matrices/") (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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (columns_form_matrix formula-decl nil matrices "matrices/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (form_matrix_square application-judgement "FullMatrix" matrices "matrices/")) nil)) (A66_inv_TCC1 0 (A66_inv_TCC1-1 nil 3620408236 ("" (grind) nil nil) ((listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (every adt-def-decl "boolean" list_adt nil)) nil)) (A66_inv_TCC2 0 (A66_inv_TCC2-1 nil 3620408236 ("" (grind) nil nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (every adt-def-decl "boolean" list_adt nil)) nil)) (A66_inv_TCC3 0 (A66_inv_TCC3-1 nil 3620408236 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (A66_TCC1 0 (A66_TCC1-1 nil 3621152270 ("" (skeep) (("" (eval-formula) nil nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil)) nil)) (A66_TCC2 0 (A66_TCC2-1 nil 3621152270 ("" (grind) nil nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (every adt-def-decl "boolean" list_adt nil)) nil)) (A66_TCC3 0 (A66_TCC3-1 nil 3621152270 ("" (grind) nil 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/") (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)) (A66_TCC4 0 (A66_TCC4-1 nil 3621152270 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (multi_sturm_tarski_6by6 0 (multi_sturm_tarski_6by6-1 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" (lemma "tensor_power_rows_alt") (("2" (inst?) (("2" (assert) (("2" (lemma "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" (lemma "tensor_power_columns_alt") (("1" (inst?) (("1" (assert) (("1" (replace -1 :dir rl) (("1" (expand "min" +) (("1" (case "NOT columns(A66_inv) = 6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (lemma "mult_tarski_query_simple_6_above_2") (("2" (inst - "GF" "KF" "base_n(6,i)" "a" "k" "n") (("1" (assert) (("1" (replace -4) (("1" (replace -13) (("1" (invoke (case "%1 = %2") (! -1 1) (! 2 2)) (("1" (assert) nil nil) ("2" (hide (-1 3)) (("2" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIES a1*a2 = b1*b2") (("1" (rewrite -1 1) (("1" (hide 2) (("1" (rewrite "access_row") (("1" (lemma "tensor_entry") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (expand "sign_coeff6_zero") (("1" (rewrite "product_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (case "NOT rows(A66_inv)=6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (replace -3) (("2" (expand "entry_pick" +) (("2" (case "NOT FORALL (ii1,jj2:upto(5)): IF ii1 = 0 THEN (IF jj2 >= 3 THEN 0 ELSE 1 ENDIF) ELSIF ii1 = 1 THEN (IF jj2 = 1 THEN 1 ELSIF jj2 = 2 THEN -1 ELSE 0 ENDIF) ELSIF ii1 = 2 THEN (IF 1 <= jj2 AND jj2 <= 2 THEN 1 ELSE 0 ENDIF) ELSIF ii1 = 3 THEN (IF 1 <= jj2 AND jj2 <= 2 THEN -1 ELSIF jj2 = 3 THEN 1 ELSE 0 ENDIF) ELSIF ii1 = 4 THEN (IF jj2 <= 1 THEN -1 ELSIF jj2 = 4 THEN 1 ELSE 0 ENDIF) ELSIF ii1 = 5 THEN (IF jj2 = 0 OR jj2 = 2 THEN -1 ELSIF jj2 = 5 THEN 1 ELSE 0 ENDIF) ELSE 0 ENDIF = entry(A66_inv)(ii1, jj2)") (("1" (hide-all-but 1) (("1" (eval-formula) nil nil)) nil) ("2" (expand "sign_coeff6_zero_entry" +) (("2" (inst - "base_n(6,i)(n!2)" "base_n(6,n!1)(n!2)") (("1" (assert) (("1" (hide-all-but 1) (("1" (lemma "base_n_lt_n") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (skeep) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "access_col") (("2" (expand "NSol_vect6k" +) (("2" (rewrite "entry_form_matrix") (("2" (hide 2) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide-all-but 1) (("3" (skosimp*) (("3" (lemma "base_n_lt_n") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (lemma "base_n_lt_n") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (lemma "base_n_lt_n") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "tensor_power_rows_alt") (("2" (inst?) (("2" (expand "rows" -1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (lemma "mult_tarski_query_simple_6_0_to_3") (("2" (inst - "GF" "base_n(6,i)" "KF" "a" "k" "n") (("2" (assert) (("2" (replace -10) (("2" (replace -1 +) (("2" (rewrite "length_row" +) (("1" (rewrite "length_col" +) (("1" (assert) (("1" (lemma "tensor_power_columns_alt") (("1" (inst?) (("1" (assert) (("1" (replace -1 :dir rl) (("1" (expand "min" +) (("1" (case "NOT columns(A66_inv) = 6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (rewrite "sigma_eq") (("2" (hide 4) (("2" (skosimp*) (("2" (expand "sign_prod_coeff6" +) (("2" (case "EXISTS (p: upto(k)): base_n(6, n!1)(p) >= 3") (("1" (replace -1) (("1" (case "access(row(tensor_power_alt(A66_inv, 1 + k))(i))(n!1) = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (rewrite "access_row") (("2" (lemma "tensor_entry") (("2" (inst?) (("2" (assert) (("2" (replaces -1) (("2" (expand "sign_prod_coeff6") (("2" (case "NOT rows(A66_inv)=6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (replace -3) (("2" (assert) (("2" (lemma "product_eq_zero[nat]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (skeep -2) (("2" (inst + "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" (inst + "p") (("1" (inst - "base_n(6,i)(p)" "base_n(6,n!1)(p)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "base_n_lt_n") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (eval-formula) 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" (case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIES a1*a2 = b1*b2") (("1" (rewrite -1 2) (("1" (hide 3) (("1" (rewrite "access_row") (("1" (lemma "tensor_entry") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (case "NOT rows(A66_inv)=6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (replace -3) (("2" (assert) (("2" (expand "sign_prod" +) (("2" (rewrite "product_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (hide -) (("1" (expand "entry_pick" +) (("1" (inst + "n!2") (("1" (inst + "n!2") (("1" (assert) (("1" (expand "sig_seq") (("1" (case "FORALL (ii1,ii2:upto(2)): entry(A66_inv)(ii1,ii2) = sig(ii2)^ii1") (("1" (inst - "base_n(6,i)(n!2)" "base_n(6,n!1)(n!2)") (("1" (assert) nil nil)) nil) ("2" (eval-formula 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skeep) (("3" (inst + "x1") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "upper_is_bound") (("2" (inst?) (("2" (assert) (("2" (split -1) (("1" (assert) nil nil) ("2" (expand "upper_index") (("2" (lift-if) (("2" (ground) (("2" (lemma "log_nat_bounds") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (case "log_nat(n!1,6)`1<=k") (("1" (assert) nil nil) ("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "6" "k" "log_nat(n!1,6)`1-1") (("2" (typepred "n!1") (("2" (expand "^") (("2" (flatten) (("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" (hide 3) (("2" (rewrite "access_col") (("2" (expand "NSol_vect6k" +) (("2" (rewrite "entry_form_matrix") (("1" (expand "NSol_seq6" 1) (("1" (replace 2) (("1" (expand "NSol_all") (("1" (expand "NSol") (("1" (case "Sol(k, a, n, GF, KF, sig_seq(base_n(6, n!1))) = Sol_all(k, a, n, GF, KF, base_n(6, n!1))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (iff) (("2" (expand "Sol" 1) (("2" (expand "Sol_all" 1) (("2" (ground) (("1" (skosimp 1) (("1" (inst - "i!1") (("1" (inst + "i!1") (("1" (assert) (("1" (expand "sig_seq") (("1" (expand "sig") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i!1") (("2" (expand "sig_seq") (("2" (expand "sig") (("2" (lift-if) (("2" (assert) (("2" (inst + "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" (hide 2) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (expand "rows" -3 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst - "6" "i!1" "x1!1") (("2" (assert) (("2" (inst + "x1!1") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "upper_is_bound") (("2" (inst?) (("2" (assert) (("2" (expand "upper_index") (("2" (lift-if) (("2" (ground) (("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" (skeep) (("1" (assert) nil nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "log_nat_bounds") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (expand "^") (("2" (assert) (("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "6" "k" "log_nat(i!1,6)`1-1") (("2" (typepred "i!1") (("2" (flatten) (("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) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (>= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" 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) (< const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (rows_mult formula-decl nil matrices "matrices/") (tensor_power_rows_alt formula-decl nil tensor_product "matrices/") (nat_exp application-judgement "nat" exponentiation nil) (columns_mult formula-decl nil matrices "matrices/") (dot_eq_sigma formula-decl nil matrices "matrices/") (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (TQ_fam const-decl "int" poly_families nil) (subrange type-eq-decl nil integers nil) (base_n def-decl "nat" base_repr "reals/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (entry_form_matrix formula-decl nil matrices "matrices/") (form_matrix_square application-judgement "FullMatrix" matrices "matrices/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sig_seq const-decl "subrange(-1, 1)" poly_families nil) (sign_prod const-decl "subrange(-1, 1)" poly_families nil) (int_exp application-judgement "int" exponentiation nil) (sig const-decl "subrange(-1, 1)" poly_families nil) (x1 skolem-const-decl "nat" tarski_query_matrix nil) (upper_is_bound formula-decl nil base_repr "reals/") (upper_index const-decl "nat" base_repr "reals/") (above nonempty-type-eq-decl nil integers nil) (both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (int_expt application-judgement "int" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat "reals/") (log_nat_bounds formula-decl nil log_nat "reals/") (NSol const-decl "nat" poly_families nil) (i!1 skolem-const-decl "nat" tarski_query_matrix nil) (Sol_all const-decl "finite_set[real]" poly_families nil) (Sol const-decl "finite_set[real]" poly_families 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) (p skolem-const-decl "upto(k)" tarski_query_matrix nil) (n!1 skolem-const-decl "subrange(0, 6 ^ (1 + k) - 1)" tarski_query_matrix nil) (product_eq_zero formula-decl nil product "reals/") (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (sign_prod_coeff6 const-decl "subrange(-1, 1)" poly_families nil) (NSol_seq6 const-decl "nat" poly_families nil) (mult_tarski_query_simple_6_0_to_3 formula-decl nil poly_families nil) (length_col formula-decl nil matrices "matrices/") (tensor_power_columns_alt formula-decl nil tensor_product "matrices/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (mult_tarski_query_simple_6_above_2 formula-decl nil poly_families nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (access_col formula-decl nil matrices "matrices/") (tensor_entry formula-decl nil tensor_product "matrices/") (base_n_lt_n formula-decl nil base_repr "reals/") (n!1 skolem-const-decl "subrange(0, 6 ^ (1 + k) - 1)" tarski_query_matrix nil) (n!2 skolem-const-decl "subrange(0, k)" tarski_query_matrix nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (product_eq formula-decl nil product "reals/") (sign_coeff6_zero_entry const-decl "subrange(-1, 1)" poly_families nil) (entry_pick const-decl "real" tensor_product "matrices/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (access_row formula-decl nil matrices "matrices/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_eq formula-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sign_coeff6_zero const-decl "subrange(-1, 1)" poly_families nil) (NSol_all const-decl "nat" poly_families nil) (access const-decl "real" matrices "matrices/") (i skolem-const-decl "below(rows(TQ_vect6k(k, a, n, GF, KF)))" tarski_query_matrix nil) (KF skolem-const-decl "[nat -> nat]" tarski_query_matrix nil) (GF skolem-const-decl "[nat -> [nat -> int]]" tarski_query_matrix nil) (n skolem-const-decl "posnat" tarski_query_matrix nil) (a skolem-const-decl "[nat -> int]" tarski_query_matrix nil) (k skolem-const-decl "nat" tarski_query_matrix nil) (length_row formula-decl nil matrices "matrices/") (x1!1 skolem-const-decl "nat" tarski_query_matrix nil) (nat_expt application-judgement "nat" exponentiation nil) (expt def-decl "real" exponentiation nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (entry_mult formula-decl nil matrices "matrices/") (posint_exp application-judgement "posint" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NSol_vect6k const-decl "{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" tarski_query_matrix nil) (A66_inv const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6}" tarski_query_matrix nil) (tensor_power_alt def-decl "PosFullMatrix" tensor_product "matrices/") (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices "matrices/") (col def-decl "VectorN(rows(M))" matrices "matrices/") (VectorN type-eq-decl nil matrices "matrices/") (row const-decl "Vector" matrices "matrices/") (* const-decl "real" matrices "matrices/") (Vector type-eq-decl nil matrices "matrices/") (entry const-decl "real" matrices "matrices/") (MatrixMN type-eq-decl nil matrices "matrices/") (TQ_vect6k const-decl "{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" tarski_query_matrix nil) (PosFullMatrix type-eq-decl nil matrices "matrices/") (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices "matrices/") (rows const-decl "nat" matrices "matrices/") (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (FullMatrix type-eq-decl nil matrices "matrices/") (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Matrix type-eq-decl nil matrices "matrices/") (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (full_matrix_eq formula-decl nil matrices "matrices/") (mult_full application-judgement "FullMatrix" matrices "matrices/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) nil)) (multi_sturm_tarski_NSol 0 (multi_sturm_tarski_NSol-1 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) = tensor_power_alt(A66, 1 + k)*(tensor_power_alt(A66_inv, 1 + k) * NSol_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" (lemma "tensor_power_rows") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "invertible?") (("2" (inst + "A66") (("2" (hide-all-but 1) (("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) ((multi_sturm_tarski_6by6 formula-decl nil tarski_query_matrix nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (mult_full application-judgement "FullMatrix" matrices "matrices/") (NSol_vect6k const-decl "{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" tarski_query_matrix nil) (TQ_vect6k const-decl "{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" tarski_query_matrix nil) (^ const-decl "real" exponentiation nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (A66 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6 AND M = inverse(A66_inv)}" tarski_query_matrix nil) (A66_inv const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6}" tarski_query_matrix nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv "matrices/") (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices "matrices/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (SquareMatrix type-eq-decl nil matrices "matrices/") (invertible? const-decl "bool" matrix_inv "matrices/") (det def-decl "real" matrix_props "matrices/") (/= const-decl "boolean" notequal nil) (Square type-eq-decl nil matrices "matrices/") (tensor_power_alt def-decl "PosFullMatrix" tensor_product "matrices/") (PosFullMatrix type-eq-decl nil matrices "matrices/") (FullMatrix type-eq-decl nil matrices "matrices/") (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices "matrices/") (col def-decl "VectorN(rows(M))" matrices "matrices/") (VectorN type-eq-decl nil matrices "matrices/") (row const-decl "Vector" matrices "matrices/") (* const-decl "real" matrices "matrices/") (Vector type-eq-decl nil matrices "matrices/") (entry const-decl "real" matrices "matrices/") (MatrixMN type-eq-decl nil matrices "matrices/") (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices "matrices/") (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (rows const-decl "nat" matrices "matrices/") (length def-decl "nat" list_props nil) (Matrix type-eq-decl nil matrices "matrices/") (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (list type-decl nil list_adt nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (tensor_power_rows_alt formula-decl nil tensor_product "matrices/") (power_assoc formula-decl nil tensor_product "matrices/") (invertible_tensor_power formula-decl nil tensor_product "matrices/") (mult_Id_left formula-decl nil matrices "matrices/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_exp application-judgement "nat" exponentiation nil) (tensor_power_rows formula-decl nil tensor_product "matrices/") (mult_inverse_left formula-decl nil matrix_inv "matrices/") (tensor_power def-decl "PosFullMatrix" tensor_product "matrices/") (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (matrix_mult_assoc formula-decl nil matrices "matrices/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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)) shostak)) (A63_TCC1 0 (A63_TCC1-1 nil 3621167024 ("" (skeep) (("" (split) (("1" (eval-formula) nil nil) ("2" (flatten) (("2" (eval-formula -1) nil nil)) nil)) nil)) nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (A63_TCC2 0 (A63_TCC2-1 nil 3621167024 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (A63_TCC3 0 (A63_TCC3-1 nil 3621167024 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (A63_def 0 (A63_def-1 nil 3621167232 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (multi_sturm_tarski_NSol63 0 (multi_sturm_tarski_NSol63-2 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" (replaces -1 :dir rl) (("1" (lemma "tensor_power_rows_alt") (("1" (inst - "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" (split -) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "columns_mult") (("1" (inst?) (("1" (split -) (("1" (replaces -1) (("1" (assert) nil 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)) nil)) 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)) 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" (lemma "tensor_power_rows_alt") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "j") (("2" (case "NOT columns(tensor_power_alt(A66, 1 + k) * TQ_vect6k(k, a, n, GF, KF)) = 1") (("1" (lemma "columns_mult") (("1" (inst?) (("1" (assert) (("1" (lemma "tensor_power_rows_alt") (("1" (inst?) (("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" (lemma "tensor_power_rows_alt") (("2" (inst - "A66" "1+k") (("2" (lemma "tensor_power_rows_alt") (("2" (inst - "A63" "1+k") (("2" (assert) (("2" (lemma "dot_eq_sigma") (("2" (expand "*" +) (("2" (rewrite -1 +) (("2" (rewrite -1 +) (("2" (rewrite "length_row") (("1" (rewrite "length_row") (("1" (rewrite "length_col") (("1" (rewrite "length_col") (("1" (lemma "tensor_power_columns_alt") (("1" (inst - "A63" "1+k") (("1" (lemma "tensor_power_columns_alt") (("1" (inst - "A66" "1+k") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (replace -2 :dir rl) (("1" (expand "min" +) (("1" (case "NOT columns(A66) = 6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (case "NOT columns(A63) = 3") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (name "siggy" "LAMBDA (i:nat): base_n_to_nat(6,base_n(3,i),k)") (("2" (invoke (name "F" "%1") (! 2 2 3)) (("2" (replaces -1) (("2" (invoke (name "G" "%1") (! 2 1 3)) (("2" (replaces -1) (("2" (lemma "sigma_inj") (("2" (inst - "F" "G" "3^(1+k)-1" "6^(1+k)-1" "0" "0" "siggy") (("2" (assert) (("2" (hide 3) (("2" (split 1) (("1" (skeep) (("1" (expand "siggy" 1) (("1" (assert) (("1" (split 1) (("1" (assert) nil nil) ("2" (lemma "base_n_to_nat_lt") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (assert) (("1" (case "FORALL (i1,i2:int): i1<i2 IMPLIES i1<=i2-1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "siggy" -1) (("2" (lemma "base_n_to_nat_unique") (("2" (inst?) (("2" (assert) (("2" (inst - "k") (("2" (split -) (("1" (lemma "base_n_is_n_alt") (("1" (inst - "3" "i!1" "k") (("1" (lemma "base_n_is_n_alt") (("1" (inst - "3" "j!1" "k") (("1" (assert) (("1" (replaces -1 +) (("1" (replaces -1 +) (("1" (lemma "base_n_to_nat_eq") (("1" (inst?) (("1" (assert) (("1" (inst - "k") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) (("2" (lemma "base_n_lt_n") (("2" (hide -2) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (expand "G" +) (("3" (case "access(col(TQ_vect6k(k, a, n, GF, KF))(0))(i!1) = 0") (("1" (assert) nil nil) ("2" (hide 3) (("2" (rewrite "access_col") (("2" (expand "TQ_vect6k" 1) (("2" (rewrite "entry_form_matrix") (("1" (lift-if) (("1" (ground) (("1" (name "jj" "base_n_to_nat(3,base_n(6,i!1),k)") (("1" (inst 3 "jj") (("1" (expand "siggy" +) (("1" (expand "jj" 3) (("1" (lemma "base_n_base_n_to_nat") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (lemma "base_n_to_nat_eq") (("1" (inst - "6" "k" "k" "base_n(3, base_n_to_nat(3, base_n(6, i!1), k))" "base_n(6,i!1)") (("1" (replace -2) (("1" (replaces -1) (("1" (lemma "base_n_is_n_alt") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst + "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "jj" 1) (("2" (lemma "base_n_to_nat_lt") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (case "FORALL (i1,i2:int): i1<i2 IMPLIES i1<=i2-1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (inst + "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (assert) (("2" (assert) (("2" (inst + "x1!1") (("1" (assert) nil nil) ("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-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" (skeep) (("4" (expand "F" 1) (("4" (expand "G" 1) (("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" (hide 2) (("1" (lemma "tensor_entry_alt") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "tensor_entry_alt") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (rewrite "product_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (case "NOT rows(A66)=6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (replace -4) (("2" (replace -5) (("2" (case "NOT rows(A63) = 6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (expand "entry_pick" +) (("2" (case "base_n(6, siggy(i!1)) = base_n(3, i!1)") (("1" (replaces -1) (("1" (rewrite "A63_def" 1) (("1" (lemma "base_n_lt_n") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "siggy" 1) (("2" (lemma "base_n_base_n_to_nat") (("2" (inst?) (("2" (split -) (("1" (decompose-equality 1) (("1" (case "x!1<=k") (("1" (inst - "x!1") nil nil) ("2" (assert) (("2" (lemma "base_n_0") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (lemma "base_n_0") (("1" (replace -2) (("1" (inst - "3" "i!1" "x!1") (("1" (assert) (("1" (typepred "i!1") (("1" (lemma "both_sides_expt_gt1_le_aux") (("1" (inst - "3" "k" "x!1-1") (("1" (expand "^") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "base_n_to_nat_lt") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (lemma "both_sides_expt_gt1_le_aux") (("1" (inst - "6" "k" "x!1-1") (("1" (expand "^") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "siggy" 1) (("2" (lemma "base_n_to_nat_lt") (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "TQ_vect6k" +) (("2" (expand "TQ_vect3k" +) (("2" (rewrite "entry_form_matrix") (("1" (rewrite "entry_form_matrix") (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (split +) (("1" (flatten) (("1" (skeep -1) (("1" (expand "siggy" -1) (("1" (lemma "base_n_base_n_to_nat") (("1" (inst?) (("1" (split -) (("1" (rewrite -1 -2) (("1" (lemma "base_n_lt_n") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "base_n(3, i!1)=base_n(6, siggy(i!1))") (("1" (assert) nil nil) ("2" (hide 3) (("2" (hide 2) (("2" (expand "siggy" +) (("2" (lemma "base_n_base_n_to_nat") (("2" (inst?) (("2" (split -) (("1" (decompose-equality 1) (("1" (case "x!1<=k") (("1" (rewrite -2) nil nil) ("2" (lemma "base_n_0") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (replace -1) (("1" (lemma "base_n_0") (("1" (inst - "6" _ _) (("1" (inst?) (("1" (assert) (("1" (lemma "base_n_to_nat_lt") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (lemma "both_sides_expt_gt1_le_aux") (("1" (inst - "6" "k" "x!1-1") (("1" (expand "^") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "both_sides_expt_gt1_le_aux") (("2" (inst - "3" "k" "x!1-1") (("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "siggy" 1) (("2" (lemma "base_n_to_nat_lt") (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (assert) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) (("2" (inst + "x1!1") (("1" (assert) nil nil) ("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-1") (("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) (("2" (assert) (("2" (lemma "base_n_lt_n") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("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" (hide 3) (("2" (lemma "tensor_power_rows_alt") (("2" (inst?) (("2" (expand "rows" -1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (expand "rows" -3 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) ((multi_sturm_tarski_NSol formula-decl nil tarski_query_matrix nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (mult_full application-judgement "FullMatrix" matrices "matrices/") (NOT const-decl "[bool -> bool]" booleans nil) (rows_mult formula-decl nil matrices "matrices/") (nat_exp application-judgement "nat" exponentiation nil) (tensor_power_rows_alt formula-decl nil tensor_product "matrices/") (columns_mult formula-decl nil matrices "matrices/") (posint_exp application-judgement "posint" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry_mult formula-decl nil matrices "matrices/") (dot_eq_sigma formula-decl nil matrices "matrices/") (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (length_row formula-decl nil matrices "matrices/") (length_col formula-decl nil matrices "matrices/") (tensor_power_columns_alt formula-decl nil tensor_product "matrices/") (access const-decl "real" matrices "matrices/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_inj formula-decl nil sigma_nat "reals/") (siggy skolem-const-decl "[nat -> nat]" tarski_query_matrix nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (base_n_lt_n formula-decl nil base_repr "reals/") (base_n_to_nat_lt formula-decl nil base_repr "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (base_n_is_n_alt formula-decl nil base_repr "reals/") (base_n_to_nat_eq formula-decl nil base_repr "reals/") (base_n_to_nat_unique formula-decl nil base_repr "reals/") (G skolem-const-decl "[nat -> real]" tarski_query_matrix nil) (x1!1 skolem-const-decl "nat" tarski_query_matrix nil) (base_n_0 formula-decl nil base_repr "reals/") (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posnat_expt application-judgement "posnat" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil) (i!2 skolem-const-decl "nat" tarski_query_matrix nil) (base_n_base_n_to_nat formula-decl nil base_repr "reals/") (k skolem-const-decl "nat" tarski_query_matrix nil) (jj skolem-const-decl "nat" tarski_query_matrix nil) (form_matrix_square application-judgement "FullMatrix" matrices "matrices/") (entry_form_matrix formula-decl nil matrices "matrices/") (TQ_fam const-decl "int" poly_families nil) (access_col formula-decl nil matrices "matrices/") (F skolem-const-decl "[nat -> real]" tarski_query_matrix nil) (access_row formula-decl nil matrices "matrices/") (nat_expt application-judgement "nat" exponentiation nil) (x!1 skolem-const-decl "nat" tarski_query_matrix nil) (x1!1 skolem-const-decl "nat" tarski_query_matrix nil) (i!1 skolem-const-decl "subrange(0, 3 ^ (1 + k) - 1)" tarski_query_matrix nil) (A63_def formula-decl nil tarski_query_matrix nil) (x!1 skolem-const-decl "nat" tarski_query_matrix nil) (product_eq formula-decl nil product "reals/") (entry_pick const-decl "real" tensor_product "matrices/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (tensor_entry_alt formula-decl nil tensor_product "matrices/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (base_n def-decl "nat" base_repr "reals/") (base_n_to_nat const-decl "nat" base_repr "reals/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (TQ_vect3k const-decl "{v: PosFullMatrix | rows(v) = 3 ^ (k + 1) AND columns(v) = 1}" tarski_query_matrix nil) (A63 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" tarski_query_matrix nil) (TQ_vect6k const-decl "{v: PosFullMatrix | rows(v) = 6 ^ (k + 1) AND columns(v) = 1}" tarski_query_matrix nil) (^ const-decl "real" exponentiation nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (A66 const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6 AND M = inverse(A66_inv)}" tarski_query_matrix nil) (A66_inv const-decl "{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 6}" tarski_query_matrix nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv "matrices/") (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices "matrices/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (SquareMatrix type-eq-decl nil matrices "matrices/") (invertible? const-decl "bool" matrix_inv "matrices/") (det def-decl "real" matrix_props "matrices/") (/= const-decl "boolean" notequal nil) (Square type-eq-decl nil matrices "matrices/") (tensor_power_alt def-decl "PosFullMatrix" tensor_product "matrices/") (PosFullMatrix type-eq-decl nil matrices "matrices/") (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices "matrices/") (col def-decl "VectorN(rows(M))" matrices "matrices/") (VectorN type-eq-decl nil matrices "matrices/") (row const-decl "Vector" matrices "matrices/") (* const-decl "real" matrices "matrices/") (Vector type-eq-decl nil matrices "matrices/") (entry const-decl "real" matrices "matrices/") (MatrixMN type-eq-decl nil matrices "matrices/") (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices "matrices/") (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices "matrices/") (FullMatrix type-eq-decl nil matrices "matrices/") (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices "matrices/") (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) (full_matrix_eq formula-decl nil matrices "matrices/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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)) nil) (multi_sturm_tarski_NSol63-1 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" (replaces -1 :dir rl) (("1" (lemma "tensor_power_rows_alt") (("1" (inst - "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" (split -) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "columns_mult") (("1" (inst?) (("1" (split -) (("1" (replaces -1) (("1" (assert) nil 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)) nil)) 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)) 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" (lemma "tensor_power_rows_alt") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "j") (("2" (case "NOT columns(tensor_power_alt(A66, 1 + k) * TQ_vect6k(k, a, n, GF, KF)) = 1") (("1" (lemma "columns_mult") (("1" (inst?) (("1" (assert) (("1" (lemma "tensor_power_rows_alt") (("1" (inst?) (("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" (lemma "tensor_power_rows_alt") (("2" (inst - "A66" "1+k") (("2" (lemma "tensor_power_rows_alt") (("2" (inst - "A63" "1+k") (("2" (assert) (("2" (lemma "dot_eq_sigma") (("2" (expand "*" +) (("2" (rewrite -1 +) (("2" (rewrite -1 +) (("2" (rewrite "length_row") (("1" (rewrite "length_row") (("1" (rewrite "length_col") (("1" (rewrite "length_col") (("1" (lemma "tensor_power_columns_alt") (("1" (inst - "A63" "1+k") (("1" (lemma "tensor_power_columns_alt") (("1" (inst - "A66" "1+k") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (replace -2 :dir rl) (("1" (expand "min" +) (("1" (case "NOT columns(A66) = 6") (("1" (assert) nil nil) ("2" (replace -1) (("2" (case "NOT columns(A63) = 3") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (name "siggy" "LAMBDA (i:nat): base_n_to_nat(6,base_n(3,i),k+1)") (("2" (invoke (name "F" "%1") (! 2 2 3)) (("2" (replaces -1) (("2" (invoke (name "G" "%1") (! 2 1 3)) (("2" (replaces -1) (("2" (lemma "sigma_inj") (("2" (inst - "F" "G" "3^(1+k)-1" "6^(1+k)-1" "0" "0" "siggy") (("2" (assert) (("2" (hide 3) (("2" (split 1) (("1" (skeep) (("1" (expand "siggy" 1) (("1" (assert) (("1" (split 1) (("1" (assert) nil nil) ("2" (lemma "base_n_to_nat_lt") (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil)) 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" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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)))
¤ 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.405Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26