|
(linear_dependence
(zerow_TCC1 0
(zerow_TCC1-1 nil 3620493442
("" (skeep)
(("" (splash +)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (flatten)
(("3" (skeep)
(("3" (case "i=0")
(("1" (case "j=0")
(("1" (grind) nil nil)
("2" (typepred (j)) (("2" (grind) nil nil)) nil))
nil)
("2" (grind)
(("2" (typepred (i)) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, 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)
(real nonempty-type-from-decl nil reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" 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 "[T, T -> boolean]" equalities nil)
(length def-decl "nat" list_props nil)
(VectorN type-eq-decl nil matrices nil)
(zero const-decl "VectorN(n)" matrices nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(null adt-constructor-decl "(null?)" list_adt nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(rows const-decl "nat" matrices nil)
(Matrix 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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/")
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(zerow_dim 0
(zerow_dim-1 nil 3620567942
("" (skeep)
(("" (split 1)
(("1" (expand "rows")
(("1" (ground) (("1" (grind) nil nil)) nil)) nil)
("2" (expand "zerow") (("2" (grind) nil nil)) nil))
nil))
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/")
(zero const-decl "VectorN(n)" matrices nil)
(zerow const-decl "PosFullMatrix" linear_dependence nil)
(length def-decl "nat" list_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(rows const-decl "nat" matrices 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)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs 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))
shostak))
(zecolumn_dim 0
(zecolumn_dim-1 nil 3620568042
("" (skeep)
(("" (expand "zecolumn")
(("" (rewrite "rows_transpose")
(("" (rewrite "columns_transpose")
(("" (lemma "zerow_dim")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((zecolumn const-decl "PosFullMatrix" linear_dependence nil)
(columns_transpose formula-decl nil matrices nil)
(zerow_dim formula-decl nil linear_dependence nil)
(zerow const-decl "PosFullMatrix" linear_dependence 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)
(rows_transpose formula-decl nil matrices nil))
shostak))
(row2mat_TCC1 0
(row2mat_TCC1-1 nil 3620493442
("" (skeep)
(("" (splash)
(("1" (typepred (A))
(("1" (expand "columns")
(("1" (ground)
(("1" (expand "columns")
(("1" (ground)
(("1" (case "length(row(A)(j)) = columns(A)")
(("1" (ground) nil nil)
("2" (ground)
(("2" (rewrite "length_row")
(("2" (typepred (j))
(("2" (expand "rows") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (ground) (("2" (grind) nil nil)) nil)
("3" (flatten)
(("3" (skeep)
(("3" (case "i=0")
(("1" (case-replace "j_1=0")
(("1" (replace -2) (("1" (propax) nil nil)) nil)
("2" (typepred (j_1)) (("2" (ground) nil nil)) nil))
nil)
("2" (typepred (i)) (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, 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)
(real nonempty-type-from-decl nil reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(Vector type-eq-decl nil matrices nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
(Matrix type-eq-decl nil matrices 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)
(row const-decl "Vector" matrices 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)
(null adt-constructor-decl "(null?)" list_adt nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(length_row formula-decl nil matrices nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(length_singleton formula-decl nil more_list_props "structures/"))
nil))
(row2mat_dim 0
(row2mat_dim-1 nil 3620568149
("" (skeep)
(("" (typepred (A))
(("" (split 1)
(("1" (grind) nil nil)
("2" (typepred "row2mat(A, j)")
(("2" (lemma "matrices.length_row")
(("2" (inst-cp -1 "A" "j")
(("2" (split -2)
(("1" (replace -1 :dir rl)
(("1" (typepred "columns(row2mat(A,j))")
(("1" (split -2)
(("1" (flatten) (("1" (ground) nil nil)) nil)
("2" (skeep)
(("2" (case "i=0")
(("1" (replace -1)
(("1" (replace -2 :dir rl)
(("1" (grind) nil nil)) nil))
nil)
("2" (typepred (i))
(("2" (hide-all-but (-1 1))
(("2"
(ground)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred (j))
(("2" (hide-all-but (-1 1)) (("2" (grind) nil nil))
nil))
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)
(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)
(list type-decl nil list_adt 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
(length_row formula-decl nil matrices nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(row2mat const-decl "PosFullMatrix" linear_dependence nil)
(row const-decl "Vector" matrices nil))
shostak))
(sum_rows_TCC1 0
(sum_rows_TCC1-1 nil 3620493442
("" (skeep)
(("" (splash +)
(("1" (rewrite "columns_add")
(("1" (rewrite "columns_scal") (("1" (ground) nil nil)) nil))
nil)
("2" (rewrite "rows_add")
(("2" (rewrite "rows_scal") (("2" (ground) nil nil)) nil)) nil)
("3" (flatten)
(("3" (typepred "(M + f(j) * row2mat(A, j))")
(("3" (skeep)
(("3" (inst-cp - "i")
(("3" (inst - "j_1") (("3" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, 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)
(real nonempty-type-from-decl nil reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(Matrix type-eq-decl nil matrices nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(length def-decl "nat" list_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(rows const-decl "nat" matrices nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props 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)
(MatrixMN type-eq-decl nil matrices nil)
(entry const-decl "real" matrices nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl
"{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
matrices nil)
(FullMatrix type-eq-decl nil matrices nil)
(> const-decl "bool" reals nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "{A: MatrixMN(rows(M), columns(M)) |
FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
nil)
(row2mat const-decl "PosFullMatrix" linear_dependence nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(columns_scal formula-decl nil 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)
(columns_add formula-decl nil matrices nil)
(rows_scal formula-decl nil matrices nil)
(rows_add formula-decl nil matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(sum_rows_TCC2 0
(sum_rows_TCC2-1 nil 3620493442 ("" (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)
(int_minus_int_is_int application-judgement "int" integers 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rows const-decl "nat" matrices nil))
nil))
(sum_rows_TCC3 0
(sum_rows_TCC3-2 nil 3620570095
("" (skeep)
(("" (splash +)
(("1" (rewrite "columns_add")
(("1" (rewrite "columns_scal") (("1" (ground) nil nil)) nil))
nil)
("2" (rewrite "rows_add")
(("2" (rewrite "rows_scal") (("2" (ground) nil nil)) nil)) nil)
("3" (flatten)
(("3" (typepred "(M + f(j) * row2mat(A, j))")
(("3" (skeep)
(("3" (inst-cp - "i")
(("3" (inst - "j_1") (("3" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, 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)
(real nonempty-type-from-decl nil reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(Matrix type-eq-decl nil matrices nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(length def-decl "nat" list_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(rows const-decl "nat" matrices nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props 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)
(MatrixMN type-eq-decl nil matrices nil)
(entry const-decl "real" matrices nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl
"{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
matrices nil)
(FullMatrix type-eq-decl nil matrices nil)
(> const-decl "bool" reals nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "{A: MatrixMN(rows(M), columns(M)) |
FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
nil)
(row2mat const-decl "PosFullMatrix" linear_dependence nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(columns_scal formula-decl nil 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)
(columns_add formula-decl nil matrices nil)
(rows_scal formula-decl nil matrices nil)
(rows_add formula-decl nil matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil)
(sum_rows_TCC3-1 nil 3620493442 ("" (subtype-tcc) nil nil) nil nil))
(sum_rows_TCC4 0
(sum_rows_TCC4-1 nil 3620493442 ("" (termination-tcc) nil nil) nil
nil))
(sum_rows_TCC5 0
(sum_rows_TCC5-1 nil 3620493442 ("" (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)
(int_minus_int_is_int application-judgement "int" integers nil)
(rows const-decl "nat" matrices nil))
nil))
(sum_rows_TCC6 0
(sum_rows_TCC6-1 nil 3620493442 ("" (subtype-tcc) nil nil) nil nil))
(sum_rows_eq 0
(sum_rows_eq-2 "alt-proof" 3620557971
(""
(case "FORALL (n:nat, A,M: PosFullMatrix, f, g: [nat -> real], j: below(rows(A))):
n=j IMPLIES ((FORALL (k: subrange(0, j)): f(k) = g(k)) IMPLIES
sum_rows(A, f, j, M) =
sum_rows(A, g, j, M))")
(("1" (skeep)
(("1" (inst -1 "j" "A" "M" "f" "g" "j")
(("1" (split -1)
(("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (skeep)
(("1" (replace -1 :dir rl)
(("1" (expand "sum_rows")
(("1" (inst -2 "0")
(("1" (replace -2) (("1" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "sum_rows" 1)
(("2" (lift-if 1)
(("2" (split 1)
(("1" (flatten)
(("1" (inst -4 "j")
(("1" (replace -4) (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (inst-cp -3 "j")
(("2" (replace -4)
(("2"
(inst -1 "A" "M + g(j) * row2mat(A, j)" "f"
"g" "j-1")
(("1" (split -1)
(("1" (propax) nil nil)
("2" (skeep) (("2" (inst -2 "k") nil nil))
nil)
("3" (ground) nil nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(A skolem-const-decl "PosFullMatrix" linear_dependence nil)
(j skolem-const-decl "below(rows(A))" linear_dependence nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(MatrixMN type-eq-decl nil matrices nil)
(entry const-decl "real" matrices nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl
"{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
matrices nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "{A: MatrixMN(rows(M), columns(M)) |
FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
nil)
(row2mat const-decl "PosFullMatrix" linear_dependence nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types 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)
(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)
(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)
(subrange type-eq-decl nil integers nil)
(sum_rows def-decl "PosFullMatrix" linear_dependence nil))
shostak)
(sum_rows_eq-1 nil 3620555529
(""
(case "FORALL (n:nat, A: PosFullMatrix, f, g: [nat -> real], j: below(rows(A))):
n=j IMPLIES ((FORALL (k: subrange(0, j)): f(k) = g(k)) IMPLIES
sum_rows(A, f, j, zerow(columns(A))) =
sum_rows(A, g, j, zerow(columns(A))))")
(("1" (skeep)
(("1" (inst -1 "j" "A" "f" "g" "j")
(("1" (split -1)
(("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (skeep)
(("1" (replace -1 :dir rl)
(("1" (expand "sum_rows")
(("1" (inst -2 "0")
(("1" (replace -2) (("1" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "sum_rows" 1)
(("2" (lift-if 1)
(("2" (split 1)
(("1" (flatten)
(("1" (inst -4 "j")
(("1" (replace -4) (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (inst -3 "j")
(("2" (replace -3)
(("2" (inst -1 "A" "f" "g" "j-1")
(("1" (split -1)
(("1" (ground) (("1" (postpone) nil nil))
nil)
("2" (postpone) nil nil)
("3" (postpone) nil nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(sum_rows_add_start_TCC1 0
(sum_rows_add_start_TCC1-2 nil 3620570216
("" (skeep)
(("" (splash +)
(("1" (rewrite "columns_add") (("1" (ground) nil nil)) nil)
("2" (rewrite "rows_add") (("2" (ground) nil nil)) nil)
("3" (flatten)
(("3" (typepred "(M + N)")
(("3" (skeep)
(("3" (inst-cp - "i")
(("3" (inst - "j_1") (("3" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, 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)
(real nonempty-type-from-decl nil reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(Matrix type-eq-decl nil matrices nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(length def-decl "nat" list_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(rows const-decl "nat" matrices nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props 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)
(MatrixMN type-eq-decl nil matrices nil)
(entry const-decl "real" matrices nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl
"{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
matrices nil)
(FullMatrix type-eq-decl nil matrices nil)
(> const-decl "bool" reals nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(columns_add formula-decl nil matrices nil)
(rows_add formula-decl nil matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil)
(sum_rows_add_start_TCC1-1 nil 3620563385 ("" (subtype-tcc) nil nil)
nil nil))
(sum_rows_add_start 0
(sum_rows_add_start-1 nil 3620563440
(""
(case "FORALL (n:nat, A, M, N: PosFullMatrix, f: [nat -> real], j: below(rows(A))):
n=j IMPLIES
sum_rows(A, f, j, M + N) = sum_rows(A, f, j, M) + N")
(("1" (skeep) (("1" (inst -1 "j" "A" "M" "N" "f" "j") nil nil))
nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (skeep)
(("1" (replace -1 :dir rl)
(("1" (expand "sum_rows")
(("1" (ground)
(("1" (lemma "matrix_add_comm")
(("1" (inst -1 "N" "f(0) * row2mat(A, 0)")
(("1" (ground)
(("1" (rewrite "matrix_add_assoc" 1)
(("1" (rewrite "matrix_add_assoc" 1)
(("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "sum_rows" 1)
(("2" (lift-if 1)
(("2" (split 1)
(("1" (flatten) (("1" (ground) nil nil)) nil)
("2" (flatten)
(("2" (hide -2)
(("2" (rewrite "matrix_add_assoc" 2)
(("2" (rewrite "matrix_add_comm" (2 2))
(("2" (rewrite "matrix_add_assoc" 2 :dir rl)
(("2"
(inst -1 "A" "M + f(j) * row2mat(A, j)"
"N" "f" "j-1")
(("1"
(split -1)
(("1" (propax) nil nil)
("2"
(reveal -2)
(("2" (ground) nil nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skeep)
(("3" (splash +)
(("1" (rewrite "columns_add") (("1" (ground) nil nil))
nil)
("2" (rewrite "rows_add") (("2" (ground) nil nil)) nil)
("3" (flatten)
(("3" (skeep)
(("3" (typepred "M+N")
(("3" (inst-cp - "i")
(("3" (inst - "j_1") (("3" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skeep)
(("3" (typepred "M + N")
(("3" (split 1)
(("1" (flatten)
(("1" (skeep)
(("1" (inst-cp -3 "i")
(("1" (inst-cp - "j_1") (("1" (ground) nil nil)) nil))
nil))
nil))
nil)
("2" (ground)
(("2" (rewrite "rows_add") (("2" (ground) nil nil)) nil))
nil)
("3" (rewrite "columns_add") (("3" (ground) nil nil)) nil))
nil))
nil))
nil))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(columns_add formula-decl nil matrices nil)
(rows_add formula-decl nil matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(A skolem-const-decl "PosFullMatrix" linear_dependence nil)
(j skolem-const-decl "below(rows(A))" linear_dependence nil)
(matrix_add_comm formula-decl nil matrices nil)
(matrix_add_assoc formula-decl nil matrices nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "{A: MatrixMN(rows(M), columns(M)) |
FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
nil)
(row2mat const-decl "PosFullMatrix" linear_dependence nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types 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)
(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)
(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)
(sum_rows def-decl "PosFullMatrix" linear_dependence nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(MatrixMN type-eq-decl nil matrices nil)
(entry const-decl "real" matrices nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl
"{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
matrices nil))
shostak))
(subtract_same_scal 0
(subtract_same_scal-1 nil 3620554565
("" (skeep)
(("" (typepred "f(j) * row2mat(A, j) - f(j) * row2mat(A, j)")
(("" (typepred "0 * row2mat(A, j)")
(("" (lemma "matrix2array" ("SM" "0*row2mat(A,j)"))
(("1" (replace -1 1)
(("1" (hide -1)
(("1"
(lemma "matrix2array"
("SM"
"(f(j) * row2mat(A, j) - f(j) * row2mat(A, j))"))
(("1" (replace -1 1)
(("1" (hide -1)
(("1" (rewrite "rows_sub")
(("1" (rewrite "columns_sub")
(("1" (expand "max")
(("1" (rewrite "rows_scal")
(("1" (rewrite "rows_scal")
(("1"
(rewrite "columns_scal")
(("1"
(rewrite "columns_scal")
(("1"
(lemma "form_matrix_eq")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(hide -1)
(("1"
(split -1)
(("1" (propax) nil nil)
("2"
(skeep)
(("2"
(inst -6 "i" "j_1")
(("2"
(inst -10 "i" "j_1")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (skeep)
(("2" (inst-cp -7 "i")
(("2" (inst -7 "j_1") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (ground)
(("2" (skeep)
(("2" (inst-cp -3 "i")
(("2" (inst -3 "j_1") (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((row2mat const-decl "PosFullMatrix" linear_dependence 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(M)) |
FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl
"{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) - entry(N)(i, j)}"
matrices nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
(= const-decl "[T, T -> boolean]" equalities 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)
(list type-decl nil list_adt 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)
(matrix2array formula-decl nil matrices nil)
(rows_sub 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_times_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(form_matrix_eq formula-decl nil matrices nil)
(columns_scal formula-decl nil matrices nil)
(rows_scal formula-decl nil matrices nil)
(columns_sub formula-decl nil matrices nil))
shostak))
(sum_lem_prep_TCC1 0
(sum_lem_prep_TCC1-1 nil 3620563013 ("" (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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(rows const-decl "nat" matrices nil))
nil))
(sum_lem_prep 0
(sum_lem_prep-1 nil 3620565983
(""
(case "FORALL (n:nat, A, M: PosFullMatrix, f: [nat -> real], j: below(rows(A)),
k: below(1 + j)):
n=j IMPLIES
sum_rows(A, f WITH [k := 0], j, M) =
sum_rows(A, f, j, M) - f(k) * row2mat(A, k)")
(("1" (skeep) (("1" (inst -1 "j" "A" "M" "f" "j" "k") nil nil))
nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (skeep)
(("1" (replace -1 :dir rl)
(("1" (expand "sum_rows")
(("1" (typepred (k))
(("1" (case-replace "k=0")
(("1" (simplify 1)
(("1" (expand "-")
(("1" (expand "sub")
(("1" (rewrite "matrix_add_assoc" 1)
(("1" (lemma "subtract_same_scal")
(("1" (inst?)
(("1"
(expand "-")
(("1"
(expand "sub")
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (expand "sum_rows" 1)
(("2" (lift-if 1)
(("2" (split 1)
(("1" (flatten) (("1" (ground) nil nil)) nil)
("2" (flatten)
(("2" (split 2)
(("1" (flatten)
(("1" (lemma "sum_rows_eq")
(("1"
(inst -1 "A" "M + 0 * row2mat(A, j)"
"f WITH [k := 0]" "f" "j-1")
(("1" (split -1)
(("1"
(replace -1)
(("1"
(replace -2 1 :dir rl)
(("1"
(expand "-" 1)
(("1"
(expand "sub")
(("1"
(rewrite
"sum_rows_add_start"
1
:dir
rl)
(("1"
(rewrite
"matrix_add_assoc"
1)
(("1"
(lemma
"subtract_same_scal")
(("1"
(inst -1 "A" "f" "j")
(("1"
(expand "-")
(("1"
(expand "sub")
(("1"
(replace -1)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide (2 3))
(("2"
(splash +)
(("1"
(flatten)
(("1"
(typepred
"-1 * (f(j) * row2mat(A, j))")
(("1"
(skeep)
(("1"
(inst-cp - "i")
(("1"
(inst - "j_1!1")
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "columns_scal")
(("2"
(rewrite
"columns_scal")
(("2"
(lemma "row2mat_dim")
(("2"
(inst?)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(rewrite "rows_scal")
(("3"
(rewrite "rows_scal")
(("3"
(lemma "row2mat_dim")
(("3"
(inst?)
(("3"
(ground)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(flatten)
(("4"
(typepred
"-1 * (f(j) * row2mat(A, j))")
(("4"
(skeep)
(("4"
(inst-cp - "i")
(("4"
(inst - "j_1!1")
(("4"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skeep)
(("2"
(typepred (k_1))
(("2"
(ground)
(("2"
(replace -3)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (inst?)
(("1" (split -1)
(("1" (propax) nil nil)
("2" (ground) nil nil))
nil)
("2" (ground) nil nil)
("3" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sum_rows_eq formula-decl nil linear_dependence nil)
(rows_scal formula-decl nil matrices nil)
(columns_scal formula-decl nil matrices nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.39 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.
|
