Quelle matrices.prf
Sprache: Lisp
|
|
(matrices (Mr2V_TCC1 0 (Mr2V_TCC1-1 nil 3478652004 ("" (subtype-tcc) nil nil) nil nil)) (Mc2V_TCC1 0 (Mc2V_TCC1-1 nil 3478652004 ("" (subtype-tcc) nil nil) nil nil)) (transpose2 0 (transpose2-1 nil 3460302788 ("" (grind) (("" (apply-extensionality :hide? t) (("" (apply-extensionality :hide? t) nil nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (transpose const-decl "Matrix" matrices nil)) shostak)) (identity?_TCC1 0 (identity?_TCC1-1 nil 3460338896 ("" (subtype-tcc) nil nil) ((Matrix type-eq-decl nil matrices nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (< const-decl "bool" reals 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) (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) (square? const-decl "bool" matrices nil)) nil)) (I_TCC1 0 (I_TCC1-1 nil 3485108508 ("" (subtype-tcc) nil nil) ((square? const-decl "bool" matrices nil) (identity? const-decl "bool" matrices nil)) nil)) (ident_trans 0 (thm "thm" 3521298470 ("" (skosimp) (("" (apply-extensionality) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (apply-extensionality 1) (("3" (case "x!1=x!2 or x!1/=x!2") (("1" (split) (("1" (replace -1) (("1" (expand "I" 1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil) ("2" (hide 2 3 4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (I const-decl "(identity?)" matrices nil) (identity? const-decl "bool" matrices 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_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) (transpose const-decl "Matrix" matrices nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak) (ident_trans-1 nil 3521297780 ("" (skosimp) (("" (apply-extensionality) (("1" (typepred "I!1") (("1" (expand "identity?") (("1" (flatten) (("1" (expand "square?") (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil) nil shostak)) (plus_TCC1 0 (plus_TCC1-1 nil 3460338896 ("" (subtype-tcc) nil nil) nil nil)) (plus_TCC2 0 (plus_TCC2-1 nil 3460338896 ("" (subtype-tcc) nil nil) nil nil)) (plus_assoc_TCC1 0 (plus_assoc_TCC1-1 nil 3460559183 ("" (subtype-tcc) nil nil) nil nil)) (plus_assoc_TCC2 0 (plus_assoc_TCC2-1 nil 3460559183 ("" (subtype-tcc) nil nil) ((+ const-decl "Matrix" matrices nil)) nil)) (plus_assoc_TCC3 0 (plus_assoc_TCC3-1 nil 3460559183 ("" (subtype-tcc) nil nil) ((+ const-decl "Matrix" matrices nil)) nil)) (plus_assoc 0 (plus_assoc-1 nil 3460559233 ("" (grind-with-ext) nil nil) ((+ const-decl "Matrix" matrices nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (plus_comm_TCC1 0 (plus_comm_TCC1-1 nil 3460559183 ("" (subtype-tcc) nil nil) nil nil)) (plus_comm 0 (plus_comm-1 nil 3460559184 ("" (grind-with-ext) 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) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (M!1 skolem-const-decl "Matrix" matrices nil) (N!1 skolem-const-decl "(LAMBDA (N): M!1`rows = N`rows AND M!1`cols = N`cols)" matrices nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "Matrix" matrices nil)) shostak)) (zero_left_ident 0 (zero_left_ident-1 nil 3460559511 ("" (grind-with-ext) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (zero? const-decl "bool" matrices nil) (Zero type-eq-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (Z!1 skolem-const-decl "Zero" matrices nil) (M!1 skolem-const-decl "(LAMBDA (N): Z!1`rows = N`rows AND Z!1`cols = N`cols)" matrices nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "Matrix" matrices nil)) shostak)) (zero_right_ident_TCC1 0 (zero_right_ident_TCC1-1 nil 3460559482 ("" (subtype-tcc) nil nil) nil nil)) (zero_right_ident 0 (zero_right_ident-1 nil 3460559483 ("" (grind-with-ext) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (zero? const-decl "bool" matrices nil) (Zero type-eq-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_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) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "Matrix" matrices nil)) shostak)) (times_TCC1 0 (times_TCC1-1 nil 3460338896 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (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) (< 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (times_TCC2 0 (times_TCC2-1 nil 3460338896 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (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) (< 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) (nat nonempty-type-eq-decl nil naturalnumbers 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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (times_TCC3 0 (times_TCC3-1 nil 3460338896 ("" (subtype-tcc) nil nil) nil nil)) (times_TCC4 0 (times_TCC4-1 nil 3498283619 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (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) (< 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (times_TCC5 0 (times_TCC5-1 nil 3519735992 ("" (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (times_TCC6 0 (times_TCC6-1 nil 3547271647 ("" (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (int_minus_int_is_int application-judgement "int" integers 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)) (zero_times_left_TCC1 0 (zero_times_left_TCC1-1 nil 3460559888 ("" (subtype-tcc) nil nil) nil nil)) (zero_times_left 0 (zero_times_left-1 nil 3460559888 ("" (grind-with-ext :if-match nil) (("" (inst? :copy? t) (("" (assert) (("" (replace -4 :hide? t) (("" (assert) (("" (case-replace "(LAMBDA (k: below(Z!1`cols)):
Z!1`matrix(i!1, k) * M!1`matrix(k, j!1)) = (LAMBDA (k:
below(Z!1`cols)): 0)") (("1" (use "sigma_const[below(Z!1`cols)]") (("1" (assert) nil nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (sigma_nat application-judgement "nat" vectors "vectors/") (int_plus_int_is_int application-judgement "int" integers nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_const formula-decl nil sigma "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" sigma "reals/") (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) (< 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (Zero type-eq-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (zero? const-decl "bool" matrices nil) (* const-decl "Matrix" matrices nil)) shostak)) (zero_times_right_TCC1 0 (zero_times_right_TCC1-1 nil 3460559888 ("" (subtype-tcc) nil nil) nil nil)) (zero_times_right 0 (zero_times_right-1 nil 3460563301 ("" (grind-with-ext :if-match nil) (("" (inst? :copy? t) (("" (replace -4 :hide? t) (("" (assert) (("" (case-replace "(LAMBDA (k: below(M!1`cols)):
M!1`matrix(i!1, k) * Z!1`matrix(k, j!1)) = (LAMBDA (k:
below(M!1`cols)): 0)") (("1" (use "sigma_const[below(M!1`cols)]") (("1" (assert) nil nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_const formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (sigma_nat application-judgement "nat" vectors "vectors/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" sigma "reals/") (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) (< 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (Zero type-eq-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (zero? const-decl "bool" matrices nil) (* const-decl "Matrix" matrices nil)) shostak)) (sigma_lem_TCC1 0 (sigma_lem_TCC1-1 nil 3460351676 ("" (subtype-tcc) nil nil) nil nil)) (sigma_lem_TCC2 0 (sigma_lem_TCC2-1 nil 3460351676 ("" (subtype-tcc) nil nil) nil nil)) (sigma_lem_TCC3 0 (sigma_lem_TCC3-1 nil 3547271647 ("" (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) (below type-eq-decl nil naturalnumbers nil) (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)) (sigma_lem 0 (sigma_lem-1 nil 3460351677 ("" (skolem-typepred) (("" (lemma "sigma_with[below(n!1)]") (("" (inst?) (("" (inst -1 "lambda (k: below(n!1)): 0" "r!1" "j!1") (("" (assert) (("" (replace -1) (("" (assert) (("" (hide -1) (("" (use "sigma_const[below(n!1)]") (("" (replace -1) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_with formula-decl nil sigma "reals/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_const formula-decl nil sigma "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_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) (sigma_nat application-judgement "nat" vectors "vectors/") (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (below type-eq-decl nil naturalnumbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers 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) (> const-decl "bool" reals 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) (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)) shostak)) (right_mult_ident 0 (right_mult_ident-1 nil 3460338931 ("" (skolem-typepred) (("" (expand "identity?") (("" (flatten) (("" (expand "*") (("" (apply-extensionality :hide? t) (("1" (grind) nil nil) ("2" (apply-extensionality :hide? t) (("2" (case-replace "(LAMBDA (k: below(M!1`cols)):
M!1`matrix(x!1, k) * I!1`matrix(k, x!2)) = (LAMBDA (k:
below(M!1`cols)): if k = x!2 then M!1`matrix(x!1, x!2) else
0 endif)" :hide? t) (("1" (case-replace "(LAMBDA (k: below(M!1`cols)):
IF k = x!2 THEN M!1`matrix(x!1, x!2) ELSE 0 ENDIF) = (LAMBDA
(k: below(M!1`cols)): 0) WITH [(x!2) := M!1`matrix(x!1,
x!2)]" :hide? t) (("1" (use "sigma_lem") nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (lift-if) (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil) ("4" (hide 2) (("4" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("1" (inst?) (("1" (replace -2) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil) ("3" (grind) nil nil)) nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "Matrix" matrices 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_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (x!2 skolem-const-decl "below(I!1`cols)" matrices nil) (sigma_lem formula-decl nil matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (square? const-decl "bool" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (M!1 skolem-const-decl "Matrix" matrices nil) (I!1 skolem-const-decl "{I: Matrix | identity?(I) AND M!1`cols = I`rows}" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IFF 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/") (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (identity? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (left_mult_ident_TCC1 0 (left_mult_ident_TCC1-1 nil 3460570872 ("" (subtype-tcc) nil nil) nil nil)) (left_mult_ident 0 (left_mult_ident-1 nil 3460570900 ("" (skolem-typepred) (("" (expand "identity?") (("" (expand "*") (("" (apply-extensionality :hide? t) (("1" (apply-extensionality :hide? t) (("1" (flatten) (("1" (case-replace "(LAMBDA (k: below(I!1`cols)):
I!1`matrix(x!1, k) * M!1`matrix(k, x!2)) = (LAMBDA (k:
below(I!1`cols)): if k = x!1 then M!1`matrix(x!1,
x!2) else 0 endif)" :hide? t) (("1" (case-replace "(LAMBDA (k: below(I!1`cols)):
IF k = x!1 THEN M!1`matrix(x!1, x!2) ELSE 0 ENDIF) = (LAMBDA
(k: below(I!1`cols)): 0) WITH [(x!1) :=
M!1`matrix(x!1, x!2)]" :hide? t) (("1" (assert) (("1" (use "sigma_lem") (("1" (grind) nil nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (lift-if) (("1" (propax) nil nil)) nil) ("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (lift-if) (("1" (inst? -2) (("1" (assert) (("1" (replace -2) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil) ((number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" 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/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (I!1 skolem-const-decl "{I: Matrix | identity?(I) AND M!1`rows = I`cols}" matrices nil) (M!1 skolem-const-decl "Matrix" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (x!3 skolem-const-decl "below(I!1`cols)" matrices nil) (sigma_lem formula-decl nil matrices nil) (x!1 skolem-const-decl "below(I!1`rows)" matrices 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) (square? const-decl "bool" matrices nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" vectors "vectors/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "Matrix" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (identity? const-decl "bool" matrices nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (ident_vect_TCC1 0 (ident_vect_TCC1-1 nil 3519990170 ("" (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) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (identity? const-decl "bool" matrices nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (>= 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (I!1 skolem-const-decl "{I: Matrix | identity?(I)}" matrices nil) (x2!1 skolem-const-decl "nat" matrices nil) (< const-decl "bool" reals nil) (square? const-decl "bool" matrices 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)) (ident_vect 0 (thm "thm" 3519991955 ("" (skosimp) (("" (expand "*") (("" (skosimp) (("" (apply-extensionality) (("1" (hide 2) (("1" (typepred "I!1") (("1" (expand "identity?") (("1" (flatten) (("1" (lemma "sigma_middle[below[I!1`cols]]") (("1" (inst -1 "LAMBDA (k: below(I!1`cols)): I!1`matrix(x!2, k) * x!1(k)" "I!1`cols-1" "x!2" "0") (("1" (assert) (("1" (typepred "x!2") (("1" (expand "square?") (("1" (replace -3) (("1" (assert) (("1" (replace -2) (("1" (case "sigma(0, x!2 - 1,
LAMBDA (k: below(I!1`cols)): I!1`matrix(x!2, k) * x!1(k))=0") (("1" (replace -1) (("1" (assert) (("1" (case "sigma(1 + x!2, I!1`cols - 1,
LAMBDA (k: below(I!1`cols)): I!1`matrix(x!2, k) * x!1(k))=0") (("1" (replace -1) (("1" (assert) (("1" (copy -6) (("1" (inst -1 "x!2" "x!2") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[below[I!1`cols]]") (("2" (inst -1 "I!1`cols-1" "1+x!2") (("2" (lemma "sigma_eq[below[I!1`cols]]") (("2" (inst?) (("2" (inst -1 "LAMBDA (k: below(I!1`cols)): I!1`matrix(x!2, k) * x!1(k)") (("2" (assert) (("2" (skosimp) (("2" (inst -6 "x!2" "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sigma_zero[below[I!1`cols]]") (("2" (inst -1 "x!2-1" "0") (("2" (lemma "sigma_eq[below[I!1`cols]]") (("2" (inst?) (("2" (inst -1 "LAMBDA (k: below(I!1`cols)): I!1`matrix(x!2, k) * x!1(k)") (("2" (assert) (("2" (skosimp) (("2" (inst -5 "x!2" "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil) ("3" (skosimp) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "Vector[M`rows]" matrices nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (identity? const-decl "bool" matrices nil) (Vector type-eq-decl nil vectors "vectors/") (Index type-eq-decl nil vectors "vectors/") (* const-decl "[numfield, numfield -> numfield]" 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/") (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (I!1 skolem-const-decl "{I: Matrix | identity?(I)}" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_zero formula-decl nil sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (subrange type-eq-decl nil integers nil) (sigma_nat application-judgement "nat" vectors "vectors/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (square? const-decl "bool" matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (below type-eq-decl nil nat_types nil) (sigma_middle formula-decl nil sigma "reals/")) shostak) (ident_vect-1 nil 3519990183 ("" (skosimp) (("" (expand "*") (("" (apply-extensionality) (("1" (expand "I") (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ((sigma_middle formula-decl nil sigma "reals/") (sigma_nat application-judgement "nat" vectors "vectors/") (sigma_eq formula-decl nil sigma "reals/") (sigma_zero 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/") (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/")) shostak)) (sigma_prop_TCC1 0 (sigma_prop_TCC1-1 nil 3460578385 ("" (subtype-tcc) nil nil) nil nil)) (sigma_prop_TCC2 0 (sigma_prop_TCC2-1 nil 3460578385 ("" (subtype-tcc) nil nil) nil nil)) (sigma_prop_TCC3 0 (sigma_prop_TCC3-1 nil 3460578385 ("" (subtype-tcc) nil nil) nil nil)) (sigma_prop_TCC4 0 (sigma_prop_TCC4-1 nil 3460578385 ("" (subtype-tcc) nil nil) nil nil)) (sigma_prop 0 (sigma_prop-1 nil 3460578386 ("" (skosimp) (("" (case-replace "m!1 - 1 = 0") (("1" (grind) (("1" (use "sigma_scal[below(n!1)]") (("1" (assert) nil nil)) nil)) nil) ("2" (generalize "m!1 - 1" "mm" "below(m!1)") (("2" (induct "mm") (("2" (skosimp*) (("2" (expand "sigma" 2 3) (("2" (expand "sigma" 2 1) (("2" (use "sigma_scal[below(n!1)]") (("2" (replace -1 :hide? t) (("2" (assert) (("2" (replace -2) (("2" (grind) (("2" (use "sigma_scal[below(n!1)]") (("2" (replace -1 :hide? t) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (real_times_real_is_real application-judgement "real" reals nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sigma_scal formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-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) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma def-decl "real" sigma "reals/") (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (sigma_comm_TCC1 0 (sigma_comm_TCC1-1 nil 3460644071 ("" (subtype-tcc) nil nil) nil nil)) (sigma_comm_TCC2 0 (sigma_comm_TCC2-1 nil 3460644071 ("" (subtype-tcc) nil nil) nil nil)) (sigma_comm 0 (sigma_comm-1 nil 3460644071 ("" (skosimp*) (("" (generalize "m!1 - 1" "mm" "below(m!1)") (("" (induct "mm") (("1" (flatten) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1 4) (("2" (expand "sigma" 1 1) (("2" (replace -2 :hide? t) (("2" (rewrite "sigma_sum[below(n!1)]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals 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) (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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_sum formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (below_induction formula-decl nil bounded_nat_inductions nil) (pred type-eq-decl nil defined_types nil)) shostak)) (mult_assoc_TCC1 0 (mult_assoc_TCC1-1 nil 3460573525 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (mult_assoc_TCC2 0 (mult_assoc_TCC2-1 nil 3460573525 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (mult_assoc 0 (mult_assoc-1 nil 3460573526 ("" (skolem-typepred) (("" (expand "*") (("" (apply-extensionality :hide? t) (("" (lemma "sigma_prop") (("" (inst? :copy? t) (("" (replace -2 :hide? t) (("" (inst -1 "N!1`cols" "M!1`cols" "LAMBDA (k_1: below(N!1`cols)): P!1`matrix(k_1, x!2)" "LAMBDA (k_1: below(N!1`cols), k: below(M!1`cols)):
M!1`matrix(x!1, k) * N!1`matrix(k, k_1)") (("" (assert) (("" (replace -1) (("" (rewrite "sigma_comm") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "Matrix" matrices nil) (sigma_prop formula-decl nil matrices nil) (sigma_comm formula-decl nil matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posint nonempty-type-eq-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (P!1 skolem-const-decl "{P | N!1`cols = P`rows}" matrices nil) (N!1 skolem-const-decl "{N | M!1`cols = N`rows}" matrices nil) (M!1 skolem-const-decl "Matrix" matrices nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND 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/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_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) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (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)) shostak)) (mult_assoc_vect_TCC1 0 (mult_assoc_vect_TCC1-1 nil 3519735992 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (mult_assoc_vect_TCC2 0 (mult_assoc_vect_TCC2-1 nil 3519735992 ("" (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) (= const-decl "[T, T -> boolean]" equalities nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices nil) (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) (>= 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) (nat nonempty-type-eq-decl nil naturalnumbers 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)) nil)) (mult_assoc_vect_TCC3 0 (mult_assoc_vect_TCC3-1 nil 3519735992 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (mult_assoc_vect 0 (thm "thm" 3519907836 ("" (skosimp) (("" (expand "*") (("" (apply-extensionality) (("1" (hide 2) (("1" (lemma "sigma_prop") (("1" (inst?) (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_comm") (("1" (inst?) (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (name "aa" "LAMBDA (j_1: below(N!1`cols)):
sigma(0, M!1`cols - 1,
LAMBDA (i_1: below(M!1`cols)):
M!1`matrix(x!1, i_1) *
(N!1`matrix(i_1, j_1) * V!1(j_1)))") (("1" (replace -1) (("1" (name "bb" "LAMBDA (k_1: below(N!1`cols)):
sigma(0, M!1`cols - 1,
LAMBDA (k: below(M!1`cols)):
M!1`matrix(x!1, k) * N!1`matrix(k, k_1))
* V!1(k_1)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[N!1`cols]]") (("1" (inst -1 "aa" "bb" "N!1`cols-1" "0") (("1" (case "(FORALL (n: subrange(0, N!1`cols - 1)): aa(n) = bb(n))") (("1" (assert) nil nil) ("2" (skosimp) (("2" (hide -1 -2 2) (("2" (expand "aa") (("2" (expand "bb") (("2" (lemma "sigma_eq[below[M!1`cols]]") (("2" (lemma "sigma_scal[below[M!1`cols]]") (("2" (inst -1 "LAMBDA (k: below(M!1`cols)):
M!1`matrix(x!1, k) * N!1`matrix(k, n!1)" "V!1(n!1)" "M!1`cols-1" "0") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil) ("5" (skosimp) (("5" (assert) nil nil)) nil) ("6" (skosimp) (("6" (assert) nil nil)) nil) ("7" (skosimp) (("7" (assert) nil nil)) nil) ("8" (skosimp) (("8" (assert) nil nil)) nil) ("9" (skosimp) (("9" (assert) nil nil)) nil)) nil)) nil)) nil) ((* const-decl "Matrix" matrices nil) (* const-decl "Vector[M`rows]" matrices nil) (posint nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (sigma_comm formula-decl nil matrices nil) (sigma_eq formula-decl nil sigma "reals/") (below type-eq-decl nil nat_types nil) (subrange type-eq-decl nil integers nil) (bb skolem-const-decl "[below(N!1`cols) -> real]" matrices nil) (sigma_scal formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (aa skolem-const-decl "[below(N!1`cols) -> real]" matrices nil) (sigma_prop formula-decl nil matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (<= const-decl "bool" reals nil) (N!1 skolem-const-decl "{N | M!1`cols = N`rows}" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (M!1 skolem-const-decl "Matrix" matrices nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND 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/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (Matrix type-eq-decl nil matrices nil) (below type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak) (mult_assoc_vect-1 nil 3519904272 ("" (skosimp) (("" (expand "*") (("" (apply-extensionality 1) (("1" (postpone) nil nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil) ("6" (postpone) nil nil) ("7" (postpone) nil nil) ("8" (postpone) nil nil) ("9" (postpone) nil nil)) nil)) nil)) nil) ((sigma_eq formula-decl nil sigma "reals/") (sigma_scal 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/") (Index type-eq-decl nil vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/")) shostak)) (left_distributive_TCC1 0 (left_distributive_TCC1-1 nil 3460644970 ("" (subtype-tcc) nil nil) ((+ const-decl "Matrix" matrices nil)) nil)) (left_distributive_TCC2 0 (left_distributive_TCC2-1 nil 3460644970 ("" (subtype-tcc) nil nil) nil nil)) (left_distributive_TCC3 0 (left_distributive_TCC3-1 nil 3460644970 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (left_distributive 0 (left_distributive-1 nil 3460644993 ("" (skolem-typepred) (("" (expand "*") (("" (expand "+") (("" (apply-extensionality :hide? t) (("1" (lemma "sigma_sum[below(M!1`cols)]") (("1" (inst?) (("1" (replace -1 :hide? t) (("1" (propax) nil nil)) nil) ("2" (typepred "x!2") (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("3" (hide 2) (("3" (typepred "x!2") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil)) nil)) nil)) nil) ((* const-decl "Matrix" matrices nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" 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/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (M!1 skolem-const-decl "Matrix" matrices nil) (N!1 skolem-const-decl "{N | M!1`cols = N`rows}" matrices nil) (P!1 skolem-const-decl "(LAMBDA (N_1: Matrix): N!1`rows = N_1`rows AND N!1`cols = N_1`cols)" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (x!2 skolem-const-decl "below((N!1 + P!1)`cols)" matrices nil) (sigma_sum formula-decl nil sigma "reals/") (+ const-decl "Matrix" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (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)) shostak)) (right_distributive_TCC1 0 (right_distributive_TCC1-1 nil 3460644970 ("" (subtype-tcc) nil nil) ((+ const-decl "Matrix" matrices nil)) nil)) (right_distributive_TCC2 0 (right_distributive_TCC2-1 nil 3460644970 ("" (subtype-tcc) nil nil) nil nil)) (right_distributive_TCC3 0 (right_distributive_TCC3-1 nil 3460644970 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "Matrix" matrices nil)) nil)) (right_distributive 0 (right_distributive-1 nil 3460645380 ("" (skolem-typepred) (("" (expand "same_dim?") (("" (expand "+") (("" (expand "*") (("" (apply-extensionality :hide? t) (("1" (same-name "sigma[below(N!1`cols)]" "sigma[below(M!1`cols)]") (("1" (replace -1 :hide? t) (("1" (flatten) (("1" (replace -2) (("1" (rewrite "sigma_sum[below(M!1`cols)]") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil) ("7" (grind) nil nil) ("8" (grind) nil nil) ("9" (grind) nil nil) ("10" (grind) nil nil) ("11" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "Matrix" matrices nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" 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/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (N!1 skolem-const-decl "(LAMBDA (N): M!1`rows = N`rows AND M!1`cols = N`cols)" matrices nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (P!1 skolem-const-decl "{P | M!1`cols = P`rows}" matrices nil) (M!1 skolem-const-decl "Matrix" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_sum formula-decl nil sigma "reals/") (* const-decl "Matrix" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (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)) shostak)) (left_distributive_vect 0 (thm "thm" 3520937517 ("" (skosimp) (("" (apply-extensionality) (("" (case "(M!1 * v1!1 - M!1 * v2!1)(x!1)=(M!1 * v1!1)(x!1) - (M!1 * v2!1)(x!1)") (("1" (replace -1) (("1" (assert) (("1" (expand "*" 1) (("1" (hide -1 2) (("1" (lemma "sigma_minus[below[M!1`cols]]") (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_eq[below[M!1`cols]]") (("1" (inst?) (("1" (assert) (("1" (skosimp) (("1" (assert) (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (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) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (Index type-eq-decl nil vectors "vectors/") (* const-decl "Vector[M`rows]" matrices nil) (- const-decl "real" vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sigma_minus formula-decl nil sigma "reals/") (below type-eq-decl nil nat_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq formula-decl nil sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak) (left_distributive_vect-1 nil 3520937054 ("" (skosimp) (("" (grind) (("" (apply-extensionality) (("" (postpone) nil nil)) nil)) nil)) nil) ((Index type-eq-decl nil vectors "vectors/") (- const-decl "real" vectors "vectors/") (Vector type-eq-decl nil vectors "vectors/") (sigma_minus formula-decl nil sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/")) shostak)) (transpose_product_TCC1 0 (transpose_product_TCC1-1 nil 3460646315 ("" (subtype-tcc) nil nil) ((transpose const-decl "Matrix" matrices nil)) nil)) (transpose_product 0 (transpose_product-1 nil 3460646316 ("" (skolem-typepred) (("" (expand "transpose") (("" (expand "*") (("" (apply-extensionality :hide? t) (("1" (same-name "sigma[below(N!1`rows)]" "sigma[below(M!1`cols)]") (("1" (replace -1) (("1" (replace -2 :dir rl) (("1" (case-replace "(LAMBDA (k: below(M!1`cols)):
M!1`matrix(x!2, k) * N!1`matrix(k, x!1)) = (LAMBDA (k: below(N!1`rows)):
N!1`matrix(k, x!1) * M!1`matrix(x!2, k))") (("1" (hide 2) (("1" (assert) (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil) ("2" (grind) (("2" (typepred "x!2") (("2" (grind) nil nil)) nil)) nil) ("3" (typepred "x!1") (("3" (grind) nil nil)) nil) ("4" (typepred "x!1") (("4" (grind) nil nil)) nil) ("5" (typepred "x!2") (("5" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "x!2") (("2" (grind) nil nil)) nil)) nil) ("3" (hide 2) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil) ("4" (hide 2) (("4" (typepred "x!1") (("4" (grind) nil nil)) nil)) nil) ("5" (hide 2) (("5" (typepred "x!2") (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil)) nil)) nil)) nil) ((transpose const-decl "Matrix" matrices nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" 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/") (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (M!1 skolem-const-decl "Matrix" matrices nil) (N!1 skolem-const-decl "{N | M!1`cols = N`rows}" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (x!2 skolem-const-decl "below((M!1 * N!1)`rows)" matrices nil) (x!1 skolem-const-decl "below((M!1 * N!1)`cols)" matrices nil) (* const-decl "Matrix" matrices nil) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (below type-eq-decl nil naturalnumbers nil) (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)) shostak)) (trans_mat_scal_TCC1 0 (trans_mat_scal_TCC1-1 nil 3520248087 ("" (subtype-tcc) nil nil) ((transpose const-decl "Matrix" matrices nil)) nil)) (trans_mat_scal_TCC2 0 (trans_mat_scal_TCC2-1 nil 3520248087 ("" (subtype-tcc) nil nil) ((transpose const-decl "Matrix" matrices nil)) nil)) (trans_mat_scal 0 (thm "thm" 3521308146 ("" (skosimp) (("" (expand "*") (("" (lemma "sigma_prop") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (lemma "sigma_comm") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (name "aa" "LAMBDA (j_1: below(A!1`cols)):
sigma(0, A!1`rows - 1,
LAMBDA (i_1: below(A!1`rows)):
x!1(i_1) * (A!1`matrix(i_1, j_1) * y!1(j_1)))") (("1" (replace -1) (("1" (name "bb" "LAMBDA (i_1: Index[transpose(A!1)`rows]):
sigma(0, transpose(A!1)`cols - 1,
LAMBDA (k: below(transpose(A!1)`cols)):
transpose(A!1)`matrix(i_1, k) * x!1(k))
* y!1(i_1)") (("1" (replace -1) (("1" (hide -1 -2) (("1" (lemma "sigma_eq[below[A!1`cols]]") (("1" (inst?) (("1" (inst -1 "bb") (("1" (case "A!1`cols=transpose(A!1)`rows") (("1" (replace -1 :actuals? t :hide? t) (("1" (assert) (("1" (hide 2) (("1" (grind) (("1" (expand "aa") (("1" (expand "bb") (("1" (lemma "sigma_eq[below[A!1`cols]]") (("1" (name "a1" "LAMBDA (i_1: below(A!1`rows)):
x!1(i_1) * (A!1`matrix(i_1, n!1) * y!1(n!1))") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sigma_scal[below[transpose(A!1)`cols]]") (("1" (inst?) (("1" (inst -1 "y!1(n!1)") (("1" (swap-rel -1) (("1" (case " sigma(0, transpose(A!1)`cols - 1,
LAMBDA (k: below(transpose(A!1)`cols)):
transpose(A!1)`matrix(n!1, k) * x!1(k))
* y!1(n!1)= y!1(n!1) *
sigma(0, transpose(A!1)`cols - 1,
LAMBDA (k: below(transpose(A!1)`cols)):
transpose(A!1)`matrix(n!1, k) * x!1(k))") (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (name "a2" " LAMBDA (i: below[transpose(A!1)`cols]):
y!1(n!1) * (transpose(A!1)`matrix(n!1, i) * x!1(i))") (("1" (replace -1) (("1" (lemma "sigma_eq[below[A!1`rows]]") (("1" (inst?) (("1" (inst -1 "a2") (("1" (case "transpose(A!1)`cols=A!1`rows") (("1" (replace -1 :actuals? t :hide? t) (("1" (assert) (("1" (assert) (("1" (hide 2) (("1" (grind) (("1" (expand "a1") (("1" (expand "a2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (hide 2) (("4" (grind) nil nil)) nil) ("5" (hide 2) (("5" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) | |
