| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/matrices/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 751 kB |
|
SSL tensor_product.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(tensor_product (not_null 0 (not_null-1 nil 3615549872 ("" (skosimp*) (("" (grind) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty? const-decl "bool" matrices nil) (rows const-decl "nat" matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (length def-decl "nat" list_props nil)) shostak)) (mod_int 0 (mod_int-1 nil 3618130444 ("" (skeep) (("" (split) (("1" (expand "mod") (("1" (grind) nil nil)) nil) ("2" (cross-mult) (("2" (expand "mod") (("2" (cancel-by 1 "n") nil nil)) nil)) nil)) nil)) nil) ((mod const-decl "{k | abs(k) < abs(j)}" mod nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (= const-decl "[T, T -> boolean]" equalities nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nil application-judgement "below(m)" mod nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)) shostak)) (tensor_fun_TCC1 0 (tensor_fun_TCC1-1 nil 3614943215 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (rows const-decl "nat" matrices nil)) nil)) (tensor_fun_TCC2 0 (tensor_fun_TCC2-1 nil 3614943215 ("" (skosimp*) (("" (expand "mod") (("" (case-replace "rows(B!1) * floor(i!1 / rows(B!1)) / rows(B!1) = floor(i!1 / rows(B!1))") (("1" (split 1) (("1" (ground) nil nil) ("2" (ground) (("2" (typepred (i!1)) (("2" (div-by -1 "rows(B!1)") (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_div_pos_ge1 formula-decl nil real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types 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) (rows const-decl "nat" matrices nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (tensor_fun_TCC3 0 (tensor_fun_TCC3-1 nil 3614943215 ("" (subtype-tcc) nil nil) ((rows const-decl "nat" matrices nil)) nil)) (tensor_fun_TCC4 0 (tensor_fun_TCC4-5 nil 3614947199 ("" (skosimp*) (("" (expand "mod") (("" (case-replace "columns(B!1) * floor(j!1 / columns(B!1)) / columns(B!1) = floor(j!1 / columns(B!1))") (("1" (split 1) (("1" (ground) nil nil) ("2" (ground) (("2" (typepred (j!1)) (("2" (div-by -1 "columns(B!1)") (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_div_pos_ge1 formula-decl nil real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (PosFullMatrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil) (tensor_fun_TCC4-4 nil 3614947172 ("" (skosimp*) (("" (expand "mod") (("" (case-replace "columns(B!1) * floor(j!1 / columns(B!1)) / columns(B!1) = floor(j!1 / columns(B!1))") (("1" (split 1) (("1" (ground) nil) ("2" (ground) (("2" (typepred (i!1)) (("2" (div-by -1 "columns(B!1)") (("2" (ground) nil))))))))) ("2" (cross-mult 1) nil) ("3" (ground) nil)))))) nil) nil nil) (tensor_fun_TCC4-3 nil 3614947143 ("" (skosimp*) (("" (expand "mod") (("" (case-replace "columns(B!1) * floor(i!1 / columns(B!1)) / columns(B!1) = floor(j!1 / columns(B!1))") (("1" (split 1) (("1" (ground) nil) ("2" (ground) (("2" (typepred (i!1)) (("2" (div-by -1 "columns(B!1)") (("2" (ground) nil))))))))) ("2" (cross-mult 1) nil) ("3" (ground) nil)))))) nil) nil nil) (tensor_fun_TCC4-2 nil 3614947074 ("" (skosimp*) (("" (expand "mod") (("" (case-replace "columns(B!1) * floor(i!1 / columns(B!1)) / columns(B!1) = floor(i!1 / columns(B!1))") (("1" (split 1) (("1" (ground) nil nil) ("2" (ground) (("2" (typepred (i!1)) (("2" (div-by -1 "columns(B!1)") (("2" (ground) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil) nil nil) (tensor_fun_TCC4-1 nil 3614943215 ("" (subtype-tcc) nil nil) nil nil)) (tensor_fun_TCC5 0 (tensor_fun_TCC5-1 nil 3614943215 ("" (skosimp*) (("" (lemma "mod_pos") (("" (inst?) (("1" (flatten) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil) ((mod_pos formula-decl nil mod nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (rows const-decl "nat" matrices nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (tensor_fun_TCC6 0 (tensor_fun_TCC6-1 nil 3614943215 ("" (skosimp*) (("" (lemma "mod_pos") (("" (inst?) (("1" (flatten) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil) ((mod_pos formula-decl nil mod nil) (PosFullMatrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (FullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (tensor_prod_TCC1 0 (tensor_prod_TCC1-1 nil 3615032070 ("" (skeep) (("" (rewrite "rows_form_matrix") (("" (lemma "columns_form_matrix") (("" (inst?) (("" (typepred (A)) (("" (typepred (B)) (("" (mult-ineq -7 -3) (("" (mult-ineq -9 -5) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rows_form_matrix formula-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (tensor_fun const-decl "[[nat, nat] -> real]" tensor_product nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (gt_times_gt_any1 formula-decl nil extra_real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (columns_form_matrix formula-decl nil matrices nil)) nil)) (entry_tensor_prod 0 (entry_tensor_prod-1 nil 3618677832 ("" (skeep) (("" (expand "tensor_prod") (("" (decompose-equality) (("" (rewrite "entry_form_matrix") (("" (lift-if) (("" (ground) (("1" (expand "tensor_fun") (("1" (propax) nil nil)) nil) ("2" (expand "tensor_fun") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tensor_prod const-decl "PosFullMatrix" tensor_product nil) (entry_form_matrix formula-decl nil matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (tensor_fun const-decl "[[nat, nat] -> real]" tensor_product nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (row const-decl "Vector" matrices nil) (Vector type-eq-decl nil matrices nil) (MatrixMN type-eq-decl nil matrices 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) (length def-decl "nat" list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (entry const-decl "real" matrices nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (form_matrix_square application-judgement "FullMatrix" matrices nil)) shostak)) (tensor_rows 0 (tensor_rows-1 nil 3615042678 ("" (skosimp*) (("" (lemma "rows_form_matrix") (("" (inst -1 "rows(A!1) * rows(B!1)" "columns(A!1) * columns(B!1)" "tensor_fun(A!1, B!1)") (("" (expand "tensor_prod") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((rows_form_matrix formula-decl nil matrices nil) (tensor_prod const-decl "PosFullMatrix" tensor_product nil) (tensor_fun const-decl "[[nat, nat] -> real]" tensor_product nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (rows const-decl "nat" matrices nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) shostak)) (tensor_cols 0 (tensor_cols-1 nil 3615042993 ("" (skosimp*) (("" (lemma "columns_form_matrix") (("" (expand "tensor_prod") (("" (inst -1 "rows(A!1)*rows(B!1)" "columns(A!1)*columns(B!1)" "tensor_fun(A!1, B!1)") (("" (split) (("1" (lemma "zero_times3") (("1" (inst -1 "rows(A!1)" "rows(B!1)") (("1" (flatten) (("1" (hide -2) (("1" (prop) (("1" (typepred (A!1)) (("1" (ground) nil nil)) nil) ("2" (typepred (B!1)) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((columns_form_matrix formula-decl nil matrices nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (tensor_fun const-decl "[[nat, nat] -> real]" tensor_product nil) (zero_times3 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (tensor_prod const-decl "PosFullMatrix" tensor_product nil)) shostak)) (tensor_mult_entry_TCC1 0 (tensor_mult_entry_TCC1-1 nil 3615558345 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil)) nil)) (tensor_mult_entry_TCC2 0 (tensor_mult_entry_TCC2-1 nil 3615558345 ("" (skeep) (("" (grind) (("" (case "m1/rows(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (cross-mult 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ((rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (rows const-decl "nat" matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (B skolem-const-decl "PosFullMatrix" tensor_product nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil)) nil)) (tensor_mult_entry_TCC3 0 (tensor_mult_entry_TCC3-1 nil 3615558345 ("" (subtype-tcc) nil nil) ((rows const-decl "nat" matrices nil)) nil)) (tensor_mult_entry_TCC4 0 (tensor_mult_entry_TCC4-1 nil 3615558345 ("" (skeep) (("" (grind) (("" (case "n1/columns(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ((rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (rows const-decl "nat" matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (PosFullMatrix type-eq-decl nil matrices nil)) nil)) (tensor_mult_entry_TCC5 0 (tensor_mult_entry_TCC5-1 nil 3615558345 ("" (skeep) (("" (lemma "mod_pos") (("" (inst?) (("" (flatten) nil nil)) nil)) nil)) nil) ((mod_pos formula-decl nil mod nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (rows const-decl "nat" matrices nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (tensor_mult_entry_TCC6 0 (tensor_mult_entry_TCC6-1 nil 3615558345 ("" (skeep) (("" (lemma "mod_pos") (("" (inst?) (("" (flatten) nil nil)) nil)) nil)) nil) ((mod_pos formula-decl nil mod nil) (PosFullMatrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (FullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (tensor_mult_entry 0 (tensor_mult_entry-1 nil 3615627026 ("" (skeep) (("" (lemma "entry_mult") (("" (inst-cp -1 "tensor_prod(A,B)" "tensor_prod(A2, B2)" "m1" "n1") (("" (case "m1<rows(tensor_prod(A,B)) AND n1<columns(tensor_prod(A2, B2))") (("1" (lift-if -3) (("1" (split -3) (("1" (flatten) (("1" (hide (-1 -2)) (("1" (lemma "form_matrix_mult") (("1" (inst -1 "tensor_fun(A,B)" "tensor_fun(A2, B2)" "rows(A)*rows(B)" "columns(A)*columns(B)" "columns(A2)*columns(B2)") (("1" (expand "tensor_prod" 1) (("1" (replace -6 1 :dir rl) (("1" (replace -7 1 :dir rl) (("1" (split -1) (("1" (replace -1) (("1" (lemma "entry_form_matrix") (("1" (inst -1 "LAMBDA (i, j: nat): IF i > rows(A) * rows(B) OR j > columns(A2) * columns(B2) THEN 0 ELSE sigma(0, columns(A) * columns(B) - 1, LAMBDA (d: nat): tensor_fun(A, B)(i, d) * tensor_fun(A2, B2)(d, j)) ENDIF" "m1" "n1" "rows(A)*rows(B)" "columns(A2)*columns(B2)") (("1" (lemma "tensor_rows") (("1" (inst -1 "A" "B") (("1" (lemma "tensor_cols") (("1" (inst -1 "A2" "B2") (("1" (replace -2 -6) (("1" (replace -1 -7) (("1" (case-replace "IF m1 < rows(A) * rows(B) AND n1 < columns(A2) * columns(B2) THEN IF m1 > rows(A) * rows(B) OR n1 > columns(A2) * columns(B2) THEN 0 ELSE sigma(0, columns(A) * columns(B) - 1, LAMBDA (d: nat): tensor_fun(A, B)(m1, d) * tensor_fun(A2, B2)(d, n1)) ENDIF ELSE 0 ENDIF = sigma(0, columns(A) * columns(B) - 1, LAMBDA (d: nat): tensor_fun(A, B)(m1, d) * tensor_fun(A2, B2)(d, n1))") (("1" (replace -4) (("1" (hide (-1 -4 -5)) (("1" (expand "tensor_fun") (("1" (lemma "sigma_eq") (("1" (inst -1 "LAMBDA (d: nat): IF m1 < rows(A) * rows(B) THEN IF d < columns(A) * columns(B) THEN entry(A) ((m1 - mod(m1, rows(B))) / rows(B), (d - mod(d, columns(B))) / columns(B)) * entry(B)(mod(m1, rows(B)), mod(d, columns(B))) ELSE 0 ENDIF ELSE 0 ENDIF * IF d < rows(A2) * rows(B2) THEN IF n1 < columns(A2) * columns(B2) THEN entry(A2) ((d - mod(d, rows(B2))) / rows(B2), (n1 - mod(n1, columns(B2))) / columns(B2)) * entry(B2) (mod(d, rows(B2)), mod(n1, columns(B2))) ELSE 0 ENDIF ELSE 0 ENDIF" "LAMBDA (d: nat): entry(A) ((m1 - mod(m1, rows(B))) / rows(B), (d - mod(d, columns(B))) / columns(B)) * entry(B)(mod(m1, rows(B)), mod(d, columns(B))) * entry(A2) ((d - mod(d, rows(B2))) / rows(B2), (n1 - mod(n1, columns(B2))) / columns(B2)) * entry(B2) (mod(d, rows(B2)), mod(n1, columns(B2))) " "columns(A)*columns(B)-1" "0") (("1" (split -1) (("1" (replace -1) (("1" (lemma "sigma_product2") (("1" (hide -2) (("1" (replace -9 1 :dir rl) (("1" (inst -1 "LAMBDA (d:nat): entry(A) ((m1 - mod(m1, rows(B))) / rows(B), d)* entry(A2) (d, (n1 - mod(n1, columns(B2))) / columns(B2))" "LAMBDA (d:nat): entry(B)(mod(m1, rows(B)), d)*entry(B2)(d, mod(n1, columns(B2)))" "columns(A)" "columns(B)") (("1" (replace -1 :dir rl) (("1" (lemma "matrix2array") (("1" (case "FORALL (M, M2: PosFullMatrix, r, c:nat): columns(M) =rows(M2) AND r<rows(M) AND c<columns(M2 entry(M*M2)(r,c) = sigma(0, columns(M)-1, LAMBDA(d:nat): entry(M)(r,d)*entry(M2)(d, c) (("1" (inst -1 "A" "A2" "(m1 - mod(m1, rows(B))) / rows(B)" " (n1 - mod(n1, columns(B2))) / columns(B2)") (("1" (split -1) (("1" (replace -1) (("1" (hide (-1 -3 -9)) (("1" (reveal -4) (("1" (inst -1 "B" "B2" "mod(m1, rows(B))" "mod(n1, columns(B2))") (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "mod_pos") (("3" (inst -1 "m1" "rows(B)") (("3" (ground) nil nil)) nil)) nil) ("4" (lemma "mod_pos") (("4" (inst -1 "n1" "columns(B2)") (("4" (ground) nil nil)) nil)) nil)) nil) ("2" (lemma "mod_pos") (("2" (inst -1 "n1" "columns(B2)") (("2" (ground) nil nil)) nil)) nil) ("3" (lemma "mod_pos") (("3" (inst -1 "m1" "rows(B)") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (hide-all-but (1 -6)) (("3" (lemma "mod_pos") (("3" (inst -1 "m1" "rows(B)") (("3" (ground) (("3" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -7)) (("4" (cross-mult 1) (("4" (lemma "mod_pos") (("4" (inst -1 "n1" "columns(B2)") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (case "n1/columns(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) (("3" (case "m1/rows(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (cross-mult 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skeep) (("2" (inst-cp -4 "M") (("2" (inst -4 "M2") (("2" (case-replace "M*M2 = form_matrix(entry(M), rows(M), columns(M))* form_matrix(entry(M2), rows(M2), co (("1" (lemma "form_matrix_mult") (("1" (inst -1 "entry(M)" "entry(M2)" "rows(M)" "columns(M)" "columns(M2)") (("1" (split -1) (("1" (replace -3) (("1" (replace -1) (("1" (lemma "entry_form_matrix2") (("1" (inst -1 "LAMBDA (i, j: nat): IF i > rows(M) OR j > columns(M2) THEN 0 ELSE sigma(0, rows(M2) - 1, LAMBDA (d: nat): entry(M)(i, d) * entry(M2)(d, j)) ENDIF" "r" "c" "rows(M)" "columns(M2)") (("1" (hide (-2 -3)) (("1" (prop) (("1" (lift-if -1) (("1" (prop) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "mod_pos") (("2" (inst -1 "n1" "columns(B2)") (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "mod_pos") (("3" (inst -1 "m1" "rows(B)") (("3" (ground) nil nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (grind) (("4" (case "n1/columns(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (grind) (("5" (case "m1/rows(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (cross-mult 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (typepred (n)) (("2" (case "n<columns(A)*columns(B) AND n<rows(A2)*rows(B2)") (("1" (lift-if 1) (("1" (prop) (("1" (lift-if 1) (("1" (prop) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-3 -4 -5 -8 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "mod_pos") (("2" (inst -1 "n1" "columns(B2)") (("2" (ground) nil nil)) nil)) nil) ("3" (skeep) (("3" (lemma "mod_pos") (("3" (inst -1 "d" "rows(B2)") (("3" (ground) nil nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (grind) (("4" (cross-mult) (("4" (case "n1/columns(B2)>=0") (("1" (ground) nil nil) ("2" (grind) (("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (skeep) (("5" (grind) (("5" (case "d/rows(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (cross-mult 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide-all-but 1) (("6" (skeep) (("6" (lemma "mod_pos") (("6" (inst -1 "d" "columns(B)") (("6" (ground) nil nil)) nil)) nil)) nil)) nil) ("7" (hide-all-but 1) (("7" (lemma "mod_pos") (("7" (inst -1 "m1" "rows(B)") (("7" (ground) nil nil)) nil)) nil)) nil) ("8" (hide-all-but 1) (("8" (skeep) (("8" (grind) (("8" (case "d/columns(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("9" (hide-all-but 1) (("9" (grind) (("9" (case "m1/rows(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (cross-mult 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("10" (hide-all-but 1) (("10" (skeep) (("10" (lemma "mod_pos") (("10" (inst -1 "n1" "columns(B2)") (("10" (ground) nil nil)) nil)) nil)) nil)) nil) ("11" (hide-all-but 1) (("11" (skeep) (("11" (lemma "mod_pos") (("11" (inst -1 "d" "rows(B2)") (("11" (ground) nil nil)) nil)) nil)) nil)) nil) ("12" (hide-all-but 1) (("12" (skeep) (("12" (grind) (("12" (case "n1/columns(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("13" (hide-all-but 1) (("13" (skeep) (("13" (grind) (("13" (case "d/rows(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("14" (hide-all-but 1) (("14" (skeep) (("14" (lemma "mod_pos") (("14" (inst -1 "d" "columns(B)") (("14" (ground) nil nil)) nil)) nil)) nil)) nil) ("15" (hide-all-but 1) (("15" (skeep) (("15" (lemma "mod_pos") (("15" (inst -1 "m1" "rows(B)") (("15" (ground) nil nil)) nil)) nil)) nil)) nil) ("16" (hide-all-but 1) (("16" (skeep) (("16" (grind) (("16" (case "d/columns(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("17" (hide-all-but 1) (("17" (skeep) (("17" (grind) (("17" (case "m1/rows(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-6 -7 1)) (("2" (ground) nil nil)) nil) ("3" (hide-all-but 1) (("3" (typepred (A)) (("3" (typepred (B)) (("3" (mult-ineq -4 -8) (("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (typepred (A)) (("4" (typepred (B)) (("4" (mult-ineq -4 -8) (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (typepred (B)) (("2" (typepred (A)) (("2" (mult-ineq -4 -8) (("2" (hide-all-but (-1 3)) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (typepred (A)) (("2" (typepred (B)) (("2" (hide-all-but (-4 -8 1)) (("2" (mult-ineq -1 -2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred (A)) (("3" (typepred (B)) (("3" (hide-all-but (-3 -7 1)) (("3" (mult-ineq -1 -2) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (lift-if -2) (("2" (split -2) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (hide 2) (("2" (split 1) (("1" (inst -2 "A" "A2" "(m1 - mod(m1, rows(B))) / rows(B)" " (n1 - mod(n1, columns(B2))) / columns(B2)") (("1" (lift-if -2) (("1" (split -2) (("1" (flatten) (("1" (hide-all-but (1 -1)) (("1" (lemma "tensor_rows") (("1" (inst -1 "A" "B") (("1" (replace -1) (("1" (hide -1) (("1" (case "FORALL (a,b:nat): a<b IMPLIES a<=b-1") (("1" (inst -1 "(m1 - mod(m1, rows(B))) / rows(B)" "rows(A)") (("1" (prop) (("1" (cross-mult -1) (("1" (lemma "mod_pos") (("1" (inst -1 "m1" "rows(B)") (("1" (flatten) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (case "m1/rows(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (cross-mult 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred (B2)) (("2" (lemma "mod_pos") (("2" (inst -1 "n1" "columns(B2)") (("2" (flatten) (("2" (hide-all-but 1) (("2" (grind) (("2" (case "n1/columns(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) (("3" (case "m1/rows(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (cross-mult 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -2 "A" "A2" "(m1 - mod(m1, rows(B))) / rows(B)" " (n1 - mod(n1, columns(B2))) / columns(B2)") (("1" (lift-if -2) (("1" (split -2) (("1" (flatten) (("1" (hide-all-but (-2 1)) (("1" (case "FORALL (a,b:nat): a<b IMPLIES a<=b-1") (("1" (inst -1 "(n1 - mod(n1, columns(B2))) / columns(B2) " " columns(A2)") (("1" (prop) (("1" (lemma "tensor_cols") (("1" (inst -1 "A2" "B2") (("1" (replace -1) (("1" (cross-mult -2) (("1" (lemma "mod_pos") (("1" (inst -1 "n1" "columns(B2)") (("1" (flatten) (("1" (hide -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (case "n1/columns(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (case "n1/columns(B2)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) (("3" (case "m1/rows(B)>=0") (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) nil nil) ("3" (cross-mult 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((entry_mult formula-decl nil matrices nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (tensor_fun const-decl "[[nat, nat] -> real]" tensor_product nil) (int_minus_int_is_int application-judgement "int" integers nil) (entry_form_matrix formula-decl nil matrices nil) (tensor_rows formula-decl nil tensor_product nil) (tensor_cols formula-decl nil tensor_product nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq formula-decl nil sigma "reals/") (sigma_product2 formula-decl nil sigma_nat "reals/") (MatrixMN type-eq-decl nil matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (even_times_int_is_even application-judgement "even_int" integers nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (mod_pos formula-decl nil mod nil) (posreal nonempty-type-eq-decl nil real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (entry_form_matrix2 formula-decl nil matrices nil) (mult_full application-judgement "FullMatrix" matrices nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (matrix2array formula-decl nil matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (subrange type-eq-decl nil integers nil) (entry const-decl "real" matrices nil) (n1 skolem-const-decl "nat" tensor_product nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (m1 skolem-const-decl "nat" tensor_product nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (gt_times_gt_any1 formula-decl nil extra_real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (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) (B2 skolem-const-decl "PosFullMatrix" tensor_product nil) (A2 skolem-const-decl "PosFullMatrix" tensor_product nil) (B skolem-const-decl "PosFullMatrix" tensor_product nil) (A skolem-const-decl "PosFullMatrix" tensor_product nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (form_matrix_mult formula-decl nil matrices nil) (div_mult_pos_le1 formula-decl nil real_props nil) (tensor_prod const-decl "PosFullMatrix" tensor_product nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (invertible_tensor_TCC1 0 (invertible_tensor_TCC1-1 nil 3615032070 ("" (skeep) (("" (lemma "tensor_rows") (("" (inst?) (("" (replace -1) (("" (lemma "tensor_cols") (("" (inst?) (("" (replace -1) (("" (typepred (AA)) (("" (replace -5) (("" (typepred (BB)) (("" (replace -5) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tensor_rows formula-decl nil tensor_product nil) (NOT const-decl "[bool -> bool]" booleans nil) (tensor_cols formula-decl nil tensor_product nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) nil)) (invertible_tensor_TCC2 0 (invertible_tensor_TCC2-1 nil 3615032070 ("" (skeep) (("" (split 1) (("1" (lemma "tensor_rows" ("A" "AA" "B" "BB")) (("1" (lemma "tensor_cols" ("A" "AA" "B" "BB")) (("1" (typepred (AA)) (("1" (replace -5) (("1" (typepred (BB)) (("1" (replace -5) (("1" (replace -11) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil) ((tensor_cols formula-decl nil tensor_product nil) (NOT const-decl "[bool -> bool]" booleans nil) (tensor_rows formula-decl nil tensor_product nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil)) nil)) (invertible_tensor_TCC3 0 (invertible_tensor_TCC3-1 nil 3615032070 ("" (skeep) nil nil) nil nil)) (invertible_tensor_TCC4 0 (invertible_tensor_TCC4-1 nil 3615032070 ("" (skeep) nil nil) nil nil)) (invertible_tensor 0 (invertible_tensor-1 nil 3615040307 ("" (skeep) (("" (expand "invertible?") (("" (skolem -1 "AAinv") (("" (skolem -2 "BBinv") (("" (lemma "inverse_unique") (("" (inst-cp -1 "AAinv" "AA") (("" (inst -1 "BBinv" "BB") (("" (lemma "inverse_unique") (("" (flatten) (("" (split -2) (("1" (flatten) (("1" (replace -2 :dir rl) (("1" (split -6) (("1" (flatten) (("1" (replace -2 :dir rl) (("1" (inst -9 "tensor_prod(AAinv, BBinv)" "tensor_prod(AA, BB)") (("1" (split -9) (("1" (flatten) (("1" (replace -2 :dir rl) (("1" (expand "invertible?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (rewrite "tensor_rows") (("2" (rewrite "tensor_rows") (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (hide 4) (("3" (case "tensor_prod(AA, BB) * tensor_prod(AAinv, BBinv) = Id(rows(tensor_prod(AA, BB)))") (("1" (ground) nil nil) ("2" (hide 2) (("2" (lemma "full_matrix_eq") (("2" (inst -1 "tensor_prod(AA, BB) * tensor_prod(AAinv, BBinv) " " Id(rows(tensor_prod(AA, BB)))") (("2" (flatten) (("2" (hide -1) (("2" (lemma "rows_mult") (("2" (inst -1 "tensor_prod(AA, BB) " " tensor_prod(AAinv, BBinv)") (("2" (replace -1) (("2" (lemma "rows_Id") (("2" (inst -1 "rows(tensor_prod(AA,BB))") (("2" (replace -1) (("2" (hide (-1 -2)) (("2" (lemma "columns_mult") (("2" (inst -1 "tensor_prod(AA, BB) " " tensor_prod(AAinv, BBinv)") (("2" (split -1) (("1" (lemma "columns_Id") (("1" (inst -1 "rows(tensor_prod(AA,BB))") (("1" (replace -1) (("1" (replace -2) (("1" (lemma "tensor_cols") (("1" (inst -1 "AAinv" "BBinv") (("1" (typepred (AAinv)) (("1" (replace -5 :dir rl) (("1" (hide (-1 -2 -3 -4 -5)) (("1" (typepred (BBinv)) (("1" (replace -5 :dir rl) (("1" (hide (-1 -2 -3 -4 -5)) (("1" (lemma "tensor_rows") (("1" (inst? -1) (("1" (replace -14) (("1" (replace -17) (("1" (replace -1) (("1" (replace -2) (("1" (split -5) (("1" (propax) nil nil) ("2" (skeep) (("2" (lemma "tensor_mult_entry") (("2" (inst -1 "AA" "AAinv" "BB" "BBinv" "i" "j") (("2" (typepred (AA)) (("2" (replace -5 -6 :dir rl) (("2" (hide (-1 -2 -3 -4 -5)) (("2" (typepred (BB)) (("2" (replace -5 -6 :dir rl) (("2" (hide (-1 -2 -3 -4 -5)) (("2" (split -1) (("1" (replace -1 1) (("1" (typepred (BBinv)) (("1" (replace -5 1 :dir rl) (("1" (hide (-1 -2 -3 -4 -5)) (("1" (replace -17 1) (("1" (replace -9 1) (("1" (replace -13 1) (("1" (lemma "entry_Id") (("1" (inst-cp -1 "i" "j" "rows(AA)*rows(BB)") (("1" (inst-cp -1 "(i - mod(i, rows(BB))) / rows(BB)" "(j - mod(j, rows(BB))) / rows(BB)" "rows(AA)") (("1" (inst -1 "mod(i, rows(BB))" "mod(j, rows(BB))" "rows(BB)") (("1" (case "mod(i, rows(BB))<rows(BB) AND mod(j, rows(BB))<rows(BB)") (("1" (case "(i - mod(i, rows(BB))) / rows(BB) < rows(AA) AND (j - mod(j, rows(BB))) / rows(BB) < rows(AA)") (("1" (case-replace "mod(i, rows(BB)) = mod(j, rows(BB))") (("1" (case-replace "i=j") (("1" (lift-if -4) (("1" (split -4) (("1" (flatten) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil) ("2" (flatten) (("2" (replace -2) (("2" (lift-if -8) (("2" (split -8) (("1" (flatten) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil) ("2" (flatten) (("2" (replace -2) (("2" (lift-if -8) (("2" (split -8) (("1" (flatten) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil) ("2" (flatten) (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(i - mod(j, rows(BB))) / rows(BB) /= (j - mod(j, rows(BB))) / rows(BB)") (("1" (lift-if -5) (("1" (split -5) (("1" (flatten) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil) ("2" (flatten) (("2" (replace -2) (("2" (lift-if -8) (("2" (split -8) (("1" (flatten) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (replace -2) (("3" (lift-if -9) (("3" (split -9) (("1" (flatten) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (replace -2) (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-4 -5 -6)) (("2" (simplify 1) (("2" (expand "/=") (("2" (cross-mult -1) (("2" (cancel-by -1 "rows(BB)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lift-if -3) (("2" (split -3) (("1" (flatten) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (replace -2) (("3" (case "i/=j") (("1" (lift-if -9) (("1" (split -9) (("1" (flatten) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (replace -2) (("3" (simplify 4) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil) ("2" (expand "/=") (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) ("2" (split 1) (("1" (typepred (i)) (("1" (lemma "rows_mult") (("1" (inst -1 "tensor_prod(AA, BB)" "tensor_prod(AAinv, BBinv)") (("1" (replace -1) (("1" (replace -8 -2) (("1" (cross-mult 1) (("1" (lemma "mod_pos") (("1" (inst -1 "i" "rows(BB)") (("1" (flatten) (("1" (hide-all-but (-1 -2 -4 1)) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred (j)) (("2" (replace -10 -1) (("2" (lemma "mod_pos") (("2" (inst -1 "j" "rows(BB)") (("2" (flatten) (("2" (hide-all-but (-1 -2 -3 1)) (("2" (cross-mult 1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "mod_pos") (("2" (split 1) (("1" (inst -1 "i" "rows(BB)") (("1" (flatten) nil nil)) nil) ("2" (inst -1 "j" "rows(BB)") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "mod_pos") (("2" (inst -1 "j" "rows(BB)") (("2" (flatten) nil nil)) nil)) nil) ("3" (lemma "mod_pos") (("3" (inst -1 "i" "rows(BB)") (("3" (flatten) nil nil)) nil)) nil)) nil) ("2" (hide (-1 -2 2 3 4)) (("2" (typepred (j)) (("2" (replace -5) (("2" (lemma "mod_pos") (("2" (inst -1 "j" "rows(BB)") (("2" (flatten) (("2" (hide-all-but (-1 -2 -3 1)) (("2" (split) (("1" (grind) nil nil) ("2" (cross-mult) (("2" (expand "mod") (("2" (case "j>=0") (("1" (div-by -1 "rows(BB)") (("1" (ground) (("1" (typepred ("rows(BB)")) (("1" (case "floor(j/rows(BB))>=0") (("1" (mult-ineq -1 -2) (("1" (ground) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "mod_pos") (("3" (inst -1 "i" "rows(BB)") (("3" (typepred (i)) (("3" (reveal -18) (("3" (replace -1) (("3" (hide-all-but (-2 -3 1)) (("3" (flatten) (("3" (split) (("1" (grind) nil nil) ("2" (case "i>=0") (("1" (expand "mod") (("1" (cross-mult 1) (("1" (typepred ("rows(BB)")) (("1" (div-by -2 "rows(BB)") (("1" (case "floor(i/rows(BB))>=0") (("1" (mult-ineq -1 -2) (("1" (grind) nil nil)) nil) ("2" (case "i/rows(BB)>=0") (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "nonempty?(tensor_prod(AA, BB))") (("1" (name-replace "TP" "tensor_prod(AA, BB)") (("1" (hide-all-but (-1 -2)) (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "tensor_rows") (("2" (inst? -1) (("2" (typepred (AA)) (("2" (typepred (BB)) (("2" (hide (-1 -2 -6 -7)) (("2" (lemma "tensor_cols") (("2" (inst? -1) (("2" (mult-ineq -6 -3) (("2" (mult-ineq -6 -3) (("2" (expand "nonempty?") (("2" (replace -3) (("2" (replace -10) (("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "tensor_rows") (("2" (inst?) (("2" (replace -1) (("2" (lemma "tensor_cols") (("2" (inst?) (("2" (replace -1) (("2" (typepred (AA)) (("2" (replace -5) (("2" (hide -) (("2" (typepred (BB)) (("2" (replace -5) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "tensor_rows") (("3" (inst?) (("3" (replace -1) (("3" (lemma "tensor_cols") (("3" (inst?) (("3" (replace -1) (("3" (typepred (AAinv)) (("3" (replace -5) (("3" (hide -) (("3" (typepred (BBinv)) (("3" (replace -5) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((invertible? const-decl "bool" matrix_inv nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (BBinv skolem-const-decl "Square" tensor_product nil) (AAinv skolem-const-decl "Square" tensor_product nil) (tensor_prod const-decl "PosFullMatrix" tensor_product nil) (BB skolem-const-decl "Square" tensor_product nil) (AA skolem-const-decl "Square" tensor_product nil) (rows_Id formula-decl nil matrices nil) (columns_mult formula-decl nil matrices 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) (div_mult_pos_ge1 formula-decl nil real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (integer nonempty-type-from-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (ge_times_ge_any1 formula-decl nil extra_real_props nil) (both_sides_div_pos_ge1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (div_cancel4 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel3 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mod_pos formula-decl nil mod nil) (posreal nonempty-type-eq-decl nil real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (j skolem-const-decl "below(columns(tensor_prod(AA, BB) * tensor_prod(AAinv, BBinv)))" tensor_product nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (i skolem-const-decl "below(rows(tensor_prod(AA, BB) * tensor_prod(AAinv, BBinv)))" tensor_product nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (entry_Id formula-decl nil matrices nil) (tensor_mult_entry formula-decl nil tensor_product nil) (NOT const-decl "[bool -> bool]" booleans nil) (tensor_cols formula-decl nil tensor_product nil) (columns_Id formula-decl nil matrices nil) (gt_times_gt_any1 formula-decl nil extra_real_props nil) (nonempty? const-decl "bool" matrices nil) (rows_mult formula-decl nil matrices nil) (full_matrix_eq formula-decl nil matrices nil) (MatrixMN type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (SquareMatrix type-eq-decl nil matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (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 nil) (mult_full application-judgement "FullMatrix" matrices nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (tensor_rows formula-decl nil tensor_product nil) (inverse_unique formula-decl nil matrix_inv nil)) shostak)) (TQMat_TCC1 0 (TQMat_TCC1-1 nil 3615032070 ("" (ground) (("" (grind) nil nil)) nil) ((every adt-def-decl "boolean" list_adt nil)) nil)) (TQMat_TCC2 0 (TQMat_TCC2-1 nil 3615032070 ("" (grind) nil nil) ((every adt-def-decl "boolean" list_adt nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (TQMat_TCC3 0 (TQMat_TCC3-1 nil 3615032070 ("" (split) (("1" (flatten) (("1" (eval-formula) (("1" (skeep) (("1" (case "(i=0 OR i=1 OR i=2) AND (j=0 OR j=1 OR j=2)") (("1" (ground) (("1" (replaces -1) (("1" (replaces -1) (("1" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil)) nil) ("2" (hide (2 3)) (("2" (typepred "i") (("2" (typepred "j") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil) ((columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nth def-decl "T" list_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (length def-decl "nat" list_props nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (FALSE const-decl "bool" booleans 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)) (TQMatInv_TCC1 0 (TQMatInv_TCC1-1 nil 3615032070 ("" (grind) nil nil) ((every adt-def-decl "boolean" list_adt nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (TQMatInv_TCC2 0 (TQMatInv_TCC2-1 nil 3615032070 ("" (grind) nil nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (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)) (TQMatInv_TCC3 0 (TQMatInv_TCC3-1 nil 3615032070 ("" (split) (("1" (flatten) (("1" (skeep) (("1" (case "(i=0 OR i=1 OR i=2) AND (j=0 OR j=1 OR j=2)") (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (typepred "j") (("2" (typepred "i") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil) ((columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (rows const-decl "nat" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (length def-decl "nat" list_props nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nth def-decl "T" list_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (invTQ 0 (invTQ-1 nil 3615032864 ("" (expand "invertible?") (("" (inst 1 "TQMatInv") (("" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (TQMatInv const-decl "Square" tensor_product nil) (row const-decl "Vector" matrices nil) (access const-decl "real" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (dot def-decl "real" matrices nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (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 nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (mult_full application-judgement "FullMatrix" matrices nil) (TQMat const-decl "Square" tensor_product nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (invertible? const-decl "bool" matrix_inv nil)) shostak)) (is_invTQ_TCC1 0 (is_invTQ_TCC1-1 nil 3615033026 ("" (flatten) (("" (expand "invertible?") (("" (inst 1 "TQMatInv") (("" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil) ((invertible? const-decl "bool" matrix_inv nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (TQMat const-decl "Square" tensor_product nil) (mult_full application-judgement "FullMatrix" matrices nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (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 nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (dot def-decl "real" matrices nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (col def-decl "VectorN(rows(M))" matrices nil) (access const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (TQMatInv const-decl "Square" tensor_product nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) nil)) (is_invTQ 0 (is_invTQ-1 nil 3615033027 ("" (lemma "inverse_unique") (("" (case "TQMat*TQMatInv = Id(rows(TQMat))") (("1" (inst -2 "TQMatInv" "TQMat") (("1" (split -2) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (hide (-1 2)) (("2" (grind) nil nil)) nil) ("3" (ground) nil nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (grind) nil nil)) nil) ("3" (hide (-1 2)) (("3" (grind) nil nil)) nil)) nil)) nil) ((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 nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (SquareMatrix type-eq-decl nil matrices nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (TQMatInv const-decl "Square" tensor_product nil) (TQMat const-decl "Square" tensor_product nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (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 nil) (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (mult_full application-judgement "FullMatrix" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (access const-decl "real" matrices nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (dot def-decl "real" matrices nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (inverse_unique formula-decl nil matrix_inv nil)) shostak)) (tensor_power_TCC1 0 (tensor_power_TCC1-1 nil 3615903379 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (tensor_power_TCC2 0 (tensor_power_TCC2-1 nil 3615903379 ("" (termination-tcc) nil nil) nil nil)) (invertible_tensor_power_TCC1 0 (invertible_tensor_power_TCC1-1 nil 3615903379 ("" (induct "n") (("1" (ground) nil nil) ("2" (flatten) (("2" (ground) nil nil)) nil) ("3" (skeep) (("3" (skeep) (("3" (case-replace "j=0") (("1" (expand "tensor_power") (("1" (typepred (A)) (("1" (propax) nil nil)) nil)) nil) ("2" (case-replace "tensor_power(A, j+1) = tensor_prod(A, tensor_power(A,j))") (("1" (rewrite "tensor_rows") (("1" (rewrite "tensor_cols") (("1" (split -2) (("1" (inst?) (("1" (prop) (("1" (typepred (A)) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil) ("2" (hide (-1 3)) (("2" (name-replace "TPj" "tensor_power(A, j)") (("2" (expand "tensor_power") (("2" (lift-if) (("2" (split) (("1" (flatten) nil nil) ("2" (flatten) (("2" (ground) (("2" (expand "TPj") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (TPj skolem-const-decl "PosFullMatrix" tensor_product nil) (tensor_rows formula-decl nil tensor_product nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (tensor_cols formula-decl nil tensor_product nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (tensor_prod const-decl "PosFullMatrix" tensor_product nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (tensor_power def-decl "PosFullMatrix" tensor_product nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (invertible? const-decl "bool" matrix_inv nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (FullMatrix type-eq-decl nil matrices nil) (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 nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types 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)) (invertible_tensor_power_TCC2 0 (invertible_tensor_power_TCC2-1 nil 3615903379 ("" (lemma "invertible_tensor_power_TCC1") (("" (skeep) (("" (inst?) (("" (ground) nil nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (invertible_tensor_power_TCC1 subtype-tcc nil tensor_product nil)) nil)) (invertible_tensor_power_TCC3 0 (invertible_tensor_power_TCC3-1 nil 3615903379 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (rows const-decl "nat" matrices nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (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 nil) (invertible? const-decl "bool" matrix_inv nil) (/= const-decl "boolean" notequal nil)) nil)) (invertible_tensor_power 0 (invertible_tensor_power-1 nil 3615911176 ("" (induct "n") (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (skeep) (("3" (case-replace "j=0") (("1" (skeep) (("1" (expand "tensor_power") (("1" (propax) nil nil)) nil)) nil) ("2" (skeep) (("2" (case-replace "tensor_power(A, j+1) = tensor_prod(A, tensor_power(A, j))") (("1" (case-replace "tensor_power(inverse(A), j+1) = tensor_prod(inverse(A), tensor_power(inverse(A), j)) (("1" (case "invertible?(inverse(A))") (("1" (split -4) (("1" (inst-cp -1 "A") (("1" (split -2) (("1" (flatten) (("1" (replace -2 :dir rl) (("1" (lemma "invertible_tensor") (("1" (inst -1 "A" "tensor_power(A, j)") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (expand "invertible?" 1) (("2" (expand "invertible?") (("2" (skeep -5) (("2" (case "IQ= inverse(A)") (("1" (inst 1 "A") (("1" (replace -1) (("1" (ground) nil nil)) nil)) nil) ("2" (lemma "inverse_unique") (("2" (inst -1 "IQ" "A") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name-replace "TP" "tensor_power(inverse(A),j)") (("2" (expand "tensor_power") (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) nil nil) ("2" (flatten) (("2" (expand "TP") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (ground) nil nil)) nil) ("2" (name-replace "TP" "tensor_power(A,j)") (("2" (expand "tensor_power") (("2" (lift-if 1) (("2" (split 1) (("1" (ground) nil nil) ("2" (ground) (("1" (expand "TP") (("1" (propax) nil nil)) nil) ("2" (expand "TP") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (skeep) nil nil)) nil) ("5" (lemma "invertible_tensor_power_TCC2") (("5" (skeep) (("5" (inst?) nil nil)) nil)) nil) ("6" (lemma "invertible_tensor_power_TCC1") (("6" (skeep) (("6" (inst?) nil nil)) nil)) nil)) nil) ((invertible_tensor_power_TCC1 subtype-tcc nil tensor_product nil) (n skolem-const-decl "nat" tensor_product nil) (invertible_tensor_power_TCC2 subtype-tcc nil tensor_product nil) (n skolem-const-decl "nat" tensor_product nil) (TP skolem-const-decl "PosFullMatrix" tensor_product nil) (inverse_unique formula-decl nil matrix_inv nil) (mult_full application-judgement "FullMatrix" matrices nil) (invertible_tensor formula-decl nil tensor_product nil) (TP skolem-const-decl "PosFullMatrix" tensor_product nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (tensor_prod const-decl "PosFullMatrix" tensor_product nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (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 nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (SquareMatrix type-eq-decl nil matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (pred type-eq-decl nil defined_types nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrix_inv nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (tensor_power def-decl "PosFullMatrix" tensor_product nil)) shostak)) (tensor_power_rows_TCC1 0 (tensor_power_rows_TCC1-1 nil 3618074804 ("" (subtype-tcc) nil nil) ((rows const-decl "nat" matrices nil)) nil)) (tensor_power_rows 0 (tensor_power_rows-1 nil 3618074805 ("" (skolem 1 ("A" "_")) (("" (induct "n") (("1" (ground) nil nil) ("2" (flatten) (("2" (ground) nil nil)) nil) ("3" (skeep) (("3" (split -1) (("1" (expand "tensor_power" 1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (ground) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "tensor_rows") (("2" (expand "^") (("2" (expand "expt" 2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "j=0") (("1" (expand "tensor_power") (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "tensor_power") (("2" (lift-if 3) (("2" (split 3) (("1" (flatten) nil nil) ("2" (flatten) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (tensor_power def-decl "PosFullMatrix" tensor_product nil) (nat_induction formula-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (tensor_rows formula-decl nil tensor_product nil) (expt def-decl "real" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nat_expt application-judgement "nat" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_exp application-judgement "nat" exponentiation nil)) shostak)) (tensor_power_columns_TCC1 0 (tensor_power_columns_TCC1-1 nil 3618075082 ("" (subtype-tcc) nil nil) nil nil)) (tensor_power_columns 0 (tensor_power_columns-3 nil 3618075244 ("" (skolem 1 ("A" "_")) (("" (induct "n") (("1" (ground) nil nil) ("2" (flatten) (("2" (ground) nil nil)) nil) ("3" (skeep) (("3" (split -1) (("1" (expand "tensor_power" 1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (ground) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "tensor_cols") (("2" (expand "^") (("2" (expand "expt" 2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "j=0") (("1" (expand "tensor_power") (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "tensor_power") (("2" (lift-if 3) (("2" (split 3) (("1" (flatten) nil nil) ("2" (flatten) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (FullMatrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (tensor_power def-decl "PosFullMatrix" tensor_product nil) (nat_induction formula-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (tensor_cols formula-decl nil tensor_product nil) (expt def-decl "real" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nat_expt application-judgement "nat" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_exp application-judgement "nat" exponentiation nil)) nil) (tensor_power_columns-2 nil 3618075185 ("" (skolem 1 ("A" "_")) (("" (induct "n") (("1" (ground) nil) ("2" (flatten) (("2" (ground) nil))) ("3" (skeep) (("3" (split -1) (("1" (expand "tensor_power" 1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (ground) (("1" (grind) nil))))) ("2" (flatten) (("2" (rewrite "tensor_columns") (("2" (expand "^") (("2" (expand "expt" 2) (("2" (ground) nil))))))))))))))) ("2" (case-replace "j=0") (("1" (expand "tensor_power") (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (propax) nil))))))))) ("2" (expand "tensor_power") (("2" (lift-if 3) (("2" (split 3) (("1" (flatten) nil) ("2" (flatten) (("2" (ground) nil)))))))))))))))))) nil) nil nil) (tensor_power_columns-1 nil 3618075083 ("" (postpone) nil nil) nil shostak)) (mod_eq_lem_alt_TCC1 0 (mod_eq_lem_alt_TCC1-1 nil 3618745682 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil)) nil)) (mod_eq_lem_alt 0 (mod_eq_lem_alt-1 nil 3618745689 ("" (skeep) (("" (lemma "mod_sum") (("" (inst - "mod(i,n)" "n" "mod((i - mod(i, n)) / n, m)") (("1" (replaces -1) (("1" (assert) (("1" (assert) (("1" (case "mod(mod(i,n),n) = mod(i,n)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "mod_of_mod") (("2" (inst - "0" "i" "n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "mod_int_quot") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mod_sum formula-decl nil mod nil) (mod_int_quot formula-decl nil mod_lems "ints/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mod_of_mod formula-decl nil mod nil) (= const-decl "[T, T -> boolean]" equalities nil) (int_plus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (i skolem-const-decl "nat" tensor_product nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (n skolem-const-decl "posnat" tensor_product nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "below(m)" mod nil)) nil)) (tensor_prod_assoc 0 (tensor_prod_assoc-1 nil 3618677717 ("" (skeep) (("" (rewrite "full_matrix_eq") (("" (case "NOT (rows(tensor_prod(A, tensor_prod(B, C))) = rows(tensor_prod(tensor_prod(A, B), C)) AND columns(tensor_prod(A, tensor_prod(B, C))) = columns(tensor_prod(tensor_prod(A, B), C)))") (("1" (hide 2) (("1" (split) (("1" (rewrite "tensor_rows") (("1" (rewrite "tensor_rows") (("1" (rewrite "tensor_rows") (("1" (rewrite "tensor_rows") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "tensor_cols") (("2" (rewrite "tensor_cols") (("2" (rewrite "tensor_cols") (("2" (rewrite "tensor_cols") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (rewrite "entry_tensor_prod") (("2" (rewrite "entry_tensor_prod") (("2" (typepred "i") (("2" (typepred "j") (("2" (copy -2) (("2" (copy -2) (("2" (rewrite "tensor_cols" -1) (("2" (rewrite "tensor_cols" -1) (("2" (rewrite "tensor_rows" -2) (("2" (rewrite "tensor_rows" -2) (("2" (assert) (("2" (expand "tensor_fun" +) (("2" (rewrite "tensor_rows" 1) (("2" (rewrite "tensor_rows" 1) (("2" (rewrite "tensor_cols" 1) (("2" (rewrite "tensor_cols" 1) (("2" (assert) (("2" (rewrite "entry_tensor_prod" 1) (("2" (rewrite "entry_tensor_prod" 1) (("2" (expand "tensor_fun" +) (("2" (label "igz" 1) (("2" (hide "igz") (("2" (case "NOT FORALL (MN:Matrix,ii,jj,kk,pp:nat): (ii=kk AND jj=pp) IMPLIES entry(MN)(ii,jj) = ent (("1" (skeep) (("1" (assert) nil nil)) nil) ("2" (case "NOT FORALL (aa,bb,cc,dd,ee,ff:real): (aa=dd AND bb=ee AND cc=ff) IMPLIES aa*(bb*cc)=(dd* (("1" (skeep) (("1" (assert) nil nil)) nil) ("2" (label "ski" -1) (("2" (reveal "igz") (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (rewrite "ski" 1) (("1" (hide 2) (("1" (copy -6) (("1" (inst? -1) (("1" (assert) (("1" (hide 2) (("1" (split 1) (("1" (rewrite "mod_mult_quot") (("1" (assert) nil nil)) nil) ("2" (rewrite "mod_mult_quot") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "mod_int_quot") (("2" (rewrite -1 1) (("2" (rewrite "mod_int_quot" 1) nil nil)) nil)) nil)) nil) ("3" (lemma "mod_int_quot") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (rewrite "mod_int_quot" 1) (("4" (rewrite "mod_int_quot" 1) nil nil)) nil)) nil) ("5" (lemma "mod_int_quot") (("5" (inst?) (("5" (assert) nil nil)) nil)) nil) ("6" (rewrite "mod_int_quot" 1) nil nil) ("7" (rewrite "mod_int_quot" 1) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (copy -6) (("2" (inst? -1) (("1" (assert) (("1" (hide 2) (("1" (split 1) (("1" (rewrite "mod_mult_quot") (("1" (assert) (("1" (rewrite "mod_eq_lem_alt") nil nil)) nil)) nil) ("2" (rewrite "mod_mult_quot" 1) (("2" (assert) (("2" (rewrite "mod_eq_lem_alt") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "mod_int_quot") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "mod_pos") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "mod_int_quot") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "mod_pos") (("4" (inst?) (("1" (assert) nil nil) ("2" (lemma "mod_int_quot") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (lemma "mod_int_quot") (("5" (inst?) (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (rewrite "mod_int_quot") (("6" (lemma "mod_pos") (("6" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("7" (rewrite "mod_int_quot") (("7" (lemma "mod_pos") (("7" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (copy -6) (("3" (inst? -1) (("1" (assert) (("1" (hide 2) (("1" (split) (("1" (rewrite "mod_mult_quot") (("1" (lemma "mod_sum") (("1" (inst - "mod(i,rows(C))" "rows(C)" "mod((i - mod(i, rows(C))) / rows(C), rows(B))") (("1" (replaces -1) (("1" (lemma "mod_of_mod") (("1" (inst - "0" "i" "rows(C)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "mod_int_quot") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "mod_mult_quot") (("2" (lemma "mod_sum") (("2" (inst - "mod(j,columns(C))" "columns(C)" "mod((j - mod(j, columns(C))) / columns(C), columns(B))") (("1" (replaces -1) (("1" (lemma "mod_of_mod") (("1" (inst - "0" "j" "columns(C)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "mod_int_quot") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "mod_pos") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "mod_pos") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil) ("4" (lemma "mod_pos") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil) ("5" (lemma "mod_pos") (("5" (inst?) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "mod_pos") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (lemma "mod_pos") (("5" (inst?) (("5" (assert) nil nil)) nil)) nil) ("6" (lemma "mod_pos") (("6" (inst?) (("1" (assert) nil nil) ("2" (lemma "mod_int_quot") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("7" (lemma "mod_pos") (("7" (inst?) (("1" (assert) nil nil) ("2" (lemma "mod_int_quot") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("8" (lemma "mod_int_quot") (("8" (inst?) (("8" (lemma "mod_int_quot") (("8" (inst?) nil nil)) nil)) nil)) nil) ("9" (assert) (("9" (lemma "mod_int_quot") (("9" (inst?) (("9" (assert) nil nil)) nil)) nil)) nil) ("10" (rewrite "mod_int_quot") (("10" (rewrite "mod_int_quot") nil nil)) nil) ("11" (lemma "mod_int_quot") (("11" (inst?) (("11" (assert) nil nil)) nil)) nil) ("12" (hide 2) (("12" (lemma "mod_pos") (("12" (inst?) (("12" (assert) nil nil)) nil)) nil)) nil) ("13" (hide 2) (("13" (lemma "mod_pos") (("13" (inst?) (("13" (assert) nil nil)) nil)) nil)) nil) ("14" (hide 2) (("14" (rewrite "mod_int_quot") (("14" (lemma "mod_pos") (("14" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("15" (hide 2) (("15" (rewrite "mod_int_quot") (("15" (lemma "mod_pos") (("15" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("16" (hide 2) (("16" (rewrite "mod_int_quot") nil nil)) nil) ("17" (hide 2) (("17" (rewrite "mod_int_quot") nil nil)) nil)) nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (lemma "mod_pos") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (cross-mult 1) (("3" (lemma "mod_pos") (("3" (inst?) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 1) (("4" (lemma "mod_pos") (("4" (inst - "j" "columns(B)*columns(C)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("5" (hide 1) (("5" (lemma "mod_pos") (("5" (hide-all-but (-1 1)) (("5" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "posreal_times_posreal_is_posreal") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((full_matrix_eq formula-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (tensor_prod const-decl "PosFullMatrix" tensor_product nil) (tensor_fun const-decl "[[nat, nat] -> real]" tensor_product nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (mod_of_mod formula-decl nil mod nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mod_sum formula-decl nil mod nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (mod_eq_lem_alt formula-decl nil tensor_product nil) (nil application-judgement "below(m)" mod nil) (mod_pos formula-decl nil mod nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (mod_mult_quot formula-decl nil mod_lems "ints/") (int_plus_int_is_int application-judgement "int" integers nil) (mod_int_quot formula-decl nil mod_lems "ints/") (j skolem-const-decl "below(columns(tensor_prod(A, tensor_prod(B, C))))" tensor_product nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (i skolem-const-decl "below(rows(tensor_prod(A, tensor_prod(B, C))))" tensor_product nil) (C skolem-const-decl "PosFullMatrix" tensor_product nil) (B skolem-const-decl "PosFullMatrix" tensor_product nil) (A skolem-const-decl "PosFullMatrix" tensor_product nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (entry const-decl "real" matrices nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry_tensor_prod formula-decl nil tensor_product nil) (tensor_cols formula-decl nil tensor_product nil) (tensor_rows formula-decl nil tensor_product nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (power_assoc 0 (power_assoc-1 nil 3618676254 ("" (case "FORALL (A: PosFullMatrix, k,i:nat):i<=k IMPLIES tensor_power(A, i+1) = tensor_power_alt(A, i+1)") (("1" (skeep) (("1" (inst - "A" "n-1" "n-1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "k") (("1" (assert) (("1" (skeep) (("1" (case "NOT i = 0") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (assert) (("2" (assert) (("2" (hide -1) (("2" (expand "tensor_power") (("2" (expand "tensor_power_alt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (case "j = 0") (("1" (assert) (("1" (skeep) (("1" (case "i = 0") (("1" (inst - "A" "0") (("1" (assert) nil nil)) nil) ("2" (case "NOT i = 1") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (inst - "A" "0") (("2" (assert) (("2" (hide (-1 -2)) (("2" (hide 1) (("2" (expand "tensor_power_alt") (("2" (expand "tensor_power_alt") (("2" (expand "tensor_power") (("2" (expand "tensor_power") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (case "NOT i = j+1") (("1" (assert) (("1" (inst - "A" "i") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "tensor_power" +) (("2" (inst-cp - "A" "j") (("2" (assert) (("2" (replace -3 +) (("2" (expand "tensor_power_alt" + 1) (("2" (inst-cp - "A" "j-1") (("2" (assert) (("2" (replace -3 + :dir rl) (("2" (expand "tensor_power_alt" +) (("2" (replace -4 + :dir rl) (("2" (expand "tensor_power" + 2) (("2" (rewrite "tensor_prod_assoc") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tensor_prod_assoc formula-decl nil tensor_product nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (tensor_power def-decl "PosFullMatrix" tensor_product nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (tensor_power_alt def-decl "PosFullMatrix" tensor_product nil)) shostak)) (tensor_power_rows_alt 0 (tensor_power_rows_alt-1 nil 3618751580 ("" (skeep) (("" (lemma "power_assoc" ("A" "A" "n" "n")) (("" (replace -1 :dir rl) (("" (rewrite "tensor_power_rows") nil nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (power_assoc formula-decl nil tensor_product nil) (tensor_power_rows formula-decl nil tensor_product nil)) shostak)) (tensor_power_columns_alt 0 (tensor_power_columns_alt-1 nil 3618751702 ("" (skeep) (("" (lemma "power_assoc" ("A" "A" "n" "n")) (("" (replace -1 :dir rl) (("" (rewrite "tensor_power_columns") nil nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (power_assoc formula-decl nil tensor_product nil) (tensor_power_columns formula-decl nil tensor_product nil)) shostak)) (TQXL_TCC1 0 (TQXL_TCC1-1 nil 3618049647 ("" (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)) (TQXL_TCC2 0 (TQXL_TCC2-1 nil 3618049647 ("" (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)) (TQXL_TCC3 0 (TQXL_TCC3-1 nil 3618049647 ("" (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)) (TQXLinv_TCC1 0 (TQXLinv_TCC1-1 nil 3618049647 ("" (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)) (TQXLinv_TCC2 0 (TQXLinv_TCC2-1 nil 3618049647 ("" (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)) (TQXLinv_TCC3 0 (TQXLinv_TCC3-1 nil 3618049647 ("" (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)) (invTQXL 0 (invTQXL-1 nil 3618050460 ("" (split) (("1" (expand "invertible?") (("1" (inst 1 "TQXLinv") (("1" (eval-formula) nil nil)) nil)) nil) ("2" (expand "invertible?") (("2" (inst 1 "TQXL") (("2" (eval-formula) nil nil)) nil)) nil)) nil) ((TQXL const-decl "Square" tensor_product nil) (invertible? const-decl "bool" matrix_inv nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (TQXLinv const-decl "Square" tensor_product nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (is_invTQXL_TCC1 0 (is_invTQXL_TCC1-1 nil 3618049647 ("" (lemma "invTQXL") (("" (ground) nil nil)) nil) ((invTQXL formula-decl nil tensor_product nil)) nil)) (is_invTQXL_TCC2 0 (is_invTQXL_TCC2-1 nil 3618049647 ("" (flatten) (("" (lemma "invTQXL") (("" (ground) nil nil)) nil)) nil) ((invTQXL formula-decl nil tensor_product nil)) nil)) (is_invTQXL 0 (is_invTQXL-1 nil 3618050673 ("" (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)) (RowToMat_TCC1 0 (RowToMat_TCC1-1 nil 3618069795 ("" (skeep) (("" (split) (("1" (flatten) (("1" (case "length[list[real]]((: row(M)(k) :)) = 1") (("1" (skeep) (("1" (case-replace "i=0") (("1" (case-replace "j=0") (("1" (typepred (j)) (("1" (ground) nil nil)) nil)) nil) ("2" (typepred (i)) (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil) ("2" (ground) (("2" (expand "rows") (("2" (ground) nil nil)) nil)) nil) ("3" (case-replace "columns((: row(M)(k) :)) = columns(M)") (("1" (typepred (M)) (("1" (propax) nil nil)) nil) ("2" (lemma "matrices.length_row") (("2" (inst-cp -1 "M" "k") (("2" (split -2) (("1" (replace -1 :dir rl) (("1" (inst -2 "(: row(M)(k) :)" "0") (("1" (split -2) (("1" (case-replace "row((: row(M)(k) :))(0) = row(M)(k)") (("1" (replace -2 :dir rl) (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (case-replace "length[list[real]]((: row(M)(k) :)) = 1") (("1" (skeep) (("1" (case-replace "i=0") (("1" (case-replace "j=0") (("1" (typepred (j)) (("1" (ground) nil nil)) nil)) nil) ("2" (typepred (i)) (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil) ("2" (typepred (k)) (("2" (expand "rows") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((null adt-constructor-decl "(null?)" list_adt nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (row const-decl "Vector" matrices nil) (Matrix type-eq-decl nil matrices nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Vector type-eq-decl nil matrices nil) (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (length_singleton formula-decl nil more_list_props "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length_row formula-decl nil matrices nil) (k skolem-const-decl "below(rows(M))" tensor_product nil) (M skolem-const-decl "PosFullMatrix" tensor_product nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (RtM 0 (RtM-1 nil 3621071529 ("" (skeep) (("" (expand "RowToMat") (("" (expand "row2mat") (("" (propax) nil nil)) nil)) nil)) nil) ((RowToMat const-decl "PosFullMatrix" tensor_product nil) (row2mat const-decl "PosFullMatrix" linear_dependence nil)) shostak)) (RowToMat_rows 0 (RowToMat_rows-1 nil 3618157882 ("" (skeep) (("" (expand "RowToMat") (("" (ground) (("" (grind) nil nil)) nil)) nil)) nil) ((RowToMat const-decl "PosFullMatrix" tensor_product nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (rows const-decl "nat" matrices nil) (length def-decl "nat" list_props nil) (row const-decl "Vector" matrices nil)) shostak)) (RowToMat_columns 0 (RowToMat_columns-1 nil 3618157905 ("" (skeep) (("" (typepred (k)) (("" (grind) (("" (lemma "matrices.length_row") (("" (inst -1 "M" "k") (("" (split -1) (("1" (expand "row") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (rows const-decl "nat" matrices nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (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) (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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (length_row formula-decl nil matrices nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (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) (row const-decl "Vector" matrices nil) (RowToMat const-decl "PosFullMatrix" tensor_product nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) shostak)) (RowToMat_entry 0 (RowToMat_entry-1 nil 3618668435 ("" (skeep) (("" (expand "entry") (("" (expand "access") (("" (lemma "RowToMat_columns") (("" (lemma "RowToMat_rows") (("" (inst -2 "M" "k") (("" (lift-if 1) (("" (lift-if 1) (("" (lift-if 1) (("" (split 1) (("1" (flatten) (("1" (split 1) (("1" (flatten) (("1" (name-replace "RK" "row(M)(k)") (("1" (expand "RowToMat") (("1" (expand "row") (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (ground) (("2" (typepred (k)) (("2" (ground) (("2" (expand "rows") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lift-if 2) (("2" (split 2) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (case-replace "nth((: nth(M, k) :), 0) = nth(M,k)") (("1" (expand "RK") (("1" (expand "row") (("1" (lift-if 2) (("1" (split 2) (("1" (flatten) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (typepred (n)) (("2" (name-replace "NMK" "nth(M, k)") (("2" (expand "nth") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "length_row" -1) (("1" (rewrite "length_row" 1) (("1" (ground) nil nil) ("2" (typepred (k)) (("2" (expand "rows") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (inst?) (("2" (expand "rows") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split 2) (("1" (flatten) (("1" (rewrite "length_row" 2) (("1" (rewrite "length_row" -1) (("1" (ground) nil nil)) nil) ("2" (inst?) (("2" (ground) (("2" (expand "rows") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((entry const-decl "real" matrices nil) (RowToMat_columns formula-decl nil tensor_product nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (Vector type-eq-decl nil matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length_singleton formula-decl nil more_list_props "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (RK skolem-const-decl "Vector" tensor_product nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (RowToMat const-decl "PosFullMatrix" tensor_product nil) (length_row formula-decl nil matrices nil) (RowToMat_rows formula-decl nil tensor_product nil) (access const-decl "real" matrices nil)) shostak)) (RowToMat_tensor_prod_TCC1 0 (RowToMat_tensor_prod_TCC1-1 nil 3618142292 ("" (skeep) (("" (rewrite "tensor_rows") (("" (ground) nil nil)) nil)) nil) ((tensor_rows formula-decl nil tensor_product nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (RowToMat_tensor_prod_TCC2 0 (RowToMat_tensor_prod_TCC2-1 nil 3618142292 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rows const-decl "nat" matrices nil)) nil)) (RowToMat_tensor_prod_TCC3 0 (RowToMat_tensor_prod_TCC3-1 nil 3618142292 ("" (skeep) (("" (lemma "mod_int" ("k" "k" "n" "rows(N)")) (("" (prop) (("" (cross-mult 1) (("" (typepred (k)) (("" (lemma "mod_pos") (("" (inst?) (("" (flatten) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (rows const-decl "nat" matrices nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (mod_int formula-decl nil tensor_product nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mod_pos formula-decl nil mod nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (RowToMat_tensor_prod_TCC4 0 (RowToMat_tensor_prod_TCC4-1 nil 3618142292 ("" (skeep) (("" (lemma "mod_pos" ("i" "k" "m" "rows(N)")) (("" (propax) nil nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (rows const-decl "nat" matrices nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (mod_pos formula-decl nil mod nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (RowToMat_tensor_prod 0 (RowToMat_tensor_prod-1 nil 3618143199 ("" (skeep) (("" (lemma "more_list_props[list[real]].list_extensionality") (("" (inst?) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (propax) nil nil) ("2" (lemma "tensor_rows") (("2" (inst -1 "RowToMat(M, (k - mod(k, rows(N))) / rows(N))" " RowToMat(N, mod(k, rows(N)))") (("1" (expand "rows") (("1" (replace -1) (("1" (case "FORALL (A:PosFullMatrix, kk:below(rows(A))): length(RowToMat(A, kk))=1") (("1" (inst-cp -1 "tensor_prod(M, N)" " k") (("1" (inst-cp -1 "M" " (k - mod(k, length(N))) / length(N)") (("1" (inst -1 "N" " mod(k, length(N))") (("1" (ground) nil nil) ("2" (lemma "mod_pos") (("2" (inst?) (("1" (flatten) nil nil) ("2" (typepred (N)) (("2" (expand "rows") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "mod_int" ("k" "k" "n" "rows(N)")) (("2" (expand "rows") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "mod_pos" ("i" "k" "m" "rows(N)")) (("2" (flatten) nil nil)) nil) ("3" (lemma "mod_int" ("k" "k" "n" "rows(N)")) (("3" (propax) nil nil)) nil)) nil)) nil) ("3" (skeep) (("3" (typepred (n)) (("3" (case-replace "length(RowToMat(tensor_prod(M, N), k))=1") (("1" (case-replace "n=0") (("1" (expand "nth") (("1" (case "FORALL(A:PosFullMatrix, kk:below(rows(A))): rows(RowToMat(A, kk)) = 1") (("1" --> -------------------- --> maximum size reached --> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.983Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26