|
(linear_map_def (vec_expan?_TCC1 0 (vec_expan?_TCC1-1 nil 3518951076 ("" (subtype-tcc) nil nil) nil nil)) (vec_expan?_TCC2 0 (vec_expan?_TCC2-1 nil 3518951076 ("" (subtype-tcc) nil nil) nil nil)) (vec_expan?_TCC3 0 (vec_expan?_TCC3-1 nil 3547179707 ("" (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 "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Index type-eq-decl nil vectors "vectors/") (integer nonempty-type-from-decl nil integers 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)) (vec_repre_bases 0 (thm "vec_bases" 3519556744 ("" (skosimp) (("" (expand "SigmaV") (("" (apply-extensionality) (("1" (hide 2) (("1" (lemma "sigma_middle[Index[n!1]]") (("1" (inst -1 "LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2)" "n!1-1" "x!2" "0") (("1" (assert) (("1" (replace -1) (("1" (case " sigma(0, x!2 - 1, LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2))=0") (("1" (replace -1) (("1" (case " sigma(1 + x!2, n!1 - 1,
LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2))=0") (("1" (replace -1) (("1" (assert) (("1" (expand "*" 1) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[ Index[n!1]]") (("2" (inst -1 "n!1-1" "1+x!2") (("2" (lemma "sigma_eq[ Index[n!1]]") (("2" (inst -1 " LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2)" "LAMBDA (i: Index[n!1]): 0" "n!1-1" "1+x!2") (("2" (assert) (("2" (hide 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[ Index[n!1]]") (("2" (inst -1 "x!2-1" "0") (("2" (assert) (("2" (lemma "sigma_eq[ Index[n!1]]") (("2" (inst -1 " LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2)" "(LAMBDA (i: Index[n!1]): 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) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((SigmaV const-decl "Vector[n]" sigma_vector nil) (sigma_nat application-judgement "nat" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (sigma_zero formula-decl nil sigma "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Vector" vectors "vectors/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_middle formula-decl nil sigma "reals/") (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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (below type-eq-decl nil nat_types nil) (n!1 skolem-const-decl "posnat" linear_map_def nil) (Vector type-eq-decl nil vectors "vectors/") (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 "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (Index type-eq-decl nil vectors "vectors/") (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) (vec_repre_bases-1 nil 3518951134 ("" (skosimp) (("" (apply-extensionality) (("" (expand "SigmaV") (("" (assert) (("" (lemma "sigma_middle[Index[n!1]]") (("1" (inst -1 "LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2)" "n!1-1" "x!2" "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case "sigma(0, x!2 - 1, LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2))=0") (("1" (replace -1) (("1" (assert) (("1" (case " sigma(1 + x!2, n!1 - 1,
LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2))=0") (("1" (replace -1) (("1" (assert) (("1" (expand "*" 1) (("1" (assert) (("1" (expand "e" 1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (lemma "sigma_eq[Index[n!1]]") (("2" (lemma "sigma_zero[Index[n!1]]") (("2" (inst -1 "n!1-1" "1+x!2") (("2" (inst -2 "LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2)" "(LAMBDA (i: Index[n!1]): 0)" "n!1-1" "1+x!2") (("2" (assert) (("2" (skosimp) (("2" (expand "*" 1) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (lemma "sigma_zero[Index[n!1]]") (("2" (inst -1 "x!2-1" "0") (("2" (lemma "sigma_eq[Index[n!1]]") (("2" (inst -1 "LAMBDA (j: Index[n!1]): (x!1 * e(n!1))(j)(x!2)" "(LAMBDA (i: Index[n!1]): 0)" "x!2-1" "0") (("2" (assert) (("2" (skosimp) (("2" (expand "*" 1) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((SigmaV const-decl "Vector[n]" sigma_vector nil) (sigma_nat application-judgement "nat" vectors "vectors/") (sigma_nnreal application-judgement "nnreal" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (sigma_zero formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (sigma_middle formula-decl nil sigma "reals/") (Vector type-eq-decl nil vectors "vectors/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (Index type-eq-decl nil vectors "vectors/")) shostak)) (cano_base 0 (cano_base-1 nil 3518781153 ("" (skosimp) (("" (expand "base?") (("" (split) (("1" (expand "unit?") (("1" (skosimp) (("1" (expand "*") (("1" (lemma "sigma_middle[ Index[n!1]]") (("1" (inst -1 " LAMBDA (i: Index[n!1]): e(n!1)(i!1)(i) * e(n!1)(i!1)(i)" "n!1-1" "i!1" "0") (("1" (assert) (("1" (replace -1) (("1" (case " sigma(0, i!1 - 1,
LAMBDA (i: Index[n!1]): e(n!1)(i!1)(i) * e(n!1)(i!1)(i))=0") (("1" (replace -1) (("1" (assert) (("1" (case " sigma(1 + i!1, n!1 - 1,
LAMBDA (i: Index[n!1]): e(n!1)(i!1)(i) * e(n!1)(i!1)(i))=0") (("1" (replace -1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[ Index[n!1]]") (("2" (inst -1 "n!1-1" "1+i!1") (("2" (swap-rel -1) (("2" (replace -1) (("2" (lemma "sigma_eq [Index[n!1]]") (("2" (inst -1 " LAMBDA (i: Index[n!1]): e(n!1)(i!1)(i) * e(n!1)(i!1)(i)" "LAMBDA (i: Index[n!1]): 0" "n!1-1" "1+i!1") (("2" (assert) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[ Index[n!1]]") (("2" (inst -1 "i!1-1" "0") (("2" (swap-rel -1) (("2" (lemma "sigma_eq[Index[n!1]]") (("2" (inst -1 " (LAMBDA (i: Index[n!1]): 0)" " LAMBDA (i: Index[n!1]): e(n!1)(i!1)(i) * e(n!1)(i!1)(i)" "i!1-1" "0") (("2" (swap-rel -2) (("2" (assert) (("2" (skosimp) (("2" (hide 2) (("2" (grind) nil 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) ("2" (expand "ortho?") (("2" (skosimp) (("2" (expand "*") (("2" (lemma "sigma_zero[ Index[n!1]]") (("1" (inst -1 "n!1-1" "0") (("1" (lemma "sigma_eq [Index[n!1]]") (("1" (inst -1 " LAMBDA (i: Index[n!1]): e(n!1)(i!1)(i) * e(n!1)(j!1)(i)" " (LAMBDA (i: Index[n!1]): 0)" "n!1-1" "0") (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "vec_expan?") (("3" (skosimp) (("3" (lemma "vec_repre_bases") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((base? const-decl "bool" linear_map_def nil) (vec_expan? const-decl "bool" linear_map_def nil) (vec_repre_bases formula-decl nil linear_map_def nil) (ortho? const-decl "bool" linear_map_def nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (unit? const-decl "bool" linear_map_def nil) (* const-decl "real" vectors "vectors/") (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) (below type-eq-decl nil nat_types nil) (Vector type-eq-decl nil vectors "vectors/") (e const-decl "[below[n] -> Vector[n]]" linear_map_def 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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" vectors "vectors/") (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_eq formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma def-decl "real" sigma "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (sigma_middle formula-decl nil sigma "reals/") (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) (Index type-eq-decl nil vectors "vectors/")) shostak)) (linear_map_e?_TCC1 0 (linear_map_e?_TCC1-1 nil 3519034071 ("" (subtype-tcc) nil nil) nil nil)) (linear_map_e?_TCC2 0 (linear_map_e?_TCC2-1 nil 3519034071 ("" (subtype-tcc) nil nil) nil nil)) (linear_map_e?_TCC3 0 (linear_map_e?_TCC3-1 nil 3519034071 ("" (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) (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) (integer nonempty-type-from-decl nil integers nil) (Index type-eq-decl nil vectors "vectors/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (linear_map_e?_TCC4 0 (linear_map_e?_TCC4-1 nil 3519034071 ("" (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) (real_ge_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) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (linear_map_e?_TCC5 0 (linear_map_e?_TCC5-1 nil 3519732414 ("" (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) (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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Index type-eq-decl nil vectors "vectors/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (linear_map_e?_TCC6 0 (linear_map_e?_TCC6-1 nil 3519732414 ("" (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) (real_ge_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) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (linear_map_e_comp_TCC1 0 (linear_map_e_comp_TCC1-1 nil 3519732414 ("" (subtype-tcc) nil nil) ((linear_map_e? const-decl "bool" linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def nil) (same? const-decl "bool" linear_map nil)) nil)) (linear_map_e_comp 0 (linear_map_e_comp-1 nil 3519732440 ("" (skosimp) (("" (expand "linear_map_e?") (("" (skosimp) (("" (expand "linear_map_e?") (("" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (expand "o" 1) (("3" (expand "o" 1) (("3" (inst -2 "l!1") (("3" (inst -1 "l!1") (("3" (inst -2 "x!1" "F!1") (("3" (replace -2) (("3" (hide -2) (("3" (expand "o") (("3" (inst -1 "x!1" "LAMBDA (x: below[l!1]): g!1`mp(F!1(x))") (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (expand "*") (("1" (decompose-equality -1) (("1" (inst -1 "x!2") (("1" (expand "SigmaV") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (grind) nil nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (skosimp) (("4" (grind) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (grind) nil nil)) nil) ("6" (hide 2) (("6" (grind) nil nil)) nil) ("7" (hide 2) (("7" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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/") (OR const-decl "[bool, bool -> bool]" booleans nil) (same? const-decl "bool" linear_map nil) (f!1 skolem-const-decl "Map(m!1, p!1)" linear_map_def nil) (p!1 skolem-const-decl "posnat" linear_map_def nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_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) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "Vector" vectors "vectors/") (l!1 skolem-const-decl "posnat" linear_map_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (n!1 skolem-const-decl "posnat" linear_map_def nil) (Maping type-eq-decl nil linear_map nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (m!1 skolem-const-decl "posnat" linear_map_def nil) (Map type-eq-decl nil linear_map nil) (g!1 skolem-const-decl "Map(n!1, m!1)" linear_map_def nil) (below type-eq-decl nil nat_types nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (O const-decl "T3" function_props nil) (O const-decl "Maping" linear_map nil)) shostak)) (bijecti_fun_equa 0 (thm "thm" 3483112991 ("" (skosimp) (("" (expand "bijective?") (("" (flatten) (("" (split) (("1" (expand "injective?") (("1" (skosimp) (("1" (inst -3 "x1!1" "x2!1") (("1" (lemma "extensionality_postulate[Vector[n],Vector[n]]") (("1" (inst -1 "k!1" "h!1") (("1" (assert) (("1" (name "hh" "k!1 = h!1") (("1" (replace -1) (("1" (assert) (("1" (skosimp) (("1" (expand "hh") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp) (("2" (inst -3 "y!1") (("2" (skosimp) (("2" (case "k!1(x!1)=h!1(x!1)") (("1" (inst 1 "x!1") (("1" (assert) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" linear_map nil)) shostak) (bijecti_fun_equa-1 nil 3483090827 ("" (skosimp) (("" (grind) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil) ((Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/")) shostak)) (equa_basis_n_TCC1 0 (equa_basis_n_TCC1-1 nil 3518781149 ("" (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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (linear_map_e? const-decl "bool" linear_map_def 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (equa_basis_n_TCC2 0 (equa_basis_n_TCC2-1 nil 3518781149 ("" (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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (linear_map_e? const-decl "bool" linear_map_def 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (equa_basis_n_TCC3 0 (equa_basis_n_TCC3-1 nil 3519034153 ("" (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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (linear_map_e? const-decl "bool" linear_map_def 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (equa_basis_n 0 (thm "thm" 3520682693 ("" (skosimp) (("" (typepred "h!1") (("" (typepred "k!1") (("" (apply-extensionality 1) (("" (apply-extensionality 1) (("" (lemma "vec_repre_bases") (("" (inst -1 "n!1" "x!1") (("1" (replace -1) (("1" (expand "linear_map_e?") (("1" (inst -4 "n!1") (("1" (inst -7 "n!1") (("1" (expand "linear_map_e?") (("1" (inst -7 "x!1" "e(n!1)") (("1" (replace -7) (("1" (inst -4 "x!1" "e(n!1)") (("1" (replace -4) (("1" (expand "SigmaV" 1) (("1" (apply-extensionality 1) (("1" (hide 2 3) (("1" (lemma "sigma_eq[Index[n!1]]") (("1" (hide 2) (("1" (inst -1 "LAMBDA (j: Index[n!1]): (x!1 * (h!1`mp o e(n!1)))(j)(x!2)" "LAMBDA (j: Index[n!1]): (x!1 * (k!1`mp o e(n!1)))(j)(x!2)" "n!1-1" "0") (("1" (name "ff" "(FORALL (n: subrange(0, n!1 - 1)):
(x!1 * (h!1`mp o e(n!1)))(n)(x!2) =
(x!1 * (k!1`mp o e(n!1)))(n)(x!2))") (("1" (replace -1) (("1" (hide -1) (("1" (case "ff") (("1" (assert) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "ff" 1) (("2" (skosimp) (("2" (replace -9) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (replace -6) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) (("3" (replace -5) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4) (("2" (assert) 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) (vec_repre_bases formula-decl nil linear_map_def nil) (linear_map_e? const-decl "bool" linear_map_def nil) (O const-decl "T3" function_props nil) (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector 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) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_eq formula-decl nil sigma "reals/") (real_ge_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_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Vector" vectors "vectors/") (ff skolem-const-decl "boolean" linear_map_def nil) (subrange type-eq-decl nil integers nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (below type-eq-decl nil nat_types nil) (e const-decl "[below[n] -> Vector[n]]" linear_map_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (n!1 skolem-const-decl "posnat" linear_map_def nil) (m!1 skolem-const-decl "posnat" linear_map_def nil) (h!1 skolem-const-decl "Map_linear(n!1, m!1)" linear_map_def nil) (Index type-eq-decl nil vectors "vectors/") (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak) (thm "thm" 3519038240 ("" (skosimp) (("" (typepred "h!1") (("" (typepred "k!1") (("" (apply-extensionality 1) (("" (apply-extensionality 1) (("" (lemma "vec_repre_bases") (("" (inst -1 "n!1" "x!1") (("1" (replace -1) (("1" (expand "linear_map_e?") (("1" (inst -4 "n!1") (("1" (inst -7 "n!1") (("1" (expand "linear_map_e?") (("1" (inst -7 "x!1" "e(n!1)") (("1" (replace -7) (("1" (inst -4 "x!1" "e(n!1)") (("1" (replace -4) (("1" (expand "SigmaV" 1) (("1" (apply-extensionality 1) (("1" (hide 2 3) (("1" (lemma "sigma_eq[Index[n!1]]") (("1" (hide 2) (("1" (inst -1 "LAMBDA (j: Index[n!1]): (x!1 * (h!1`mp o e(n!1)))(j)(x!2)" "LAMBDA (j: Index[n!1]): (x!1 * (k!1`mp o e(n!1)))(j)(x!2)" "n!1-1" "0") (("1" (name "ff" "(FORALL (n: subrange(0, n!1 - 1)):
(x!1 * (h!1`mp o e(n!1)))(n)(x!2) =
(x!1 * (k!1`mp o e(n!1)))(n)(x!2))") (("1" (replace -1) (("1" (hide -1) (("1" (case "ff") (("1" (assert) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "ff" 1) (("2" (skosimp) (("2" (replace -9) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (replace -6) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) (("3" (replace -5) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -6) (("2" (replace -3) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (assert) nil nil)) nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Index type-eq-decl nil vectors "vectors/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (* const-decl "Vector" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (Vector type-eq-decl nil vectors "vectors/") (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil)) shostak) (thm "thm" 3483351540 ("" (skosimp) (("" (expand "linear_map_e?") (("" (apply-extensionality 1) (("1" (expand "same_dim?") (("1" (propax) nil nil)) nil) ("2" (expand "same_dim?") (("2" (propax) nil nil)) nil) ("3" (apply-extensionality 1) (("3" (lemma "vec_repre_bases") (("3" (inst -1 "h!1`dom" "x!1") (("3" (replace -1) (("3" (inst -2 "h!1`dom") (("3" (inst -3 "h!1`dom") (("3" (expand "linear_map_e?") (("3" (inst -2 "x!1" "e(h!1`dom)") (("3" (replace -2) (("3" (inst -3 "x!1" "e(h!1`dom)") (("1" (expand "SigmaV") (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Map type-eq-decl nil linear_map nil) (Maping type-eq-decl nil linear_map nil) (Vector type-eq-decl nil vectors "vectors/") (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (* const-decl "Vector" vectors "vectors/") (SigmaV const-decl "Vector[n]" sigma_vector nil) (Index type-eq-decl nil vectors "vectors/")) shostak) (equa_basis_n-1 nil 3483186415 ("" (skosimp) (("" (lemma "vec_repre_base_map") (("" (lemma "extensionality[Vector[n],Vector[n]]") (("" (inst -1 "h!1" "k!1") (("" (name "mm" "FORALL (x: Vector[n]): h!1(x) = k!1(x)") (("" (replace -1) (("" (case "mm") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (expand "mm" 1) (("2" (skosimp) (("2" (copy -3) (("2" (inst -1 "e!1" "h!1" "x!1") (("2" (assert) (("2" (assert) (("2" (inst -2 "e!1" "k!1" "x!1") (("2" (assert) (("2" (expand "sigmaV") (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (* const-decl "Vector" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/")) shostak)) (linear_map_characterization 0 (teo "fin" 3546882650 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (expand "linear_map_e?") (("1" (induct "l") (("1" (case "l!1=0") (("1" (expand "linear_map_e?") (("1" (skosimp) (("1" (replace -1 2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (expand "linear_map_e?") (("1" (skosimp) (("1" (replace -1) (("1" (hide -2) (("1" (expand "SigmaV") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "o") (("1" (expand "linear_map?") (("1" (flatten) (("1" (expand "homogeneous?") (("1" (expand "*" 1 1) (("1" (expand "*" 1 1) (("1" (inst -4 "x!1(0)" "F!1(0)") (("1" (expand "*" -4 1) (("1" (case "f!1`mp(LAMBDA (i: Index[f!1`dom]): x!1(0) * F!1(0)(i)) =f!1`mp(LAMBDA (i: below[n!1]): x!1(0) * F!1(0)(i))") (("1" (replace -1) (("1" (replace -5) (("1" (hide -1) (("1" (typepred "f!1") (("1" (hide -6) (("1" (apply-extensionality) (("1" (hide 2) (("1" (expand "*") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (replace -1) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -4 2) (("2" (lemma "congruence[Vector[f!1`dom],Vector[n!1]]") (("2" (inst -1 "f!1`mp" "f!1`mp" "LAMBDA (i: Index[f!1`dom]): x!1(0) * F!1(0)(i)" "LAMBDA (i: below[n!1]): x!1(0) * F!1(0)(i)") (("1" (case " ((LAMBDA (i: Index[f!1`dom]): x!1(0) * F!1(0)(i)) =
(LAMBDA (i: below[n!1]): x!1(0) * F!1(0)(i)))") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality) (("2" (typepred "f!1") (("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "f!1") (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "f!1") (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "linear_map_e?") (("2" (skosimp) (("2" (expand "*") (("2" (expand "o") (("2" (lemma "SigmaV_last[below[1+j!1],n!1]") (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]): x!1(i) * F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "*") (("1" (expand "+") (("1" (copy -3) (("1" (expand "linear_map?" -1) (("1" (flatten) (("1" (expand "additive?") (("1" (inst -1 "LAMBDA (i_1: Index[n!1]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)" "LAMBDA (i_1: Index[n!1]):x!1(j!1) * F!1(j!1)(i_1)") (("1" (expand "+" -1 1) (("1" (lemma "congruence[Vector[f!1`dom],Vector[f!1`codom]]") (("1" (typepred "f!1") (("1" (inst -3 "f!1`mp" "f!1`mp" "LAMBDA (i_1: Index[f!1`dom]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)
+ x!1(j!1) * F!1(j!1)(i_1)" "LAMBDA (i_1: Index[n!1]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)
+ x!1(j!1) * F!1(j!1)(i_1)") (("1" (case " ((LAMBDA (i_1: Index[f!1`dom]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)
+ x!1(j!1) * F!1(j!1)(i_1))
=
(LAMBDA (i_1: Index[n!1]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)
+ x!1(j!1) * F!1(j!1)(i_1)))") (("1" (replace -1 -4) (("1" (replace -1) (("1" (replace -4) (("1" (hide -1 -4) (("1" (inst -4 " LAMBDA (i: Index[j!1]): x!1(i)" " LAMBDA (i: Index[j!1]): F!1(i)") (("1" (case "SigmaV[below[j!1], n!1]
(0, j!1 - 1,
LAMBDA (i_2: Index[j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i_2) * F!1(i_2)(i_1))=LAMBDA (i_1: Index[n!1]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)") (("1" (replace -1 -5) (("1" (hide -1) (("1" (replace -4 2) (("1" (hide -4) (("1" (expand "homogeneous?") (("1" (expand "*") (("1" (inst -3 "x!1(j!1)" "F!1(j!1)") (("1" (lemma "congruence[Vector[f!1`dom],Vector[f!1`codom
]]") (("1" (inst -1 "f!1`mp" "f!1`mp" "LAMBDA (i: Index[f!1`dom]): x!1(j!1) * F!1(j!1)(i)" "LAMBDA (i_1: Index[n!1]): x!1(j!1) * F!1(j!1)(i_1)") (("1" (case " ((LAMBDA (i: Index[f!1`dom]): x!1(j!1) * F!1(j!1)(i)) =
(LAMBDA (i_1: Index[n!1]): x!1(j!1) * F!1(j!1)(i_1)))") (("1" (replace -1 -2) (("1" (replace -1) (("1" (replace -4) (("1" (hide -1) (("1" (lemma "SigmaV_last[below[1+j!1],f!1`codom]") (("1" (hide -4) (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[f!1`codom]): x!1(i) * f!1`mp(F!1(i))(i_1)" "j!1" "0") (("1" (assert) (("1" (expand "SigmaV") (("1" (case " (LAMBDA (i_1: below[f!1`codom]):
sigma(0, j!1,
LAMBDA (j: below[1 + j!1]): x!1(j) * f!1`mp(F!1(j))(i_1)))= (LAMBDA (i_1: below[n!1]):
sigma(0, j!1,
LAMBDA (j: below[1 + j!1]): x!1(j) * f!1`mp(F!1(j))(i_1)))") (("1" (replace -1 -2) (("1" (replace -2 2) (("1" (hide -1 -2) (("1" (case " (LAMBDA (i: below[n!1]):
sigma(0, j!1 - 1,
LAMBDA (j: below[j!1]): x!1(j) * f!1`mp(F!1(j))(i)))= LAMBDA (i_1: below[f!1`codom]):
sigma(0, j!1 - 1,
LAMBDA (j: below[1 + j!1]): x!1(j) * f!1`mp(F!1(j))(i_1))") (("1" (replace -1 2) (("1" (propax) nil nil)) nil) ("2" (hide 3) (("2" (apply-extensionality) (("1" (hide 2) (("1" (lemma "sigma_restrict_dom") (("1" (inst -1 "j!1" "j!1" "LAMBDA (j: below[j!1]): x!1(j) * f!1`mp(F!1(j))(x!2)" " LAMBDA (j: below[1 + j!1]): x!1(j) * f!1`mp(F!1(j))(x!2)") (("1" (assert) nil nil) ("2" (hide 2 3 -4) (("2" (skosimp) (("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2 3 -3 -4) (("3" (skosimp) (("3" (skosimp) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (replace -1) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (typepred "y!1") (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (replace -1) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (typepred "y!1") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (replace -1) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -5 3) (("2" (apply-extensionality) (("1" (skosimp) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (typepred "y!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (typepred "y!1") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (replace -1) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (replace -3) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (replace -2) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (typepred "y!1") (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (replace -2) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -4 -6 3) (("2" (apply-extensionality) (("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide -4) (("2" (apply-extensionality) (("1" (hide 2) (("1" (expand "SigmaV") (("1" (lemma "sigma_restrict_dom") (("1" (inst -1 "j!1" "j!1" "LAMBDA (j: below[j!1]): x!1(j) * F!1(j)(x!2)" "LAMBDA (j: Index[1 + j!1]): x!1(j) * F!1(j)(x!2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (typepred "y!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide -4 -6) (("2" (hide -3) (("2" (apply-extensionality) (("1" (skosimp) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (typepred "y!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3 -4) (("3" (skosimp) (("3" (hide -3) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (hide -6 3) (("4" (hide -5) (("4" (typepred "y!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (skosimp) (("5" (typepred "y!1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -3 3) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (typepred "y!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "linear_map_e?") (("2" (flatten) (("2" (expand "linear_map_e?") (("2" (expand "linear_map?") (("2" (split) (("1" (expand "additive?") (("1" (skosimp) (("1" (inst -1 "2") (("1" (assert) (("1" (expand "SigmaV") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (inst -1 "LAMBDA (i:below[2]):1" "_") (("1" (assert) (("1" (inst -1 "(LAMBDA (i: below[2]): x!1) WITH [(1) := y!1]") (("1" (assert) (("1" (grind) (("1" (case " f!1`mp(LAMBDA (i_1: below[n!1]): x!1(i_1) + y!1(i_1)) =f!1`mp(x!1 + y!1)") (("1" (replace -1 -2) (("1" (hide -1) (("1" (replace -1) (("1" (expand "+" 1 2) (("1" (apply-extensionality) (("1" (typepred "f!1") (("1" (skosimp) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "congruence[Vector[n!1],Vector[f!1`codom]]") (("2" (inst -1 "f!1`mp" "f!1`mp" "LAMBDA (i_1: below[n!1]): x!1(i_1) + y!1(i_1)" "x!1+y!1") (("1" (case " (LAMBDA (i_1: below[n!1]): x!1(i_1) + y!1(i_1)) = x!1 + y!1") (("1" (assert) nil nil) ("2" (apply-extensionality) nil nil) ("3" (typepred "f!1") (("3" (skosimp) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "f!1") (("3" (skosimp) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "homogeneous?") (("2" (skosimp) (("2" (inst -1 "1") (("2" (inst -1 "LAMBDA (i: below[1]): a!1" "LAMBDA (i: below[1]): x!1") (("1" (expand "SigmaV") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) (("1" (typepred "f!1") (("1" (expand "*" -3 1) (("1" (expand "*" -3 1) (("1" (expand "*" 1 1) (("1" (case "f!1`mp(LAMBDA (i_1: below[n!1]): a!1 * x!1(i_1)) = f!1`mp(LAMBDA (i: Index[f!1`dom]): a!1 * x!1(i))") (("1" (replace -1 -4) (("1" (replace -4 1) (("1" (hide -1) (("1" (hide -3) (("1" (expand "*") (("1" (apply-extensionality) (("1" (hide 2) (("1" (expand "*") (("1" (expand "o") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (lemma "congruence[Vector[f!1`dom],Vector[f!1`codom]]") (("2" (inst -1 "f!1`mp" "f!1`mp" "LAMBDA (i_1: below[n!1]): a!1 * x!1(i_1)" "LAMBDA (i: Index[f!1`dom]): a!1 * x!1(i)") (("1" (case " ((LAMBDA (i_1: below[n!1]): a!1 * x!1(i_1)) =
(LAMBDA (i: Index[f!1`dom]): a!1 * x!1(i)))") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (apply-extensionality) (("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (typepred "f!1") (("2" (replace -1) (("2" (assert) 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) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_restrict_dom formula-decl nil sigma_lemmas nil) (additive? const-decl "bool" linear_map_def nil) (+ const-decl "real" vectors "vectors/") (SigmaV_last formula-decl nil sigma_vector nil) (SigmaV const-decl "Vector[n]" sigma_vector nil) (linear_map? const-decl "bool" linear_map_def nil) (homogeneous? const-decl "bool" linear_map_def nil) (* const-decl "Vector" vectors "vectors/") (congruence formula-decl nil functions 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) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (j!1 skolem-const-decl "nat" linear_map_def nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (Index type-eq-decl nil vectors "vectors/") (below type-eq-decl nil nat_types nil) (f!1 skolem-const-decl "Map(n!1, n!1)" linear_map_def nil) (n!1 skolem-const-decl "posnat" linear_map_def nil) (< const-decl "bool" reals nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (* const-decl "[[T -> real], [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil) (O const-decl "T3" function_props nil) (sigma def-decl "real" sigma "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (Map type-eq-decl nil linear_map nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (linear_map_e? const-decl "bool" linear_map_def nil) (nonneg_int nonempty-type-eq-decl nil integers 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 "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types 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) (scal_1 formula-decl nil vectors "vectors/")) shostak) (sigmas "sigmas" 3546882051 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (expand "linear_map_e?") (("1" (induct "l") (("1" (case "l!1=0") (("1" (expand "linear_map_e?") (("1" (skosimp) (("1" (replace -1 2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "j!1=0") (("1" (expand "linear_map_e?") (("1" (skosimp) (("1" (replace -1) (("1" (hide -2) (("1" (expand "SigmaV") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "o") (("1" (expand "linear_map?") (("1" (flatten) (("1" (expand "homogeneous?") (("1" (expand "*" 1 1) (("1" (expand "*" 1 1) (("1" (inst -4 "x!1(0)" "F!1(0)") (("1" (expand "*" -4 1) (("1" (case "f!1`mp(LAMBDA (i: Index[f!1`dom]): x!1(0) * F!1(0)(i)) =f!1`mp(LAMBDA (i: below[n!1]): x!1(0) * F!1(0)(i))") (("1" (replace -1) (("1" (replace -5) (("1" (hide -1) (("1" (typepred "f!1") (("1" (hide -6) (("1" (apply-extensionality) (("1" (hide 2) (("1" (expand "*") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "y!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (replace -1) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -4 2) (("2" (lemma "congruence[Vector[f!1`dom],Vector[n!1]]") (("2" (inst -1 "f!1`mp" "f!1`mp" "LAMBDA (i: Index[f!1`dom]): x!1(0) * F!1(0)(i)" "LAMBDA (i: below[n!1]): x!1(0) * F!1(0)(i)") (("1" (case " ((LAMBDA (i: Index[f!1`dom]): x!1(0) * F!1(0)(i)) =
(LAMBDA (i: below[n!1]): x!1(0) * F!1(0)(i)))") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality) (("2" (typepred "f!1") (("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "f!1") (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "f!1") (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "linear_map_e?") (("2" (skosimp) (("2" (expand "*") (("2" (expand "o") (("2" (lemma "SigmaV_last[below[1+j!1],n!1]") (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]): x!1(i) * F!1(i)" "j!1" "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "*") (("1" (expand "+") (("1" (copy -3) (("1" (expand "linear_map?" -1) (("1" (flatten) (("1" (expand "additive?") (("1" (inst -1 "LAMBDA (i_1: Index[n!1]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)" "LAMBDA (i_1: Index[n!1]):x!1(j!1) * F!1(j!1)(i_1)") (("1" (expand "+" -1 1) (("1" (lemma "congruence[Vector[f!1`dom],Vector[f!1`codom]]") (("1" (typepred "f!1") (("1" (inst -3 "f!1`mp" "f!1`mp" "LAMBDA (i_1: Index[f!1`dom]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)
+ x!1(j!1) * F!1(j!1)(i_1)" "LAMBDA (i_1: Index[n!1]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)
+ x!1(j!1) * F!1(j!1)(i_1)") (("1" (case " ((LAMBDA (i_1: Index[f!1`dom]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)
+ x!1(j!1) * F!1(j!1)(i_1))
=
(LAMBDA (i_1: Index[n!1]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)
+ x!1(j!1) * F!1(j!1)(i_1)))") (("1" (replace -1 -4) (("1" (replace -1) (("1" (replace -4) (("1" (hide -1 -4) (("1" (inst -4 " LAMBDA (i: Index[j!1]): x!1(i)" " LAMBDA (i: Index[j!1]): F!1(i)") (("1" (case "SigmaV[below[j!1], n!1]
(0, j!1 - 1,
LAMBDA (i_2: Index[j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i_2) * F!1(i_2)(i_1))=LAMBDA (i_1: Index[n!1]):
SigmaV(0, j!1 - 1,
LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[n!1]): x!1(i) * F!1(i)(i_1))
(i_1)") (("1" (replace -1 -5) (("1" (hide -1) (("1" (replace -4 2) (("1" (hide -4) (("1" (expand "homogeneous?") (("1" (expand "*") (("1" (inst -3 "x!1(j!1)" "F!1(j!1)") (("1" (lemma "congruence[Vector[f!1`dom],Vector[f!1`codom
]]") (("1" (inst -1 "f!1`mp" "f!1`mp" "LAMBDA (i: Index[f!1`dom]): x!1(j!1) * F!1(j!1)(i)" "LAMBDA (i_1: Index[n!1]): x!1(j!1) * F!1(j!1)(i_1)") (("1" (case " ((LAMBDA (i: Index[f!1`dom]): x!1(j!1) * F!1(j!1)(i)) =
(LAMBDA (i_1: Index[n!1]): x!1(j!1) * F!1(j!1)(i_1)))") (("1" (replace -1 -2) (("1" (replace -1) (("1" (replace -4) (("1" (hide -1) (("1" (lemma "SigmaV_last[below[1+j!1],f!1`codom]") (("1" (hide -4) (("1" (inst -1 " LAMBDA (i: Index[1 + j!1]):
LAMBDA (i_1: Index[f!1`codom]): x!1(i) * f!1`mp(F!1(i))(i_1)" "j!1" "0") (("1" (assert) (("1" (expand "SigmaV") (("1" (case " (LAMBDA (i_1: below[f!1`codom]):
sigma(0, j!1,
LAMBDA (j: below[1 + j!1]): x!1(j) * f!1`mp(F!1(j))(i_1)))= (LAMBDA (i_1: below[n!1]):
sigma(0, j!1,
LAMBDA (j: below[1 + j!1]): x!1(j) * f!1`mp(F!1(j))(i_1)))") (("1" (replace -1 -2) (("1" (replace -2 2) (("1" (hide -1 -2) (("1" (case " (LAMBDA (i: below[n!1]):
sigma(0, j!1 - 1,
LAMBDA (j: below[j!1]): x!1(j) * f!1`mp(F!1(j))(i)))= LAMBDA (i_1: below[f!1`codom]):
sigma(0, j!1 - 1,
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.29 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.
|
