| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/matrices/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 371 kB |
|
Impressum matrix_inv.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(matrix_inv (left_inv_TCC1 0 (left_inv_TCC1-1 nil 3615726331 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (SquareMatrix type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil)) nil)) (left_inv_TCC2 0 (left_inv_TCC2-1 nil 3615726331 ("" (skeep) (("" (skosimp*) nil nil)) nil) nil nil)) (left_inv_TCC3 0 (left_inv_TCC3-2 nil 3615802147 ("" (skeep) (("" (skeep) (("" (case "diagonal?(dg`ans)") (("1" (label "idz" -1) (("1" (hide "idz") (("1" (skeep) (("1" (case "NOT diagonal?(newT)") (("1" (hide 2) (("1" (replace -3 +) (("1" (expand "diagonal?") (("1" (skosimp*) (("1" (rewrite "entry_form_matrix") (("1" (lift-if) (("1" (assert) nil nil)) nil) ("2" (hide 3) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "diagonal_simple_prod") (("2" (inst - "false" "rows(S)" "newT") (("1" (assert) (("1" (split) (("1" (case "rows(newT) = rows(S) AND columns(newT) = rows(S)") (("1" (flatten) (("1" (assert) (("1" (rewrite "matrix_mult_assoc") (("1" (rewrite "full_matrix_eq") (("1" (split) (("1" (rewrite "rows_mult") (("1" (assert) nil nil)) nil) ("2" (rewrite "columns_mult") (("1" (assert) (("1" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rows") (("2" (expand "length" -2 1) (("2" (rewrite "length_rows" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "entry_mult") (("3" (lift-if) (("3" (split 1) (("1" (flatten) (("1" (expand "*" + 1) (("1" (rewrite "dot_eq_sigma") (("1" (rewrite "length_row") (("1" (replace -4) (("1" (rewrite "length_col") (("1" (rewrite "rows_mult") (("1" (expand "min" 1) (("1" (rewrite "entry_Id") (("1" (assert) (("1" (rewrite "columns_mult" -2) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (rewrite "sigma_restrict_eq_0") (("1" (hide 3) (("1" (skosimp*) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (case "i!1 = i!2") (("1" (typepred "dg") (("1" (assert) (("1" (replace -16 :dir rl) (("1" (replace -3) (("1" (reveal "idz") (("1" (expand "diagonal?") (("1" (inst - "i!2" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "diagonal?") (("2" (inst - "i!1" "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (lemma "sigma_eq_one_arg2") (("2" (inst?) (("2" (inst - "j!1") (("2" (assert) (("2" (split -1) (("1" (replaces -1) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (typepred "dg") (("1" (assert) (("1" (replace -16 1) (("1" (rewrite "entry_form_matrix") (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (lemma "det_upper_triangular_zero") (("1" (inst - "R*S") (("1" (assert) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (rewrite "access_row") (("2" (rewrite "access_col") (("2" (typepred "dg") (("2" (reveal "idz") (("2" (expand "diagonal?") (("2" (inst - "i!2" "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "columns_mult" 1) (("1" (assert) (("1" (rewrite "entry_eq_0") (("1" (ground) nil nil)) nil)) nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -5 1) (("2" (rewrite "rows_form_matrix") (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (assert) nil nil) ("2" (skosimp*) nil nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "rows_mult") (("2" (assert) (("2" (replace -5 1) (("2" (rewrite "rows_form_matrix") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "rows_mult") (("3" (rewrite "columns_mult" 1) (("1" (replace -5 1) (("1" (rewrite "rows_form_matrix") (("1" (assert) nil nil) ("2" (skosimp*) nil nil)) nil)) nil) ("2" (typepred "newT") (("2" (expand "rows") (("2" (lemma "rows_form_matrix") (("2" (inst?) (("1" (assert) (("1" (expand "rows" -1) (("1" (expand "length" -1 1) (("1" (rewrite "length_rows" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (rewrite "rows_mult") (("4" (replace -5) (("4" (rewrite "rows_form_matrix") (("1" (assert) nil nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil) ("5" (rewrite "columns_mult" 1) (("1" (assert) nil nil) ("2" (lemma "rows_form_matrix") (("2" (inst?) (("1" (assert) (("1" (expand "rows" -1 1) (("1" (expand "length" -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "rows(newT) = rows(S)") (("1" (case "columns(newT) = rows(S)") (("1" (assert) (("1" (flatten) (("1" (lemma "form_matrix_square") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -5 +) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("1" (assert) nil nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4 1) (("2" (rewrite "rows_form_matrix") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "dg") (("2" (assert) (("2" (expand "diagonal?") (("2" (skosimp*) (("2" (inst - "i!1" "j!1") (("2" (inst - "i!1" "j!1") (("2" (assert) (("2" (rewrite "entry_eq_0" 3) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((diagonal_simple_prod formula-decl nil matrix_det nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (form_matrix_square judgement-tcc nil matrices nil) (mult_full application-judgement "FullMatrix" matrices nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (full_matrix_eq formula-decl nil matrices nil) (entry_eq_0 formula-decl nil matrices nil) (dot_eq_sigma formula-decl nil matrices 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) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (entry_Id formula-decl nil matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_one_arg2 formula-decl nil sigma "reals/") (det_upper_triangular_zero formula-decl nil matrix_det nil) (subrange type-eq-decl nil integers nil) (access_row formula-decl nil matrices nil) (access_col formula-decl nil matrices nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (access const-decl "real" matrices 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/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (length_col formula-decl nil matrices nil) (length_row formula-decl nil matrices nil) (entry_mult formula-decl nil matrices nil) (columns_mult formula-decl nil matrices nil) (length_rows formula-decl nil matrices nil) (rows_mult formula-decl nil matrices nil) (matrix_mult_assoc formula-decl nil matrices nil) (columns_form_matrix formula-decl nil matrices nil) (rows_form_matrix formula-decl nil matrices nil) (newT skolem-const-decl "{M: MatrixMN(rows(S), rows(S)) | FORALL (i_1: below(rows(S)), j_1: below(rows(S))): nth(row(M)(i_1), j_1) = IF i_1 /= j_1 OR entry(R * S)(i_1, i_1) = 0 THEN 0 ELSE 1 / entry(R * S)(i_1, i_1) ENDIF}" matrix_inv nil) (R skolem-const-decl "SquareMatrix(rows(S))" matrix_inv nil) (S skolem-const-decl "{S | det(S) /= 0}" matrix_inv nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry_form_matrix formula-decl nil matrices nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (diagonal? const-decl "bool" matrix_det nil) (SquareMatrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (rows const-decl "nat" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (upper_triangular? const-decl "bool" matrix_det nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (is_simple_prod? const-decl "bool" matrix_det nil) (FALSE const-decl "bool" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil)) nil) (left_inv_TCC3-1 nil 3615726331 ("" (skeep) (("" (skeep) (("" (skeep) (("" (label "newTname" -3) (("" (split +) (("1" (rewrite "matrix_mult_assoc") (("1" (label "Rname" -2) (("1" (typepred "dg") (("1" (replace "Rname" :dir rl) (("1" (assert) (("1" (replace -3) (("1" (rewrite "full_matrix_eq" 1) (("1" (assert) (("1" (case "NOT (rows(newT * dg`ans) = rows(Id(rows(S))) AND columns(newT * dg`ans) = columns(Id(rows(S))))") (("1" (hide 2) (("1" (rewrite "rows_mult") (("1" (rewrite "columns_mult") (("1" (assert) (("1" (replace "newTname" 1) (("1" (rewrite "rows_form_matrix") (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "newT") (("2" (expand "length" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (typepred "i") (("2" (typepred "j") (("2" (assert) (("2" (rewrite "entry_Id" 1) (("2" (rewrite "entry_mult" 1) (("2" (assert) (("2" (case "NOT rows(newT)=rows(S)") (("1" (replace "newTname" 1) (("1" (rewrite "rows_form_matrix") (("1" (skosimp*) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "*" 1) (("2" (rewrite "dot_eq_sigma") (("2" (case "NOT columns(newT)=columns(S)") (("1" (assert) (("1" (replace "newTname" 1) (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_col" 1) (("2" (rewrite "length_row" 1) (("1" (expand "min") (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (rewrite "sigma_restrict_eq_0") (("1" (hide 3) (("1" (skosimp*) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (case "i!1 = i") (("1" (inst - "i!1" "j") (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (mult_left_inv_right_TCC1 0 (mult_left_inv_right_TCC1-1 nil 3615802707 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (rows const-decl "nat" matrices nil)) nil)) (mult_left_inv_right 0 (mult_left_inv_right-1 nil 3615802708 ("" (skeep) (("" (typepred "left_inv(S)") (("" (case "NOT (left_inv(S) * S)*left_inv(S) = Id(rows(S))*left_inv(S)") (("1" (assert) nil nil) ("2" (rewrite "mult_Id_left") (("2" (rewrite "matrix_mult_assoc") (("1" (case "NOT det(left_inv(S))/=0") (("1" (flatten) (("1" (case "NOT det(left_inv(S)*S) = det(Id(rows(S)))") (("1" (assert) nil nil) ("2" (rewrite "det_mult") (("2" (rewrite "det_Id") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "NOT left_inv(left_inv(S))*(left_inv(S) * (S * left_inv(S))) = left_inv(left_inv(S (("1" (assert) nil nil) ("2" (lemma "matrix_mult_assoc") (("2" (inst - "S*left_inv(S)" "left_inv(left_inv(S))" "left_inv(S)") (("2" (assert) (("2" (split -1) (("1" (replaces -1 :dir rl) (("1" (typepred "left_inv(left_inv(S))") (("1" (replace -7) (("1" (rewrite "mult_Id_left") (("1" (assert) nil nil) ("2" (rewrite "rows_mult") (("2" (assert) nil nil)) nil) ("3" (rewrite "rows_mult") (("3" (assert) (("3" (rewrite "columns_mult") (("3" (typepred "S") (("3" (expand "rows") (("3" (assert) (("3" (expand "length") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "left_inv(S)") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "S") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((left_inv const-decl "{Q: SquareMatrix(rows(S)) | Q * S = Id(rows(S))}" matrix_inv nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (SquareMatrix type-eq-decl nil matrices nil) (det def-decl "real" matrix_props nil) (/= const-decl "boolean" notequal nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (mult_Id_left formula-decl nil matrices nil) (det_Id formula-decl nil matrix_props nil) (real_times_real_is_real application-judgement "real" reals nil) (det_mult formula-decl nil matrix_diag nil) (rows_mult formula-decl nil matrices nil) (columns_mult formula-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (matrix_mult_assoc formula-decl nil matrices nil) (mult_full application-judgement "FullMatrix" matrices nil)) shostak)) (invertible?_TCC1 0 (invertible?_TCC1-1 nil 3615800573 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil)) nil)) (invertible_rew 0 (invertible_rew-1 nil 3615803598 ("" (skeep) (("" (expand "invertible?") (("" (ground) (("1" (skosimp*) (("1" (inst + "IQ!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "left_inv(SQ)") (("2" (assert) (("2" (typepred "left_inv(SQ)") (("2" (assert) (("2" (rewrite "mult_left_inv_right") nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "IQ!1") (("3" (assert) (("3" (case "IQ!1 = left_inv(SQ)") (("1" (replaces -1) (("1" (rewrite "mult_left_inv_right") (("1" (flatten) (("1" (lemma "det_mult") (("1" (inst - "SQ" "left_inv(SQ)") (("1" (assert) (("1" (typepred "left_inv(SQ)") (("1" (replace -7) (("1" (rewrite "det_Id") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT (IQ!1 * SQ)*left_inv(SQ) = Id(rows(SQ))*left_inv(SQ)") (("1" (assert) nil nil) ("2" (rewrite "matrix_mult_assoc" -1) (("1" (rewrite "mult_left_inv_right") (("1" (rewrite "mult_Id_left") (("1" (rewrite "mult_Id_right") nil nil)) nil) ("2" (flatten) (("2" (lemma "det_mult") (("2" (inst - "SQ" "IQ!1") (("2" (assert) (("2" (lemma "det_Id") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "SQ") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (lemma "det_mult") (("3" (inst - "SQ" "IQ!1") (("3" (assert) (("3" (lemma "det_Id") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (inst + "IQ") (("4" (assert) (("4" (case "det(IQ)=0") (("1" (assert) (("1" (lemma "det_mult") (("1" (inst - "IQ" "SQ") (("1" (assert) (("1" (lemma "det_Id") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "SQ = left_inv(IQ)") (("1" (replaces -1) (("1" (rewrite "mult_left_inv_right") (("1" (assert) nil nil)) nil)) nil) ("2" (case "NOT left_inv(SQ)*(SQ*IQ) = left_inv(SQ)*Id(rows(SQ))") (("1" (assert) nil nil) ("2" (rewrite "matrix_mult_assoc" :dir rl) (("1" (typepred "left_inv(SQ)") (("1" (replace -7) (("1" (rewrite "mult_Id_left") (("1" (rewrite "mult_Id_right") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "SQ") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (lemma "det_mult") (("3" (inst - "IQ" "SQ") (("3" (assert) (("3" (lemma "det_Id") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((invertible? const-decl "bool" matrix_inv nil) (mult_Id_right formula-decl nil matrices nil) (mult_Id_left formula-decl nil matrices nil) (matrix_mult_assoc formula-decl nil matrices nil) (det_Id formula-decl nil matrix_props nil) (real_times_real_is_real application-judgement "real" reals nil) (det_mult formula-decl nil matrix_diag nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (SquareMatrix type-eq-decl nil matrices nil) (MatrixMN type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (left_inv const-decl "{Q: SquareMatrix(rows(S)) | Q * S = Id(rows(S))}" matrix_inv nil) (NOT const-decl "[bool -> bool]" booleans nil) (mult_left_inv_right formula-decl nil matrix_inv nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_full application-judgement "FullMatrix" matrices nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (inverse_TCC1 0 (inverse_TCC1-1 nil 3614960158 ("" (skeep) (("" (typepred "SQ") (("" (assert) (("" (expand "invertible?") (("" (skeep) (("" (lemma "det_mult") (("" (inst - "IQ" "SQ") (("" (assert) (("" (lemma "det_Id") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((invertible? const-decl "bool" matrix_inv nil) (det def-decl "real" matrix_props nil) (/= const-decl "boolean" notequal nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (det_mult formula-decl nil matrix_diag nil) (mult_full application-judgement "FullMatrix" matrices nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (det_Id formula-decl nil matrix_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (inverse_TCC2 0 (inverse_TCC2-1 nil 3615726331 ("" (skeep) (("" (assert) (("" (typepred "left_inv(SQ)") (("1" (assert) (("1" (rewrite "mult_left_inv_right") (("1" (typepred "SQ") (("1" (assert) (("1" (expand "invertible?") (("1" (skeep) (("1" (assert) (("1" (lemma "det_mult") (("1" (assert) (("1" (inst - "IQ" "SQ") (("1" (assert) (("1" (lemma "det_Id") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "SQ") (("2" (assert) (("2" (expand "invertible?") (("2" (skeep) (("2" (lemma "det_mult") (("2" (inst - "IQ" "SQ") (("2" (assert) (("2" (lemma "det_Id") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mult_full application-judgement "FullMatrix" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (det_Id formula-decl nil matrix_props nil) (det_mult formula-decl nil matrix_diag nil) (mult_left_inv_right formula-decl nil matrix_inv 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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (SquareMatrix type-eq-decl nil matrices nil) (MatrixMN type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (left_inv const-decl "{Q: SquareMatrix(rows(S)) | Q * S = Id(rows(S))}" matrix_inv nil) (invertible? const-decl "bool" matrix_inv nil)) nil)) (mult_inverse_left_TCC1 0 (mult_inverse_left_TCC1-1 nil 3614960158 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (invertible? const-decl "bool" matrix_inv nil) (/= const-decl "boolean" notequal nil)) nil)) (mult_inverse_left_TCC2 0 (mult_inverse_left_TCC2-1 nil 3615638749 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (invertible? const-decl "bool" matrix_inv nil)) nil)) (mult_inverse_left 0 (mult_inverse_left-1 nil 3615804506 ("" (skeep) (("" (assert) nil nil)) nil) ((mult_full application-judgement "FullMatrix" matrices nil)) shostak)) (mult_inverse_right 0 (mult_inverse_right-1 nil 3615804514 ("" (skeep) (("" (assert) nil nil)) nil) ((mult_full application-judgement "FullMatrix" matrices nil)) shostak)) (inverse_unique 0 (inverse_unique-1 nil 3615804524 ("" (skeep) (("" (assert) (("" (rewrite "invertible_rew") (("" (ground) (("1" (inst + "IQ") (("1" (assert) nil nil)) nil) ("2" (lemma "det_mult") (("2" (inst - "SQ" "IQ") (("2" (assert) (("2" (lemma "det_Id") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "NOT (IQ*SQ)*inverse(SQ)=Id(rows(SQ))*inverse(SQ)") (("1" (assert) nil nil) ("2" (rewrite "matrix_mult_assoc") (("1" (rewrite "mult_inverse_right") (("1" (rewrite "mult_Id_right") (("1" (rewrite "mult_Id_left") nil nil)) nil) ("2" (rewrite "invertible_rew") (("2" (flatten) (("2" (inst + "IQ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "SQ") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (case "NOT (IQ*SQ)*inverse(SQ) = Id(rows(SQ))*inverse(SQ)") (("1" (assert) nil nil) ("2" (rewrite "matrix_mult_assoc") (("1" (rewrite "mult_inverse_right") (("1" (rewrite "mult_Id_right") (("1" (rewrite "mult_Id_left") (("1" (replaces -1) (("1" (rewrite "mult_inverse_right") nil nil)) nil)) nil)) nil) ("2" (rewrite "invertible_rew") (("2" (flatten) (("2" (inst + "IQ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "SQ") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (lemma "det_mult") (("3" (inst - "SQ" "IQ") (("3" (assert) (("3" (lemma "det_Id") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (lemma "det_mult") (("5" (inst - "IQ" "SQ") (("5" (assert) (("5" (lemma "det_Id") (("5" (inst?) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (lemma "det_mult") (("6" (inst - "IQ" "SQ") (("6" (assert) (("6" (lemma "det_Id") (("6" (inst?) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (case "NOT inverse(SQ)*(SQ*IQ)=inverse(SQ)*Id(rows(SQ))") (("1" (assert) nil nil) ("2" (rewrite "matrix_mult_assoc" :dir rl) (("1" (rewrite "mult_inverse_left") (("1" (rewrite "mult_Id_left") (("1" (rewrite "mult_Id_right") nil nil)) nil) ("2" (rewrite "invertible_rew") (("2" (flatten) (("2" (inst 2 "IQ") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "SQ") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("8" (case "det(SQ) = 0") (("1" (lemma "det_mult") (("1" (inst - "IQ" "SQ") (("1" (assert) (("1" (lemma "det_Id") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT inverse(SQ)*(SQ*IQ)=inverse(SQ)*Id(rows(SQ))") (("1" (assert) nil nil) ("2" (rewrite "matrix_mult_assoc" :dir rl) (("1" (rewrite "mult_Id_right") (("1" (rewrite "mult_inverse_left") (("1" (rewrite "mult_Id_left") (("1" (replace -1) (("1" (rewrite "mult_inverse_left") nil nil)) nil)) nil) ("2" (rewrite "invertible_rew") nil nil)) nil)) nil) ("2" (typepred "SQ") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mult_full application-judgement "FullMatrix" matrices nil) (det_Id formula-decl nil matrix_props nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (det_mult formula-decl nil matrix_diag nil) (matrix_mult_assoc formula-decl nil matrices nil) (mult_Id_right formula-decl nil matrices nil) (mult_Id_left formula-decl nil matrices nil) (mult_inverse_right formula-decl nil matrix_inv nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (MatrixMN type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (invertible? const-decl "bool" matrix_inv nil) (SquareMatrix type-eq-decl nil matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (mult_inverse_left formula-decl nil matrix_inv nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (invertible_rew formula-decl nil matrix_inv nil)) shostak)) (invertible_det 0 (invertible_det-1 nil 3615805638 ("" (skeep) (("" (rewrite "invertible_rew") (("" (ground) (("1" (skeep) (("1" (lemma "det_mult") (("1" (inst?) (("1" (assert) (("1" (lemma "det_Id") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (lemma "det_mult") (("2" (inst?) (("2" (assert) (("2" (lemma "det_Id") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((invertible_rew formula-decl nil matrix_inv nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (det_Id formula-decl nil matrix_props nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (mult_full application-judgement "FullMatrix" matrices nil) (det_mult formula-decl nil matrix_diag nil)) shostak)) (invertible_mult_TCC1 0 (invertible_mult_TCC1-1 nil 3615806004 ("" (skeep) (("" (rewrite "rows_mult") (("" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "S") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rows_mult formula-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_full application-judgement "FullMatrix" matrices nil) (columns_mult formula-decl nil matrices nil)) nil)) (invertible_mult 0 (invertible_mult-1 nil 3615806004 ("" (skeep) (("" (rewrite "det_mult") (("" (lemma "nzreal_times_nzreal_is_nzreal") (("" (case "FORALL (rr,ss:real): rr*ss=0 IFF (rr=0 OR ss=0)") (("1" (inst?) (("1" (hide -2) (("1" (lemma "invertible_det") (("1" (inst-cp - "S") (("1" (inst - "R") (("1" (lemma "invertible_det") (("1" (inst - "S*R") (("1" (lemma "det_mult") (("1" (inst?) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (rewrite "rows_mult") (("2" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "S") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil) ((det_mult formula-decl nil matrix_diag nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (real_times_real_is_real application-judgement "real" reals 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) (rows_mult formula-decl nil matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (columns_mult formula-decl nil matrices nil) (MatrixMN type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (S skolem-const-decl "Square" matrix_inv nil) (R skolem-const-decl "Square" matrix_inv nil) (mult_full application-judgement "FullMatrix" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (invertible_det formula-decl nil matrix_inv nil) (det def-decl "real" matrix_props nil) (zero_times3 formula-decl nil real_props nil) (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil)) shostak)) (inverse_mult_TCC1 0 (inverse_mult_TCC1-1 nil 3615805789 ("" (skeep) (("" (assert) (("" (lemma "det_mult") (("" (inst - "R" "S") (("" (assert) (("" (rewrite "invertible_det") (("" (rewrite "invertible_det") (("" (rewrite "invertible_det") (("1" (assert) (("1" (case "FORALL (izb:bool): (izb OR izb) = izb") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (hide -1) (("1" (lemma "nzreal_times_nzreal_is_nzreal") (("1" (inst - "det(S)" "det(R)") (("1" (rewrite "rows_mult") (("1" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "S") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (iff) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "rows_mult") (("2" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "S") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mult_full application-judgement "FullMatrix" matrices nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (invertible_det formula-decl nil matrix_inv nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (MatrixMN type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (S skolem-const-decl "Square" matrix_inv nil) (R skolem-const-decl "Square" matrix_inv nil) (nzreal nonempty-type-eq-decl nil reals nil) (columns_mult formula-decl nil matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (rows_mult formula-decl nil matrices nil) (nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (det_mult formula-decl nil matrix_diag nil)) nil)) (inverse_mult 0 (inverse_mult-1 nil 3615805789 ("" (skeep) (("" (lemma "inverse_unique") (("" (inst - "inverse(R)*inverse(S)" "S*R") (("1" (assert) (("1" (hide 2) (("1" (rewrite "rows_mult") (("1" (rewrite "rows_mult") (("1" (assert) (("1" (rewrite "matrix_mult_assoc" :dir rl) (("1" (rewrite "matrix_mult_assoc") (("1" (rewrite "mult_inverse_left") (("1" (rewrite "mult_Id_right") (("1" (rewrite "mult_inverse_left") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "invertible_det" 1) nil nil)) nil) ("2" (typepred "inverse(S)") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "S") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "rows_mult") (("2" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "inverse(R)") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inverse_unique formula-decl nil matrix_inv nil) (columns_mult formula-decl nil matrices nil) (rows_mult formula-decl nil matrices nil) (invertible_det formula-decl nil matrix_inv nil) (mult_Id_right formula-decl nil matrices nil) (mult_inverse_left formula-decl nil matrix_inv nil) (NOT const-decl "[bool -> bool]" booleans nil) (matrix_mult_assoc formula-decl nil matrices nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt 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) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (rows const-decl "nat" matrices nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (invertible? const-decl "bool" matrix_inv nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (SquareMatrix type-eq-decl nil matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (R skolem-const-decl "Square" matrix_inv nil) (S skolem-const-decl "Square" matrix_inv nil) (mult_full application-judgement "FullMatrix" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (det_inverse_TCC1 0 (det_inverse_TCC1-1 nil 3615806915 ("" (skeep) (("" (assert) (("" (rewrite "invertible_det") nil nil)) nil)) nil) ((Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (invertible_det formula-decl nil matrix_inv nil)) nil)) (det_inverse 0 (det_inverse-1 nil 3615806916 ("" (skeep) (("" (lemma "mult_inverse_left") (("" (inst?) (("" (split -1) (("1" (assert) (("1" (lemma "det_mult") (("1" (inst?) (("1" (assert) (("1" (lemma "det_Id") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "invertible_det") nil nil)) nil)) nil)) nil)) nil)) nil) ((mult_inverse_left formula-decl nil matrix_inv nil) (det_mult formula-decl nil matrix_diag nil) (det_Id formula-decl nil matrix_props nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (SquareMatrix type-eq-decl nil matrices nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrix_inv nil) (det def-decl "real" matrix_props nil) (/= const-decl "boolean" notequal nil) (mult_full application-judgement "FullMatrix" matrices nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (invertible_det formula-decl nil matrix_inv nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (inverse_invertible 0 (inverse_invertible-1 nil 3615807168 ("" (skeep) (("" (assert) (("" (rewrite "invertible_det" 1) (("" (rewrite "det_inverse") (("" (ground) nil nil)) nil)) nil)) nil)) nil) ((det_inverse formula-decl nil matrix_inv nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (SquareMatrix type-eq-decl nil matrices nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrix_inv nil) (det def-decl "real" matrix_props nil) (/= const-decl "boolean" notequal nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (invertible_det formula-decl nil matrix_inv nil)) shostak)) (inverse_inverse_TCC1 0 (inverse_inverse_TCC1-1 nil 3615807119 ("" (skeep) (("" (rewrite "invertible_det") (("" (rewrite "invertible_det") (("" (rewrite "det_inverse") (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil) ((invertible_det formula-decl nil matrix_inv nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (det_inverse formula-decl nil matrix_inv nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (SquareMatrix type-eq-decl nil matrices nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrix_inv nil) (det def-decl "real" matrix_props nil) (/= const-decl "boolean" notequal nil)) nil)) (inverse_inverse 0 (inverse_inverse-1 nil 3615807120 ("" (skeep) (("" (lemma "inverse_unique") (("" (inst - "S" "inverse(S)") (("" (assert) nil nil)) nil)) nil)) nil) ((inverse_unique formula-decl nil matrix_inv nil) (mult_full application-judgement "FullMatrix" matrices nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (SquareMatrix type-eq-decl nil matrices nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (invertible? const-decl "bool" matrix_inv nil) (det def-decl "real" matrix_props nil) (/= const-decl "boolean" notequal nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (GH_TCC1 0 (GH_TCC1-1 nil 3615807808 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (GH_TCC2 0 (GH_TCC2-1 nil 3615807808 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (GH_TCC3 0 (GH_TCC3-1 nil 3615807808 ("" (skeep) (("" (rewrite "rows_form_matrix") (("" (lemma "columns_form_matrix") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((columns_form_matrix formula-decl nil 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) (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)) nil)) (GH_TCC4 0 (GH_TCC4-1 nil 3615808555 ("" (skeep) (("" (rewrite "rows_form_matrix") (("" (lemma "columns_form_matrix") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (rows_form_matrix formula-decl nil 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (rat nonempty-type-eq-decl nil rationals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nat_exp application-judgement "nat" exponentiation nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (columns_form_matrix formula-decl nil matrices nil)) nil)) (det_nonzero_simple_prod 0 (det_nonzero_simple_prod-4 nil 3616760142 ("" (skeep) (("" (lemma "inverse_inverse") (("" (inst?) (("" (assert) (("" (expand "inverse" -1 1) (("" (expand "left_inv") (("" (case "FORALL (i:nat): i<rows(S) IMPLIES entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i)/=0") (("1" (name "FG" "LAMBDA (FF:[nat->real]): (LAMBDA (i,j:nat): IF i/=j THEN 0 ELSE FF(i) ENDIF)") (("1" (case "FORALL (FF:[nat->real],n:nat): (FORALL (i:nat): i<n+1 IMPLIES FF(i)/=0) IMPLIES is_s (("1" (name "FFZ" "LAMBDA (i:nat): IF i>=rows(S) OR entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S))(i,i)=0 THEN 0 ELSE 1/entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S))(i,i) ENDIF") (("1" (name "G5" "FG(FFZ)") (("1" (case "(LAMBDA (i, j): IF i /= j OR entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i) = 0 THEN 0 ELSE 1 / entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i) ENDIF) = G5") (("1" (replace -1) (("1" (replace -7 2 :dir rl) (("1" (rewrite "mult_simple_prod") (("1" (hide 3) (("1" (rewrite "rows_mult" 1) (("1" (rewrite "rows_form_matrix") (("1" (expand "G5" 1) (("1" (rewrite -4 1) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "FFZ" -2) (("1" (assert) (("1" (inst -8 "i!1") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (rewrite "rows_mult") (("2" (rewrite "rows_form_matrix") (("2" (typepred "diag(true,false,inverse(S))") (("2" (assert) (("2" (hide-all-but (-4 1)) (("2" (lemma "is_simple_prod_implic") (("2" (inst - "false" "false" "rows(inverse(S))" "diag(TRUE, FALSE, inverse(S))`multip" "true" "false") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (rewrite "rows_form_matrix") (("3" (assert) (("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("1" (expand "G5") (("1" (expand "FG" 1) (("1" (expand "FFZ" 1) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (inst -5 "x!1") (("1" (assert) (("1" (case "x!1/=x!2") (("1" (assert) nil nil) ("2" (flatten) (("2" (assert) (("2" (ground) (("1" (rewrite "entry_eq_0" 1) (("1" (flatten) (("1" (rewrite "rows_mult") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "entry_eq_0" 2) (("2" (flatten) (("2" (rewrite "rows_mult") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil) ("3" (skosimp*) nil nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (skeep) (("2" (expand "is_simple_prod?") (("2" (name "FMG" "LAMBDA (i:nat): Esr(1+n)(i,FF(i))") (("2" (inst + "FMG" "n") (("2" (assert) (("2" (split 1) (("1" (expand "is_simple_seq?") (("1" (skeep) (("1" (inst + "p" "FF(p)") (("1" (assert) (("1" (expand "FMG" 1) (("1" (case "p < 1+n") (("1" (assert) (("1" (expand "FMG" 3) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "full_matrix_eq" 2) (("2" (skosimp*) (("2" (rewrite "entry_Esr") (("2" (rewrite "entry_Id") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "full_matrix_eq" 1) (("2" (split) (("1" (rewrite "rows_form_matrix") (("1" (assert) nil nil)) nil) ("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (case "FORALL (k:nat): FORALL (ii,jj:nat): ii<1+n AND jj<1+n AND k<=n IMPLIES entry(prod_mat(1+n)(F (("1" (inst - "n") (("1" (inst?) (("1" (assert) (("1" (split -1) (("1" (replaces -1) (("1" (rewrite "entry_form_matrix") (("1" (expand "FG" 1) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (typepred "i!1") (("1" (rewrite "rows_form_matrix") nil nil)) nil) ("2" (typepred "i!1") (("2" (rewrite "rows_form_matrix") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (rewrite "rows_form_matrix") nil nil)) nil) ("3" (assert) (("3" (typepred "j!1") (("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "k") (("1" (skeep) (("1" (assert) (("1" (expand "prod_mat" 1) (("1" (expand "FMG" 1) (("1" (rewrite "entry_Esr") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (assert) (("2" (expand "prod_mat" +) (("2" (rewrite "entry_mult") (("2" (assert) (("2" (expand "*" + 1) (("2" (rewrite "dot_eq_sigma") (("2" (rewrite "length_row") (("1" (rewrite "length_col") (("1" (assert) (("1" (expand "FMG" 1 1) (("1" (assert) (("1" (typepred "prod_mat(1 + n) (LAMBDA (i: nat): Esr(1 + n)(i, FF(i)), j)") (("1" (hide (-1 -2)) (("1" (replace -3 :dir rl) (("1" (replace -4) (("1" (assert) (("1" (expand "FMG" 1 1) (("1" (rewrite "rows_Esr") (("1" (assert) (("1" (expand "min") (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (lemma "sigma_eq_one_arg2") (("1" (inst?) (("1" (inst - "ii") (("1" (assert) (("1" (split -1) (("1" (replaces -1) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (inst - "ii" "ii") (("1" (assert) (("1" (replaces -7 1) (("1" (expand "FMG" 1) (("1" (rewrite "entry_Esr" 1) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (rewrite "access_row") (("2" (inst - "ii" "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) nil nil) ("2" (flatten) (("2" (assert) (("2" (lemma "sigma_eq_one_arg2") (("2" (inst?) (("2" (inst - "ii") (("2" (assert) (("2" (split -1) (("1" (replaces -1) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (inst - "ii" "ii") (("1" (assert) (("1" (replaces -1) (("1" (replaces -5) (("1" (expand "FMG" +) (("1" (rewrite "entry_Esr") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "access_row") (("2" (inst - "ii" "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lift-if) (("2" (assert) (("2" (rewrite "sigma_restrict_eq_0") (("2" (skosimp*) (("2" (rewrite "access_row") (("2" (rewrite "access_col") (("2" (assert) (("2" (inst - "ii" "i!2") (("2" (assert) (("2" (replace -5) (("2" (lift-if) (("2" (split 1) (("1" (flatten) (("1" (assert) (("1" (expand "FMG" 1) (("1" (rewrite "entry_Esr") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (expand "FMG" 1) (("1" (rewrite "entry_Esr") nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "prod_mat(1+n)(FMG,j)") (("2" (assert) (("2" (expand "rows") (("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) ("3" (skeep) (("3" (rewrite "rows_form_matrix") (("3" (assert) (("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (lemma "det_inverse") (("2" (inst - "S") (("2" (assert) (("2" (case "det(inverse(S))=0") (("1" (assert) nil nil) ("2" (assert) (("2" (typepred "diag(TRUE, FALSE, inverse(S))") (("2" (replace -3) (("2" (assert) (("2" (inst -6 "i" "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inverse_inverse formula-decl nil matrix_inv nil) (left_inv const-decl "{Q: SquareMatrix(rows(S)) | Q * S = Id(rows(S))}" matrix_inv nil) (det_inverse formula-decl nil matrix_inv nil) (Esr const-decl "SquareMatrix(pn)" matrix_det nil) (prod_mat def-decl "SquareMatrix(pn)" matrix_det nil) (entry_mult formula-decl nil matrices nil) (length_row formula-decl nil matrices nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (access const-decl "real" matrices nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (subrange type-eq-decl nil integers nil) (access_col formula-decl nil matrices nil) (access_row formula-decl nil matrices nil) (sigma_eq_one_arg2 formula-decl nil sigma "reals/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (rows_Esr formula-decl nil matrix_det nil) (length_col formula-decl nil matrices nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_times_real_is_real application-judgement "real" reals nil) (dot_eq_sigma formula-decl nil matrices nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (entry_form_matrix formula-decl nil matrices nil) (is_simple_seq? const-decl "bool" matrix_det nil) (FMG skolem-const-decl "[nat -> SquareMatrix(1 + n)]" matrix_inv nil) (entry_Id formula-decl nil matrices nil) (entry_Esr formula-decl nil matrix_det nil) (full_matrix_eq formula-decl nil matrices nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (columns_form_matrix formula-decl nil matrices nil) (is_simple_prod_implic formula-decl nil matrix_det nil) (rows_form_matrix formula-decl nil matrices nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (FFZ skolem-const-decl "[nat -> real]" matrix_inv nil) (G5 skolem-const-decl "[[nat, nat] -> real]" matrix_inv nil) (rows_mult formula-decl nil matrices nil) (mult_simple_prod formula-decl nil matrix_det nil) (mult_full application-judgement "FullMatrix" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry_eq_0 formula-decl nil matrices nil) (FG skolem-const-decl "[[nat -> real] -> [[nat, nat] -> real]]" matrix_inv nil) (S skolem-const-decl "Square" matrix_inv nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (SquareMatrix type-eq-decl nil matrices nil) (upper_triangular? const-decl "bool" matrix_det nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (is_simple_prod? const-decl "bool" matrix_det nil) (FALSE const-decl "bool" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (det def-decl "real" matrix_props nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (diag const-decl "{SGI: [# ans: SquareMatrix(rows(S)), multip: SquareMatrix(rows(S)), inv: SquareMatrix(rows(S)) #] | upper_triangular?(SGI`ans) AND (FORALL (k, p): k < rows(S) AND p < rows(S) AND entry(SGI`ans)(k, p) /= 0 IMPLIES (k = p OR (k < p AND entry(SGI`ans)(p, p) = 0))) AND (comp_matrix IMPLIES SGI`multip * S = SGI`ans AND is_simple_prod?(rows(S), FALSE, FALSE)(SGI`multip)) AND (comp_matrix AND comp_inverse IMPLIES (SGI`inv * SGI`multip = Id(rows(S)) AND SGI`multip * SGI`inv = Id(rows(S)) AND is_simple_prod?(rows(S), FALSE, FALSE)(SGI`inv))) AND det(SGI`ans) = det(S) AND (det(S) /= 0 IFF (FORALL (k, p): k < rows(S) AND p < rows(S) IMPLIES (entry(SGI`ans)(k, p) /= 0 IFF k = p)))}" matrix_diag nil) (TRUE const-decl "bool" booleans nil) (invertible? const-decl "bool" matrix_inv nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) nil) (det_nonzero_simple_prod-3 nil 3616753803 ("" (skeep) (("" (lemma "inverse_inverse") (("" (inst?) (("" (assert) (("" (expand "inverse" -1 1) (("" (expand "left_inv") (("" (case "FORALL (i:nat): i<rows(S) IMPLIES entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i)/=0") (("1" (name "FG" "LAMBDA (FF:[nat->real]): (LAMBDA (i,j:nat): IF i/=j THEN 0 ELSE FF(i) ENDIF)") (("1" (case "FORALL (FF:[nat->real],n:nat): (FORALL (i:nat): i<n+1 IMPLIES FF(i)/=0) IMPLIES is_s (("1" (name "FFZ" "LAMBDA (i:nat): IF i>=rows(S) OR entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S))(i,i)=0 THEN 0 ELSE 1/entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S))(i,i) ENDIF") (("1" (name "G5" "FG(FFZ)") (("1" (case "(LAMBDA (i, j): IF i /= j OR entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i) = 0 THEN 0 ELSE 1 / entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i) ENDIF) = G5") (("1" (replace -1) (("1" (replace -7 2 :dir rl) (("1" (rewrite "mult_simple_prod") (("1" (hide 3) (("1" (rewrite "rows_mult" 1) (("1" (rewrite "rows_form_matrix") (("1" (expand "G5" 1) (("1" (rewrite -4 1) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "FFZ" -2) (("1" (assert) (("1" (inst -8 "i!1") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (rewrite "rows_mult") (("2" (rewrite "rows_form_matrix") (("2" (typepred "diag(true,false,inverse(S))") (("2" (assert) (("2" (hide-all-but (-4 1)) (("2" (lemma "is_simple_prod_implic") (("2" (inst - "false" "false" "rows(inverse(S))" "diag(TRUE, FALSE, inverse(S))`multip" "true" "false") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (rewrite "rows_form_matrix") (("3" (assert) (("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("1" (expand "G5") (("1" (expand "FG" 1) (("1" (expand "FFZ" 1) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (inst -5 "x!1") (("1" (assert) (("1" (case "x!1/=x!2") (("1" (assert) nil nil) ("2" (flatten) (("2" (assert) (("2" (ground) (("1" (rewrite "entry_eq_0" 1) (("1" (flatten) (("1" (rewrite "rows_mult") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "entry_eq_0" 2) (("2" (flatten) (("2" (rewrite "rows_mult") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil) ("3" (skosimp*) nil nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (case "FORALL (FF: [nat -> real], n: nat,k:nat): k<=n AND (FORALL (i: nat): i < 1 + k IMPLIES FF(i) /= 0) AND (forall (i:nat): i>k AND i<1+n IMPLIES FF(i)=1) IMPLIES is_simple_prod?(1 + n, TRUE, FALSE) (form_matrix(FG(FF), 1 + n, 1 + n))") (("1" (skeep) (("1" (inst - "FF" "n" "n") (("1" (assert) (("1" (replace -1) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "k") (("1" (skeep) (("1" (assert) (("1" (expand "is_simple_prod?") (("1" (expand "is_simple_seq?") (("1" (inst + "LAMBDA (j:nat): Esr(1+n)(0,FF(0))" "0") (("1" (split +) (("1" (skeep) (("1" (inst? 3) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "prod_mat" +) (("2" (expand "FG") (("2" (expand "Esr") (("2" (rewrite "full_matrix_eq") (("2" (split +) (("1" (rewrite "rows_form_matrix") (("1" (rewrite "rows_form_matrix") nil nil)) nil) ("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) (("2" (replaces -1) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "entry_form_matrix") (("3" (rewrite "entry_form_matrix") (("3" (lift-if) (("3" (lift-if) (("3" (assert) (("3" (ground) (("3" (inst - "i!1") (("3" (inst - "i!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (skeep) (("2" (name "FF1" "LAMBDA (i:nat): IF i<1+j THEN FF(i) ELSE 1 ENDIF") (("2" (inst - "FF1" "n") (("2" (assert) (("2" (split -2) (("1" (expand "is_simple_prod?") (("1" (skeep) (("1" (name "FMnew" "LAMBDA (qr:nat): IF qr<=k THEN FM(qr) ELSIF qr = k+1 THEN Esr(1+n)(qr,FF(qr)) ELSE Id(1+n) END (("1" (inst + "FMnew" "k+1") (("1" (assert) (("1" (split 1) (("1" (expand "is_simple_seq?") (("1" (skeep) (("1" (inst - "p") (("1" (assert) (("1" (expand "FMnew" +) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (assert) (("1" (ground) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (inst 4 "p" "FF(p)") (("1" (assert) (("1" (rewrite "full_matrix_eq" 1) (("1" (skosimp*) (("1" (rewrite "entry_Esr" 1) (("1" (rewrite "entry_Id" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "prod_mat" +) (("2" (case "NOT prod_mat(1 + n)(FMnew, k) = prod_mat(1 + n)(FM, k)") (("1" (rewrite "prod_mat_eq") (("1" (skosimp*) (("1" (expand "FMnew" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (replace -3 :dir rl) (("2" (rewrite "full_matrix_eq" 1) (("2" (split 1) (("1" (rewrite "rows_form_matrix") (("1" (rewrite "rows_mult") (("1" (rewrite "rows_form_matrix") nil nil)) nil)) nil) ("2" (rewrite "columns_mult") (("1" (expand "FMnew" 1) (("1" (rewrite "columns_Esr") (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "form_matrix(FG(FF1),1+n,1+n)") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "entry_mult") (("3" (rewrite "entry_form_matrix") (("3" (rewrite "rows_form_matrix") (("3" (assert) (("3" (expand "FMnew" + 1) (("3" (rewrite "columns_Esr") (("3" (assert) (("3" (lift-if) (("3" (split 1) (("1" (flatten) (("1" (expand "*" 1) (("1" (rewrite "dot_eq_sigma") (("1" (case "i!1 /= j!1") (("1" (flatten) (("1" (expand "FG" 2 1) (("1" (assert) (("1" (rewrite "sigma_restrict_eq_0" 2) (("1" (hide 3) (("1" (skosimp*) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (expand "FMnew" 1) (("1" (rewrite "entry_Esr") (("1" (assert) (("1" (rewrite "entry_form_matrix") (("1" (expand "FG" 1) (("1" (expand "FF1") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) (("2" (expand "FG" 1 1) (("2" (rewrite "length_row") (("2" (rewrite "length_col") (("2" (expand "FMnew" 1 1) (("2" (rewrite "rows_Esr") (("2" (assert) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (split -1) (("1" (assert) nil nil) ("2" (replaces -1) (("2" (assert) (("2" (expand "min") (("2" (lemma "sigma_eq_one_arg2") (("2" (inst?) (("2" (inst - "j!1") (("2" (assert) (("2" (split -1) (("1" (replaces -1) (("1" (assert) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (expand "FMnew" 1) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil) (det_nonzero_simple_prod-2 nil 3616753755 ("" (skeep) (("" (lemma "inverse_inverse") (("" (inst?) (("" (assert) (("" (expand "inverse" -1 1) (("" (expand "left_inv") (("" (case "FORALL (i:nat): i<rows(S) IMPLIES entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i)/=0") (("1" (name "FG" "LAMBDA (FF:[nat->real]): (LAMBDA (i,j:nat): IF i/=j THEN 0 ELSE FF(i) ENDIF)") (("1" (case "FORALL (FF:[nat->real],n:nat): (FORALL (i:nat): i<n+1 IMPLIES FF(i)/=0) IMPLIES is_s (("1" (name "FFZ" "LAMBDA (i:nat): IF i>=rows(S) OR entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S))(i,i)=0 THEN 0 ELSE 1/entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S))(i,i) ENDIF") (("1" (name "G5" "FG(FFZ)") (("1" (case "(LAMBDA (i, j): IF i /= j OR entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i) = 0 THEN 0 ELSE 1 / entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i) ENDIF) = G5") (("1" (replace -1) (("1" (replace -7 2 :dir rl) (("1" (rewrite "mult_simple_prod") (("1" (hide 3) (("1" (rewrite "rows_mult" 1) (("1" (rewrite "rows_form_matrix") (("1" (expand "G5" 1) (("1" (rewrite -4 1) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "FFZ" -2) (("1" (assert) (("1" (inst -8 "i!1") (("1" (assert) (("1" (assert) nil))))))))))))))))))))))) ("2" (hide 3) (("2" (rewrite "rows_mult") (("2" (rewrite "rows_form_matrix") (("2" (typepred "diag(true,false,inverse(S))") (("2" (assert) (("2" (hide-all-but (-4 1)) (("2" (lemma "is_simple_prod_implic") (("2" (inst - "false" "false" "rows(inverse(S))" "diag(TRUE, FALSE, inverse(S))`multip" "true" "false") (("2" (assert) nil))))))))))))))))) ("3" (hide 3) (("3" (rewrite "rows_form_matrix") (("3" (assert) (("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) nil))))))))))))))))) ("2" (decompose-equality 1) (("1" (expand "G5") (("1" (expand "FG" 1) (("1" (expand "FFZ" 1) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (inst -5 "x!1") (("1" (assert) (("1" (case "x!1/=x!2") (("1" (assert) nil) ("2" (flatten) (("2" (assert) (("2" (ground) (("1" (rewrite "entry_eq_0" 1) (("1" (flatten) (("1" (rewrite "rows_mult") (("1" (assert) nil))))))) ("2" (rewrite "entry_eq_0" 2) (("2" (flatten) (("2" (rewrite "rows_mult") (("2" (assert) nil))))))))))))))))))))))))))))))))))) ("2" (skosimp*) nil))) ("3" (skosimp*) nil))))) ("2" (skosimp*) nil))) ("2" (hide-all-but 1) (("2" (assert) (("2" (case "FORALL (FF: [nat -> real], n: nat,k:nat): k<=n AND (FORALL (i: nat): i < 1 + k IMPLIES FF(i) /= 0) AND (forall (i:nat): i>k AND i<1+n IMPLIES FF(i)=1) IMPLIES is_simple_prod?(1 + n, TRUE, FALSE) (form_matrix(FG(FF), 1 + n, 1 + n))") (("1" (skeep) (("1" (inst - "FF" "n" "n") (("1" (assert) (("1" (replace -1) (("1" (skosimp*) (("1" (assert) nil))))))))))) ("2" (hide 2) (("2" (induct "k") (("1" (skeep) (("1" (assert) (("1" (expand "is_simple_prod?") (("1" (expand "is_simple_seq?") (("1" (inst + "LAMBDA (j:nat): Esr(1+n)(0,FF(0))" "0") (("1" (split +) (("1" (skeep) (("1" (inst? 3) (("1" (assert) nil))))) ("2" (expand "prod_mat" +) (("2" (expand "FG") (("2" (expand "Esr") (("2" (rewrite "full_matrix_eq") (("2" (split +) (("1" (rewrite "rows_form_matrix") (("1" (rewrite "rows_form_matrix") nil))) ("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) (("2" (replaces -1) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) nil))))))))))))) ("3" (skosimp*) (("3" (rewrite "entry_form_matrix") (("3" (rewrite "entry_form_matrix") (("3" (lift-if) (("3" (lift-if) (("3" (assert) (("3" (ground) (("3" (inst - "i!1") (("3" (inst - "i!1") (("3" (assert) nil))))))))))))))))))))))))))))))))))))))))) ("2" (skeep) (("2" (assert) (("2" (skeep) (("2" (name "FF1" "LAMBDA (i:nat): IF i<1+j THEN FF(i) ELSE 1 ENDIF") (("2" (inst - "FF1" "n") (("2" (assert) (("2" (split -2) (("1" (expand "is_simple_prod?") (("1" (skeep) (("1" (name "FMnew" "LAMBDA (qr:nat): IF qr<=k THEN FM(qr) ELSIF qr = k+1 THEN Ess(1+n)(qr,FF(qr)) ELSE Id(1+n) END (("1" (inst + "FMnew" "k+1") (("1" (assert) (("1" (split 1) (("1" (expand "is_simple_seq?") (("1" (skeep) (("1" (inst - "p") (("1" (assert) (("1" (expand "FMnew" +) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (assert) (("1" (ground) nil))))) ("2" (flatten) (("2" (assert) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (inst 4 "p" "FF(p)") (("1" (assert) (("1" (postpone) nil))))))))) ("2" (postpone) nil))))))))))))))))))))))) ("2" (postpone) nil))))))) ("2" (postpone) nil))))))) ("2" (postpone) nil) ("3" (postpone) nil))))))))))))))) ("3" (postpone) nil))))) ("3" (postpone) nil))))))) ("3" (postpone) nil))))) ("2" (postpone) nil)))))))))))))) nil) nil nil) (det_nonzero_simple_prod-1 nil 3616748905 ("" (skeep) (("" (lemma "inverse_inverse") (("" (inst?) (("" (assert) (("" (expand "inverse" -1 1) (("" (expand "left_inv") (("" (case "FORALL (i:nat): i<rows(S) IMPLIES entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i)/=0") (("1" (name "FG" "LAMBDA (FF:[nat->real]): (LAMBDA (i,j:nat): IF i/=j THEN 0 ELSE FF(i) ENDIF)") (("1" (case "FORALL (FF:[nat->real],n:nat): (FORALL (i:nat): i<n+1 IMPLIES FF(i)/=0) IMPLIES is_s (("1" (name "FFZ" "LAMBDA (i:nat): IF i>=rows(S) OR entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S))(i,i)=0 THEN 0 ELSE 1/entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S))(i,i) ENDIF") (("1" (name "G5" "FG(FFZ)") (("1" (case "(LAMBDA (i, j): IF i /= j OR entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i) = 0 THEN 0 ELSE 1 / entry(diag(TRUE, FALSE, inverse(S))`multip * inverse(S)) (i, i) ENDIF) = G5") (("1" (replace -1) (("1" (replace -7 2 :dir rl) (("1" (rewrite "mult_simple_prod") (("1" (hide 3) (("1" (rewrite "rows_mult" 1) (("1" (rewrite "rows_form_matrix") (("1" (expand "G5" 1) (("1" (rewrite -4 1) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "FFZ" -2) (("1" (assert) (("1" (inst -8 "i!1") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (rewrite "rows_mult") (("2" (rewrite "rows_form_matrix") (("2" (typepred "diag(true,false,inverse(S))") (("2" (assert) (("2" (hide-all-but (-4 1)) (("2" (lemma "is_simple_prod_implic") (("2" (inst - "false" "false" "rows(inverse(S))" "diag(TRUE, FALSE, inverse(S))`multip" "true" "false") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (rewrite "rows_form_matrix") (("3" (assert) (("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("1" (expand "G5") (("1" (expand "FG" 1) (("1" (expand "FFZ" 1) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (inst -5 "x!1") (("1" (assert) (("1" (case "x!1/=x!2") (("1" (assert) nil nil) ("2" (flatten) (("2" (assert) (("2" (ground) (("1" (rewrite "entry_eq_0" 1) (("1" (flatten) (("1" (rewrite "rows_mult") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "entry_eq_0" 2) (("2" (flatten) (("2" (rewrite "rows_mult") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil) ("3" (skosimp*) nil nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (case "FORALL (FF: [nat -> real], n: nat,k:nat): k<=n AND (FORALL (i: nat): i < 1 + k IMPLIES FF(i) /= 0) AND (forall (i:nat): i>k AND i<1+n IMPLIES FF(i)=1) IMPLIES is_simple_prod?(1 + n, TRUE, FALSE) (form_matrix(FG(FF), 1 + n, 1 + n))") (("1" (skeep) (("1" (inst - "FF" "n" "n") (("1" (assert) (("1" (replace -1) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "k") (("1" (skeep) (("1" (assert) (("1" (expand "is_simple_prod?") (("1" (expand "is_simple_seq?") (("1" (inst + "LAMBDA (j:nat): Esr(1+n)(0,FF(0))" "0") (("1" (split +) (("1" (skeep) (("1" (inst? 3) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "prod_mat" +) (("2" (expand "FG") (("2" (expand "Esr") (("2" (rewrite "full_matrix_eq") (("2" (split +) (("1" (rewrite "rows_form_matrix") (("1" (rewrite "rows_form_matrix") nil nil)) nil) ("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) (("2" (replaces -1) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "entry_form_matrix") (("3" (rewrite "entry_form_matrix") (("3" (lift-if) (("3" (lift-if) (("3" (assert) (("3" (ground) (("3" (inst - "i!1") (("3" (inst - "i!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (skeep) (("2" (name "FF1" "LAMBDA (i:nat): IF i<1+j THEN FF(i) ELSE 1 ENDIF") (("2" (inst - "FF1" "n") (("2" (assert) (("2" (split -2) (("1" (expand "is_simple_prod?") (("1" (skeep) (("1" (name "FMnew" "LAMBDA (qr:nat): IF qr<=k THEN FM(qr) ELSIF qr = k+1 THEN Ers(1+n)(qr,FF(qr)) ELSE Id(1+n) END (("1" (inst + "FMnew" "k+1") (("1" (assert) (("1" (split 1) (("1" (expand "is_simple_seq?") (("1" (skeep) (("1" (inst - "p") (("1" (assert) (("1" (expand "FMnew" +) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (assert) (("1" (ground) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (inst 4 "p" "FF(p)") (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (mult_induction_TCC1 0 (mult_induction_TCC1-1 nil 3616766004 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices 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) (rows const-decl "nat" matrices nil) (/= const-decl "boolean" notequal nil)) nil)) (mult_induction_TCC2 0 (mult_induction_TCC2-1 nil 3616766004 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil) (/= const-decl "boolean" notequal nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (Easr const-decl "SquareMatrix(pn)" matrix_det nil)) nil)) (mult_induction_TCC3 0 (mult_induction_TCC3-1 nil 3616766371 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil) (/= const-decl "boolean" notequal nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (Esr const-decl "SquareMatrix(pn)" matrix_det nil) (Easr const-decl "SquareMatrix(pn)" matrix_det nil)) nil)) (mult_induction_TCC4 0 (mult_induction_TCC4-1 nil 3616766561 ("" (skeep) (("" (skeep) (("" (rewrite "rows_mult") (("" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "Q") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((columns_mult formula-decl nil matrices nil) (mult_full application-judgement "FullMatrix" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (SquareMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (rows_mult formula-decl nil matrices nil)) nil)) (mult_induction 0 (mult_induction-1 nil 3616766005 ("" (skeep) (("" (lemma "det_nonzero_simple_prod") (("" (inst?) (("" (assert) (("" (expand "is_simple_prod?") (("" (skeep) (("" (case "EXISTS (z:nat): z<=k AND det(FM(z)) = 0") (("1" (skeep) (("1" (case "FORALL (j:nat): z+j<=k IMPLIES det(prod_mat(rows(S))(FM,z+j)) = 0") (("1" (inst - "k-z") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (induct "j") (("1" (assert) (("1" (expand "prod_mat" +) (("1" (lift-if) (("1" (ground) (("1" (rewrite "det_mult") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "prod_mat" +) (("2" (rewrite "det_mult") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (z:nat): z<=k IMPLIES P(prod_mat(rows(S))(FM,z))") (("1" (inst - "k") (("1" (assert) nil nil)) nil) ("2" (induct "z") (("1" (assert) (("1" (expand "prod_mat" +) (("1" (expand "is_simple_seq?") (("1" (assert) (("1" (inst - "0") (("1" (assert) (("1" (split -) (("1" (skeep) (("1" (inst - "i" "j" "r") (("1" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i" "r") (("2" (assert) (("2" (flatten) (("2" (replace -5) (("2" (inst + "0") (("2" (assert) (("2" (replace -2) (("2" (rewrite "det_Esr") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "prod_mat" +) (("2" (rewrite -8 1) (("2" (expand "is_simple_seq?") (("2" (inst - "1+j") (("2" (assert) (("2" (split -) (("1" (skosimp*) (("1" (inst - "i!1" "j!1" "r!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i" "r") (("2" (assert) (("2" (flatten) (("2" (replace -7) (("2" (replace -2) (("2" (inst + "1+j") (("2" (replace -2) (("2" (assert) (("2" (rewrite "det_Esr") 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) ((det_nonzero_simple_prod formula-decl nil matrix_inv nil) (mult_full application-judgement "FullMatrix" matrices nil) (is_simple_seq? const-decl "bool" matrix_det nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (det_Esr formula-decl nil matrix_det nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (real_times_real_is_real application-judgement "real" reals nil) (det_mult formula-decl nil matrix_diag nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (k skolem-const-decl "nat" matrix_inv nil) (z skolem-const-decl "nat" matrix_inv nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (prod_mat def-decl "SquareMatrix(pn)" matrix_det nil) (SquareMatrix type-eq-decl nil matrices nil) (det def-decl "real" matrix_props nil) (is_simple_prod? const-decl "bool" matrix_det nil) (Square type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (det_transpose 0 (det_transpose-1 nil 3616766723 ("" (skeep) (("" (case "rows(SM)/=columns(SM) OR rows(transpose(SM))/=columns(transpose(SM)) OR rows(t (("1" (case "rows(SM)/=columns(SM)") (("1" (hide -2) (("1" (flatten) (("1" (expand "det" 2) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (rewrite "rows_transpose") (("1" (rewrite "columns_transpose") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "rows_transpose") (("2" (rewrite "columns_transpose") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "rows_transpose") (("2" (rewrite "columns_transpose") (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "det(SM)/=0") (("1" (flatten) (("1" (lemma "mult_induction") (("1" (inst - "SM" "LAMBDA (KV:SquareMatrix(rows(SM))): det(transpose(KV)) = det(KV)") (("1" (assert) (("1" (split) (("1" (skeep) (("1" (rewrite "transpose_Easr") (("1" (rewrite "det_Easr") (("1" (rewrite "det_Easr") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (rewrite "transpose_Esr") nil nil)) nil) ("3" (rewrite "transpose_Id") nil nil) ("4" (skeep) (("4" (rewrite "transpose_mult") (("4" (rewrite "det_mult") (("1" (rewrite "det_mult") (("1" (assert) nil nil)) nil) ("2" (rewrite "rows_transpose") (("2" (rewrite "rows_transpose") (("2" (assert) nil nil)) nil)) nil) ("3" (rewrite "rows_transpose") (("3" (rewrite "columns_transpose") (("3" (assert) nil nil)) nil)) nil) ("4" (rewrite "rows_transpose") (("4" (rewrite "columns_transpose") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "mult_inverse_right") (("2" (inst - "transpose(SM)") (("2" (split -1) (("1" (case "NOT det(transpose(transpose(SM) * inverse(transpose(SM)))) = det(transpose(Id(r (("1" (assert) nil nil) ("2" (rewrite "transpose_mult") (("2" (rewrite "transpose_transpose") (("2" (rewrite "transpose_Id") (("2" (rewrite "det_Id") (("2" (rewrite "det_mult") (("1" (assert) nil nil) ("2" (rewrite "rows_transpose") (("2" (assert) nil nil)) nil) ("3" (rewrite "rows_transpose") (("3" (rewrite "columns_transpose") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "rows_mult") (("3" (assert) nil nil)) nil)) nil) ("2" (lemma "invertible_rew") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((transpose const-decl "PosFullMatrix" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (rows const-decl "nat" matrices 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 nonempty-type-from-decl nil reals nil) (Matrix type-eq-decl nil matrices 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) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (/= const-decl "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (det def-decl "real" matrix_props nil) (rows_transpose formula-decl nil matrices nil) (columns_transpose formula-decl nil matrices nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (mult_induction formula-decl nil matrix_inv nil) (det_mult formula-decl nil matrix_diag nil) (mult_full application-judgement "FullMatrix" matrices nil) (transpose_mult formula-decl nil matrices nil) (transpose_Id formula-decl nil matrices nil) (transpose_Esr formula-decl nil matrix_det nil) (det_Easr formula-decl nil matrix_det nil) (transpose_Easr formula-decl nil matrix_det nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (SquareMatrix type-eq-decl nil matrices nil) (Square type-eq-decl nil matrices nil) (SM skolem-const-decl "PosFullMatrix" matrix_inv nil) (mult_inverse_right formula-decl nil matrix_inv nil) (rows_mult formula-decl nil matrices nil) (det_Id formula-decl nil matrix_props nil) (transpose_transpose formula-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (MatrixMN type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (invertible? const-decl "bool" matrix_inv nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (inverse const-decl "{IQ | rows(IQ) = rows(SQ) AND IQ * SQ = Id(rows(SQ)) AND SQ * IQ = Id(rows(SQ))}" matrix_inv nil) (invertible_rew formula-decl nil matrix_inv nil)) shostak)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.430Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26