| products/sources/formale Sprachen/PVS/matrices/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Groebner_Basis.thy Sprache: LispUntersuchung PVS© |
|
||||||
|
(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" (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" (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" (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" (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 (("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 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 --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.82 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
