|
(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)
(("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.28 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.
|
