Quelle matrix_operator.prf
Sprache: Lisp
|
|
(matrix_operator (linear_inverse_map_n 0 (thm "thm" 3520673962 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (assert) (("1" (expand "bijective?") (("1" (expand "bijective?") (("1" (typepred "f!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (copy -1) (("3" (expand "bijective?" -2) (("3" (expand "bijective?" -2) (("3" (flatten) (("3" (expand "injective?") (("3" (inst -2 " inverse(n!1)(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1))") (("1" (case "(f!1`mp
(inverse(n!1)(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -2) (("2" (typepred "f!1") (("2" (expand "linear_map_e?") (("2" (inst -3 "l!1") (("2" (expand "linear_map_e?") (("2" (inst -3 "x!1" " (inverse(n!1)(f!1)`mp o F!1)") (("1" (replace-extensionality " f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1)))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (f!1`mp o (inverse(n!1)(f!1)`mp o F!1)))") (("1" (hide -3) (("1" (lemma "inverse_surjective[Vector[n!1],Vector[n!1]]") (("1" (copy -1) (("1" (inst -1 "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)" "f!1`mp") (("1" (expand "inverse" 1) (("1" (replace -1) (("1" (hide -1) (("1" (case "(f!1`mp o (inverse[Vector[n!1], Vector[n!1]](f!1`mp) o F!1)=F!1)
") (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (decompose-equality -1) (("1" (expand "o") (("1" (expand "SigmaV") (("1" (lemma "sigma_eq[below[l!1]]") (("1" (inst -1 " LAMBDA (j: below[l!1]): (x!1 * F!1)(j)(x!2)" "LAMBDA (j: below[l!1]):
(x!1 *
(LAMBDA (x_1: below[l!1]):
f!1`mp
(inverse[Vector[n!1], Vector[n!1]]
(f!1`mp)(F!1(x_1)))))
(j)(x!2)" "l!1-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (expand "*") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1) (("2" (hide 2) (("2" (expand "o") (("2" (inst -1 "F!1(x!2)" "f!1`mp") nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality -3) (("2" (inst -1 "x!2") (("2" (assert) (("2" (expand "o") (("2" (expand "SigmaV") (("2" (assert) (("2" (expand "inverse") (("2" (grind) 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) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((linear_map_e? const-decl "bool" linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (f!1 skolem-const-decl "Map_linear(n!1, n!1)" matrix_operator nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (< const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Index type-eq-decl nil vectors "vectors/") (OR const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (O const-decl "T3" function_props nil) (pred type-eq-decl nil defined_types nil) (epsilon const-decl "T" epsilons nil) (l!1 skolem-const-decl "posnat" matrix_operator nil) (sigma def-decl "real" sigma "reals/") (real_plus_real_is_real application-judgement "real" reals 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) (subrange type-eq-decl nil integers nil) (* const-decl "Vector" vectors "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_eq formula-decl nil sigma "reals/") (inverse const-decl "D" function_inverse nil) (surjective? const-decl "bool" functions nil) (inverse_surjective formula-decl nil function_inverse nil) (injective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (inverse const-decl "Maping" linear_map nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (Map type-eq-decl nil linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (bijective? const-decl "bool" linear_map nil)) shostak) (thm "thm" 3519987486 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (assert) (("1" (expand "bijective?") (("1" (expand "bijective?") (("1" (typepred "f!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (copy -1) (("3" (expand "bijective?" -2) (("3" (expand "bijective?" -2) (("3" (flatten) (("3" (expand "injective?") (("3" (inst -2 " inverse(n!1)(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1))") (("1" (case "(f!1`mp
(inverse(n!1)(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -2) (("2" (typepred "f!1") (("2" (expand "linear_map_e?") (("2" (inst -3 "l!1") (("2" (expand "linear_map_e?") (("2" (inst -3 "x!1" " (inverse(n!1)(f!1)`mp o F!1)") (("1" (replace-extensionality " f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1)))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (f!1`mp o (inverse(n!1)(f!1)`mp o F!1)))") (("1" (hide -3) (("1" (lemma "inverse_surjective[Vector[n!1],Vector[n!1]]") (("1" (copy -1) (("1" (inst -1 "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)" "f!1`mp") (("1" (expand "inverse" 1) (("1" (replace -1) (("1" (hide -1) (("1" (case "(f!1`mp o (inverse[Vector[n!1], Vector[n!1]](f!1`mp) o F!1)=F!1)
") (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (decompose-equality -1) (("1" (expand "o") (("1" (expand "SigmaV") (("1" (lemma "sigma_eq[below[l!1]]") (("1" (inst -1 " LAMBDA (j: below[l!1]): (x!1 * F!1)(j)(x!2)" "LAMBDA (j: below[l!1]):
(x!1 *
(LAMBDA (x_1: below[l!1]):
f!1`mp
(inverse[Vector[n!1], Vector[n!1]]
(f!1`mp)(F!1(x_1)))))
(j)(x!2)" "l!1-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (expand "*") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1) (("2" (hide 2) (("2" (expand "o") (("2" (inst -1 "F!1(x!2)" "f!1`mp") nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality -3) (("2" (inst -1 "x!2") (("2" (assert) (("2" (expand "o") (("2" (expand "SigmaV") (("2" (assert) (("2" (expand "inverse") (("2" (grind) 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) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (Vector type-eq-decl nil vectors "vectors/") (inverse const-decl "Maping" linear_map nil) (sigma_eq formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (sigma def-decl "real" sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Index type-eq-decl nil vectors "vectors/")) shostak) (NuevasDefiniciones "Defs" 3519718025 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (assert) (("1" (expand "bijective?") (("1" (expand "bijective?") (("1" (typepred "f!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (copy -1) (("3" (expand "bijective?" -2) (("3" (expand "bijective?" -2) (("3" (flatten) (("3" (expand "injective?") (("3" (inst -2 " inverse(n!1)(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1))") (("1" (case "(f!1`mp
(inverse(n!1)(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -2) (("2" (typepred "f!1") (("2" (expand "linear_map_e?") (("2" (inst -3 "l!1") (("2" (expand "linear_map_e?") (("2" (inst -3 "x!1" " (inverse(n!1)(f!1)`mp o F!1)") (("1" (replace-extensionality " f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(n!1)(f!1)`mp o F!1)))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (f!1`mp o (inverse(n!1)(f!1)`mp o F!1)))") (("1" (hide -3) (("1" (lemma "inverse_surjective[Vector[n!1],Vector[n!1]]") (("1" (copy -1) (("1" (inst -1 "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)" "f!1`mp") (("1" (expand "inverse" 1) (("1" (replace -1) (("1" (hide -1) (("1" (case "(f!1`mp o (inverse[Vector[n!1], Vector[n!1]](f!1`mp) o F!1)=F!1)
") (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (decompose-equality -1) (("1" (expand "o") (("1" (expand "SigmaV") (("1" (lemma "sigma_eq[below[l!1]]") (("1" (inst -1 " LAMBDA (j: below[l!1]): (x!1 * F!1)(j)(x!2)" "LAMBDA (j: below[l!1]):
(x!1 *
(LAMBDA (x_1: below[l!1]):
f!1`mp
(inverse[Vector[n!1], Vector[n!1]]
(f!1`mp)(F!1(x_1)))))
(j)(x!2)" "l!1-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (expand "*") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1) (("2" (hide 2) (("2" (expand "o") (("2" (inst -1 "F!1(x!2)" "f!1`mp") nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality -3) (("2" (inst -1 "x!2") (("2" (assert) (("2" (expand "o") (("2" (expand "SigmaV") (("2" (assert) (("2" (expand "inverse") (("2" (grind) 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) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (Vector type-eq-decl nil vectors "vectors/") (inverse const-decl "Maping" linear_map nil) (sigma_eq formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (sigma def-decl "real" sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Index type-eq-decl nil vectors "vectors/")) shostak) (DiceGIlbertoqueCasi "LoDiceenSerio" 3519668431 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (lemma "bijective_dim") (("1" (inst -1 "f!1") (("1" (inst -2 l!1) (("1" (flatten) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "bijective_dim") (("2" (inst -1 f!1) (("2" (inst -2 l!1) (("2" (flatten) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -1 "l!1") (("3" (flatten) (("3" (copy -4) (("3" (expand "bijective?" -5) (("3" (flatten) (("3" (expand "bijective?" -6) (("3" (flatten) (("3" (expand "injective?") (("3" (inst -6 "inverse(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1))") (("1" (case " (f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (inst -4 "x!1" " (inverse(f!1)`mp o F!1)") (("1" (hide -6) (("1" (replace-extensionality " f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (f!1`mp o (inverse(f!1)`mp o F!1)))") (("1" (expand "o") (("1" (lemma "inverse_surjective[Vector[n!1],Vector[n!1]]") (("1" (copy -1) (("1" (inst -1 "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)" "f!1`mp") (("1" (replace-extensionality " (f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))))" "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)") (("1" (expand "inverse" 1) (("1" (hide -6) (("1" (replace-extensionality "(LAMBDA (x_1: below[l!1]): f!1`mp(inverse(f!1`mp)(F!1(x_1))))" "F!1") (("1" (assert) (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst -2 "(F!1(x!2))" "f!1`mp") (("2" (assert) (("2" (grind) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (assert) (("3" (replace -5) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (replace -5) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality -1) (("2" (inst -1 x!2) (("2" (expand "SigmaV") (("2" (hide -2) (("2" (hide -5) (("2" (expand "inverse" 1) (("2" (expand "*") (("2" (assert) (("2" (expand "*") (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (replace -5) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality -4) (("2" (inst -1 "x!2") (("2" (assert) (("2" (expand "o") (("2" (expand "SigmaV") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (lemma "bijective_dim") (("2" (inst -1 "f!1") (("2" (replace -3) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "bijective_dim") (("4" (inst -1 f!1) (("4" (replace -3) (("4" (assert) (("4" (flatten) (("4" (replace -2) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "bijective_dim") (("2" (inst -1 "f!1") (("2" (assert) (("2" (flatten) (("2" (replace -2) (("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (Casi "CasideVerdad" 3519665165 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (lemma "bijective_dim") (("1" (inst -1 "f!1") (("1" (inst -2 l!1) (("1" (flatten) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "bijective_dim") (("2" (inst -1 f!1) (("2" (inst -2 l!1) (("2" (flatten) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -1 "l!1") (("3" (flatten) (("3" (copy -4) (("3" (expand "bijective?" -5) (("3" (flatten) (("3" (expand "bijective?" -6) (("3" (flatten) (("3" (expand "injective?") (("3" (inst -6 "inverse(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1))") (("1" (case " (f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (inst -4 "x!1" " (inverse(f!1)`mp o F!1)") (("1" (hide -6) (("1" (replace-extensionality " f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (f!1`mp o (inverse(f!1)`mp o F!1)))") (("1" (expand "o") (("1" (lemma "inverse_surjective[Vector[n!1],Vector[n!1]]") (("1" (copy -1) (("1" (inst -1 "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)" "f!1`mp") (("1" (replace-extensionality " (f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))))" "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)") (("1" (postpone) nil nil) ("2" (hide 2) (("2" (decompose-equality -1) (("2" (inst -1 x!2) (("2" (expand "SigmaV") (("2" (hide -2) (("2" (hide -5) (("2" (expand "inverse" 1) (("2" (expand "*") (("2" (assert) (("2" (expand "*") (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (replace -5) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality -4) (("2" (inst -1 "x!2") (("2" (assert) (("2" (expand "o") (("2" (expand "SigmaV") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (lemma "bijective_dim") (("2" (inst -1 "f!1") (("2" (replace -3) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "bijective_dim") (("4" (inst -1 f!1) (("4" (replace -3) (("4" (assert) (("4" (flatten) (("4" (replace -2) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "bijective_dim") (("2" (inst -1 "f!1") (("2" (assert) (("2" (flatten) (("2" (replace -2) (("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (BijectiveNueva "bijNueva" 3519664017 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (lemma "bijective_dim") (("1" (inst -1 "f!1") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (lemma "bijective_dim") (("2" (inst -1 "f!1") (("2" (assert) (("2" (inst -2 "l!1") (("2" (flatten) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -1 "l!1") (("3" (flatten) (("3" (copy -4) (("3" (expand "bijective?" -5) (("3" (expand "bijective?" -5) (("3" (flatten) (("3" (expand "injective?") (("3" (case "f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))") (("1" (assert) (("1" (postpone) nil nil)) nil) ("2" (hide 2 -5) (("2" (inst -4 "x!1" "(inverse(f!1)`mp o F!1)") (("1" (hide -2 -3) (("1" (hide -3) (("1" (expand "SigmaV" -2 1) (("1" (expand "SigmaV" 1 2) (("1" (expand "*" -2 1) (("1" (expand "*" 1 2) (("1" (expand "o" -2 1) (("1" (expand "o" 1) (("1" (replace-extensionality " f!1`mp
(LAMBDA (i: below[n!1]):
sigma(0, l!1 - 1,
LAMBDA (j: below[l!1]):
(x!1(j) * inverse(f!1)`mp(F!1(j)))(i)))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (f!1`mp o (inverse(f!1)`mp o F!1)))") (("1" (postpone) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (lemma "bijective_dim") (("3" (inst -1 "f!1") (("3" (assert) (("3" (split) (("1" (flatten) (("1" (typepred "x!2") (("1" (case "n!1=f!1`dom") (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (typepred " f!1`dom") (("2" (typepred "n!1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp) (("5" (skosimp) (("5" (lemma "bijective_dim") (("5" (inst -1 "f!1") (("5" (assert) (("5" (case " f!1`dom=n!1") (("1" (replace -1 -2) (("1" (assert) (("1" (flatten) (("1" (replace -3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skosimp) (("6" (typepred "i!1") (("6" (lemma "bijective_dim") (("6" (inst -1 "f!1") (("6" (case " f!1`dom=n!1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (split) (("1" (lemma "bijective_dim") (("1" (inst -1 "f!1") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (lemma "bijective_dim") (("2" (inst -1 "f!1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -2 1) (("3" (assert) nil nil)) nil) ("4" (hide 2) (("4" (lemma "bijective_dim") (("4" (hide -6) (("4" (inst -1 "f!1") (("4" (assert) (("4" (flatten) (("4" (replace -2) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (Replace-extensionality "rep-ext" 3519660046 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (lemma "bijective_dim") (("1" (inst -1 "f!1") (("1" (assert) (("1" (flatten) (("1" (inst -4 "l!1") (("1" (flatten) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "bijective_dim") (("2" (inst -1 "f!1") (("2" (assert) (("2" (inst -2 "l!1") (("2" (flatten) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst -1 "l!1") (("3" (flatten) (("3" (copy -4) (("3" (expand "bijective?" -5) (("3" (expand "bijective?" -5) (("3" (flatten) (("3" (expand "injective?") (("3" (inst -5 " inverse(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1))") (("1" (case "f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2 -5) (("2" (inst -4 "x!1" "(inverse(f!1)`mp o F!1)") (("1" (hide -2 -3) (("1" (hide -3) (("1" (expand "SigmaV" -2 1) (("1" (expand "SigmaV" 1 2) (("1" (expand "*" -2 1) (("1" (expand "*" 1 2) (("1" (expand "o" -2 1) (("1" (expand "o" 1) (("1" (replace-extensionality " f!1`mp
(LAMBDA (i: below[n!1]):
sigma(0, l!1 - 1,
LAMBDA (j: below[l!1]):
(x!1(j) * inverse(f!1)`mp(F!1(j)))(i)))" " SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (f!1`mp o (inverse(f!1)`mp o F!1)))") (("1" (postpone) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (lemma "bijective_dim") (("3" (inst -1 "f!1") (("3" (assert) (("3" (split) (("1" (flatten) (("1" (typepred "x!2") (("1" (case "n!1=f!1`dom") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred " f!1`dom") (("2" (typepred "n!1") (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil) ("5" (postpone) nil nil) ("6" (hide 2) (("6" (skosimp) (("6" (typepred "i!1") (("6" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (split) (("1" (lemma "bijective_dim") (("1" (inst -1 "f!1") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (lemma "bijective_dim") (("2" (inst -1 "f!1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -2 1) (("3" (assert) nil nil)) nil) ("4" (hide 2) (("4" (lemma "bijective_dim") (("4" (hide -6) (("4" (inst -1 "f!1") (("4" (assert) (("4" (flatten) (("4" (replace -2) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "bijective_dim") (("3" (inst -1 "f!1") (("3" (assert) (("3" (flatten) (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (Otra "mas" 3519653941 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (skosimp) (("3" (inst -1 "l!1") (("3" (flatten) (("3" (expand "bijective?") (("3" (expand "bijective?") (("3" (flatten) (("3" (expand "injective?") (("3" (inst -4 " inverse(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1))") (("1" (case "f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -4) (("2" (inst -3 "x!1" "(inverse(f!1)`mp o F!1)") (("1" (hide -1 -2) (("1" (hide -2) (("1" (expand "SigmaV" -1 1) (("1" (expand "SigmaV" 1 2) (("1" (expand "*" -1 1) (("1" (expand "*" 1 2) (("1" (expand "o" -1 1) (("1" (expand "o" 1) (("1" (expand "inverse") (("1" (expand "inverse" -1 1) (("1" (expand "inverse" 1 2) (("1" (grind) (("1" (case " f!1`mp
((epsilon! (x: Vector[f!1`dom]):
f!1`mp(x) = SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)))= SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)") (("1" (replace -1) (("1" (hide -2) (("1" (name "pp" " x!1 * (f!1`mp o (inverse(f!1`mp) o F!1))") (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (grind) (("1" (case " f!1`mp
((epsilon! (x: Vector[f!1`dom]): f!1`mp(x) = F!1(l!1 - 1)))
(x!2)= F!1(l!1 - 1)
(x!2)") (("1" (replace -1) (("1" (assert) (("1" (name "dd" "LAMBDA (j: below[l!1]):
x!1(j) *
f!1`mp
((epsilon! (x: Vector[f!1`dom]): f!1`mp(x) = F!1(j)))
(x!2)") (("1" (replace -1) (("1" (lemma "sigma_eq[below[l!1]]") (("1" (inst -1 "LAMBDA (j: below[l!1]): x!1(j) * F!1(j)(x!2)" "dd" "l!1-2" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (expand "dd") (("1" (grind) (("1" (case " f!1`mp((epsilon! (x: Vector[f!1`dom]): f!1`mp(x) = F!1(n!2)))(x!2)= F!1(n!2)(x!2)") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (lemma "inverse_surjective[Vector[n!1],Vector[n!1]]") (("2" (inst -1 " F!1(n!2)" " f!1`mp") (("1" (lemma "inverse_surjective[Vector[f!1`dom],Vector[f!1`codom]]") (("1" (inst -1 " F!1(n!2)" "f!1`mp") (("1" (decompose-equality) (("1" (inst -1 x!2) (("1" (expand "inverse" -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst 1 "inverse(f!1`mp)(y!1)") (("2" (postpone) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("3" (expand "surjective?") (("3" (postpone) nil nil)) nil) ("4" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (rename "name" 3519653479 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (skosimp) (("3" (inst -1 "l!1") (("3" (flatten) (("3" (expand "bijective?") (("3" (expand "bijective?") (("3" (flatten) (("3" (expand "injective?") (("3" (inst -4 " inverse(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1))") (("1" (case "f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -4) (("2" (inst -3 "x!1" "(inverse(f!1)`mp o F!1)") (("1" (hide -1 -2) (("1" (hide -2) (("1" (expand "SigmaV" -1 1) (("1" (expand "SigmaV" 1 2) (("1" (expand "*" -1 1) (("1" (expand "*" 1 2) (("1" (expand "o" -1 1) (("1" (expand "o" 1) (("1" (expand "inverse") (("1" (expand "inverse" -1 1) (("1" (expand "inverse" 1 2) (("1" (grind) (("1" (case " f!1`mp
((epsilon! (x: Vector[f!1`dom]):
f!1`mp(x) = SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)))= SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)") (("1" (replace -1) (("1" (hide -2) (("1" (name "pp" " x!1 * (f!1`mp o (inverse(f!1`mp) o F!1))") (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (grind) (("1" (case " f!1`mp
((epsilon! (x: Vector[f!1`dom]): f!1`mp(x) = F!1(l!1 - 1)))
(x!2)= F!1(l!1 - 1)
(x!2)") (("1" (replace -1) (("1" (assert) (("1" (name "ll" "LAMBDA (j: below[l!1]):
x!1(j) *
f!1`mp
((epsilon! (x: Vector[f!1`dom]): f!1`mp(x) = F!1(j)))
(x!2)") (("1" (replace -1) (("1" (lemma "sigma_eq[below[l!1-1]]") (("1" (inst -1 " LAMBDA (j: below[l!1]): x!1(j) * F!1(j)(x!2)" "ll" "l!1-2" "0") (("1" (assert) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (por "sustgrind" 3519652449 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (skosimp) (("3" (inst -1 "l!1") (("3" (flatten) (("3" (expand "bijective?") (("3" (expand "bijective?") (("3" (flatten) (("3" (expand "injective?") (("3" (inst -4 " inverse(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1))") (("1" (case "f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -4) (("2" (inst -3 "x!1" "(inverse(f!1)`mp o F!1)") (("1" (hide -1 -2) (("1" (hide -2) (("1" (expand "SigmaV" -1 1) (("1" (expand "SigmaV" 1 2) (("1" (expand "*" -1 1) (("1" (expand "*" 1 2) (("1" (expand "o" -1 1) (("1" (expand "o" 1) (("1" (expand "inverse") (("1" (expand "inverse" -1 1) (("1" (expand "inverse" 1 2) (("1" (grind) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (linear_inverse_map_n-1 nil 3519647208 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (skosimp) (("3" (inst -1 "l!1") (("3" (flatten) (("3" (expand "bijective?") (("3" (expand "bijective?") (("3" (flatten) (("3" (expand "injective?") (("3" (inst -4 " inverse(f!1)`mp(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1))" " SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1))") (("1" (case "f!1`mp
(inverse(f!1)`mp
(SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)))
=
f!1`mp
(SigmaV[below[l!1], n!1]
(0, l!1 - 1, x!1 * (inverse(f!1)`mp o F!1)))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -4) (("2" (inst -3 "x!1" "(inverse(f!1)`mp o F!1)") (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (linear_comp_TCC1 0 (linear_comp_TCC1-1 nil 3519717217 ("" (subtype-tcc) nil nil) ((same? const-decl "bool" linear_map nil)) nil)) (linear_comp 0 (linear_comp-1 nil 3519726821 ("" (skosimp) (("" (typepred "f!1") (("" (typepred "g!1") (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (expand "o" 1) (("3" (expand "o" 1) (("3" (inst -3 "l!2") (("3" (inst -3 "x!1" "F!1") (("3" (replace -3) (("3" (inst -6 "l!2") (("3" (inst -6 "x!1" "g!1`mp o F!1") (("1" (expand "o" -6) (("1" (expand "o" 1) (("1" (expand "SigmaV") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Map_linear type-eq-decl nil linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def nil) (Map type-eq-decl nil linear_map 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 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (Maping type-eq-decl nil linear_map nil) (Vector type-eq-decl nil vectors "vectors/") (posnat nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (linear_map_e? const-decl "bool" linear_map_def nil) (below type-eq-decl nil nat_types nil) (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma "reals/") (* const-decl "Vector" vectors "vectors/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (l!2 skolem-const-decl "posnat" matrix_operator nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (m!1 skolem-const-decl "posnat" matrix_operator nil) (g!1 skolem-const-decl "Map_linear(n!1, m!1)" matrix_operator nil) (O const-decl "T3" function_props nil) (O const-decl "Maping" linear_map nil)) shostak)) (linear_matrix_TCC1 0 (linear_matrix_TCC1-1 nil 3519051742 ("" (subtype-tcc) nil nil) nil nil)) (linear_matrix_TCC2 0 (linear_matrix_TCC2-1 nil 3519051742 ("" (subtype-tcc) nil nil) nil nil)) (linear_matrix_TCC3 0 (linear_matrix_TCC3-1 nil 3519051742 ("" (assuming-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) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Mat type-eq-decl nil matrices nil) (integer nonempty-type-from-decl nil integers nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (linear_matrix_TCC4 0 (linear_matrix_TCC4-1 nil 3547201813 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Mat type-eq-decl nil matrices nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_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)) nil)) (linear_matrix 0 (thm "thm" 3520180838 ("" (skosimp) (("" (expand "SigmaV") (("" (apply-extensionality 1) (("1" (hide 2) (("1" (expand "*") (("1" (lemma "sigma_prop") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k)" "LAMBDA(k:below[A!1`cols],j: below[l!1]): F!1(j)(k)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_comm") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (i: below(A!1`cols),j_1:below[l!1]):
A!1`matrix(x!1, i) * F!1(j_1)(i)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (grind) nil nil)) nil) ("4" (skosimp) (("4" (grind) nil nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((SigmaV const-decl "Vector[n]" sigma_vector nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_prop formula-decl nil matrices nil) (sigma_comm formula-decl nil matrices nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (posint nonempty-type-eq-decl nil integers 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) (int_minus_int_is_int application-judgement "int" integers nil) (m!1 skolem-const-decl "posnat" matrix_operator nil) (below type-eq-decl nil nat_types nil) (l!1 skolem-const-decl "posnat" matrix_operator nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (A!1 skolem-const-decl "Mat(n!1, m!1)" matrix_operator nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Index type-eq-decl nil vectors "vectors/") (Mat type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (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)) shostak) (thm "thm" 3519987399 ("" (skosimp) (("" (expand "SigmaV") (("" (apply-extensionality 1) (("1" (hide 2) (("1" (expand "*") (("1" (lemma "sigma_prop") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k)" "LAMBDA(k:below[A!1`cols],j: below[l!1]): F!1(j)(k)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_comm") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (i: below(A!1`cols),j_1:below[l!1]):
A!1`matrix(x!1, i) * F!1(j_1)(i)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (skosimp) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ((Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil) (Index type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (sigma_comm formula-decl nil matrices nil) (sigma_prop formula-decl nil matrices nil) (SigmaV const-decl "Vector[n]" sigma_vector nil)) shostak) (thm "thm" 3519620371 ("" (skosimp) (("" (expand "SigmaV") (("" (apply-extensionality 1) (("1" (hide 2) (("1" (expand "*") (("1" (lemma "sigma_prop") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k)" "LAMBDA(k:below[A!1`cols],j: below[l!1]): F!1(j)(k)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_comm") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (i: below(A!1`cols),j_1:below[l!1]):
A!1`matrix(x!1, i) * F!1(j_1)(i)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (grind) nil nil)) nil) ("4" (skosimp) (("4" (assert) (("4" (grind) nil nil)) nil)) nil) ("5" (skosimp) (("5" (grind) nil nil)) nil)) nil)) nil)) nil) ((Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil) (Index type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (sigma_comm formula-decl nil matrices nil) (sigma_prop formula-decl nil matrices nil) (SigmaV const-decl "Vector[n]" sigma_vector nil)) shostak) (linear_matrix-1 nil 3519054322 ("" (skosimp) (("" (expand "SigmaV") (("" (apply-extensionality 1) (("1" (hide 2) (("1" (expand "*") (("1" (lemma "sigma_prop") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k)" "LAMBDA(k:below[A!1`cols],j: below[l!1]): F!1(j)(k)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_comm") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (i: below(A!1`cols),j_1:below[l!1]):
A!1`matrix(x!1, i) * F!1(j_1)(i)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (skosimp) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ((Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil) (Index type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (sigma_comm formula-decl nil matrices nil) (sigma_prop formula-decl nil matrices nil) (SigmaV const-decl "Vector[n]" sigma_vector nil)) shostak)) (equa_inv_TCC1 0 (equa_inv_TCC1-1 nil 3521281307 ("" (subtype-tcc) nil nil) ((same? const-decl "bool" linear_map nil)) nil)) (equa_inv_TCC2 0 (equa_inv_TCC2-1 nil 3521281307 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Map type-eq-decl nil linear_map nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (id const-decl "Maping" linear_map nil) (O const-decl "Maping" linear_map nil)) nil)) (equa_inv_TCC3 0 (equa_inv_TCC3-1 nil 3521281729 ("" (subtype-tcc) nil nil) ((O const-decl "Maping" linear_map nil) (id const-decl "Maping" linear_map nil) (same? const-decl "bool" linear_map nil)) nil)) (equa_inv_TCC4 0 (equa_inv_TCC4-1 nil 3521281729 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Map type-eq-decl nil linear_map nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (O const-decl "Maping" linear_map nil) (id const-decl "Maping" linear_map nil)) nil)) (equa_inv 0 (thm "thm" 3521282777 ("" (skosimp) (("" (expand "bijective?") (("" (expand "bijective?") (("" (split) (("1" (expand "injective?") (("1" (skosimp) (("1" (case "(h!1 o f!1)`mp(x1!1) = (h!1 o f!1)`mp(x2!1)") (("1" (replace -4) (("1" (assert) (("1" (expand "id" -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp) (("2" (inst 1 "g!1`mp(y!1)") (("1" (case "(f!1`mp o g!1`mp)(y!1)= f!1`mp(g!1`mp(y!1))") (("1" (swap-rel -1) (("1" (replace -1) (("1" (expand "o" -2) (("1" (replace -2) (("1" (expand "id" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" linear_map nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (O const-decl "T3" function_props nil) (id const-decl "Maping" linear_map nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (Maping type-eq-decl nil linear_map nil) (posnat nonempty-type-eq-decl nil integers nil) (Vector type-eq-decl nil vectors "vectors/") (same? const-decl "bool" linear_map nil) (O const-decl "Maping" linear_map nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Map type-eq-decl nil linear_map nil) (Index type-eq-decl nil vectors "vectors/") (injective? const-decl "bool" functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (g!1 skolem-const-decl "Map(n!1, n!1)" matrix_operator nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil)) shostak) (equa_inv-1 nil 3521281353 ("" (skosimp) (("" (split) (("1" (expand "bijective?") (("1" (expand "bijective?") (("1" (split) (("1" (expand "injective?") (("1" (skosimp) (("1" (case "(h!1 o f!1)`mp(x1!1) = (h!1 o f!1)`mp(x2!1)") (("1" (replace -4) (("1" (assert) (("1" (expand "id" -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp) (("2" (inst 1 "g!1`mp(y!1)") (("1" (case "(f!1`mp o g!1`mp)(y!1)= f!1`mp(g!1`mp(y!1))") (("1" (swap-rel -1) (("1" (replace -1) (("1" (expand "o" -2) (("1" (replace -2) (("1" (expand "id" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil) ((Index type-eq-decl nil vectors "vectors/") (Map type-eq-decl nil linear_map nil) (O const-decl "Maping" linear_map nil) (same? const-decl "bool" linear_map nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (id const-decl "Maping" linear_map nil) (bijective? const-decl "bool" linear_map nil)) shostak)) (inv_uni 0 (thm "thm" 3521294714 ("" (skosimp) (("" (split) (("1" (expand "o" -1) (("1" (apply-extensionality 1) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (apply-extensionality 1) (("3" (lemma "extensionality_postulate[Vector[n!1],Vector[n!1]]") (("3" (inst -1 "f!1`mp o g!1`mp" "id(n!1)`mp") (("1" (case "(FORALL (x: Vector[n!1]): (f!1`mp o g!1`mp)(x) = id(n!1)`mp(x))") (("1" (assert) (("1" (inst -1 "x!1") (("1" (expand "o" -1) (("1" (case "inverse(n!1)(f!1)`mp (f!1`mp(g!1`mp(x!1))) = inverse(n!1)(f!1)`mp(id(n!1)`mp(x!1))") (("1" (expand "id" -1) (("1" (assert) (("1" (expand "inverse" -1) (("1" (lemma "comp_inverse_left[Vector[n!1],Vector[n!1]]") (("1" (inst -1 "g!1`mp(x!1)" "f!1`mp") (("1" (assert) (("1" (replace -1) (("1" (expand "inverse" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "equa_inv") (("2" (inst -1 "n!1" "f!1" "g!1" "h!1") (("2" (assert) (("2" (expand "o" -1) (("2" (expand "bijective?" -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (hide 2 3 4) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil) ("3" (skosimp) (("3" (hide 2 3 4) (("3" (grind) nil nil)) nil)) nil) ("4" (hide 2 3 4) (("4" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide 2 3 4) (("3" (grind) nil nil)) nil) ("4" (grind) nil nil) ("5" (grind) nil nil)) nil) ("2" (split) (("1" (skosimp) (("1" (assert) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("3" (split) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (apply-extensionality) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (apply-extensionality 1) (("3" (expand "inverse" 1) (("3" (assert) (("3" (lemma "extensionality_postulate[Vector[n!1],Vector[n!1]]") (("3" (inst -1 "(h!1 o f!1)`mp" "id(n!1)`mp") (("1" (case "(FORALL (x: Vector[n!1]): (h!1 o f!1)`mp(x) = id(n!1)`mp(x))") (("1" (assert) (("1" (inst -1 "inverse[Vector[n!1],Vector[n!1]](f!1`mp)(x!1)") (("1" (assert) (("1" (expand "id" -1) (("1" (assert) (("1" (expand "o" -1) (("1" (assert) (("1" (expand "o" -1) (("1" (assert) (("1" (lemma "comp_inverse_right[Vector[n!1],Vector[n!1]]") (("1" (inst -1 "x!1" "f!1`mp") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (lemma "equa_inv") (("2" (inst -1 "n!1" "f!1" "g!1" "h!1") (("2" (assert) (("2" (expand "bijective?" -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (hide 2 3 4) (("4" (grind) nil nil)) nil) ("5" (hide 2 3 4) (("5" (grind) nil nil)) nil)) nil) ("2" (split) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("3" (split) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (inverse const-decl "Maping" linear_map nil) (Map type-eq-decl nil linear_map nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (extensionality_postulate formula-decl nil functions nil) (comp_inverse_left formula-decl nil function_inverse nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (equa_inv formula-decl nil matrix_operator nil) (bijective? const-decl "bool" linear_map nil) (bijective? const-decl "bool" functions nil) (inverse const-decl "D" function_inverse nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (O const-decl "T3" function_props nil) (id const-decl "Maping" linear_map nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (g!1 skolem-const-decl "Map(n!1, n!1)" matrix_operator nil) (f!1 skolem-const-decl "Map(n!1, n!1)" matrix_operator nil) (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (O const-decl "Maping" linear_map nil) (comp_inverse_right formula-decl nil function_inverse nil) (same? const-decl "bool" linear_map nil) (h!1 skolem-const-decl "Map(n!1, n!1)" matrix_operator nil)) shostak) (inv_uni-1 nil 3521284340 ("" (skosimp) (("" (split) (("1" (expand "o" -1) (("1" (apply-extensionality 1) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (apply-extensionality 1) (("3" (lemma "extensionality_postulate[Vector[n!1],Vector[n!1]]") (("3" (inst -1 "f!1`mp o g!1`mp" "id(n!1)`mp") (("1" (case "(FORALL (x: Vector[n!1]): (f!1`mp o g!1`mp)(x) = id(n!1)`mp(x))") (("1" (assert) (("1" (inst -1 "x!1") (("1" (expand "o" -1) (("1" (case "inverse(n!1)(f!1)`mp (f!1`mp(g!1`mp(x!1))) = inverse(n!1)(f!1)`mp(id(n!1)`mp(x!1))") (("1" (expand "id" -1) (("1" (assert) (("1" (expand "inverse" -1) (("1" (lemma "comp_inverse_left[Vector[n!1],Vector[n!1]]") (("1" (inst -1 "g!1`mp(x!1)" "f!1`mp") (("1" (assert) (("1" (replace -1) (("1" (expand "inverse" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "equa_inv") (("2" (inst -1 "n!1" "f!1" "g!1" "h!1") (("2" (assert) (("2" (expand "o" -1) (("2" (expand "bijective?" -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (hide 2 3 4) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil) ("3" (skosimp) (("3" (hide 2 3 4) (("3" (grind) nil nil)) nil)) nil) ("4" (hide 2 3 4) (("4" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide 2 3 4) (("3" (grind) nil nil)) nil) ("4" (grind) nil nil) ("5" (grind) nil nil)) nil) ("2" (split) (("1" (skosimp) (("1" (assert) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("3" (split) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (apply-extensionality) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (apply-extensionality 1) (("3" (expand "inverse" 1) (("3" (assert) (("3" (lemma "extensionality_postulate[Vector[n!1],Vector[n!1]]") (("3" (inst -1 "(h!1 o f!1)`mp" "id(n!1)`mp") (("1" (case "(FORALL (x: Vector[n!1]): (h!1 o f!1)`mp(x) = id(n!1)`mp(x))") (("1" (assert) (("1" (inst -1 "x!1") (("1" (postpone) nil nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (hide 2 3 4) (("4" (grind) nil nil)) nil) ("5" (hide 2 3 4) (("5" (grind) nil nil)) nil)) nil) ("2" (split) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil) ("3" (split) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((same? const-decl "bool" linear_map nil) (O const-decl "Maping" linear_map nil) (Index type-eq-decl nil vectors "vectors/") (id const-decl "Maping" linear_map nil) (bijective? const-decl "bool" linear_map nil) (Map type-eq-decl nil linear_map nil) (inverse const-decl "Maping" linear_map nil) (Maping type-eq-decl nil linear_map nil) (Vector type-eq-decl nil vectors "vectors/")) shostak)) (L_TCC1 0 (L_TCC1-1 nil 3518879978 ("" (subtype-tcc) nil nil) nil nil)) (L_TCC2 0 (L_TCC2-1 nil 3518879978 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Map type-eq-decl nil linear_map nil) (linear_map_e? const-decl "bool" linear_map_def nil) (Map_linear type-eq-decl nil linear_map_def nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (linear_map_e? const-decl "bool" linear_map_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (T_TCC1 0 (T_TCC1-1 nil 3480761416 ("" (subtype-tcc) nil nil) nil nil)) (T_TCC2 0 (T_TCC2-1 nil 3480761416 ("" (subtype-tcc) nil nil) nil nil)) (T_TCC3 0 (T_TCC3-1 nil 3518879978 ("" (subtype-tcc) nil nil) nil nil)) (T_TCC4 0 (T_TCC4-1 nil 3518879978 ("" (subtype-tcc) nil nil) nil nil)) (T_TCC5 0 (T_TCC5-1 nil 3519620172 ("" (assuming-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) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Mat type-eq-decl nil matrices nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (integer nonempty-type-from-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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)) nil)) (T_TCC6 0 (tcc "tcc" 3520690127 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (apply-extensionality) (("1" (hide 2) (("1" (expand "SigmaV") (("1" (assert) (("1" (expand "o") (("1" (expand "*") (("1" (expand "*") (("1" (lemma "sigma_prop") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (i: below[A!1`cols]):
A!1`matrix(x!2, i)" "lambda(i:below[A!1`cols],j: below[l!1]): x!1(j) * F!1(j)(i)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_comm") (("1" (inst -1 "A!1`cols" "l!1" " LAMBDA (i_1:below(A!1`cols),j_1: below(l!1)):
A!1`matrix(x!2, i_1) * (x!1(j_1) * F!1(j_1)(i_1))") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_prop") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((linear_map_e? const-decl "bool" linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def 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 nat_types nil) (O const-decl "T3" function_props nil) (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (m!1 skolem-const-decl "posnat" matrix_operator nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (Mat type-eq-decl nil matrices nil) (A!1 skolem-const-decl "Mat(m!1, n!1)" matrix_operator nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (* const-decl "Vector" vectors "vectors/") (posint nonempty-type-eq-decl nil integers nil) (sigma_comm formula-decl nil matrices nil) (sigma_prop formula-decl nil matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak) (T_TCC6-1 nil 3520674133 ("" (subtype-tcc) nil nil) ((* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil) (* const-decl "Vector" vectors "vectors/") (sigma_comm formula-decl nil matrices nil) (sigma_prop formula-decl nil matrices nil)) nil)) (T_matr_TCC1 0 (T_matr_TCC1-1 nil 3519447525 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil)) nil)) (T_matr_TCC2 0 (T_matr_TCC2-1 nil 3519447525 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Mat type-eq-decl nil matrices nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_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)) nil)) (T_matr_TCC3 0 (T_matr_TCC3-1 nil 3519733511 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Mat type-eq-decl nil matrices nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_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) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (T_matr 0 (thm "thm" 3520673892 ("" (skosimp) (("" (expand "T") (("" (apply-extensionality) (("1" (hide 2) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (grind) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (A!1 skolem-const-decl "Mat(m!1, n!1)" matrix_operator nil) (Mat type-eq-decl nil matrices nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (below type-eq-decl nil naturalnumbers nil) (m!1 skolem-const-decl "posnat" matrix_operator nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (below type-eq-decl nil nat_types 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak) (thm "thm" 3520158370 ("" (skosimp) (("" (expand "T") (("" (apply-extensionality) (("1" (hide 2) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil)) shostak) (thm "thm" 3519620399 ("" (skosimp) (("" (expand "T") (("" (apply-extensionality) (("1" (hide 2) (("1" (expand "*") (("1" (case "n!1=A!1`cols") (("1" (replace -1) (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil)) shostak) (hm "thm" 3519615120 ("" (skosimp) (("" (expand "T") (("" (apply-extensionality) (("1" (hide 2) (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil)) shostak) (T_matr-1 nil 3519447551 ("" (skosimp) (("" (expand "T") (("" (apply-extensionality) (("1" (hide 2) (("1" (expand "*") (("1" (typepred "A!1") (("1" (replace -2) (("1" (lemma "sigma_eq[below[n!1]]") (("1" (inst -1 " LAMBDA (i: below[n!1]): A!1`matrix(x!2, i) * x!1(i)" " LAMBDA (k: below(A!1`cols)): A!1`matrix(x!2, k) * x!1(k)" "n!1-1" "0") (("1" (assert) (("1" (assert) (("1" (grind) (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ((* const-decl "Vector[M`rows]" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil)) shostak)) (linear_map_T 0 (thm "thm" 3520673925 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (lemma "T_matr") (("3" (inst -1 "m!1" "n!1" "A!1" "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)") (("3" (replace -1) (("3" (lemma "linear_matrix") (("3" (inst -1 "l!1" "n!1" "m!1" "A!1" "x!1*F!1") (("3" (replace -1) (("3" (apply-extensionality 1) (("1" (hide 2) (("1" (expand "SigmaV" 1) (("1" (lemma "sigma_eq[below[l!1]]") (("1" (inst -1 "LAMBDA (j: below[l!1]): (A!1 * (x!1 * F!1)(j))(x!2)" "LAMBDA (j: below[l!1]):
(x!1 * (T(n!1, m!1)(A!1)`mp o F!1))(j)(x!2)" "l!1-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (lemma "T_matr") (("1" (expand "o" 1) (("1" (expand "*" 1) (("1" (inst -1 "m!1" "n!1" "A!1" "F!1(n!2)") (("1" (replace -1) (("1" (expand "*" 1) (("1" (lemma "sigma_scal[below[A!1`cols]]") (("1" (inst -1 "LAMBDA (k: below(A!1`cols)): A!1`matrix(x!2, k) * F!1(n!2)(k)" "x!1(n!2)" "A!1`cols-1" "0") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((linear_map_e? const-decl "bool" linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def 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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Mat type-eq-decl nil matrices nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (OR const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (linear_matrix formula-decl nil matrix_operator nil) (sigma_eq formula-decl nil sigma "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (* const-decl "Vector" vectors "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_scal formula-decl nil sigma "reals/") (l!1 skolem-const-decl "posnat" matrix_operator nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (m!1 skolem-const-decl "posnat" matrix_operator nil) (A!1 skolem-const-decl "Mat(m!1, n!1)" matrix_operator nil) (* const-decl "Vector[M`rows]" matrices nil) (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (O const-decl "T3" function_props nil) (T_matr formula-decl nil matrix_operator nil) (sigma def-decl "real" sigma "reals/") (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak) (thm "thmmm" 3519987462 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (lemma "T_matr") (("3" (inst -1 "m!1" "n!1" "A!1" "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)") (("3" (replace -1) (("3" (lemma "linear_matrix") (("3" (inst -1 "l!1" "n!1" "m!1" "A!1" "x!1*F!1") (("3" (replace -1) (("3" (apply-extensionality 1) (("1" (hide 2) (("1" (expand "SigmaV" 1) (("1" (lemma "sigma_eq[below[l!1]]") (("1" (inst -1 "LAMBDA (j: below[l!1]): (A!1 * (x!1 * F!1)(j))(x!2)" "LAMBDA (j: below[l!1]):
(x!1 * (T(n!1, m!1)(A!1)`mp o F!1))(j)(x!2)" "l!1-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (lemma "T_matr") (("1" (expand "o" 1) (("1" (expand "*" 1) (("1" (inst -1 "m!1" "n!1" "A!1" "F!1(n!2)") (("1" (replace -1) (("1" (expand "*" 1) (("1" (lemma "sigma_scal[below[A!1`cols]]") (("1" (inst -1 "LAMBDA (k: below(A!1`cols)): A!1`matrix(x!2, k) * F!1(n!2)(k)" "x!1(n!2)" "A!1`cols-1" "0") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma "reals/") (Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (* const-decl "Vector[M`rows]" matrices nil) (sigma_scal formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (Mat type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (thm "thm" 3519912292 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (lemma "T_matr") (("3" (inst -1 "m!1" "n!1" "A!1" "SigmaV[below[l!1], n!1](0, l!1 - 1, x!1 * F!1)") (("3" (replace -1) (("3" (lemma "linear_matrix") (("3" (inst -1 "l!1" "n!1" "m!1" "A!1" "x!1*F!1") (("3" (replace -1) (("3" (apply-extensionality 1) (("1" (hide 2) (("1" (expand "SigmaV" 1) (("1" (lemma "sigma_eq[below[l!1]]") (("1" (inst -1 "LAMBDA (j: below[l!1]): (A!1 * (x!1 * F!1)(j))(x!2)" "LAMBDA (j: below[l!1]):
(x!1 * (T(n!1, m!1)(A!1)`mp o F!1))(j)(x!2)" "l!1-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (lemma "T_matr") (("1" (expand "o" 1) (("1" (expand "*" 1) (("1" (inst -1 "m!1" "n!1" "A!1" "F!1(n!2)") (("1" (replace -1) (("1" (expand "*" 1) (("1" (lemma "sigma_scal[below[A!1`cols]]") (("1" (inst -1 "LAMBDA (k: below(A!1`cols)): A!1`matrix(x!2, k) * F!1(n!2)(k)" "x!1(n!2)" "A!1`cols-1" "0") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) (("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma def-decl "real" sigma "reals/") (Map_linear type-eq-decl nil linear_map_def nil) (Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (* const-decl "Vector[M`rows]" matrices nil) (sigma_scal formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (Mat type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (thm "thm" 3519623226 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (grind) nil nil) ("2" (skosimp) (("2" (lemma "T_matr") (("2" (inst -1 "m!1" "n!1" "A!1" "SigmaV(0, m!2 - 1, x!1 * F!1)") (("1" (replace -1) (("1" (lemma "linear_matrix") (("1" (inst -1 "m!2" "n!1" "m!1" "A!1" "x!1 * F!1") (("1" (replace -1) (("1" (apply-extensionality 1) (("1" (expand "SigmaV" 1) (("1" (hide 2) (("1" (lemma "sigma_eq[below[m!2]]") (("1" (inst -1 " LAMBDA (j: below[m!2]): (A!1 * (x!1 * F!1)(j))(x!2)" "LAMBDA (j: Index[m!2]):
(x!1 * (T(n!1, m!1)(A!1)`mp o F!1))(j)(x!2)" "m!2-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (lemma "T_matr") (("1" (expand "o" 1) (("1" (expand "*" 1) (("1" (inst -1 "m!1" "n!1" "A!1" "F!1(n!2)") (("1" (replace -1) (("1" (expand "*" 1) (("1" (lemma "sigma_scal[below(A!1`cols)]") (("1" (inst -1 "LAMBDA (k: below(A!1`cols)): A!1`matrix(x!2, k) * F!1(n!2)(k)" "x!1(n!2)" "A!1`cols-1" "0") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (sigma_eq formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (sigma_scal formula-decl nil sigma "reals/") (* const-decl "Vector[M`rows]" matrices nil) (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (sigma def-decl "real" sigma "reals/")) shostak) (no "no" 3483461149 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (lemma "linear_matrix") (("" (assert) (("" (lemma "T_matr") (("" (assert) (("" (hide -2) (("" (lemma "linear_matrix") (("" (expand "linear_map_e?") (("" (skosimp) (("" (inst -2 "m!1" "n!1" "A!1" "SigmaV(0,m!2-1,x!1*F!1)") (("1" (replace -2) (("1" (inst -1 "m!2" "n!1" "m!1" "A!1" "x!1*F!1") (("1" (replace -1) (("1" (expand "SigmaV" 1) (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (lemma "sigma_eq[below[m!2]]") (("1" (inst -1 "LAMBDA (j: below[m!2]): (A!1 * (x!1 * F!1)(j))(x!2)" "LAMBDA (j: Index[m!2]):
(x!1 * (T(n!1, m!1)(A!1)`mp o F!1))(j)(x!2)" "m!2-1" "0") (("1" (assert) (("1" (skosimp) (("1" (postpone) nil nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil) ("4" (grind) nil nil) ("5" (skosimp) (("5" (skosimp) (("5" (grind) nil nil)) nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Mat type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (sigma_eq formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (sigma_scal formula-decl nil sigma "reals/") (Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (* const-decl "Vector[M`rows]" matrices nil) (sigma def-decl "real" sigma "reals/")) shostak) (linear_map_T-1 nil 3483359278 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (lemma "T_matr") (("" (inst -1 "A!1" "sigmaV(0, n - 1, x!1 * F!1)") (("" (assert) (("" (replace -1) (("" (lemma "extensionality[below[n],real]") (("" (inst -1 "A!1 * sigmaV(0, n - 1, x!1 * F!1)" "sigmaV(0, n - 1, x!1 * (T(A!1) o F!1))") (("" (name "ll" "(FORALL (x: below[n]):
(A!1 * sigmaV(0, n - 1, x!1 * F!1))(x) =
sigmaV(0, n - 1, x!1 * (T(A!1) o F!1))(x))") (("" (replace -1) (("" (case "ll") (("1" (assert) nil nil) ("2" (hide -1) (("2" (expand "ll" 1) (("2" (hide -1) (("2" (skosimp) (("2" (expand "sigmaV" 1) (("2" (expand "*" 1) (("2" (name "l1" " LAMBDA (i_1: below[n]):
A!1(i_1, x!2) *
sigma(0, n - 1,
LAMBDA (j: below[n]): (x!1(j) * F!1(j))(i_1))") (("2" (replace -1) (("2" (name "l2" "LAMBDA (j: below[n]): (x!1(j) * (T(A!1) o F!1)(j))(x!2)") (("2" (replace -1) (("2" (lemma "sigma_eq[below[n]]") (("2" (inst -1 "l1" "l2" "n-1" "0") (("2" (name "t1" "(FORALL (n_1: subrange(0, n - 1)): l1(n_1) = l2(n_1))") (("2" (replace -1) (("2" (case "t1") (("1" (assert) nil nil) ("2" (expand "t1" 1) (("2" (skosimp) (("2" (expand "l1" 1) (("2" (expand "l2" 1) (("2" (expand "o") (("2" (lemma "T_matr") (("2" (inst -1 "A!1" "F!1(n!1)") (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (sigma def-decl "real" sigma "reals/") (sigma_scal formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/")) shostak)) (map_matrix_bij 0 (thm "thm" 3520673991 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (apply-extensionality) (("" (hide 2) (("" (expand "L") (("" (lemma "linear_map_T") (("" (inst -1 "m!1" "n!1" "A!1") (("" (lemma "T_matr") (("" (inst -1 "m!1" "n!1" "A!1" "e(n!1)(x!2)") (("" (replace -1) (("" (expand "*") (("" (lemma "sigma_middle[below(A!1`cols)]") (("1" (inst -1 " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "A!1`cols-1" "x!2" "0") (("1" (assert) (("1" (replace -1) (("1" (case "sigma(0, x!2 - 1,
LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)) = 0") (("1" (replace -1) (("1" (assert) (("1" (case "sigma(1 + x!2, A!1`cols - 1,
LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k))=0") (("1" (replace -1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[below(A!1`cols)]") (("2" (inst -1 "A!1`cols-1" "1+x!2") (("2" (swap-rel -1) (("2" (replace -1) (("2" (lemma "sigma_eq[below(A!1`cols)]") (("2" (inst -1 " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "(LAMBDA (i: below(A!1`cols)): 0)" "A!1`cols-1" "1+x!2") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_zero[below(A!1`cols)]") (("2" (inst -1 "x!2-1" "0") (("2" (swap-rel -1) (("2" (hide 2) (("2" (swap-rel 1) (("2" (lemma "sigma_eq[below(A!1`cols)]") (("2" (inst -1 "LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "(LAMBDA (i: below(A!1`cols)): 0)" "x!2-1" "0") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (Mat type-eq-decl nil matrices nil) (Map_linear type-eq-decl nil linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def nil) (Map type-eq-decl nil linear_map nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Maping type-eq-decl nil linear_map nil) (Vector type-eq-decl nil vectors "vectors/") (> 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (Index type-eq-decl nil vectors "vectors/") (below type-eq-decl nil nat_types nil) (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (* const-decl "Vector[M`rows]" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil sigma "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (linear_map_e? const-decl "bool" linear_map_def nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (* const-decl "Vector" vectors "vectors/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_zero formula-decl nil sigma "reals/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (sigma_nat application-judgement "nat" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma def-decl "real" sigma "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (sigma_middle formula-decl nil sigma "reals/") (T_matr formula-decl nil matrix_operator nil) (linear_map_T formula-decl nil matrix_operator nil)) shostak) (thm "thm" 3519987610 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (apply-extensionality) (("" (hide 2) (("" (expand "L") (("" (lemma "linear_map_T") (("" (inst -1 "m!1" "n!1" "A!1") (("" (lemma "T_matr") (("" (inst -1 "m!1" "n!1" "A!1" "e(n!1)(x!2)") (("" (replace -1) (("" (expand "*") (("" (lemma "sigma_middle[below(A!1`cols)]") (("" (inst -1 " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "A!1`cols-1" "x!2" "0") (("" (assert) (("" (replace -1) (("" (case "sigma(0, x!2 - 1,
LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)) = 0") (("1" (replace -1) (("1" (assert) (("1" (case "sigma(1 + x!2, A!1`cols - 1,
LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k))=0") (("1" (replace -1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[below(A!1`cols)]") (("2" (inst -1 "A!1`cols-1" "1+x!2") (("2" (swap-rel -1) (("2" (replace -1) (("2" (lemma "sigma_eq[below(A!1`cols)]") (("2" (inst -1 " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "(LAMBDA (i: below(A!1`cols)): 0)" "A!1`cols-1" "1+x!2") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_zero[below(A!1`cols)]") (("2" (inst -1 "x!2-1" "0") (("2" (swap-rel -1) (("2" (hide 2) (("2" (swap-rel 1) (("2" (lemma "sigma_eq[below(A!1`cols)]") (("2" (inst -1 "LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "(LAMBDA (i: below(A!1`cols)): 0)" "x!2-1" "0") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_middle formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (sigma_nat application-judgement "nat" vectors "vectors/") (sigma_zero formula-decl nil sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (* const-decl "Vector" vectors "vectors/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (* const-decl "Vector[M`rows]" matrices nil) (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (Mat type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (thm "thm" 3519909524 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (apply-extensionality) (("" (hide 2) (("" (expand "L") (("" (lemma "linear_map_T") (("" (inst -1 "m!1" "n!1" "A!1") (("" (lemma "T_matr") (("" (inst -1 "m!1" "n!1" "A!1" "e(n!1)(x!2)") (("" (replace -1) (("" (expand "*") (("" (lemma "sigma_middle[below(A!1`cols)]") (("1" (inst -1 " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "A!1`cols-1" "x!2" "0") (("1" (assert) (("1" (replace -1) (("1" (case "sigma(0, x!2 - 1,
LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)) = 0") (("1" (replace -1) (("1" (assert) (("1" (case "sigma(1 + x!2, A!1`cols - 1,
LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k))=0") (("1" (replace -1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[below(A!1`cols)]") (("2" (inst -1 "A!1`cols-1" "1+x!2") (("2" (swap-rel -1) (("2" (replace -1) (("2" (lemma "sigma_eq[below(A!1`cols)]") (("2" (inst -1 " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "(LAMBDA (i: below(A!1`cols)): 0)" "A!1`cols-1" "1+x!2") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_zero[below(A!1`cols)]") (("2" (inst -1 "x!2-1" "0") (("2" (swap-rel -1) (("2" (hide 2) (("2" (swap-rel 1) (("2" (lemma "sigma_eq[below(A!1`cols)]") (("2" (inst -1 "LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "(LAMBDA (i: below(A!1`cols)): 0)" "x!2-1" "0") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_middle formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (sigma_nat application-judgement "nat" vectors "vectors/") (sigma_zero formula-decl nil sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (* const-decl "Vector" vectors "vectors/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (* const-decl "Vector[M`rows]" matrices nil) (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (Mat type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (thm "thm" 3519625149 ("" (skosimp) (("" (apply-extensionality) (("" (hide 2) (("" (apply-extensionality) (("" (hide 2) (("" (expand "L") (("" (lemma "linear_map_T") (("" (inst -1 "m!1" "n!1" "A!1") (("" (lemma "T_matr") (("" (inst -1 "m!1" "n!1" "A!1" "e(n!1)(x!2)") (("1" (replace -1) (("1" (expand "*") (("1" (lemma "sigma_middle[below(A!1`cols)]") (("1" (inst -1 " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "A!1`cols-1" "x!2" "0") (("1" (assert) (("1" (replace -1) (("1" (case "sigma(0, x!2 - 1,
LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)) = 0") (("1" (replace -1) (("1" (assert) (("1" (case "sigma(1 + x!2, A!1`cols - 1,
LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k))=0") (("1" (replace -1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[below(A!1`cols)]") (("2" (inst -1 "A!1`cols-1" "1+x!2") (("2" (swap-rel -1) (("2" (replace -1) (("2" (lemma "sigma_eq[below(A!1`cols)]") (("2" (inst -1 " LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "(LAMBDA (i: below(A!1`cols)): 0)" "A!1`cols-1" "1+x!2") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_zero[below(A!1`cols)]") (("2" (inst -1 "x!2-1" "0") (("2" (swap-rel -1) (("2" (hide 2) (("2" (swap-rel 1) (("2" (lemma "sigma_eq[below(A!1`cols)]") (("2" (inst -1 "LAMBDA (k: below(A!1`cols)):
A!1`matrix(x!1, k) * e(n!1)(x!2)(k)" "(LAMBDA (i: below(A!1`cols)): 0)" "x!2-1" "0") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_middle formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (sigma_nat application-judgement "nat" vectors "vectors/") (sigma_zero formula-decl nil sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (* const-decl "Vector" vectors "vectors/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (* const-decl "Vector[M`rows]" matrices nil) (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (Mat type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (thm "thm" 3482753444 ("" (skosimp) (("" (lemma "comp_equal_matri_n") (("" (inst -1 "L(e!1)(T(A!1))" "A!1") (("" (name "aa" "FORALL (i: below[n], j: below[n]): L(e!1)(T(A!1))(i, j) = A!1(i, j)") (("" (replace -1) (("" (case "aa") (("1" (assert) nil nil) ("2" (expand "aa" 1) (("2" (skosimp) (("2" (expand "L" 1) (("2" (lemma "T_A") (("2" (inst -1 "A!1" "e!1" "i!1" "j!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_middle formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (sigma_nat application-judgement "nat" vectors "vectors/") (sigma_zero formula-decl nil sigma "reals/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (* const-decl "Vector" vectors "vectors/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (* const-decl "Vector[M`rows]" matrices nil) (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (Mat type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak) (one-1 nil 3482752798 ("" (skosimp) (("" (expand "L") (("" (lemma "comp_equal_matri") (("" (inst -1 "LAMBDA (i, j: below[n]): T(A!1)(e!1(i))(j)" "A!1") (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil) ((Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/")) shostak)) (operator_TCC1 0 (operator_TCC1-1 nil 3519051742 ("" (subtype-tcc) nil nil) nil nil)) (operator_TCC2 0 (operator_TCC2-1 nil 3519051742 ("" (subtype-tcc) nil nil) nil nil)) (operator 0 (thm "thm" 3519625216 ("" (skosimp) (("" (apply-extensionality) 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) (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Map type-eq-decl nil linear_map nil) (linear_map_e? const-decl "bool" linear_map_def nil) (Map_linear type-eq-decl nil linear_map_def nil) (Mat type-eq-decl nil matrices nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator 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)) shostak) (thm "thm" 3482754329 ("" (skosimp) (("" (lemma "comp_equal_matri_n") (("" (inst -1 "L(e!1)(f!1)" "L(e!1)(g!1)") (("" (name "ff" "(FORALL (i: below[n], j: below[n]):
L(e!1)(f!1)(i, j) = L(e!1)(g!1)(i, j))") (("" (replace -1) (("" (case "ff") (("1" (assert) nil nil) ("2" (expand "ff" 1) (("2" (skosimp) (("2" (expand "L" 1) (("2" (expand "=" -4) (("2" (inst -4 "e!1(i!1)") (("2" (lemma "extensionality_postulate[below[n],real]") (("2" (inst -1 " f!1(e!1(i!1))" "g!1(e!1(i!1))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil) (Map_linear type-eq-decl nil linear_map_def nil) (Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (Vector type-eq-decl nil vectors "vectors/")) shostak) (operator-1 nil 3482659208 ("" (skosimp) (("" (expand "L") (("" (grind) (("" (grind) (("" (postpone) nil nil)) nil)) nil)) nil)) nil) ((Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/")) shostak)) (Iso 0 (thm "thm" 3519629781 ("" (skosimp) (("" (expand "bijective?") (("" (split) (("1" (expand "injective?") (("1" (skosimp) (("1" (apply-extensionality) (("1" (lemma "extensionality_postulate[[below[m!1],below[n!1]],real]") (("1" (lemma "equa_basis_n") (("1" (expand "L") (("1" (inst -2 " (LAMBDA (j: below[m!1], i: below[n!1]): x1!1`mp(e(n!1)(i))(j))" "(LAMBDA (j: below[m!1], i: below[n!1]): x2!1`mp(e(n!1)(i))(j))") (("1" (assert) (("1" (apply-extensionality 1) (("1" (apply-extensionality 1) (("1" (inst -1 "m!1" "n!1" "x1!1" "x2!1") (("1" (assert) (("1" (hide 1 2 4 5) (("1" (apply-extensionality 1) (("1" (apply-extensionality 1) (("1" (hide 2 3) (("1" (expand "o") (("1" (inst -1 "(x!4,x!3)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp) (("2" (lemma "map_matrix_bij") (("2" (inst -1 "m!1" "n!1" "y!1") (("2" (inst 1 "T(n!1, m!1)(y!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (map_matrix_bij formula-decl nil matrix_operator nil) (T const-decl "[Mat(m, n) -> Map_linear(n, m)]" matrix_operator nil) (Mat type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil) (below type-eq-decl nil naturalnumbers nil) (injective? const-decl "bool" functions nil) (posnat nonempty-type-eq-decl nil integers nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def nil) (Map type-eq-decl nil linear_map 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 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) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equa_basis_n formula-decl nil linear_map_def nil) (m!1 skolem-const-decl "posnat" matrix_operator nil) (n!1 skolem-const-decl "posnat" matrix_operator nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (x1!1 skolem-const-decl "Map_linear(n!1, m!1)" matrix_operator nil) (x2!1 skolem-const-decl "Map_linear(n!1, m!1)" matrix_operator nil) (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (Index type-eq-decl nil vectors "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (O const-decl "T3" function_props nil) (L const-decl "[Map_linear(n, m) -> Mat(m, n)]" matrix_operator nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (extensionality_postulate formula-decl nil functions nil)) shostak) (thm "thm" 3483370869 ("" (skosimp) (("" (expand "bijective?") (("" (split) (("1" (expand "injective?") (("1" (skosimp) (("1" (apply-extensionality) (("1" (lemma "extensionality_postulate[[below[m!1],below[n!1]],real]") (("1" (lemma "equa_basis_n") (("1" (expand "L") (("1" (inst -2 " (LAMBDA (j: below[m!1], i: below[n!1]): x1!1`mp(e(n!1)(i))(j))" "(LAMBDA (j: below[m!1], i: below[n!1]): x2!1`mp(e(n!1)(i))(j))") (("1" (assert) (("1" (apply-extensionality 1) (("1" (apply-extensionality 1) (("1" (inst -1 "m!1" "n!1" "x1!1" "x2!1") (("1" (assert) (("1" (hide 1 2 4 5) (("1" (apply-extensionality 1) (("1" (apply-extensionality 1) (("1" (hide 2 3) (("1" (expand "o") (("1" (inst -1 "(x!4,x!3)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ((Index type-eq-decl nil vectors "vectors/") (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (equa_basis_n formula-decl nil linear_map_def nil) (Map type-eq-decl nil linear_map nil) (Map_linear type-eq-decl nil linear_map_def nil) (Maping type-eq-decl nil linear_map nil) (Vector type-eq-decl nil vectors "vectors/") (Matrix type-eq-decl nil matrices nil) (Mat type-eq-decl nil matrices nil)) shostak) (thm "thm" 3483359130 ("" (skosimp) (("" (expand "bijective?") (("" (split) (("1" (expand "injective?") (("1" (skosimp) (("1" (name "gg" "FORALL (i: below[n]): x1!1(e!1(i)) = x2!1(e!1(i))") (("1" (case "gg") (("1" (assert) (("1" (typepred "x1!1") (("1" (lemma "equa_basis_n") (("1" (inst -1 "e!1" "x1!1" "x2!1") (("1" (assert) (("1" (name "ff" "FORALL (i: below[n]): x1!1(e!1(i)) = x2!1(e!1(i))") (("1" (replace -1) (("1" (assert) (("1" (typepred "x1!1") (("1" (lemma "extensionality[Vector[n],Vector[n]]") (("1" (inst -1 "x1!1" "x2!1") (( | |