|
(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]):
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.34 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
