Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale sprachen/PVS/linear_algebra/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: matrix_lemmas.prf Sprache: Lisp

Original von: PVS^©

(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):
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.