(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 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 " " 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 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 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 " " 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 )):1 * (h!1 `mp o e(n!1 )))(n)(x!2 ) =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 )):1 * (h!1 `mp o e(n!1 )))(n)(x!2 ) =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 " " 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 " " 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 " ") ((" 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 " ") ((" 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 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(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]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1)" " LAMBDA (i_1: Index[n!1 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1)") ((" 1 " (case " ((LAMBDA (i_1: Index[f!1 `dom]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1))LAMBDA (i_1: Index[n!1 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))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 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(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 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]):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 ]):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 ]):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]):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" " 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 " " 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 " ") ((" 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 " ") ((" 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 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(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]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1)" " LAMBDA (i_1: Index[n!1 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1)") ((" 1 " (case " ((LAMBDA (i_1: Index[f!1 `dom]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1))LAMBDA (i_1: Index[n!1 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))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 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(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 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]):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 ]):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 ]):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]):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 " (postpone) nil nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil) (" 4 " (postpone) nil nil) (" 5 " (postpone) nil nil) (" 6 " (postpone) nil nil)) nil)) nil) (" 3 " (postpone) nil nil) (" 4 " (postpone) nil nil) (" 5 " (postpone) nil nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil) (" 4 " (postpone) nil nil) (" 5 " (postpone) nil nil) (" 6 " (postpone) nil nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil)) nil) (" 2 " (postpone) nil nil)) nil)) nil) (" 2 " (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil) (" 4 " (postpone) nil nil) (" 5 " (postpone) nil nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil) (" 4 " (postpone) nil nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) 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" " 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) ((scal_1 formula-decl nil vectors " vectors/") (Vector type-eq-decl nil vectors " vectors/") (Maping type-eq-decl nil linear_map nil) (Map type-eq-decl nil linear_map nil) (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/") (* const-decl " Vector" vectors " vectors/") (SigmaV const-decl " Vector[n]" sigma_vector nil) (SigmaV_last formula-decl nil sigma_vector nil) (+ const-decl " real" vectors " vectors/") (sigma_restrict_dom formula-decl nil sigma_lemmas nil) (T_high type-eq-decl nil sigma " reals/") (T_low type-eq-decl nil sigma " reals/")) shostak) (cas " cas" 3546881191 (" " (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 " 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 " ") ((" 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 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(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]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1)" " LAMBDA (i_1: Index[n!1 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1)") ((" 1 " (case " ((LAMBDA (i_1: Index[f!1 `dom]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1))LAMBDA (i_1: Index[n!1 ]):0 , j!1 - 1 ,LAMBDA (i: Index[1 + j!1 ]):LAMBDA (i_1: Index[n!1 ]): x!1 (i) * F!1 (i)(i_1))1 (j!1 ) * F!1 (j!1 )(i_1)))") ((" 1 " (replace -1 -4) ((" 1 " (replace -1) ((" 1 " (replace -4) ((" 1 " (hide -1 -4) ((" 1 " (lemma " SigmaV_last[below[1 + j!1 ], n!1 ]") ((" 1 " (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil) (" 4 " (postpone) nil nil) (" 5 " (postpone) nil nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil) (" 4 " (postpone) nil nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil) (" 3 " (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) 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 " 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) nil shostak) (casi " casi" 3546877678 (" " (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 " ") ((" 2 " (postpone) 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 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) nil shostak) (encamino " encamino" 3546876789 (" " (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 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 " ") ((" 2 " (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil)) nil)) nil) nil shostak) (linear_map_characterization-1 nil 3546585937 (" " (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 " n!1 " " x!1 (0 )" " F!1 (0 )") ((" 1 " (case " f!1 `mp(x!1 (0 ) * F!1 (0 ))= f!1 `mp(LAMBDA (i: below[n!1 ]): x!1 (0 ) * F!1 (0 )(i))") ((" 1 " (replace -1 -5) ((" 1 " (hide -1) ((" 1 " (grind) ((" 1 " (hide -2 -3 -4) ((" 1 " (expand " *") ((" 1 " (grind) ((" 1 " (typepred " f!1 ") ((" 1 " (grind) ((" 1 " (apply-extensionality) ((" 1 " (hide 2) ((" 1 " (skosimp) ((" 1 " (grind) nil nil)) nil)) nil) (" 2 " (hide 2) ((" 2 " (skosimp) ((" 2 " (skosimp) ((" 2 " (hide -4) ((" 2 " (assert) ((" 2 " (grind) nil nil)) nil)) nil)) nil)) nil)) nil) (" 3 " (hide -4 2) ((" 3 " (skosimp) ((" 3 " (skosimp) ((" 3 " (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (hide 2) ((" 2 " (hide -4) ((" 2 " (apply-extensionality) ((" 1 " (hide 2) ((" 1 " (grind) ((" 1 " (expand " *" 1) ((" 1 " (propax) nil nil)) nil)) nil)) nil) (" 2 " (hide 2) ((" 2 " (skosimp) ((" 2 " (hide -3) ((" 2 " (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 3 " (hide -4 2) ((" 3 " (skosimp) ((" 3 " (hide -3) ((" 3 " (grind) nil 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 " (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) (" 2 " (postpone) nil nil)) nil)) nil) nil shostak)))
Messung V0.5 in Prozent C=100 H=-53 G=80
¤ Dauer der Verarbeitung: 0.62 Sekunden
(vorverarbeitet am 2026-06-04)
¤ *© Formatika GbR, Deutschland
