|
|
|
|
Quelle matrix_lemmas.prf
Sprache: Lisp
|
|
(matrix_lemmas (matrix_prod_zero 0 (matrix_prod_zero-1 nil 3543746245 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (expand "*") (("" (expand "zero") (("" (lemma "sigma_zero[below[A!1`cols]]") (("1" (inst -1 "A!1`cols-1" "0") nil nil) ("2" (skosimp) (("2" (typepred "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (Index type-eq-decl nil vectors "vectors/") (zero const-decl "Vector" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (comp_zero formula-decl nil vectors "vectors/") (sigma_zero formula-decl nil sigma "reals/") (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_nat application-judgement "nat" vectors "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (minus_rows 0 (minus_rows-1 nil 3543731935 ("" (skeep) (("" (grind) nil nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "Matrix" matrices nil)) shostak)) (minus_cols 0 (minus_cols-1 nil 3543735462 ("" (skosimp) (("" (grind) nil nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "Matrix" matrices nil)) shostak)) (transpose_rows 0 (transpose_rows-1 nil 3542467523 ("" (skosimp) (("" (grind) nil nil)) nil) ((transpose const-decl "Matrix" matrices nil)) shostak)) (transpose_cols 0 (transpose_cols-1 nil 3542467532 ("" (skosimp) (("" (grind) nil nil)) nil) ((transpose const-decl "Matrix" matrices nil)) shostak)) (product_rows_TCC1 0 (product_rows_TCC1-1 nil 3542479780 ("" (subtype-tcc) nil nil) nil nil)) (product_rows 0 (product_rows-1 nil 3542479864 ("" (skosimp) (("" (grind) nil nil)) nil) ((* const-decl "Matrix" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (product_cols 0 (product_cols-1 nil 3542480056 ("" (skosimp) (("" (grind) nil nil)) nil) ((* const-decl "Matrix" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (product_rows2_TCC1 0 (product_rows2_TCC1-1 nil 3543297472 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (product_rows2 0 (product_rows2-1 nil 3543297499 ("" (skosimp) (("" (lemma "product_rows") (("" (inst -1 "A!1*B!1" "C!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "product_rows") (("1" (inst -1 "A!1" "B!1") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "product_cols") (("2" (inst -1 "A!1" "B!1") (("2" (replace -1 1) (("2" (hide -1) (("2" (typepred "C!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_rows formula-decl nil matrix_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (product_cols formula-decl nil matrix_lemmas nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (A!1 skolem-const-decl "Matrix" matrix_lemmas nil) (B!1 skolem-const-decl "{B: Matrix | B`rows = A!1`cols}" matrix_lemmas nil) (C!1 skolem-const-decl "{C: Matrix | C`rows = B!1`cols}" matrix_lemmas nil) (* const-decl "Matrix" matrices nil)) shostak)) (product_cols2 0 (product_cols2-1 nil 3543297777 ("" (skosimp) (("" (lemma "product_cols") (("" (inst -1 "A!1*B!1" "C!1") (("" (hide 2) (("" (lemma "product_cols") (("" (inst -1 "A!1" "B!1") (("" (replace -1 1) (("" (typepred "C!1") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_cols formula-decl nil matrix_lemmas nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (A!1 skolem-const-decl "Matrix" matrix_lemmas nil) (B!1 skolem-const-decl "{B: Matrix | B`rows = A!1`cols}" matrix_lemmas nil) (C!1 skolem-const-decl "{C: Matrix | C`rows = B!1`cols}" matrix_lemmas nil) (* const-decl "Matrix" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil)) shostak)) (product_rows3_TCC1 0 (product_rows3_TCC1-1 nil 3543414339 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (product_rows3 0 (product_rows3-1 nil 3543414344 ("" (skosimp) (("" (lemma "product_rows2") (("" (inst -1 "A!1*B!1" "C!1" "D!1") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_rows") (("1" (inst -1 "A!1" "B!1") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "product_cols") (("2" (inst -1 "A!1" "B!1") (("2" (replace -1) (("2" (hide -1) (("2" (typepred "C!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_rows2 formula-decl nil matrix_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (product_cols formula-decl nil matrix_lemmas nil) (product_rows formula-decl nil matrix_lemmas nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (A!1 skolem-const-decl "Matrix" matrix_lemmas nil) (B!1 skolem-const-decl "{B: Matrix | B`rows = A!1`cols}" matrix_lemmas nil) (C!1 skolem-const-decl "{C: Matrix | C`rows = B!1`cols}" matrix_lemmas nil) (* const-decl "Matrix" matrices nil)) shostak)) (product_cols3 0 (product_cols3-1 nil 3543425970 ("" (skosimp) (("" (lemma "product_cols2") (("" (inst -1 "A!1*B!1" "C!1" "D!1") (("" (lemma "product_cols") (("" (inst -1 "A!1" "B!1") (("" (replace -1 1) (("" (typepred "C!1") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_cols2 formula-decl nil matrix_lemmas nil) (product_cols formula-decl nil matrix_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (A!1 skolem-const-decl "Matrix" matrix_lemmas nil) (B!1 skolem-const-decl "{B: Matrix | B`rows = A!1`cols}" matrix_lemmas nil) (C!1 skolem-const-decl "{C: Matrix | C`rows = B!1`cols}" matrix_lemmas nil) (* const-decl "Matrix" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil)) shostak)) (product_rows4_TCC1 0 (product_rows4_TCC1-1 nil 3543414462 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (product_rows4 0 (product_rows4-1 nil 3543414498 ("" (skosimp) (("" (lemma "product_rows3") (("" (inst -1 "A!1*B!1" "C!1" "D!1" "E!1") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_rows") (("1" (inst -1 "A!1" "B!1") nil nil)) nil)) nil)) nil) ("2" (lemma "product_cols") (("2" (inst -1 "A!1" "B!1") (("2" (replace -1) (("2" (typepred "C!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_rows3 formula-decl nil matrix_lemmas nil) (product_cols formula-decl nil matrix_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (product_rows formula-decl nil matrix_lemmas nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (A!1 skolem-const-decl "Matrix" matrix_lemmas nil) (B!1 skolem-const-decl "{B: Matrix | B`rows = A!1`cols}" matrix_lemmas nil) (C!1 skolem-const-decl "{C: Matrix | C`rows = B!1`cols}" matrix_lemmas nil) (* const-decl "Matrix" matrices nil)) shostak)) (product_cols4 0 (thm "finished" 3543426202 ("" (skosimp) (("" (lemma "product_cols3") (("" (inst -1 "A!1*B!1" "C!1" "D!1" "E!1") (("" (lemma "product_cols") (("" (inst -1 "A!1" "B!1") (("" (replace -1) (("" (typepred "C!1") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_cols3 formula-decl nil matrix_lemmas nil) (product_cols formula-decl nil matrix_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (A!1 skolem-const-decl "Matrix" matrix_lemmas nil) (B!1 skolem-const-decl "{B: Matrix | B`rows = A!1`cols}" matrix_lemmas nil) (C!1 skolem-const-decl "{C: Matrix | C`rows = B!1`cols}" matrix_lemmas nil) (* const-decl "Matrix" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil)) shostak) (product_cols4-1 nil 3543426080 ("" (skosimp) (("" (lemma "product_cols3") (("" (inst -1 "A!1*B!1" "C!1" "D!1" "E!1") (("1" (replace -1 1) (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ((Matrix type-eq-decl nil matrices nil)) shostak)) (inverse_ident_TCC1 0 (inverse_ident_TCC1-1 nil 3541004541 ("" (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) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (* const-decl "Matrix" matrices nil) (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (inverse_ident 0 (inverse_ident-1 nil 3541141862 ("" (skolem-typepred) (("" (expand "square?") (("" (expand "invertible?") (("" (skolem-typepred) (("" (expand "square?") (("" (expand "inverse") (("" (typepred "the! (N: Square | N`rows = N!1`rows): inverse?(N!1)(N)") (("1" (hide -1 -2) (("1" (lemma "inverse_unique") (("1" (inst-cp -1 "N!1" "the! (N: Square | (N`rows = N!1`rows)): inverse?(N!1)(N)" "N!2") (("1" (replace -2 :hide? t) (("1" (expand "inverse?") (("1" (flatten) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "singleton?") (("2" (lemma "inverse_unique") (("2" (inst -1 "N!1" _ _) (("2" (inst 1 "N!2") (("2" (skolem-typepred) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "singleton?") (("2" (lemma "inverse_unique") (("2" (inst -1 "N!1" _ _) (("2" (inst 1 "N!2") (("2" (skolem-typepred) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (N!1 skolem-const-decl "(invertible?)" matrix_lemmas nil) (inverse_unique formula-decl nil matrices nil) (set type-eq-decl nil sets nil) (singleton? const-decl "bool" sets nil) (the const-decl "(p)" sets nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (ident_inverse_TCC1 0 (ident_inverse_TCC1-1 nil 3541004884 ("" (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) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (* const-decl "Matrix" matrices nil) (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (ident_inverse 0 (ident_inverse-1 nil 3541232876 ("" (skolem-typepred) (("" (expand "square?") (("" (expand "invertible?") (("" (skolem-typepred) (("" (expand "square?") (("" (expand "inverse") (("" (typepred "the! (N: Square | N`rows = N!1`rows): inverse?(N!1)(N)") (("1" (hide -1 -2) (("1" (lemma "inverse_unique") (("1" (inst-cp -1 "N!1" "the! (N: Square | (N`rows = N!1`rows)): inverse?(N!1)(N)" "N!2") (("1" (replace -2 :hide? t) (("1" (expand "inverse?") (("1" (flatten) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "singleton?") (("2" (lemma "inverse_unique") (("2" (inst -1 "N!1" _ _) (("2" (inst 1 "N!2") (("2" (skolem-typepred) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "singleton?") (("2" (lemma "inverse_unique") (("2" (inst -1 "N!1" _ _) (("2" (inst 1 "N!2") (("2" (skolem-typepred) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (N!1 skolem-const-decl "(invertible?)" matrix_lemmas nil) (inverse_unique formula-decl nil matrices nil) (set type-eq-decl nil sets nil) (singleton? const-decl "bool" sets nil) (the const-decl "(p)" sets nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (ident_mat_prod_TCC1 0 (ident_mat_prod_TCC1-1 nil 3542987349 ("" (subtype-tcc) nil nil) ((I const-decl "(identity?)" matrices nil)) nil)) (ident_mat_prod_TCC2 0 (ident_mat_prod_TCC2-1 nil 3542987349 ("" (subtype-tcc) nil nil) ((I const-decl "(identity?)" matrices nil)) nil)) (ident_mat_prod 0 (thm "finished" 3542989769 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (expand "*") (("" (typepred "x!2") (("" (expand "I" -1) (("" (lemma "sigma_middle[below[matrices.I(n!1)`cols]]") (("1" (inst -1 "_" "_" "_" "0") (("1" (inst -1 "_" "_" "x!2") (("1" (inst -1 " LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k)" " matrices.I(n!1)`cols - 1") (("1" (assert) (("1" (case " matrices.I(n!1)`cols=n!1") (("1" (replace -1 -2) (("1" (hide -1) (("1" (assert) (("1" (case " sigma(0, n!1 - 1,
LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k))= sigma(0, matrices.I(n!1)`cols - 1,
LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k))") (("1" (replace -1 -2) (("1" (hide -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (case " sigma(0, x!2 - 1,
LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k))=0") (("1" (replace -1) (("1" (hide -1) (("1" (case " sigma(1 + x!2, n!1 - 1,
LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k))=0") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "I") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma " sigma_restrict_eq_0[below(matrices.I(n!1)`cols)]") (("2" (inst -1 "LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k)" "n!1 - 1" "1 + x!2") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (expand "I") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_restrict_eq_0[ below(matrices.I(n!1)`cols)]") (("2" (inst -1 " LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k)" "x!2-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (expand "I") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (case "n!1= matrices.I(n!1)`cols") (("1" (name "dd" " LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k)") (("1" (replace -1) (("1" (hide -1) (("1" (name "ee" " sigma(0, matrices.I(n!1)`cols - 1, dd)") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (expand "ee") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skosimp) (("3" (typepred "k!1") (("3" (expand "I") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "I") (("2" (typepred "y!1") (("2" (expand "I") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (identity? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (Index type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_high type-eq-decl nil sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sigma def-decl "real" sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (ee skolem-const-decl "real" matrix_lemmas nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (x!2 skolem-const-decl "Index[matrices.I(n!1)`rows]" matrix_lemmas nil) (n!1 skolem-const-decl "posnat" matrix_lemmas nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (sigma_middle formula-decl nil sigma "reals/") (NOT const-decl "[bool -> bool]" booleans nil)) shostak) (dos "dos" 3542989477 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (expand "*") (("" (typepred "x!2") (("" (expand "I" -1) (("" (lemma "sigma_middle[below[matrices.I(n!1)`cols]]") (("1" (inst -1 "_" "_" "_" "0") (("1" (inst -1 "_" "_" "x!2") (("1" (inst -1 " LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k)" " matrices.I(n!1)`cols - 1") (("1" (assert) (("1" (case " matrices.I(n!1)`cols=n!1") (("1" (replace -1 -2) (("1" (hide -1) (("1" (assert) (("1" (case " sigma(0, n!1 - 1,
LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k))= sigma(0, matrices.I(n!1)`cols - 1,
LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k))") (("1" (replace -1 -2) (("1" (hide -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (case " sigma(0, x!2 - 1,
LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k))=0") (("1" (replace -1) (("1" (hide -1) (("1" (case " sigma(1 + x!2, n!1 - 1,
LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k))=0") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "I") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (case "n!1= matrices.I(n!1)`cols") (("1" (name "dd" " LAMBDA (k: below(matrices.I(n!1)`cols)):
matrices.I(n!1)`matrix(x!2, k) * x!1(k)") (("1" (replace -1) (("1" (hide -1) (("1" (name "ee" " sigma(0, matrices.I(n!1)`cols - 1, dd)") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (expand "ee") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skosimp) (("3" (typepred "k!1") (("3" (expand "I") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "I") (("2" (typepred "y!1") (("2" (expand "I") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_middle formula-decl nil sigma "reals/") (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Vector type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (Index type-eq-decl nil vectors "vectors/") (I const-decl "(identity?)" matrices nil) (identity? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (ident_mat_prod-1 nil 3542986254 ("" (skosimp) (("" (postpone) nil nil)) nil) nil shostak)) (inverse_rows 0 (teo "finish" 3543297183 ("" (skosimp) (("" (lemma "inverse_ident") (("" (inst -1 "N!1") (("" (typepred "N!1") (("" (expand "square?") (("" (hide -2) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inverse_ident formula-decl nil matrix_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (* const-decl "Matrix" matrices nil) (sigma def-decl "real" sigma "reals/") (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil)) shostak) (thm "finished" 3543296828 ("" (skosimp) (("" (lemma "inverse_ident") (("" (inst -1 "N!1") (("" (lemma "product_rows") (("" (inst -1 "inverse(N!1)" "N!1") (("1" (replace -2 -1) (("1" (hide -2) (("1" (expand "I") (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ((inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (sigma def-decl "real" sigma "reals/") (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (inverse_rows-1 nil 3543296524 ("" (skosimp) (("" (postpone) nil nil)) nil) nil shostak)) (inverse_cols 0 (inverse_cols-1 nil 3543299563 ("" (skosimp) (("" (typepred "N!1") (("" (hide -2) (("" (expand "square?") (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (* const-decl "Matrix" matrices nil) (sigma def-decl "real" sigma "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (transp_ident 0 (transp_ident-1 nil 3542536489 ("" (skosimp) (("" (apply-extensionality) (("1" (hide 2) (("1" (lemma "transpose_cols") (("1" (inst -1 "I(n!1)") (("1" (replace -1) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "transpose_rows") (("2" (inst -1 "I(n!1)") (("2" (replace -1 1) (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (apply-extensionality) (("3" (hide 2) (("3" (case "x!1=x!2") (("1" (case "x!1/=x!2") (("1" (assert) nil nil) ("2" (hide 1) (("2" (expand "I") (("2" (replace -1 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "x!1/=x!2") (("1" (hide 1) (("1" (expand "I") (("1" (grind) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (I const-decl "(identity?)" matrices nil) (identity? const-decl "bool" matrices nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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_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) (transpose const-decl "Matrix" matrices nil) (transpose_cols formula-decl nil matrix_lemmas nil) (transpose_rows formula-decl nil matrix_lemmas nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil)) shostak)) (transp_inv_TCC1 0 (thm "finished" 3542536447 ("" (skosimp) (("" (split) (("1" (typepred "M!1") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil) ("2" (typepred "M!1") (("2" (expand "invertible?" 1) (("2" (inst 1 "transpose(inverse(M!1))") (("2" (split) (("1" (hide -2) (("1" (expand "square?") (("1" (lemma "transpose_cols") (("1" (inst -1 "inverse(M!1)") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "transpose_rows") (("1" (inst -1 "inverse(M!1)") (("1" (replace -1 1) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "transpose_rows") (("2" (inst -1 "inverse(M!1)") (("2" (replace -1 1) (("2" (hide -1) (("2" (expand "square?" -1) (("2" (hide -2) (("2" (lemma "transpose_rows") (("2" (inst -1 "M!1") (("2" (replace -1 1) (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "inverse?") (("3" (split) (("1" (lemma "transpose_product") (("1" (inst -1 "inverse(M!1)" "M!1") (("1" (swap-rel -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "inverse_ident") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1 -3) (("1" (expand "square?") (("1" (lemma "transp_ident") (("1" (inst -1 "M!1`rows") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "transpose_rows") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 2) (("2" (expand "square?") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "square?") (("2" (hide -2) (("2" (lemma "transpose_product") (("2" (inst -1 "M!1" "inverse(M!1)") (("1" (swap-rel -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "ident_inverse") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "transp_ident") (("1" (inst -1 "M!1`rows") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "transpose_rows") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((transpose const-decl "Matrix" matrices nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (sigma def-decl "real" sigma "reals/") (I const-decl "(identity?)" matrices nil) (* const-decl "Matrix" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (transpose_rows formula-decl nil matrix_lemmas nil) (transpose_cols formula-decl nil matrix_lemmas nil) (inverse_ident formula-decl nil matrix_lemmas nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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_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) (transp_ident formula-decl nil matrix_lemmas nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (transpose_product formula-decl nil matrices nil) (ident_inverse formula-decl nil matrix_lemmas nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (M!1 skolem-const-decl "(invertible?)" matrix_lemmas nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil)) shostak) (falta "falta" 3542527260 ("" (skosimp) (("" (split) (("1" (typepred "M!1") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil) ("2" (typepred "M!1") (("2" (postpone) nil nil)) nil)) nil)) nil) ((inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (transpose_product formula-decl nil matrices nil) (I const-decl "(identity?)" matrices nil) (sigma def-decl "real" sigma "reals/") (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (transpose const-decl "Matrix" matrices nil)) shostak) (transp_inv_TCC1-1 nil 3542520112 ("" (subtype-tcc) nil nil) nil nil)) (transp_inv 0 (thm "finished" 3542535961 ("" (skosimp) (("" (lemma "inverse_unique") (("" (inst -1 "transpose(M!1)" " transpose(inverse(M!1))" " inverse((transpose(M!1)))") (("1" (hide 2) (("1" (expand "inverse?") (("1" (split) (("1" (lemma "ident_inverse") (("1" (inst -1 "transpose(M!1)") nil nil)) nil) ("2" (lemma "inverse_ident") (("2" (inst -1 "transpose(M!1)") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (typepred "M!1") (("1" (expand "square?") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (typepred "M!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil) ("3" (expand "inverse?") (("3" (split) (("1" (lemma "transpose_product") (("1" (inst -1 "inverse(M!1)" "M!1") (("1" (swap-rel -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "inverse_ident") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (typepred "M!1") (("1" (hide -2) (("1" (expand "square?") (("1" (lemma "transp_ident") (("1" (inst -1 "M!1`rows") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "transpose_rows") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "M!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "transpose_product") (("2" (inst -1 "M!1" "inverse(M!1)") (("1" (swap-rel -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "ident_inverse") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "transp_ident") (("1" (inst -1 "M!1`rows") (("1" (replace -1 1) (("1" (hide -1) (("1" (typepred "M!1") (("1" (expand "square?") (("1" (hide -2) (("1" (lemma "transpose_rows") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "M!1") (("2" (hide -2) (("2" (expand "square?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inverse_unique formula-decl nil matrices nil) (transpose_product formula-decl nil matrices nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (transp_ident formula-decl nil matrix_lemmas nil) (transpose_rows formula-decl nil matrix_lemmas 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (I const-decl "(identity?)" matrices nil) (* const-decl "Matrix" matrices nil) (sigma def-decl "real" sigma "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (ident_inverse formula-decl nil matrix_lemmas nil) (inverse_ident formula-decl nil matrix_lemmas nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (M!1 skolem-const-decl "(invertible?)" matrix_lemmas nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (transpose const-decl "Matrix" matrices nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil)) shostak) (mitad "mitad" 3542535856 ("" (skosimp) (("" (lemma "inverse_unique") (("" (inst -1 "transpose(M!1)" " transpose(inverse(M!1))" " inverse((transpose(M!1)))") (("1" (hide 2) (("1" (postpone) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (typepred "M!1") (("1" (expand "square?") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (typepred "M!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil) ("3" (expand "inverse?") (("3" (split) (("1" (lemma "transpose_product") (("1" (inst -1 "inverse(M!1)" "M!1") (("1" (swap-rel -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "inverse_ident") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (typepred "M!1") (("1" (hide -2) (("1" (expand "square?") (("1" (lemma "transp_ident") (("1" (inst -1 "M!1`rows") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "transpose_rows") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "M!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "transpose_product") (("2" (inst -1 "M!1" "inverse(M!1)") (("1" (swap-rel -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "ident_inverse") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "transp_ident") (("1" (inst -1 "M!1`rows") (("1" (replace -1 1) (("1" (hide -1) (("1" (typepred "M!1") (("1" (expand "square?") (("1" (hide -2) (("1" (lemma "transpose_rows") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (replace -1 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "M!1") (("2" (hide -2) (("2" (expand "square?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (transpose const-decl "Matrix" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (sigma def-decl "real" sigma "reals/") (I const-decl "(identity?)" matrices nil) (transpose_product formula-decl nil matrices nil) (inverse_unique formula-decl nil matrices nil)) shostak) (casi "casi" 3542535497 ("" (skosimp) (("" (lemma "inverse_unique") (("" (inst -1 "transpose(M!1)" " transpose(inverse(M!1))" " inverse((transpose(M!1)))") (("1" (hide 2) (("1" (postpone) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (typepred "M!1") (("1" (expand "square?") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (typepred "M!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil) ("3" (expand "inverse?") (("3" (split) (("1" (lemma "transpose_product") (("1" (inst -1 "inverse(M!1)" "M!1") (("1" (swap-rel -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "inverse_ident") (("1" (inst -1 "M!1") (("1" (replace -1 1) (("1" (hide -1) (("1" (typepred "M!1") (("1" (hide -2) (("1" (expand "square?") (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "M!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (encamino "encamino" 3542535323 ("" (skosimp) (("" (lemma "inverse_unique") (("" (inst -1 "transpose(M!1)" " transpose(inverse(M!1))" " inverse((transpose(M!1)))") (("1" (hide 2) (("1" (postpone) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (typepred "M!1") (("1" (expand "square?") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (typepred "M!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil) ("3" (expand "inverse?") (("3" (split) (("1" (lemma "transpose_product") (("1" (inst -1 "inverse(M!1)" "M!1") (("1" (swap-rel -1) (("1" (replace -1 1) (("1" (hide -1) (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "M!1") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (transp_inv-1 nil 3542520112 ("" (skolem-typepred) (("" (expand "square?") (("" (assert) (("" (hide -1) (("" (expand "invertible?") (("" (skolem-typepred) (("" (expand "square?") (("" (assert) (("" (hide -1 -2) (("" (expand "inverse") (("" (typepred "the! (N: Square | N`rows = (transpose(M!1))`rows):
inverse?((transpose(M!1)))(N)") (("1" (lemma "inverse_unique") (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (invar_inverse_TCC1 0 (thm "finished" 3541011468 ("" (skosimp) (("" (typepred "N!1") (("" (expand "square?") (("" (hide -2) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (* const-decl "Matrix" matrices nil) (sigma def-decl "real" sigma "reals/")) shostak) (skosimp "skosimp" 3541004602 ("" (skosimp) (("" (postpone) nil nil)) nil) ((invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (sigma def-decl "real" sigma "reals/")) shostak) (invar_inverse_TCC1-1 nil 3540814422 ("" (subtype-tcc) nil nil) ((inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil)) nil)) (invar_inverse 0 (thm "finished" 3541251433 ("" (skosimp) (("" (lemma "inverse_ident") (("" (inst -1 "N!1") (("" (replace -1 1) (("" (lemma "right_mult_ident") (("" (inst -1 "A!1" "I(N!1`rows)") (("" (hide -1 2) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inverse_ident formula-decl nil matrix_lemmas nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (identity? const-decl "bool" matrices 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (I const-decl "(identity?)" matrices nil) (N!1 skolem-const-decl "{N: (invertible?) | A!1`cols = N`rows}" matrix_lemmas nil) (A!1 skolem-const-decl "Matrix" matrix_lemmas nil) (right_mult_ident formula-decl nil matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil)) shostak) (invar_inverse-1 nil 3540814422 ("" (skeep) (("" (lemma "iso_inv") (("" (inst - "N" "n") (("" (split) (("1" (flatten) (("1" (replace -1) (("1" (lemma "right_mult_ident") (("1" (inst -1 "A" "I(n)") (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N") (("2" (propax) nil nil)) nil)) nil) ("3" (typepred "N") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((identity? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (right_mult_ident formula-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (casi "casi" 3541003200 ("" (skosimp) (("" (case "inverse(N!1) * N!1=I(N!1`rows)") (("1" (replace -1 1) (("1" (lemma "right_mult_ident") (("1" (inst -1 "A!1" " I(N!1`rows)") (("1" (typepred "N!1") (("1" (hide -1 -2 -4 2) (("1" (replace -1 1) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil)) nil)) nil) ((right_mult_ident formula-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (identity? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil)) shostak) (invar_inverse-1 nil 3540814422 ("" (skosimp) (("" (expand "inverse") (("" (expand "inverse?") (("" (postpone) nil nil)) nil)) nil)) nil) nil shostak)) (invar_inverse_left_TCC1 0 (thm "finished" 3541011529 ("" (skosimp) (("" (typepred "N!1") (("" (expand "square?") (("" (hide -1) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (* const-decl "Matrix" matrices nil) (sigma def-decl "real" sigma "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak) (skosimp "skosimp" 3541004914 ("" (skosimp) (("" (postpone) nil nil)) nil) ((invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (inverse? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (sigma def-decl "real" sigma "reals/")) shostak) (invar_inverse_left_TCC1-1 nil 3540814446 ("" (subtype-tcc) nil nil) ((Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil)) nil)) (invar_inverse_left 0 (thm "finished" 3541251638 ("" (skosimp) (("" (lemma "ident_inverse") (("" (inst -1 "N!1") (("" (replace -1 1) (("" (hide -1) (("" (lemma "left_mult_ident") (("" (inst -1 "B!1" "I(N!1`rows)") (("" (hide 2) (("" (grind) (("" (typepred "N!1") (("" (expand "square?") (("" (hide -2) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ident_inverse formula-decl nil matrix_lemmas nil) (left_mult_ident formula-decl nil matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (B!1 skolem-const-decl "Matrix" matrix_lemmas nil) (N!1 skolem-const-decl "{N: (invertible?) | B!1`rows = N`cols}" matrix_lemmas nil) (I const-decl "(identity?)" matrices nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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_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) (identity? const-decl "bool" matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil)) shostak) (invar_inverse_left-1 nil 3540814447 ("" (skeep) (("" (lemma "iso_inv") (("" (inst - "N" "n") (("" (split) (("1" (flatten) (("1" (replace -2) (("1" (typepred "N") (("1" (lemma "left_mult_ident") (("1" (inst -1 "B" "I(n)") (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "N") (("2" (propax) nil nil)) nil)) nil) ("3" (typepred "N") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((left_mult_ident formula-decl nil matrices nil) (I const-decl "(identity?)" matrices nil) (identity? const-decl "bool" matrices nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (invar_inverse_left-1 nil 3540814447 ("" (skosimp) (("" (case " N!1 * (inverse(N!1))=I(N!1`rows)") (("1" (replace -1 1) (("1" (lemma "left_mult_ident") (("1" (inst -1 "B!1" "I(N!1`rows)") (("1" (hide -1 2) (("1" (grind) (("1" (typepred "N!1") (("1" (expand "square?") (("1" (swap-rel -1) (("1" (replace -1 -3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (postpone) nil nil)) nil)) nil)) nil) ((left_mult_ident formula-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (identity? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil)) shostak)) (simply1_mat_vect_TCC1 0 (thm "finished" 3541011637 ("" (skosimp) (("" (skosimp) (("" (split) (("1" (flatten) (("1" (typepred "N!1") (("1" (expand "square?") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "N!1") (("2" (expand "square?") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma "reals/") (* const-decl "Matrix" matrices nil) (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak) (skosimp "skosimp" 3541003461 ("" (skosimp) (("" (postpone) nil nil)) nil) ((sigma def-decl "real" sigma "reals/") (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil)) shostak) (simply1_mat_vect_TCC1-1 nil 3540814491 ("" (subtype-tcc) nil nil) ((Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (squareMat? const-decl "bool" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (bijective? const-decl "bool" linear_map nil) (Mat type-eq-decl nil matrices nil) (Map_linear type-eq-decl nil linear_map_def nil) (inverse const-decl "Maping" linear_map nil)) nil)) (simply1_mat_vect_TCC2 0 (simply1_mat_vect_TCC2-1 nil 3540814491 ("" (subtype-tcc) nil nil) ((* const-decl "Matrix" matrices nil) (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (simply1_mat_vect 0 (thm "finished" 3541252853 ("" (skosimp) (("" (lemma "invar_inverse") (("" (inst -1 "A!1" "N!1") (("" (replace -1 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((invar_inverse formula-decl nil matrix_lemmas nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil)) shostak) (simply1_mat_vect-1 nil 3540814492 ("" (skeep) (("" (lemma "iso_inv") (("" (inst - "N" "n") (("" (typepred "N") (("" (split) (("1" (flatten) (("1" (replace -1) (("1" (lemma "right_mult_ident") (("1" (inst -1 "A" "I(n)") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((invertible? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak)) (simply2_mat_vect_TCC1 0 (simply2_mat_vect_TCC1-1 nil 3540814491 ("" (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) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "Matrix" matrices nil) (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (simply2_mat_vect_TCC2 0 (simply2_mat_vect_TCC2-1 nil 3540814491 ("" (subtype-tcc) nil nil) ((* const-decl "Matrix" matrices nil) (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (simply2_mat_vect_TCC3 0 (thm "finished" 3541011702 ("" (skosimp) (("" (skosimp) (("" (split) (("1" (flatten) (("1" (typepred "N!1") (("1" (expand "square?") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "N!1") (("2" (expand "square?") (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma "reals/") (* const-decl "Matrix" matrices nil) (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak) (skosimp "skosimp" 3541005068 ("" (skosimp) (("" (postpone) nil nil)) nil) ((sigma def-decl "real" sigma "reals/") (I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil) (Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil)) shostak) (simply2_mat_vect_TCC3-1 nil 3540814491 ("" (subtype-tcc) nil nil) ((I const-decl "(identity?)" matrices nil) (inverse? const-decl "bool" matrices nil) (inverse const-decl "{N: Square | N`rows = M`rows}" matrices nil)) nil)) (simply2_mat_vect 0 (th "finished" 3541252897 ("" (skosimp) (("" (lemma "invar_inverse_left") (("" (inst -1 "B!1" "N!1") (("1" (replace -1 1) (("1" (propax) nil nil)) nil) ("2" (typepred "N!1") (("2" (expand "square?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((invar_inverse_left formula-decl nil matrix_lemmas nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (B!1 skolem-const-decl "Matrix" matrix_lemmas nil) (bool nonempty-type-eq-decl nil booleans nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil) (N!1 skolem-const-decl "{N: (invertible?) | B!1`rows = N`rows}" matrix_lemmas nil)) shostak) (simply2_mat_vect-1 nil 3540814503 ("" (skeep) (("" (typepred "N") (("" (lemma "iso_inv") (("" (inst - "N" "n") (("" (split) (("1" (flatten) (("1" (replace -2) (("1" (lemma "left_mult_ident") (("1" (inst -1 "B" "I(n)") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((Matrix type-eq-decl nil matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrices nil)) shostak)) (distr_mat_vect_TCC1 0 (distr_mat_vect_TCC1-1 nil 3540814491 ("" (subtype-tcc) nil nil) ((+ const-decl "Matrix" matrices nil)) nil)) (distr_mat_vect_TCC2 0 (distr_mat_vect_TCC2-1 nil 3540814491 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices 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) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) nil)) (distr_mat_vect_TCC3 0 (distr_mat_vect_TCC3-1 nil 3540814491 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices 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) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) nil)) (distr_mat_vect_TCC4 0 (distr_mat_vect_TCC4-1 nil 3540814491 ("" (subtype-tcc) nil nil) ((+ const-decl "Matrix" matrices nil)) nil)) (distr_mat_vect 0 (teor "fin" 3546579357 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (lemma "comp_distr_add[A!1`rows]") (("" (inst -1 "x!1" "A!1*y!1" "B!1*y!1") (("" (replace -1 1) (("" (hide -1) (("" (expand "*") (("" (typepred "B!1") (("" (lemma "sigma_eq_index") (("" (copy -1) (("" (inst -1 "B!1`cols" "A!1`cols" " LAMBDA (k: below(B!1`cols)): B!1`matrix(x!1, k) * y!1(k)" " LAMBDA (k: below(A!1`cols)): B!1`matrix(x!1, k) * y!1(k)") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (inst -1 " (A!1 + B!1)`cols" "A!1`cols" " LAMBDA (k: below((A!1 + B!1)`cols)):
(A!1 + B!1)`matrix(x!1, k) * y!1(k)" " LAMBDA (k: below(A!1`cols)):
(A!1 + B!1)`matrix(x!1, k) * y!1(k)") (("1" (case "(A!1 + B!1)`cols = A!1`cols") (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (lemma "sigma_sum[below[A!1`cols]]") (("1" (inst -1 " LAMBDA (k: below(A!1`cols)): A!1`matrix(x!1, k) * y!1(k)" "LAMBDA (i: Index[A!1`cols]): B!1`matrix(x!1, i) * y!1(i)" "A!1`cols-1" "0") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[A!1`cols]]") (("1" (inst -1 " LAMBDA (i: Index[A!1`cols]):
(A!1 + B!1)`matrix(x!1, i) * y!1(i)" " LAMBDA (i_1: below[A!1`cols]):
A!1`matrix(x!1, i_1) * y!1(i_1) +
B!1`matrix(x!1, i_1) * y!1(i_1)" "A!1`cols-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "k!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (assert) (("2" (typepred "B!1") (("2" (swap-rel -1) (("2" (replace -1 1) (("2" (typepred "x!1") (("2" (hide -2 -3 -4 -5 -6) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "Matrix" matrices nil) (Index type-eq-decl nil vectors "vectors/") (+ const-decl "real" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (comp_distr_add formula-decl nil vectors "vectors/") (sigma_eq_index formula-decl nil sigma_lemmas nil) (real_times_real_is_real application-judgement "real" reals nil) (A!1 skolem-const-decl "Matrix" matrix_lemmas nil) (B!1 skolem-const-decl "(LAMBDA (N): A!1`rows = N`rows AND A!1`cols = N`cols)" matrix_lemmas nil) (x!1 skolem-const-decl "Index[(A!1 + B!1)`rows]" matrix_lemmas nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil nat_types nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_eq formula-decl nil sigma "reals/") (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (sigma_sum formula-decl nil sigma "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (real_le_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_plus_real_is_real application-judgement "real" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak) (th "finished" 3541263525 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (lemma "comp_distr_add[A!1`rows]") (("" (inst -1 "x!1" "A!1*y!1" "B!1*y!1") (("" (replace -1 1) (("" (hide -1) (("" (expand "*") (("" (typepred "B!1") (("" (expand "same_dim?") (("" (flatten) (("" (lemma "sigma_eq_index") (("" (copy -1) (("" (inst -1 "B!1`cols" "A!1`cols" " LAMBDA (k: below(B!1`cols)): B!1`matrix(x!1, k) * y!1(k)" " LAMBDA (k: below(A!1`cols)): B!1`matrix(x!1, k) * y!1(k)") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (inst -1 " (A!1 + B!1)`cols" "A!1`cols" " LAMBDA (k: below((A!1 + B!1)`cols)):
(A!1 + B!1)`matrix(x!1, k) * y!1(k)" " LAMBDA (k: below(A!1`cols)):
(A!1 + B!1)`matrix(x!1, k) * y!1(k)") (("1" (case "(A!1 + B!1)`cols = A!1`cols") (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (lemma "sigma_sum[below[A!1`cols]]") (("1" (inst -1 " LAMBDA (k: below(A!1`cols)): A!1`matrix(x!1, k) * y!1(k)" "LAMBDA (i: Index[A!1`cols]): B!1`matrix(x!1, i) * y!1(i)" "A!1`cols-1" "0") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[A!1`cols]]") (("1" (inst -1 " LAMBDA (i: Index[A!1`cols]):
(A!1 + B!1)`matrix(x!1, i) * y!1(i)" " LAMBDA (i_1: below[A!1`cols]):
A!1`matrix(x!1, i_1) * y!1(i_1) +
B!1`matrix(x!1, i_1) * y!1(i_1)" "A!1`cols-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "k!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil) ("4" (hide -1 2) (("4" (skosimp) (("4" (typepred "k!1") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (hide -1 2) (("5" (skosimp) (("5" (typepred "x!1") (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_sum formula-decl nil sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (sigma_eq_index formula-decl nil sigma_lemmas nil) (comp_distr_add formula-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (+ const-decl "real" vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (+ const-decl "Matrix" matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (apunto "casi" 3541262721 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (lemma "comp_distr_add[A!1`rows]") (("" (inst -1 "x!1" "A!1*y!1" "B!1*y!1") (("" (replace -1 1) (("" (hide -1) (("" (expand "*") (("" (typepred "B!1") (("" (expand "same_dim?") (("" (flatten) (("" (lemma "sigma_eq_index") (("" (copy -1) (("" (inst -1 "B!1`cols" "A!1`cols" " LAMBDA (k: below(B!1`cols)): B!1`matrix(x!1, k) * y!1(k)" " LAMBDA (k: below(A!1`cols)): B!1`matrix(x!1, k) * y!1(k)") (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (inst -1 " (A!1 + B!1)`cols" "A!1`cols" " LAMBDA (k: below((A!1 + B!1)`cols)):
(A!1 + B!1)`matrix(x!1, k) * y!1(k)" " LAMBDA (k: below(A!1`cols)):
(A!1 + B!1)`matrix(x!1, k) * y!1(k)") (("1" (case "(A!1 + B!1)`cols = A!1`cols") (("1" (assert) (("1" (replace -2 1) (("1" (hide -2) (("1" (lemma "sigma_sum[below[A!1`cols]]") (("1" (inst -1 " LAMBDA (k: below(A!1`cols)): A!1`matrix(x!1, k) * y!1(k)" "LAMBDA (i: Index[A!1`cols]): B!1`matrix(x!1, i) * y!1(i)" "A!1`cols-1" "0") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[A!1`cols]]") (("1" (inst -1 " LAMBDA (i: Index[A!1`cols]):
(A!1 + B!1)`matrix(x!1, i) * y!1(i)" " LAMBDA (i_1: below[A!1`cols]):
A!1`matrix(x!1, i_1) * y!1(i_1) +
B!1`matrix(x!1, i_1) * y!1(i_1)" "A!1`cols-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "k!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (typepred "k!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide -1 2) (("3" (skosimp) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil) ("4" (hide -1 2) (("4" (skosimp) (("4" (typepred "k!1") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (hide -1 2) (("5" (skosimp) (("5" (typepred "x!1") (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_sum formula-decl nil sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (comp_distr_add formula-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (+ const-decl "real" vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (+ const-decl "Matrix" matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (encamino "encamino" 3541258655 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (lemma "comp_distr_add[A!1`rows]") (("" (inst -1 "x!1" "A!1*y!1" "B!1*y!1") (("" (replace -1 1) (("" (hide -1) (("" (expand "*") (("" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (distr_mat_vect-1 nil 3540814516 ("" (skolem-typepred) (("" (expand "same_dim?") (("" (expand "+") (("" (expand "*") (("" (apply-extensionality :hide? t) (("1" (same-name "sigma[below(A!1`cols)]" "sigma[below(B!1`cols)]") (("1" (replace -1 :hide? t) (("1" (flatten) (("1" (replace -2) (("1" (rewrite "sigma_sum[below(B!1`cols)]") (("1" (grind) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil) ("7" (grind) nil nil) ("8" (grind) nil nil) ("9" (grind) nil nil) ("10" (grind) nil nil) ("11" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (distr_vect_mat 0 (thm "finished" 3541254265 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (lemma "comp_distr_add[A!1`rows]") (("" (inst -1 "x!2" "A!1*x!1" "A!1*y!1") (("" (replace -1 1) (("" (hide -1) (("" (expand "*") (("" (lemma "sigma_sum[below[A!1`cols]]") (("1" (inst -1 "LAMBDA (k: below(A!1`cols)): A!1`matrix(x!2, k) * x!1(k)" " LAMBDA (k: below(A!1`cols)): A!1`matrix(x!2, k) * y!1(k)" "A!1`cols-1" "0") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[A!1`cols]]") (("1" (inst -1 " LAMBDA (i: below[A!1`cols]):
A!1`matrix(x!2, i) * x!1(i) + A!1`matrix(x!2, i) * y!1(i)" " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!2, k) * (x!1 + y!1)(k)" "A!1`cols-1" "0") (("1" (case " (FORALL (n: subrange(0, A!1`cols - 1)):
A!1`matrix(x!2, n) * x!1(n) + A!1`matrix(x!2, n) * y!1(n) =
A!1`matrix(x!2, n) * (x!1 + y!1)(n))") (("1" (replace -1 -2) (("1" (propax) nil nil)) nil) ("2" | | |
