| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/linear_algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 289 kB |
|
Quelle ellipsoid.prfSprache: Lisp |
|||||||||||||||
|
(ellipsoid (ellipsoid_TCC1 0 (ellipsoid_TCC1-1 nil 3504869522 ("" (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) (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) (> 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers 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) (SquareMat type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (ellipsoid_TCC2 0 (ellipsoid_TCC2-1 nil 3504869522 ("" (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) (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) (> 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers 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) (SquareMat type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (ellipsoid_TCC3 0 (ellipsoid_TCC3-1 nil 3504869522 ("" (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) (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) (> 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers 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) (SquareMat type-eq-decl nil matrices nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (ellipsoid_TCC4 0 (ellipsoid_TCC4-1 nil 3508764162 ("" (subtype-tcc) nil nil) ((T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (ellipsoid_TCC5 0 (ellipsoid_TCC5-1 nil 3508764162 ("" (subtype-tcc) nil nil) ((T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (ellipsoid_TCC6 0 (ellipsoid_TCC6-1 nil 3508764162 ("" (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) (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) (> 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers 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) (SquareMat type-eq-decl nil matrices 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (* const-decl "real" vectors "vectors/") (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (ellipsoid_TCC7 0 (ellipsoid_TCC7-1 nil 3520826443 ("" (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) (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) (> 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers 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) (SquareMat type-eq-decl nil matrices 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (* const-decl "real" vectors "vectors/") (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (ellipsoid_TCC8 0 (ellipsoid_TCC8-1 nil 3520826443 ("" (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) (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) (> 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers 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) (SquareMat type-eq-decl nil matrices 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (* const-decl "real" vectors "vectors/") (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (ellipsoid_TCC9 0 (ellipsoid_TCC9-1 nil 3520826443 ("" (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) (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) (> 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers 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) (SquareMat type-eq-decl nil matrices 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (* const-decl "real" vectors "vectors/") (transpose 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) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (ellipsoid_TCC10 0 (ellipsoid_TCC10-1 nil 3520826443 ("" (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) (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) (> 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers 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) (SquareMat type-eq-decl nil matrices 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (* const-decl "real" vectors "vectors/") (transpose const-decl "Matrix" 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) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (ellipsoid_TCC11 0 (tcc "tcc" 3520936757 ("" (skosimp) (("" (split) (("1" (grind) nil nil) ("2" (expand "squareMat?") (("2" (assert) (("2" (typepred "M!1") (("2" (typepred "Q!1") (("2" (expand "squareMat?") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "bijec_prod") (("3" (inst?) (("1" (assert) (("1" (split) (("1" (assert) (("1" (typepred "Q!1") (("1" (typepred "M!1") (("1" (expand "square?") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "Q!1") (("2" (typepred "M!1") (("2" (expand "square?") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (lemma "bijec_prod") (("3" (inst?) (("1" (assert) (("1" (split) (("1" (assert) (("1" (hide 2 3) (("1" (typepred "M!1") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (typepred "M!1") (("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil) ("3" (lemma "bijec_transpose") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "M!1") (("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "Q!1") (("2" (typepred "M!1") (("2" (expand "square?") (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((transpose const-decl "Matrix" matrices nil) (* const-decl "Matrix" matrices nil) (square? const-decl "bool" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma "reals/") (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 type-eq-decl nil matrices nil) (number nonempty-type-decl nil numbers 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) (SquareMat type-eq-decl nil matrices nil) (squareMat? const-decl "bool" matrices nil) (M!1 skolem-const-decl "SquareMat(n!1)" ellipsoid nil) (Q!1 skolem-const-decl "SquareMat(n!1)" ellipsoid nil) (n!1 skolem-const-decl "posnat" ellipsoid nil) (= const-decl "[T, T -> boolean]" equalities nil) (bijec_transpose formula-decl nil matrix_operator nil) (bijec_prod formula-decl nil matrix_operator nil)) shostak) (ellipsoid_TCC11-1 nil 3520826443 ("" (subtype-tcc) nil nil) ((transpose const-decl "Matrix" matrices nil) (square? const-decl "bool" matrices nil) (sigma def-decl "real" sigma "reals/") (Matrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (SquareMat type-eq-decl nil matrices nil) (squareMat? const-decl "bool" matrices nil) (bijec_transpose formula-decl nil matrix_operator nil) (bijec_prod formula-decl nil matrix_operator nil)) nil)) (ellipsoid_TCC12 0 (ellipsoid_TCC12-1 nil 3520826443 ("" (subtype-tcc) nil nil) ((T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (* const-decl "real" vectors "vectors/") (transpose const-decl "Matrix" matrices nil) (* const-decl "Matrix" matrices nil) (real_minus_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)) nil)) (ellipsoid_TCC13 0 (ellipsoid_TCC13-1 nil 3520826443 ("" (subtype-tcc) nil nil) ((T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bijective? const-decl "bool" linear_map nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (* const-decl "real" vectors "vectors/") (transpose const-decl "Matrix" matrices nil) (* const-decl "Matrix" matrices nil) (real_minus_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)) nil)) (ellipsoid 0 (thm "thm" 3521305299 ("" (skosimp) (("" (replace -4) (("" (assert) (("" (lemma "add_cancel_neg2[n!1]") (("" (inst -1 "b!1" "M!1 * x!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1 :hide? t) (("1" (lemma "left_distributive_vect") (("1" (inst -1 "M!1" "x!1" "c!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "M!1" "Q!1*transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(Q!1 * transpose(M!1)) AND squareMat?(n!1)(Q!1 * transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(Q!1 * transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(Q!1*transpose(M!1))" "inv(n!1)(M!1)" "M!1*(x!1-c!1)") (("1" (reveal -8) (("1" (expand "square?") (("1" (reveal -9) (("1" (replace -2 :dir rl :actuals? t :hide? t) (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (assert) (("1" (case "inv(n!1)(M!1) * (M!1 * (x!1 - c!1))=x!1-c!1") (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(transpose(M!1)) AND squareMat?(n!1)(transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "inv(n!1)(Q!1)" "x!1-c!1") (("1" (replace -1) (("1" (lemma "trans_mat_scal") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "M!1*(x!1-c!1)" "inv(n!1)(Q!1)*(x!1-c!1)") (("1" (case "inv(n!1)(transpose(M!1))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (case "(transpose(inv(n!1)(transpose(M!1))) * (M!1 * (x!1 - c!1)))=x!1-c!1") (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-11 1)) (("1" (case "transpose(inv(n!1)(transpose(M!1)))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3) (("2" (hide 2) (("2" (lemma "tran_inv_oper") (("2" (inst -1 "M!1" "n!1") (("2" (assert) (("2" (replace -1) (("2" (lemma "transpose2") (("2" (inst -1 "inv(n!1)(M!1)") (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("1" (reveal -24) (("1" (assert) nil nil)) nil) ("2" (reveal -24) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "mult_assoc_vect") (("2" (inst -1 "inv(n!1)(M!1)" "M!1" "x!1-c!1") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (lemma "iso_inv") (("1" (inst -1 "M!1" "n!1") (("1" (assert) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (lemma "ident_vect") (("1" (inst -1 "I(n!1)" "x!1-c!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (hide-all-but 1) (("1" (grind) (("1" (typepred "M!1") (("1" (typepred "Q!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (typepred "Q!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (lemma "bijec_prod") (("3" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (hide 2) (("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (typepred "Q!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat 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) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (add_cancel_neg2 formula-decl nil vectors "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (prod_inv_oper formula-decl nil matrix_operator nil) (bijec_prod formula-decl nil matrix_operator nil) (mult_assoc_vect formula-decl nil matrices nil) (sigma def-decl "real" sigma "reals/") (iso_inv formula-decl nil matrix_operator nil) (ident_vect formula-decl nil matrices nil) (identity? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (trans_mat_scal formula-decl nil matrices 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) (tran_inv_oper formula-decl nil matrix_operator nil) (transpose2 formula-decl nil matrices nil) (inverse const-decl "Maping" linear_map nil) (inverse const-decl "D" function_inverse nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (bijec_transpose formula-decl nil matrix_operator nil) (- const-decl "real" vectors "vectors/") (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (Matrix_inv type-eq-decl nil matrix_operator nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (Map_linear type-eq-decl nil linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def nil) (Mat type-eq-decl nil matrices nil) (bijective? const-decl "bool" linear_map nil) (Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "Matrix" matrices nil) (transpose const-decl "Matrix" matrices nil) (left_distributive_vect formula-decl nil matrices nil) (* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers 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) (n!1 skolem-const-decl "posnat" ellipsoid nil) (SquareMat type-eq-decl nil matrices nil) (M!1 skolem-const-decl "SquareMat(n!1)" ellipsoid nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak) (ellipsoid-3 "thm" 3521305283 ("" (skosimp) (("" (replace -4) (("" (assert) (("" (lemma "add_cancel_neg2[n!1]") (("" (inst -1 "b!1" "M!1 * x!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1 :hide? t) (("1" (lemma "left_distributive_vect") (("1" (inst -1 "M!1" "x!1" "c!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "M!1" "Q!1*transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(Q!1 * transpose(M!1)) AND squareMat?(n!1)(Q!1 * transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(Q!1 * transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(Q!1*transpose(M!1))" "inv(n!1)(M!1)" "M!1*(x!1-c!1)") (("1" (reveal -8) (("1" (expand "square?") (("1" (reveal -9) (("1" (replace -2 :dir rl :actuals? t :hide? t) (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (assert) (("1" (case "inv(n!1)(M!1) * (M!1 * (x!1 - c!1))=x!1-c!1") (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(transpose(M!1)) AND squareMat?(n!1)(transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "inv(n!1)(Q!1)" "x!1-c!1") (("1" (replace -1) (("1" (lemma "trans_mat_scal") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "M!1*(x!1-c!1)" "inv(n!1)(Q!1)*(x!1-c!1)") (("1" (case "inv(n!1)(transpose(M!1))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (case "(transpose(inv(n!1)(transpose(M!1))) * (M!1 * (x!1 - c!1)))=x!1-c!1") (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-11 1)) (("1" (case "transpose(inv(n!1)(transpose(M!1)))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (propax) nil))) ("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil))))))))))))) ("2" (hide -1 -2 -3) (("2" (hide 2) (("2" (lemma "tran_inv_oper") (("2" (inst -1 "M!1" "n!1") (("2" (assert) (("2" (replace -1) (("2" (lemma "transpose2") (("2" (inst -1 "inv(n!1)(M!1)") (("2" (replace -1) (("2" (propax) nil))))))))))))))))))) ("3" (hide-all-but 1) (("3" (grind) nil))))))))) ("2" (hide-all-but 1) (("2" (grind) nil))))) ("2" (hide-all-but 1) (("2" (grind) (("1" (reveal -24) (("1" (assert) nil))) ("2" (reveal -24) (("2" (assert) nil))))))))))))))))))))))))) ("2" (hide 2) (("2" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil))))))))) ("3" (flatten) (("3" (hide 2) (("3" (grind) nil))))))))))))))) ("2" (hide 2) (("2" (assert) (("2" (lemma "mult_assoc_vect") (("2" (inst -1 "inv(n!1)(M!1)" "M!1" "x!1-c!1") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (lemma "iso_inv") (("1" (inst -1 "M!1" "n!1") (("1" (assert) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (lemma "ident_vect") (("1" (inst -1 "I(n!1)" "x!1-c!1") nil))))))))))))))))))) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))))))))))))) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil))))))))))))))))) ("2" (split) (("1" (hide-all-but 1) (("1" (grind) (("1" (typepred "M!1") (("1" (typepred "Q!1") (("1" (grind) nil))))))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (typepred "Q!1") (("2" (grind) nil))))))) ("3" (lemma "bijec_prod") (("3" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil))))))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))))))))) ("3" (flatten) (("3" (hide 2) (("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (typepred "Q!1") (("3" (grind) nil))))))))))))))))))))))))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil)))))))))))))) nil) ((SquareMat type-eq-decl nil matrices nil) (squareMat? 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) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (left_distributive_vect formula-decl nil matrices nil) (transpose const-decl "Matrix" matrices nil) (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) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (Matrix_inv type-eq-decl nil matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (bijec_transpose formula-decl nil matrix_operator nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inverse const-decl "Maping" linear_map nil) (transpose2 formula-decl nil matrices nil) (tran_inv_oper formula-decl nil matrix_operator nil) (trans_mat_scal formula-decl nil matrices nil) (I const-decl "(identity?)" matrices nil) (identity? const-decl "bool" matrices nil) (ident_vect formula-decl nil matrices nil) (iso_inv formula-decl nil matrix_operator nil) (sigma def-decl "real" sigma "reals/") (mult_assoc_vect formula-decl nil matrices nil) (bijec_prod formula-decl nil matrix_operator nil) (prod_inv_oper formula-decl nil matrix_operator nil) (add_cancel_neg2 formula-decl nil vectors "vectors/")) nil) (thm "thm" 3521286628 ("" (skosimp) (("" (replace -4) (("" (assert) (("" (lemma "add_cancel_neg2[n!1]") (("" (inst -1 "b!1" "M!1 * x!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1 :hide? t) (("1" (lemma "left_distributive_vect") (("1" (inst -1 "M!1" "x!1" "c!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "M!1" "Q!1*transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(Q!1 * transpose(M!1)) AND squareMat?(n!1)(Q!1 * transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(Q!1 * transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(Q!1*transpose(M!1))" "inv(n!1)(M!1)" "M!1*(x!1-c!1)") (("1" (reveal -8) (("1" (expand "square?") (("1" (reveal -9) (("1" (replace -2 :dir rl :actuals? t :hide? t) (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (assert) (("1" (case "inv(n!1)(M!1) * (M!1 * (x!1 - c!1))=x!1-c!1") (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(transpose(M!1)) AND squareMat?(n!1)(transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "inv(n!1)(Q!1)" "x!1-c!1") (("1" (replace -1) (("1" (lemma "trans_mat_scal") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "M!1*(x!1-c!1)" "inv(n!1)(Q!1)*(x!1-c!1)") (("1" (case "inv(n!1)(transpose(M!1))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (case "(transpose(inv(n!1)(transpose(M!1))) * (M!1 * (x!1 - c!1)))=x!1-c!1") (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-11 1)) (("1" (case "transpose(inv(n!1)(transpose(M!1)))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3) (("2" (hide 2) (("2" (lemma "tran_inv_oper") (("2" (inst -1 "M!1" "n!1") (("2" (assert) (("2" (replace -1) (("2" (lemma "transpose2") (("2" (inst -1 "inv(n!1)(M!1)") (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("1" (reveal -24) (("1" (assert) nil nil)) nil) ("2" (reveal -24) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "mult_assoc_vect") (("2" (inst -1 "inv(n!1)(M!1)" "M!1" "x!1-c!1") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (lemma "iso_inv") (("1" (inst -1 "M!1" "n!1") (("1" (assert) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (lemma "ident_vect") (("1" (inst -1 "I(n!1)" "x!1-c!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (hide-all-but 1) (("1" (grind) (("1" (typepred "M!1") (("1" (typepred "Q!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (typepred "Q!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (lemma "bijec_prod") (("3" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (hide 2) (("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (typepred "Q!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((add_cancel_neg2 formula-decl nil vectors "vectors/") (prod_inv_oper formula-decl nil matrix_operator nil) (bijec_prod formula-decl nil matrix_operator nil) (mult_assoc_vect formula-decl nil matrices nil) (sigma def-decl "real" sigma "reals/") (iso_inv formula-decl nil matrix_operator nil) (ident_vect formula-decl nil matrices nil) (identity? const-decl "bool" matrices nil) (I const-decl "(identity?)" matrices nil) (trans_mat_scal formula-decl nil matrices nil) (tran_inv_oper formula-decl nil matrix_operator nil) (transpose2 formula-decl nil matrices nil) (inverse const-decl "Maping" linear_map nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (bijec_transpose formula-decl nil matrix_operator nil) (- const-decl "real" vectors "vectors/") (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (Matrix_inv type-eq-decl nil matrix_operator nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (Map_linear type-eq-decl nil linear_map_def nil) (Mat type-eq-decl nil matrices nil) (bijective? const-decl "bool" linear_map nil) (Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (transpose const-decl "Matrix" matrices nil) (left_distributive_vect formula-decl nil matrices nil) (* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (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) (SquareMat type-eq-decl nil matrices nil)) shostak) (ellipsoid-2 "thm" 3521286610 ("" (skosimp) (("" (replace -4) (("" (assert) (("" (lemma "add_cancel_neg2[n!1]") (("" (inst -1 "b!1" "M!1 * x!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1 :hide? t) (("1" (lemma "left_distributive_vect") (("1" (inst -1 "M!1" "x!1" "c!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "M!1" "Q!1*transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(Q!1 * transpose(M!1)) AND squareMat?(n!1)(Q!1 * transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(Q!1 * transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(Q!1*transpose(M!1))" "inv(n!1)(M!1)" "M!1*(x!1-c!1)") (("1" (reveal -8) (("1" (expand "square?") (("1" (reveal -9) (("1" (replace -2 :dir rl :actuals? t :hide? t) (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (assert) (("1" (case "inv(n!1)(M!1) * (M!1 * (x!1 - c!1))=x!1-c!1") (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(transpose(M!1)) AND squareMat?(n!1)(transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "inv(n!1)(Q!1)" "x!1-c!1") (("1" (replace -1) (("1" (lemma "trans_mat_scal") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "M!1*(x!1-c!1)" "inv(n!1)(Q!1)*(x!1-c!1)") (("1" (case "inv(n!1)(transpose(M!1))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (case "(transpose(inv(n!1)(transpose(M!1))) * (M!1 * (x!1 - c!1)))=x!1-c!1") (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-11 1)) (("1" (case "transpose(inv(n!1)(transpose(M!1)))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (propax) nil))) ("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil))))))))))))) ("2" (hide -1 -2 -3) (("2" (hide 2) (("2" (lemma "tran_inv_oper") (("2" (inst -1 "M!1" "n!1") (("2" (assert) (("2" (replace -1) (("2" (lemma "transpose2") (("2" (inst -1 "inv(n!1)(M!1)") (("2" (replace -1) (("2" (propax) nil))))))))))))))))))) ("3" (hide-all-but 1) (("3" (grind) nil))))))))) ("2" (hide-all-but 1) (("2" (grind) nil))))) ("2" (hide-all-but 1) (("2" (grind) (("1" (reveal -24) (("1" (assert) nil))) ("2" (reveal -24) (("2" (assert) nil))))))))))))))))))))))))) ("2" (hide 2) (("2" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil))))))))) ("3" (flatten) (("3" (hide 2) (("3" (grind) nil))))))))))))))) ("2" (hide 2) (("2" (assert) (("2" (lemma "mult_assoc_vect") (("2" (inst -1 "inv(n!1)(M!1)" "M!1" "x!1-c!1") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (lemma "iso_inv") (("1" (inst -1 "M!1" "n!1") (("1" (assert) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (lemma "ident_vect") (("1" (inst -1 "I(n!1)" "x!1-c!1") nil))))))))))))))))))) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))))))))))))) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil))))))))))))))))) ("2" (split) (("1" (hide-all-but 1) (("1" (grind) (("1" (typepred "M!1") (("1" (typepred "Q!1") (("1" (grind) nil))))))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (typepred "Q!1") (("2" (grind) nil))))))) ("3" (lemma "bijec_prod") (("3" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil))))))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil))))))))))) ("3" (flatten) (("3" (hide 2) (("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (typepred "Q!1") (("3" (grind) nil))))))))))))))))))))))))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil)))))))))))))) nil) ((SquareMat type-eq-decl nil matrices nil) (squareMat? 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) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (left_distributive_vect formula-decl nil matrices nil) (transpose const-decl "Matrix" matrices nil) (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) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (Matrix_inv type-eq-decl nil matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (bijec_transpose formula-decl nil matrix_operator nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inverse const-decl "Maping" linear_map nil) (transpose2 formula-decl nil matrices nil) (tran_inv_oper formula-decl nil matrix_operator nil) (trans_mat_scal formula-decl nil matrices nil) (I const-decl "(identity?)" matrices nil) (identity? const-decl "bool" matrices nil) (ident_vect formula-decl nil matrices nil) (iso_inv formula-decl nil matrix_operator nil) (sigma def-decl "real" sigma "reals/") (mult_assoc_vect formula-decl nil matrices nil) (bijec_prod formula-decl nil matrix_operator nil) (prod_inv_oper formula-decl nil matrix_operator nil) (add_cancel_neg2 formula-decl nil vectors "vectors/")) nil) (thm "thm" 3520609934 ("" (skosimp) (("" (replace -4) (("" (assert) (("" (lemma "add_cancel_neg2[n!1]") (("" (inst -1 "b!1" "M!1 * x!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1 :hide? t) (("1" (lemma "left_distributive_vect") (("1" (inst -1 "M!1" "x!1" "c!1") (("1" (typepred "M!1") (("1" (expand "squareMat?") (("1" (replace -2 :actuals? t :hide? t) (("1" (hide -1) (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "M!1" "Q!1*transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(Q!1 * transpose(M!1)) AND squareMat?(n!1)(Q!1 * transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(Q!1 * transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(Q!1*transpose(M!1))" "inv(n!1)(M!1)" "M!1*(x!1-c!1)") (("1" (reveal -8) (("1" (expand "square?") (("1" (reveal -9) (("1" (replace -2 :dir rl :actuals? t :hide? t) (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (assert) (("1" (case "inv(n!1)(M!1) * (M!1 * (x!1 - c!1))=x!1-c!1") (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (case "square?(transpose(M!1)) AND squareMat?(n!1)(transpose(M!1)) AND bijective?(n!1)(T(n!1, n!1)(transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (replace -1) (("1" (lemma "mult_assoc_vect") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "inv(n!1)(Q!1)" "x!1-c!1") (("1" (replace -1) (("1" (lemma "trans_mat_scal") (("1" (inst -1 "inv(n!1)(transpose(M!1))" "M!1*(x!1-c!1)" "inv(n!1)(Q!1)*(x!1-c!1)") (("1" (case "inv(n!1)(transpose(M!1))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (replace -1) (("1" (case "(transpose(inv(n!1)(transpose(M!1))) * (M!1 * (x!1 - c!1)))=x!1-c!1") (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-11 1)) (("1" (case "transpose(inv(n!1)(transpose(M!1)))`rows = n!1") (("1" (replace -1 :actuals? t :hide? t) (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3) (("2" (hide 2) (("2" (lemma "tran_inv_oper") (("2" (inst -1 "M!1" "n!1") (("2" (assert) (("2" (replace -1) (("2" (lemma "transpose2") (("2" (inst -1 "inv(n!1)(M!1)") (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("1" (reveal -24) (("1" (assert) nil nil)) nil) ("2" (reveal -24) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "mult_assoc_vect") (("2" (inst -1 "inv(n!1)(M!1)" "M!1" "x!1-c!1") (("1" (replace -1 :dir rl) (("1" (assert) (("1" (lemma "iso_inv") (("1" (inst -1 "M!1" "n!1") (("1" (assert) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (lemma "ident_vect") (("1" (inst -1 "I(n!1)" "x!1-c!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (hide-all-but 1) (("1" (grind) (("1" (typepred "M!1") (("1" (typepred "Q!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (typepred "Q!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (lemma "bijec_prod") (("3" (inst -1 "Q!1" "transpose(M!1)" "n!1") (("1" (assert) (("1" (split) (("1" (hide-all-but 1) (("1" (typepred "M!1") (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil) ("3" (lemma "bijec_transpose") (("3" (inst -1 "M!1" "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (hide 2) (("3" (hide-all-but 1) (("3" (typepred "M!1") (("3" (typepred "Q!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((SquareMat type-eq-decl nil matrices nil) (squareMat? 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) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (left_distributive_vect formula-decl nil matrices nil) (transpose const-decl "Matrix" matrices nil) (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) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (Matrix_inv type-eq-decl nil matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (- const-decl "real" vectors "vectors/") (bijec_transpose formula-decl nil matrix_operator nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inverse const-decl "Maping" linear_map nil) (transpose2 formula-decl nil matrices nil) (tran_inv_oper formula-decl nil matrix_operator nil) (trans_mat_scal formula-decl nil matrices nil) (I const-decl "(identity?)" matrices nil) (identity? const-decl "bool" matrices nil) (ident_vect formula-decl nil matrices nil) (iso_inv formula-decl nil matrix_operator nil) (sigma def-decl "real" sigma "reals/") (mult_assoc_vect formula-decl nil matrices nil) (bijec_prod formula-decl nil matrix_operator nil) (prod_inv_oper formula-decl nil matrix_operator nil) (add_cancel_neg2 formula-decl nil vectors "vectors/")) shostak) (ellipsoid-1 nil 3504886332 ("" (skosimp) (("" (replace -4) (("" (assert) (("" (lemma "left_distributive_vect_n") (("" (inst -1 "M!1" "x!1" "c!1") (("" (swap-rel -1) (("" (replace -1) (("" (lemma "prod_inv_oper") (("" (inst -1 "M!1" "Q!1*transpose(M!1)" "n") (("" (assert) (("" (case " square?(M!1) AND squareMat?(n)(M!1) AND square?(Q!1 * transpose(M!1)) AND squareMat?(n)(Q!1 * transpose(M!1)) AND bijective?(n)(T(n, n)(Q!1 * transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3 -4 -5) (("1" (replace -1) (("1" (lemma "mult_assoc_vect_n") (("1" (inst -1 "inv(n)(Q!1*transpose(M!1))" "inv(n)(M!1)" "M!1*(x!1-c!1)") (("1" (replace -1) (("1" (assert) (("1" (case "inv(n)(M!1) * (M!1 * (x!1 - c!1))=x!1-c!1") (("1" (replace -1) (("1" (lemma "prod_inv_oper") (("1" (inst -1 "Q!1" "transpose(M!1)" "n") (("1" (assert) (("1" (case "square?(Q!1) AND squareMat?(n)(Q!1) AND square?(transpose(M!1)) AND squareMat?(n)(transpose(M!1)) AND bijective?(n)(T(n, n)(transpose(M!1)))") (("1" (flatten) (("1" (assert) (("1" (hide -1 -2 -3 -4 -5) (("1" (replace -1) (("1" (lemma "mult_assoc_vect_n") (("1" (inst -1 "inv(n)(transpose(M!1))" "inv(n)(Q!1)" "x!1-c!1") (("1" (replace -1) (("1" (lemma "trans_mat_scal_n") (("1" (inst -1 "inv(n)(transpose(M!1))" "M!1*(x!1-c!1)" "inv(n)(Q!1)*(x!1-c!1)") (("1" (replace -1) (("1" (case "(transpose(inv(n)(transpose(M!1))) * (M!1 * (x!1 - c!1)))=x!1-c!1") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide -1 -2 -3) (("2" (hide 2) (("2" (lemma "tran_inv_oper") (("2" (inst -1 "M!1" "n") (("2" (assert) (("2" (replace -1) (("2" (lemma "transpose2") (("2" (inst -1 "inv(n)(M!1)") (("2" (replace -1) (("2" (propax) 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) ("2" (hide 2) (("2" (split) (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (lemma "bijec_transpose") (("5" (inst -1 "M!1" "n") (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "mult_assoc_vect_n") (("2" (inst -1 "inv(n)(M!1)" "M!1" "x!1-c!1") (("2" (swap-rel -1) (("2" (replace -1) (("2" (assert) (("2" (lemma "iso_inv") (("2" (inst -1 "M!1" "n") (("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (postpone) 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) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (lemma "bijec_prod") (("5" (inst -1 "Q!1" "transpose(M!1)" "n") (("1" (assert) (("1" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (lemma "bijec_transpose") (("5" (inst -1 "M!1" "n") (("5" (assert) (("5" (hide 2 3 4) (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("3" (flatten) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((add_cancel_neg2 formula-decl nil vectors "vectors/") (Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (transpose const-decl "Matrix" matrices nil) (square? const-decl "bool" matrices nil) (Square type-eq-decl nil matrices nil) (squareMat? const-decl "bool" matrices nil) (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (bijective? const-decl "bool" linear_map nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (Matrix_inv type-eq-decl nil matrix_operator nil) (inv const-decl "[Matrix_inv(n) -> Matrix_inv(n)]" matrix_operator nil) (I const-decl "(identity?)" matrices nil) (identity? const-decl "bool" matrices nil) (iso_inv formula-decl nil matrix_operator nil) (tran_inv_oper formula-decl nil matrix_operator nil) (transpose2 formula-decl nil matrices nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (inverse const-decl "Maping" linear_map nil) (sigma def-decl "real" sigma "reals/") (bijec_transpose formula-decl nil matrix_operator nil) (bijec_prod formula-decl nil matrix_operator nil) (prod_inv_oper formula-decl nil matrix_operator nil) (- const-decl "real" vectors "vectors/")) shostak)))
¤ Dauer der Verarbeitung: 0.278 Sekunden (vorverarbeitet am 2026-04-25) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26