Quelle matrix_det.prf
Sprache: Lisp
(matrix_detnil 3615028556"" (skeep)"" (assert )"" (split)"1" (rewrite "rows_form_matrix" ) nil nil )"2" (lemma "columns_form_matrix" )"2" (assert )"2" (inst?)"2" (assert )"2" (rewrite "rows_form_matrix" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (rewrite "rows_form_matrix" ) (("3" (assert ) nil nil ))nil )"4" (lemma "columns_form_matrix" )"4" (inst?) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"FullMatrix" matricesnil )"(strict_total_order?[real])" real_props nil )nil matrices nil )nil matrices nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"boolean" notequal nil ))nil ))nil 3615030016"" (skeep)"" (expand "Esr" )"" (rewrite "entry_form_matrix" )"" (lift-if)"" (lift-if)"" (lift-if)"" (lift-if)"" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"SquareMatrix(pn)" matrix_det nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"bool" reals nil )nil integers nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrices nil ))nil 3615028664"" (skeep)"" (expand "Esr" ) (("" (rewrite "rows_form_matrix" ) nil nil ))nil ))nil )"SquareMatrix(pn)" matrix_det nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrices nil ))nil 3615028700"" (skeep)"" (expand "Esr" )"" (lemma "columns_form_matrix" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"SquareMatrix(pn)" matrix_det nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"boolean" notequal nil )"FullMatrix" matricesnil )nil matrices nil ))nil 3615047615"" (skeep)"" (lemma "det_replace_row_scal" )"" (inst - "Id(pn)" "i" "r" "row(Id(pn))(i)" )"" (assert )"" (split -)"1" (rewrite "replace_row_id" )"1" (rewrite "det_Id" )"1" (assert )"1" case "replace_row(i, r * row(Id(pn))(i))(Id(pn)) = Esr(pn)(i,r)" )"1" (assert ) nil nil )"2" (hide (-1 2))"2" (rewrite "full_matrix_eq" )"2" (skosimp*)"2" (rewrite "entry_replace_row" )"1" (rewrite "entry_Esr" )"1" rewrite "entry_Id" )"1" rewrite "access_scal" )"1" "entry_Id" )"1" "i" "j!1" "pn" )"1" expand "entry" -1)"1" assert )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "columns_Id" )"2" "r*row(Id(pn))(i)" )"2" "2" rewrite "length_row" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_row" ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )nil matrix_props nil )"real" reals nil )nil matrices nil )nil matrix_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_det nil )"(total_order?[real])" nil )nil matrices nil )nil matrices nil )nil matrix_props nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )"VectorN(length(v2))" matrices nil )"{PFM | AND AND IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)AND IF j < rows(D) AND j = i THEN access(v)(k)" matrix_props nil) "real" matrices nil )nil matrix_props nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"Vector" matrices nil )"real" matrices nil )nil matrices nil )nil matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )nil matrices nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[list -> boolean]" list_adt nil )nil reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil list_adt nil )nil numbers nil ))nil 3615817279"" (skeep)"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_transpose" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "columns_transpose" +) (("2" (assert ) nil nil ))nil )"3" (skosimp*)"3" (rewrite "entry_transpose" )"3" (rewrite "entry_Esr" )"3" (rewrite "entry_Esr" )"3" (lift-if)"3" (lift-if)"3" (lift-if)"3" (lift-if) (("3" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"PosFullMatrix" matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )nil matrix_det nil )"(total_order?[real])" nil )nil matrices nil )nil matrices nil )nil matrices nil ))nil 3615028556"" (skeep)"" (typepred "r*row(D)(i)" )"" (replace -2)"" (rewrite "length_row" 1)"" (assert )"" (lift-if)"" (ground) (("" (postpone) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"Vector" matrices nil )nil matrices nil )"VectorN(length(v2))" matrices nil )nil matrices nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities nil )nil matrices nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil list_adt nil )nil defined_types nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil matrix_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3615028557"" (skeep)"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_mult" )"1" (rewrite "rows_Esr" )"1" (rewrite "rows_replace_row" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "columns_mult" )"2" (inst?)"2" (assert ) (("2" (hide 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*)"3" (rewrite "entry_mult" )"3" (assert )"3" (expand "*" + 1)"3" (lift-if)"3" (ground)"1" (lemma "rows_Esr" )"1" (inst?)"1" (rewrite "entry_replace_row" )"1" (lift-if)"1" (ground)"1" rewrite "dot_eq_sigma" )"1" rewrite "length_row" )"1" rewrite "length_col" )"1" rewrite "columns_Esr" )"1" expand "min" )"1" "sigma_eq_one_arg" )"1" "1" "i!1" )"1" assert )"1" "1" "1" rewrite "access_scal" )"1" "entry_Esr" )"1" "1" "i!1" "i!1" )"1" assert )"1" expand "entry" "1" "1" rewrite "access_col" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "entry_Esr" )"2" "i" "i!2" "i!1" "pn" "r" )"2" assert )"2" expand "entry" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "entry_Esr" )"3" "i" "i!2" "i!1" "pn" "r" )"3" assert )"3" expand "entry" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "dot_eq_sigma" )"2" rewrite "length_row" )"2" rewrite "length_col" )"2" rewrite "columns_Esr" )"2" replace -4)"2" assert )"2" expand "min" )"2" "sigma_eq_one_arg" )"2" "2" "i!1" )"2" assert )"2" "1" "1" "entry_Esr" )"1" "1" "i!1" "i!1" )"1" assert )"1" expand "entry" "1" "1" rewrite "access_col" )"1" expand "entry" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "entry_Esr" )"2" "i" "i!2" "i!1" "pn" "r" )"2" assert )"2" expand "entry" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "entry_Esr" )"3" "i" "i!2" "i!1" "pn" "r" )"3" assert )"3" expand "entry" )"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" (hide 2)"2" (typepred "r*row(D)(i)" )"2" "2" (rewrite "length_row" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "rows_Esr" )"2" (rewrite "entry_replace_row" )"1" (expand "entry" )"1" (expand "row" )"1" (lift-if)"1" "1" expand "rows" )"1" assert )"1" expand "access" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" expand "rows" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "r*row(D)(i)" )"2" (replace -2)"2" (rewrite "length_row" ) nil nil ))nil ))nil ))nil ))nil )"3" (typepred "j!1" )"3" (lemma "columns_mult" )"3" (inst?)"3" (assert )"3" (typepred "Esr(pn)(i,r)" )"3" expand "rows" )"3" expand "length" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"FullMatrix" matrices nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"real" matrices nil )nil matrices nil )"real" matrices nil )"Vector" matrices nil )nil matrices nil )"VectorN(rows(M))" matrices nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )nil integers nil )"bool" reals nil )nil integers nil )nil matrices nil )nil matrices nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"{PFM | AND AND IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)AND IF j < rows(D) AND j = i THEN access(v)(k)" matrix_props nil) "VectorN(length(v2))" matrices nil )"(strict_total_order?[real])" real_props nil )nil matrix_props nil )nil matrix_props nil )"(total_order?[real])" nil )nil matrix_det nil )nil sigma "reals/" )nil matrices nil )nil matrix_props nil )nil matrix_det nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil matrices nil )"{k: int | k <= i AND k <= j}" nil )"real" reals nil )"(total_order?[real])" nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrices nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" "structures/" )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"{M: MatrixMN(m, n) | " nil )"posint" nil )"int" integers nil )"FullMatrix" matricesnil )nil matrices nil )nil matrix_props nil )nil matrix_det nil ))nil 3615053212"" (skeep)"" (rewrite "mult_Esr_left" )"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_replace_row" )"1" (rewrite "rows_Esr" )"1" (rewrite "rows_Id" ) nil nil )) nil ))nil )"2" (rewrite "columns_replace_row" )"2" (rewrite "columns_Esr" )"2" (rewrite "columns_Id" ) nil nil )) nil ))nil )"3" (skosimp*)"3" (rewrite "entry_replace_row" )"1" (rewrite "entry_Id" )"1" (rewrite "access_scal" )"1" (lemma "entry_Esr" )"1" (inst - "i" "j!1" "i" "pn" "1/r" )"1" (assert )"1" (expand "entry" -1)"1" (replaces -1)"1" (rewrite "entry_Esr" )"1" "1" "1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "columns_Esr" )"2" (typepred "r * row(Esr(pn)(i, 1 / r))(i)" )"2" (replace -2)"2" (rewrite "length_row" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" nil )nil matrix_det nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil matrix_det nil )nil matrices nil )nil matrix_props nil )nil matrix_det nil )nil matrices nil )nil matrix_props nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"real" reals nil )"real" matrix_det nil )nil matrix_det nil )"(total_order?[real])" nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_props nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )"real" matrices nil )nil matrices nil )"VectorN(length(v2))" matrices nil )nil matrices nil )"{PFM | AND AND IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)AND IF j < rows(D) AND j = i THEN access(v)(k)" matrix_props nil) "real" matrices nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"Vector" matrices nil )nil matrices nil )nil matrices nil ))nil 3615034417"" (skeep)"" "FM" "form_matrix(LAMBDA (k, p: nat): IF k = i AND p = j THEN 1AND p = i THEN 1AND k /= j AND k = p THEN 1") "" (replace -1)"" (split)"1" (rewrite "full_matrix_eq" )"1" (split)"1" (expand "FM" 1)"1" (rewrite "rows_form_matrix" )"1" (assert ) nil nil )) nil ))nil )"2" (expand "FM" 1)"2" (lemma "columns_form_matrix" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (skosimp*)"3" (expand "FM" 1)"3" (rewrite "entry_form_matrix" )"3" (rewrite "entry_swap" )"3" (expand "swap" )"3" (lift-if)"3" (lift-if)"3" (lift-if)"3" "3" "3" "3" assert )"3" expand "Id" +)"3" rewrite -1)"3" rewrite "entry_form_matrix" )"3" rewrite "entry_form_matrix" )"3" rewrite "entry_form_matrix" )"3" assert )"3" rewrite "rows_form_matrix" )"3" "columns_form_matrix" )"3" "3" assert )"3" "3" "3" "3" "3" "3" "3" "3" assert )"3" 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" (expand "FM" )"2" (rewrite "rows_form_matrix" ) nil nil )) nil )"3" (assert )"3" (expand "FM" )"3" (rewrite "rows_form_matrix" )"3" (lemma "columns_form_matrix" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"4" (expand "FM" 1)"4" (rewrite "rows_form_matrix" ) (("4" (assert ) nil nil ))nil ))nil )"5" (expand "FM" 1)"5" (lemma "columns_form_matrix" )"5" (inst?) (("5" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{M: MatrixMN(m, n) | " nil )"Vector" matrices nil )nil matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil list_adt nil )nil numbers nil )"FullMatrix" matricesnil )nil matrices nil )"{M: MatrixMN(pn, pn) | IF i_1 = i AND j_1 = j THEN 1AND j_1 = i THEN 1AND i_1 /= j AND i_1 = j_1 THEN 1" matrix_det nil) nil matrices nil )nil matrix_props nil )"real" matrix_props nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"real" matrices nil )nil matrices nil )nil matrices nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) "real" matrices nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3615034417"" (skeep)"" (expand "Ers" )"" (rewrite "entry_form_matrix" )"" (lift-if)"" (lift-if)"" (lift-if)"" (lift-if)"" (lift-if)"" (assert ) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"bool" reals nil )nil integers nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrices nil ))nil 3615034488"" (skeep)"" (expand "Ers" ) (("" (rewrite "rows_form_matrix" ) nil nil ))nil ))nil )"{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}" nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrices nil ))nil 3615034519"" (skeep)"" (lemma "columns_form_matrix" )"" (expand "Ers" ) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil matrices nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"FullMatrix" matricesnil )"{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}" nil ))nil 3615034641"" (skeep)"" (rewrite "full_matrix_eq" )"" (split)"1" (assert )"1" (rewrite "rows_mult" )"1" (rewrite "rows_Ers" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "columns_mult" )"2" (inst?) (("2" (assert ) (("2" (grind) nil nil )) nil ))nil ))nil )"3" (skosimp*)"3" (rewrite "entry_mult" )"3" (lift-if)"3" (ground)"1" (rewrite "entry_swap" )"1" (expand "swap" )"1" (lift-if)"1" (ground)"1" (expand "*" )"1" (rewrite "dot_eq_sigma" )"1" (rewrite "length_row" )"1" rewrite "length_col" )"1" rewrite "columns_Ers" )"1" replace -4)"1" expand "min" )"1" "sigma_eq_one_arg" )"1" "1" "j" )"1" assert )"1" "1" replace -1)"1" rewrite "access_col" )"1" expand "entry" "1" replace -2)"1" "entry_Ers" )"1" "i" "j" "i" "j" "pn" )"1" expand "entry" "1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "entry_Ers" )"2" "i" "j" "i!1" "i!2" "pn" )"2" expand "entry" "2" assert )"2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "entry_Ers" )"3" "i" "j" "i!1" "i!2" "pn" )"3" expand "entry" "3" replace "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "*" )"2" (rewrite "dot_eq_sigma" )"2" (rewrite "length_row" )"2" rewrite "length_col" )"2" rewrite "columns_Ers" )"2" replace -4)"2" expand "min" )"2" "sigma_eq_one_arg" )"2" "2" "i" )"2" assert )"2" "1" "1" "entry_Ers" )"1" "i" "j" "i!1" "i" "pn" )"1" assert )"1" expand "entry" "1" assert )"1" replace "1" expand "entry" "1" rewrite "access_col" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "entry_Ers" )"2" "i" "j" "i!1" "i!2" "pn" )"2" assert )"2" expand "entry" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "entry_Ers" )"3" "i" "j" "i!1" "i!2" "pn" )"3" assert )"3" expand "entry" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "*" )"3" (rewrite "dot_eq_sigma" )"3" (rewrite "length_row" )"3" rewrite "length_col" )"3" rewrite "columns_Ers" )"3" expand "min" )"3" assert )"3" "sigma_eq_one_arg" )"3" "3" "i!1" )"3" assert )"3" "1" "1" "entry_Ers" )"1" "i" "j" "i!1" "i!1" "pn" )"1" assert )"1" expand "entry" "1" "1" rewrite "access_col" )"1" expand "entry" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "entry_Ers" )"2" "i" "j" "i!1" "i!2" "pn" )"2" assert )"2" expand "entry" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "entry_Ers" )"3" "i" "j" "i!1" "i!2" "pn" )"3" assert )"3" expand "entry" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "i!1" )"2" (rewrite "rows_mult" ) nil nil )) nil )"3" (typepred "j!1" )"3" (lemma "columns_mult" )"3" (inst?)"3" (assert )"3" (typepred "Ers(pn)(i,j)" )"3" (expand "rows" )"3" (expand "length" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"FullMatrix" matrices nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"real" matrices nil )nil matrices nil )"real" matrices nil )"Vector" matrices nil )nil matrices nil )"VectorN(rows(M))" matrices nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )nil integers nil )"bool" reals nil )nil integers nil )nil matrices nil )nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) "{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_props nil )nil matrix_props nil )"(total_order?[real])" nil )nil matrix_det nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"real" matrices nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil matrix_det nil )nil matrix_props nil )nil sigma "reals/" )nil matrices nil )"{k: int | k <= i AND k <= j}" nil )"real" reals nil )"(total_order?[real])" nil )nil matrices nil )"real" matrix_props nil )nil matrices nil )nil matrices nil )"FullMatrix" matricesnil )"int" integers nil )"posint" nil )"{M: MatrixMN(m, n) | " nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" "structures/" )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )nil matrix_det nil )nil matrices nil ))nil 3615817501"" (skeep)"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_transpose" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "columns_transpose" ) (("2" (assert ) nil nil ))nil )"3" (skosimp*)"3" (rewrite "entry_transpose" )"3" (rewrite "entry_Ers" )"3" (rewrite "entry_Ers" )"3" (lift-if)"3" (lift-if)"3" (lift-if)"3" (lift-if)"3" (assert )"3" (lift-if)"3" (assert ) (("3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"PosFullMatrix" matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) nil matrices nil )nil matrices nil )"real" matrices nil )"Vector" matrices nil )nil matrices nil )"VectorN(rows(M))" matrices nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}" nil )nil matrix_det nil )"(total_order?[real])" nil )nil matrices nil )nil matrices nil )nil matrices nil ))nil ))nil 3615049919"" (skeep)"" (lift-if)"" (ground)"1" (replaces -1)"1" (assert )"1" (typepred "Ers(pn)(j,j)" )"1" (replaces -7)"1" (rewrite "swap_id" )"1" (rewrite "det_Id" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (typepred "Ers(pn)(i,j)" )"2" (replaces -7)"2" (rewrite "det_swap" )"2" (rewrite "det_Id" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil matrix_props nil )"real" reals nil )"{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}" nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"Vector" matrices nil )"real" matrices nil )nil matrices nil )nil matrices nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil matrix_props nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil ))nil 3615053454"" (skeep)"" (rewrite "mult_Ers_left" )"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_swap" )"1" (rewrite "rows_Ers" )"1" (rewrite "rows_Id" ) nil nil )) nil ))nil )"2" (rewrite "columns_swap" )"2" (rewrite "columns_Ers" )"2" (rewrite "columns_Id" ) nil nil )) nil ))nil )"3" (skosimp*)"3" (rewrite "entry_swap" )"3" (rewrite "entry_Id" )"3" (expand "swap" )"3" (rewrite "entry_Ers" )"3" (rewrite "entry_Ers" )"3" (rewrite "entry_Ers" )"3" (lift-if)"3" (lift-if)"3" (lift-if) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrix_det nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) nil matrices nil )nil matrices nil )"real" matrices nil )"Vector" matrices nil )nil matrices nil )"VectorN(rows(M))" matrices nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}" nil )nil matrix_det nil )nil matrices nil )nil matrix_props nil )nil matrix_det nil )nil matrices nil )nil matrix_props nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )"real" matrix_props nil )nil matrix_det nil )"(total_order?[real])" nil )nil matrices nil )nil matrices nil ))nil 3615041385"" (skeep)"" "FM" "form_matrix(LAMBDA (k, p: nat): IF k = iIF j = i AND p = i") "" (replace -1)"" (split +)"1" (expand "FM" 1)"1" (rewrite "rows_form_matrix" ) nil nil )) nil )"2" (assert )"2" (expand "FM" 1)"2" (rewrite "rows_form_matrix" )"2" (lemma "columns_form_matrix" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"3" (expand "FM" 1)"3" (rewrite "rows_form_matrix" ) (("3" (assert ) nil nil ))nil ))nil )"4" (lemma "columns_form_matrix" )"4" (expand "FM" 1)"4" (inst?) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"{M: MatrixMN(m, n) | " nil )"Vector" matrices nil )nil matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil list_adt nil )nil numbers nil )"FullMatrix" matricesnil )"real" reals nil )nil matrices nil )"{M: MatrixMN(pn, pn) | IF i_1 = iIF j = i AND j_1 = i THEN 1 + r" matrix_det nil) nil matrices nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3615041737"" (skeep)"" (expand "Easr" )"" (rewrite "entry_form_matrix" )"" (lift-if)"" (assert )"" (lift-if)"" (assert )"" (lift-if)"" (assert ) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"SquareMatrix(pn)" matrix_det nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrices nil )"real" reals nil ))nil 3615046841"" (skeep)"" (expand "Easr" ) (("" (rewrite "rows_form_matrix" ) nil nil ))nil ))nil )"SquareMatrix(pn)" matrix_det nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrices nil )"real" reals nil ))nil 3615043220"" (skeep)"" (expand "Easr" )"" (lemma "columns_form_matrix" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"SquareMatrix(pn)" matrix_det nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"FullMatrix" matricesnil )nil matrices nil ))nil 3615043439"" (skeep)"" (typepred "row(D)(i)+r*row(D)(j)" )"" (replaces -2)"" (expand "max" )"" (lift-if)"" (ground)"1" (typepred "r*row(D)(j)" )"1" (rewrite "length_row" ) (("1" (assert ) nil nil ))nil ))nil )"2" (rewrite "length_row" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"VectorN(length(v2))" matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"Vector" matrices nil )nil matrices nil )"VectorN(max(length(v1), length(v2)))" matrices nil )nil matrices nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities nil )nil reals nil )nil matrices nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil list_adt nil )nil defined_types nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )nil matrix_props nil )"(total_order?[real])" nil ))nil ))nil 3615043440"" (skeep)"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_mult" )"1" (rewrite "rows_Easr" )"1" (rewrite "rows_replace_row" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "columns_mult" )"2" (inst?)"2" (assert )"2" (lemma "rows_Easr" )"2" (inst?)"2" (assert )"2" (expand "rows" )"2" (expand "length" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (rewrite "entry_mult" )"3" (rewrite "rows_Easr" )"3" (rewrite "entry_replace_row" )"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (assert )"1" (ground)"1" (expand "*" + 1)"1" (rewrite "dot_eq_sigma" )"1" rewrite "length_row" )"1" rewrite "columns_Easr" )"1" rewrite "length_col" )"1" expand "min" )"1" case "i = j" )"1" "sigma_eq_one_arg2" )"1" "1" "i" )"1" assert )"1" "1" "1" "entry_Easr" )"1" "1" "i!1" "i" )"1" replace "1" assert )"1" expand "entry" "1" "1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "access_col" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "entry_Easr" )"2" "2" "i!1" "i!2" )"2" assert )"2" expand "entry" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_eq_two_args" )"2" "2" "i" "j" )"2" assert )"2" "1" "1" "entry_Easr" )"1" replace -2)"1" "1" "i" "i" )"1" assert )"1" "i" "j" )"1" assert )"1" expand "entry" )"1" "1" "1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" assert )"1" rewrite "access_col" )"1" rewrite "access_col" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "entry_Easr" )"2" "2" "i!1" "i!2" )"2" assert )"2" expand "entry" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "*" )"2" (rewrite "dot_eq_sigma" )"2" rewrite "length_row" )"2" rewrite "columns_Easr" )"2" rewrite "length_col" )"2" expand "min" )"2" assert )"2" "sigma_eq_one_arg2" )"2" "2" assert )"2" "i!1" )"2" assert )"2" "1" "1" "entry_Easr" )"1" "1" "i!1" "i!1" )"1" assert )"1" expand "entry" )"1" "1" rewrite "access_col" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "entry_Easr" )"2" "2" "i!1" "i!2" )"2" assert )"2" expand "entry" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (rewrite "entry_eq_0" ) nil nil )"4" (rewrite "entry_eq_0" ) nil nil )"5" (expand "access" )"5" (lift-if)"5" "5" "row(D)(i)+r*row(D)(j)" )"5" "5" expand "max" )"5" assert )"5" "5" "1" "r*row(D)(j)" )"1" rewrite "length_row" )"1" assert )nil nil ))nil ))nil )"2" rewrite "length_row" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (rewrite "entry_eq_0" ) nil nil )"7" (rewrite "entry_eq_0" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "row(D)(i)+r*row(D)(j)" )"2" (replace -2)"2" (expand "max" )"2" (lift-if)"2" (ground)"1" (typepred "r*row(D)(j)" )"1" rewrite "length_row" )"1" (assert ) nil nil ))nil ))nil )"2" (rewrite "length_row" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"FullMatrix" matrices nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"real" matrices nil )nil matrices nil )"real" matrices nil )"Vector" matrices nil )nil matrices nil )"VectorN(rows(M))" matrices nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )nil integers nil )"bool" reals nil )nil integers nil )nil matrices nil )nil matrices nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"{PFM | AND AND IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)AND IF j < rows(D) AND j = i THEN access(v)(k)" matrix_props nil) max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"VectorN(max(length(v1), length(v2)))" matrices nil )"VectorN(length(v2))" matrices nil )nil matrices nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )nil matrix_det nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil sigma "reals/" )nil sigma "reals/" )nil matrix_det nil )"real" reals nil )nil matrices nil )nil matrix_props nil )nil matrices nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil matrices nil )"(total_order?[real])" nil )nil matrix_props nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_props nil )nil matrices nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )nil matrix_props nil )nil matrix_det nil ))nil 3615817605"" (skeep)"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_transpose" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "columns_transpose" ) (("2" (assert ) nil nil ))nil )"3" (skosimp*)"3" (rewrite "entry_transpose" )"3" (rewrite "entry_Easr" )"3" (rewrite "entry_Easr" )"3" (lift-if)"3" (assert )"3" (lift-if)"3" (assert )"3" (lift-if)"3" (assert )"3" (lift-if)"3" assert )"3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"PosFullMatrix" matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )nil matrix_det nil )"(total_order?[real])" nil )nil matrices nil )nil matrices nil )nil matrices nil ))nil 3615050470"" (skeep)"" (lift-if)"" (ground)"1" (case "Easr(pn)(i,j,r)=Esr(pn)(i,1+r)" )"1" (replaces -1) (("1" (rewrite "det_Esr" ) nil nil )) nil )"2" (hide 2)"2" (rewrite "full_matrix_eq" )"2" (split)"1" (rewrite "rows_Easr" )"1" (rewrite "rows_Esr" ) nil nil )) nil )"2" (rewrite "columns_Easr" )"2" (rewrite "columns_Esr" ) nil nil )) nil )"3" (skosimp*)"3" (rewrite "entry_Easr" )"3" (rewrite "entry_Esr" )"3" (lift-if)"3" (lift-if)"3" (lift-if)"3" (lift-if)"3" "3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "det_replace_row_sum_scal" )"2" (inst - "Id(pn)" "i" "j" "r" )"2" (assert )"2" (rewrite "rows_Id" )"2" (assert )"2" (rewrite "det_Id" )"2" case "Easr(pn)(i,j,r)=replace_row(i, row(Id(pn))(i) + r * row(Id(pn))(j))(Id(pn))" )"1" (assert ) nil nil )"2" (hide (-1 3))"2" (rewrite "full_matrix_eq" )"2" (split)"1" (rewrite "rows_Easr" )"1" rewrite "rows_replace_row" )"1" (rewrite "rows_Id" ) nil nil ))nil ))nil )"2" (rewrite "columns_Easr" )"2" rewrite "columns_replace_row" )"2" (rewrite "columns_Id" ) nil nil ))nil ))nil )"3" (skosimp*)"3" rewrite "entry_Easr" )"3" rewrite "entry_replace_row" )"1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "entry_Id" )"1" assert )"1" "entry_Id" )"1" "i" "j!1" "pn" )"1" "j" "j!1" "pn" )"1" assert )"1" expand "entry" )"1" "1" "1" assert )"1" "1" "1" "1" "1" "1" "1" "1" "1" "1" "1" "1" "1" 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" "2" rewrite "columns_Id" )"2" "row(Id(pn))(i) + r * row(Id(pn))(j)" )"2" "2" rewrite "length_row" )"2" "r*row(Id(pn))(j)" )"2" "2" rewrite "length_row" )"2" expand "max" )"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 matrix_props nil )"VectorN(length(v2))" matrices nil )"VectorN(max(length(v1), length(v2)))" matrices nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{PFM | AND AND IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)AND IF j < rows(D) AND j = i THEN access(v)(k)" matrix_props nil) "real" matrices nil )nil matrix_props nil )nil matrices nil )"real" reals nil )nil matrices nil )nil matrices nil )nil matrix_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrices nil )nil matrix_props nil )nil matrix_props nil )nil matrix_props nil )nil matrices nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"Vector" matrices nil )"real" matrices nil )nil matrices nil )nil matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"SquareMatrix(pn)" matrix_det nil )"SquareMatrix(pn)" matrix_det nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil list_adt nil )nil numbers nil )nil matrix_det nil )nil matrices nil )nil matrix_det nil )"(total_order?[real])" nil )nil matrix_det nil )nil matrix_det nil )nil matrix_det nil )nil matrix_det nil )nil matrix_det nil )"real" reals nil )"(strict_total_order?[real])" real_props nil ))nil 3615053746"" (skeep)"" (rewrite "mult_Easr_left" )"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_replace_row" )"1" (rewrite "rows_Easr" )"1" (rewrite "rows_Id" ) nil nil )) nil ))nil )"2" (rewrite "columns_replace_row" )"2" (rewrite "columns_Easr" )"2" (rewrite "columns_Id" ) nil nil )) nil ))nil )"3" (skosimp*)"3" (rewrite "entry_replace_row" )"1" (rewrite "entry_Id" )"1" (rewrite "entry_Easr" )"1" (lemma "entry_Easr" )"1" (rewrite "access_sum" )"1" (rewrite "access_scal" )"1" (inst-cp - "i" "j" "i" "j!1" "pn" "-r" )"1" (inst-cp - "i" "j" "j" "j!1" "pn" "-r" )"1" (hide -1)"1" expand "entry" -)"1" assert )"1" "1" "1" "1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "columns_Easr" )"2" (invoke (typepred "%1" ) (! 1 2 1))"2" (replaces -2)"2" (rewrite "length_row" )"2" (invoke (typepred "%1" ) (! 1 2 2 1))"2" (replace -2)"2" (rewrite "length_row" +)"2" (expand "max" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil matrix_det nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil matrix_det nil )nil matrices nil )nil matrix_props nil )nil matrix_det nil )nil matrices nil )nil matrix_props nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )nil matrix_det nil )nil matrices nil )"real" reals nil )"real" reals nil )nil matrices nil )"(total_order?[real])" nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_props nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )"real" matrices nil )nil matrices nil )"VectorN(length(v2))" matrices nil )"VectorN(max(length(v1), length(v2)))" matrices nil )nil matrices nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{PFM | AND AND IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)AND IF j < rows(D) AND j = i THEN access(v)(k)" matrix_props nil) "real" matrices nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"Vector" matrices nil )nil matrices nil )nil matrices nil ))nil 3615110328"" (skeep)"" (name "FM" "form_matrix(LAMbDA (i,j): 0,pn,pn)" )"" (replaces -1)"" (split +)"1" (expand "FM" )"1" (rewrite "rows_form_matrix" ) nil nil )) nil )"2" (assert )"2" (expand "FM" )"2" (rewrite "rows_form_matrix" )"2" (lemma "columns_form_matrix" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"3" (expand "FM" )"3" (rewrite "rows_form_matrix" ) (("3" (assert ) nil nil ))nil ))nil )"4" (expand "FM" )"4" (lemma "columns_form_matrix" )"4" (inst?) (("4" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"bool" reals nil )nil integers nil )"{M: MatrixMN(m, n) | " nil )"Vector" matrices nil )nil matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil list_adt nil )nil numbers nil )"FullMatrix" matricesnil )nil matrices nil )"{M: MatrixMN(pn, pn) | " nil )nil matrices nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3615635548 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil ))nil ))nil 3615635548 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil ))nil ))nil 3615636043 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"int" integers nil ))nil ))nil 3615638149"" (skeep)"" (rewrite "rows_remove" ) (("" (assert ) nil nil )) nil )) nil )nil matrix_props nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3615636723"" case " FORALL (S: Square, k: nat): AND rows(S)-k-2>=0 IMPLIES") "1" (skeep)"1" (inst - "S" "rows(S)-k-2" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (skeep)"1" (assert )"1" (expand "prod_diag" )"1" (rewrite "rows_remove" )"1" (assert ) (("1" (rewrite "entry_remove" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (assert )"2" (skeep)"2" (assert )"2" (expand "prod_diag" +)"2" (assert )"2" (lift-if)"2" (rewrite "rows_remove" )"2" (assert )"2" (inst - "S" )"2" (assert )"2" "2" rewrite "entry_remove" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )"4" (skosimp*)"4" (rewrite "rows_remove" ) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (hide 2)"4" (skeep)"4" (rewrite "rows_remove" ) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" nil )nil matrix_props nil )nil matrix_props nil )"odd_int" integers nil )nil naturalnumbers nil )nil defined_types nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nat" matrix_det nil )"Square" matrix_det nil )"(total_order?[real])" nil )"posint" nil )"int" integers nil )"FullMatrix" nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrix_det nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil ))nil 3615903333"" (skeep)"" (expand "upper_triangular?" )"" (expand "diagonal?" )"" (skeep)"" (inst - "i" "j" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" matrix_det nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" matrix_det nil ))nil 3615635548"" case "FORALL (S: Square,k:nat):rows(S)=k+1 AND ") "1" (skeep)"1" (inst - "S" "rows(S)-1" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (assert )"1" (skeep)"1" (expand "det" )"1" (assert )"1" (lift-if)"1" (ground)"1" (expand "rows" )"1" (expand "length" ) (("1" (assert ) nil nil ))nil ))nil )"2" (expand "prod_diag" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (assert )"2" (expand "det" + 1)"2" (lift-if)"2" (ground)"1" (expand "rows" )"1" (expand "length" ) (("1" (assert ) nil nil ))nil ))nil )"2" (lemma "sigma_eq_one_arg2" )"2" (inst?)"2" (inst - "0" )"2" (assert )"2" (split -)"1" "1" "remove(S,0,0)" )"1" assert )"1" "1" "1" expand "^" )"1" expand "expt" )"1" expand "prod_diag" + 2)"1" rewrite "prod_diag_remove_0_0" )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "rows_remove" )"2" (assert ) nil nil ))nil )"3" "3" expand "upper_triangular?" )"3" "3" rewrite "rows_remove" )"3" rewrite "entry_remove" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "rows_remove" )"2" rewrite "columns_remove" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "det_first_column_zero" )"2" "1" assert )"1" "1" rewrite "rows_remove" )"1" rewrite "entry_remove" )"1" expand "upper_triangular?" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "rows_remove" )"2" rewrite "columns_remove" )"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 )"posint" nil )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"FullMatrix" nil )"Square" matrix_det nil )nil matrix_det nil )"odd_int" integers nil )"real" exponentiation nil )nil matrix_props nil )nil matrix_props nil )nil matrix_props nil )nil matrix_props nil )"subrange(0, columns(S) - 1)" matrix_det nil )nil integers nil )"rat" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil sigma "reals/" )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )nil naturalnumbers nil )nil defined_types nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" matrix_det nil )"real" matrix_props nil )"real" matrix_det nil ))nil 3615637395"" (skeep)"" (lemma "det_upper_triangular" )"" (inst?)"" (assert )"" (replaces -1)"" case "FORALL (k:nat): rows(S)-1-k>=0 IMPLIES (prod_diag(S, rows(S)-1-k) = 0 IFF AND entry(S)(rows(S)-1-i,rows(S)-1-i) = 0))") "1" (inst - "rows(S)-1" )"1" (assert )"1" (replaces -1)"1" (ground)"1" (skeep)"1" (inst?)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" (skeep)"2" (inst + "rows(S)-1-i" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (assert )"1" (expand "prod_diag" )"1" (ground)"1" (inst + "0" ) (("1" (assert ) nil nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skeep)"2" (assert )"2" (expand "prod_diag" +)"2" (assert )"2" (ground)"1" (skosimp*)"1" "i!1" )"1" (assert ) nil nil ))nil ))nil )"2" "nzreal_times_nzreal_is_nzreal" )"2" "1" (assert ) nil nil )"2" "2" "2" "j+1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" "i!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrix_det nil )"real" matrices nil )"real" matrix_det nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )"int" integers nil )"Square" matrix_det nil )"nat" matrix_det nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" matrix_det nil )"(total_order?[real])" nil )nil defined_types nil )nil naturalnumbers nil )"posint" nil )"real" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"nat" matrix_det nil )"boolean" notequal nil )"posint" nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[list -> boolean]" list_adt nil )nil reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil list_adt nil )nil numbers nil ))nil 3615886750"" (skeep)"" (expand "upper_triangular?" )"" (skeep)"" (rewrite "entry_mult" )"" (lift-if)"" (ground)"" (expand "*" 1)"" (rewrite "dot_eq_sigma" )"" (rewrite "length_row" )"" (rewrite "length_col" )"" (rewrite "sigma_restrict_eq_0" )"" (hide 2)"" (skosimp*)"" (rewrite "access_row" )"" rewrite "access_col" )"" rewrite "access_row" )"" "i" "i!1" )"" "i!1" "j" )"" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"FullMatrix" matrices nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"Vector" matrices nil )nil matrices nil )nil matrices nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )nil matrices nil )nil integers nil )nil matrices nil )nil matrix_props nil )nil sigma "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )nil sigma "reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"(total_order?[real])" nil )nil matrix_props nil )"real" matrices nil ))nil 3615887148"" (skeep)"" (expand "lower_triangular?" )"" (skeep)"" (rewrite "entry_mult" )"" (lift-if)"" (ground)"" (expand "*" 1)"" (rewrite "dot_eq_sigma" )"" (rewrite "length_row" )"" (rewrite "length_col" )"" (rewrite "sigma_restrict_eq_0" )"" (hide 2)"" (skosimp*)"" (rewrite "access_row" )"" rewrite "access_col" )"" rewrite "access_row" )"" "i" "i!1" )"" "i!1" "j" )"" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"FullMatrix" matrices nil )nil matrices nil )nil matrices nil )"Vector" matrices nil )nil matrices nil )"VectorN(rows(M))" matrices nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )nil matrices nil )nil integers nil )nil matrices nil )nil matrix_props nil )nil sigma "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )nil sigma "reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"(total_order?[real])" nil )nil matrix_props nil )"real" matrices nil ))nil ))nil 3615887393"" (skeep)"" (expand "upper_triangular?" )"" (skeep)"" (rewrite "entry_Id" )"" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" matrix_det nil )nil matrices nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3615887410"" (skeep)"" (expand "lower_triangular?" )"" (skosimp*)"" (rewrite "entry_Id" )"" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" matrix_det nil )nil matrices nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3615887935"" (skeep)"" (expand "upper_triangular?" )"" (skosimp*)"" (rewrite "entry_Easr" )"" (lift-if)"" (lift-if)"" (lift-if)"" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )nil matrix_det nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil ))nil 3615887969"" (skeep)"" (expand "lower_triangular?" )"" (skosimp*)"" (rewrite "entry_Easr" )"" (lift-if)"" (lift-if)"" (lift-if)"" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )nil matrix_det nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil ))nil 3615822839 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3615822839 ("" (termination-tcc) nil nil ) nil nil ))nil 3615822839"" (skeep)"" (name "GG" "v(pn)(FM,k-1)" )"1" (replace -1)"1" (hide -1)"1" (typepred "GG" )"1" (rewrite "rows_mult" +)"1" (rewrite "columns_mult" +)"1" (assert ) nil nil )"2" (expand "rows" )"2" (expand "length" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil list_adt nil )nil numbers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil matrices nil )"FullMatrix" matrices nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3615823903"" (induct "k" )"1" (grind) nil nil )"2" (skeep)"2" (skeep)"2" (inst - "pn" "FM" "GM" )"2" (assert )"2" (split -)"1" (expand "prod_mat" +)"1" (inst - "1+j" ) (("1" (assert ) nil nil )) nil ))nil )"2" (skeep)"2" (inst - "i" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"FullMatrix" matrices nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"SquareMatrix(pn)" matrix_det nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil integers nil )"bool" reals nil )nil integers nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3615823426 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3615823806"" (induct "p" )"1" (skeep)"1" (assert )"1" (expand "prod_mat" + 2)"1" (expand "prod_mat" + 2)"1" (assert )"1" (lemma "prod_mat_eq" )"1" (inst?)"1" "LAMBDA (i: nat): IF i <= k THEN FM(i) ELSE GM(i - 1 - k) ENDIF") "1" (assert )"1" (skosimp*) (("1" (assert ) nil nil )) nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (inst?)"2" (expand "prod_mat" + 2)"2" (expand "prod_mat" + 3)"2" (assert )"2" (rewrite "matrix_mult_assoc" 1 :dir rl)"1" (assert ) nil nil )"2" (hide (-2 1))"2" (typepred "prod_mat(pn!1)(GM!1,j!1)" )"2" (expand "rows" )"2" (expand "length" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nat" matrix_det nil )nil matrix_det nil )"FullMatrix" matrices nil )"nonneg_int" nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"SquareMatrix(pn)" matrix_det nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"Vector" matrices nil )"real" matrices nil )nil matrices nil )"real" matrices nil )nil matrices nil )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"posint" nil ))nil 3615824896"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )nil integers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3615824880"" case "FORALL (k: nat, pn: posnat, FM: [nat -> SquareMatrix(pn)]): LAMBDA (i): FM(i + 1), k)") "1" (skeep)"1" (inst - "k-1" "pn" "FM" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (skeep)"1" (assert )"1" (expand "prod_mat" )"1" (expand "prod_mat" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (assert )"2" (inst - "pn" "FM" )"2" (assert )"2" (expand "prod_mat" +)"2" (rewrite "matrix_mult_assoc" :dir rl)"1" (assert ) nil nil )"2" "prod_mat(pn)(LAMBDA (i): FM(1 + i), j)" )"2" (expand "rows" -3)"2" (expand "length" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )nil naturalnumbers nil )nil defined_types nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nat" matrix_det nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"FullMatrix" matrices nil )"posint" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil matrices nil )"real" matrices nil )nil matrices nil )"real" matrices nil )"Vector" matrices nil )nil matrices nil )"VectorN(rows(M))" matrices nil )"{A: MatrixMN(rows(M), columns(N)) | " nil ))nil 3615885429 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )nil integers nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3615885429"" (skeep)"" (rewrite "rows_transpose" )"" (rewrite "columns_transpose" ) (("" (assert ) nil nil )) nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil matrices nil ))nil ))nil 3615885430"" (induct "k" )"1" (skeep)"1" (expand "prod_mat" ) (("1" (propax) nil nil )) nil )) nil )"2" (skeep)"2" (skeep)"2" (assert )"2" (lemma "prod_mat_expand_left" )"2" "1+j" "pn" "LAMBDA (i): IF i <= 1 + j THEN transpose(FM(1 - i + j))") "1" (assert )"1" (replaces -1)"1" (expand "prod_mat" + 1)"1" (rewrite "transpose_mult" )"1" (inst - "pn" "FM" )"1" (assert )"1" (lemma "prod_mat_eq" )"1" "j" "pn" "LAMBDA (i): IF i <= j THEN transpose(FM(j - i)) ELSE FM(i) ENDIF" "LAMBDA (i_1: nat): IF 1 + i_1 <= 1 + j THEN transpose(FM(j - i_1))") "1" "1" (assert ) nil nil )"2" "2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "rows_transpose" )"2" rewrite "columns_transpose" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" (assert ) nil nil ))nil ))nil )"4" "4" "4" rewrite "rows_transpose" )"4" rewrite "columns_transpose" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" "5" "5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (rewrite "rows_transpose" )"2" (rewrite "columns_transpose" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp*)"3" (rewrite "rows_transpose" )"3" (rewrite "columns_transpose" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skosimp*) (("4" (assert ) nil nil )) nil )) nil ))nil )"posint" nil )"int" integers nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" matrix_det nil )"posnat" matrix_det nil )"[nat -> SquareMatrix(pn)]" matrix_det nil )nil matrices nil )"FullMatrix" matrices nil )"(total_order?[real])" nil )nil matrices nil )nil matrices nil )"(total_order?[real])" nil )nil matrix_det nil )"(strict_total_order?[real])" real_props nil )nil matrix_det nil )nil naturalnumbers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"SquareMatrix(pn)" matrix_det nil )nil defined_types nil )"PosFullMatrix" matrices nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))nil 3615823242"" (skeep)"" (rewrite "rows_mult" )"" (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 ))nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"FullMatrix" matrices nil )nil matrices nil ))nil ))nil 3615823243"" (skeep)"" (expand "is_simple_prod?" )"" (skolem - ("FM" "k" ))"" (skolem - ("GM" "p" ))"" (assert )"" (flatten)"" (replace -2 +)"" (replace -4 +)"" (rewrite "mult_prod_mat" +)"" "LAMBDA (i: nat): IF i <= k THEN FM(i) ELSE GM(i - 1 - k) ENDIF" "1+k+p" )"1" (assert )"1" (expand "is_simple_seq?" )"1" (skeep)"1" (lift-if)"1" "1" "1" assert )"1" "p!1" )"1" assert )"1" (ground) nil nil ))nil ))nil ))nil ))nil )"2" "2" "p!1-1-k" )"1" assert )"1" (ground) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )"int" integers nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"nat" matrix_det nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" matrix_det nil )"int" integers nil )"nat" matrix_det nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nonneg_int" nil )"posint" nil )"posint" nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrix_det nil ))nil 3615889356"" (skeep)"" (expand "is_simple_prod?" )"" (inst + "LAMBDA (i): Id(pn)" "0" )"" (split)"1" (expand "is_simple_seq?" ) (("1" (propax) nil nil )) nil )"2" (expand "prod_mat" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )"bool" matrix_det nil )"SquareMatrix(pn)" matrix_det nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"Vector" matrices nil )"real" matrices nil )nil matrices nil )nil matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3615824263"" (skeep)"" (expand "is_simple_prod?" )"" (inst + "LAMBDA (j:nat): Esr(pn)(i,r)" "0" )"" (split)"1" (expand "is_simple_seq?" )"1" (skeep)"1" (assert ) (("1" (inst 4 "i" "r" ) nil nil )) nil ))nil ))nil )"2" (expand "prod_mat" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )"(strict_total_order?[real])" real_props nil )"bool" matrix_det nil )"SquareMatrix(pn)" matrix_det nil )"SquareMatrix(pn)" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3615824437"" (skeep)"" (expand "is_simple_prod?" )"" (inst + "LAMBDA (p:nat): Ers(pn)(i,j)" "0" )"" (split)"1" (expand "is_simple_seq?" )"1" (skeep)"1" (assert )"1" (inst + "i" "j" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "prod_mat" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )"(strict_total_order?[real])" real_props nil )"bool" matrix_det nil )"SquareMatrix(pn)" matrix_det nil )"{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}" nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"Vector" matrices nil )"real" matrices nil )nil matrices nil )nil matrices nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3615824583"" (skeep)"" (expand "is_simple_prod?" )"" (inst + "LAMBDA (p:nat): Easr(pn)(i,j,r)" "0" )"" (split)"1" (expand "is_simple_seq?" )"1" (skeep)"1" (inst 3 "i" "j" "r" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand "prod_mat" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )"(strict_total_order?[real])" real_props nil )"bool" matrix_det nil )"SquareMatrix(pn)" matrix_det nil )"SquareMatrix(pn)" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3615824734"" (expand "is_simple_prod?" )"" case "FORALL (pn: posnat, S: SquareMatrix(pn),k): AND S = prod_mat(pn)(FM, k))") "1" (skeep)"1" (skeep)"1" (inst - "pn" "S" "k" )"1" (assert )"1" (inst + "FM" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (skeep)"1" (skeep)"1" (assert )"1" (replace -2)"1" (expand "prod_mat" )"1" (expand "is_simple_seq?" )"1" (inst - "0" )"1" (assert )"1" (ground)"1" (replaces -1)"1" (rewrite "det_Id" ) nil nil )) nil )"2" (skeep)"2" replace -3)"2" rewrite "det_Easr" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (assert )"2" (skeep)"2" (assert )"2" (skeep)"2" (replace -3 +)"2" (rewrite "prod_mat_expand_left" 1)"2" "pn" "prod_mat(pn)(LAMBDA (i): FM(1 + i), j)" )"2" (assert )"2" (split -1)"1" expand "is_simple_seq?" )"1" "0" )"1" assert )"1" "1" "1" rewrite "mult_Id_left" )nil nil ))nil )"2" "2" replace -3)"2" "GV" "prod_mat(pn)(LAMBDA (i): FM(1 + i), j)" )"2" replace -1)"2" assert )"2" rewrite "mult_Easr_left" "2" rewrite "det_replace_row_sum_scal" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "LAMBDA (i): FM(1+i)" )"2" assert )"2" expand "is_simple_seq?" )"2" "2" "1+p" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" matrix_props nil )"SquareMatrix(pn)" matrix_det nil )"bool" booleans nil )"bool" matrix_det nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )nil naturalnumbers nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil defined_types nil )nil naturalnumbers nil )nil matrix_det nil )"(strict_total_order?[real])" real_props nil )nil matrix_props nil )nil matrices nil )nil matrix_det nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )"FullMatrix" matrices nil )"int" integers nil )"posint" nil )nil matrix_det nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" matrix_det nil ))nil 3615825883"" (expand "is_simple_prod?" )"" case " FORALL (pn: posnat, S, R: SquareMatrix(pn),Kz:nat,k:nat):k<=Kz AND AND ") "1" (skeep)"1" (skeep)"1" (inst - "pn" "S" "R" "k" "k" )"1" (assert )"1" (inst + "FM" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "Kz" )"1" (skeep)"1" (case "k = 0" )"1" (replaces -1)"1" (hide -1)"1" (assert )"1" (skeep)"1" (expand "is_simple_seq?" )"1" (inst - "0" )"1" (expand "prod_mat" )"1" (replace -2 :dir rl)"1" "1" "1" rewrite "mult_Id_left" )nil nil ))nil )"2" "2" replace -3 +)"2" rewrite "mult_Easr_left" +)"2" rewrite "det_replace_row_sum_scal" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (replace -3) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (skeep)"2" (case "NOT k = j+1" )"1" (inst - "pn" "S" "R" "k" )"1" (assert )"1" (inst + "FM" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (replace -1)"2" (hide -3)"2" (assert )"2" (replace -4 +)"2" (expand "prod_mat" +)"2" (rewrite "matrix_mult_assoc" )"1" "pn" "prod_mat(pn)(FM,j)" "FM(1+j)*R" "j" )"1" assert )"1" "1" replace -1)"1" assert )"1" "pn" "FM(1+j)" "R" "0" )"1" assert )"1" "LaMBDA (p:nat): FM(1+j)" )"1" "1" expand "is_simple_seq?" )"1" "1" "1+j" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "prod_mat" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "FM" )"2" "2" expand "is_simple_seq?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "rows_mult" )"2" rewrite "columns_mult" )"1" (assert ) nil nil )"2" "FM(1+j)" )"2" expand "rows" )"2" expand "length" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "FM(1+j)" )"2" expand "rows" )"2" expand "length" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"Vector" matrices nil )"real" matrices nil )nil matrices nil )"real" matrices nil )nil matrices nil )"real" matrix_props nil )"SquareMatrix(pn)" matrix_det nil )"bool" booleans nil )"bool" matrix_det nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )nil naturalnumbers nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"FullMatrix" matrices nil )nil defined_types nil )nil naturalnumbers nil )nil matrix_det nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil matrices nil )nil matrices nil )nil matrices nil )"SquareMatrix(pn)" matrix_det nil )"nat" matrix_det nil )"[nat -> SquareMatrix(pn)]" matrix_det nil )"posnat" matrix_det nil )"(strict_total_order?[real])" real_props nil )"bool" matrix_det nil ))nil 3615889893"" (skeep)"" (typepred "Easr(pn)(i,j,r)" )"" (expand "rows" )"" (expand "length" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"SquareMatrix(pn)" matrix_det nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil ))nil 3615826667"" (skeep)"" (rewrite "rows_transpose" )"" (rewrite "columns_transpose" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil ))nil ))nil 3615826668"" case "FORALL (include_scals, include_swaps: bool, pn: posnat, ") "1" (skeep)"1" (ground)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (inst - _ _ "pn" "transpose(S)" )"2" (inst?)"2" (assert )"2" (rewrite "transpose_transpose" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "is_simple_prod?" )"2" (skeep)"2" "LAMBDA (i): IF i<=k THEN transpose(FM(k-i)) ELSE FM(i) ENDIF" "k" )"1" (lemma "transpose_prod_mat" )"1" (inst?)"1" (replace -3 +)"1" (replace -1)"1" (expand "is_simple_seq?" )"1" (skeep)"1" (case "p>k" )"1" (assert )"1" "p" )"1" (ground) nil nil ))nil ))nil )"2" (assert )"2" "k-p" )"2" "1" "1" rewrite "transpose_Id" )nil nil ))nil )"2" "2" assert )"2" "2" "transpose_Ers" )"2" "2" replace -5)"2" replace -1)"2" "j" "i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "transpose_Easr" )"3" "3" replace -4)"3" replace -1)"3" assert )"3" "j" "i" "r" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" assert )"4" "4" "transpose_Esr" )"4" "4" "i" "r" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (rewrite "rows_transpose" )"2" (rewrite "columns_transpose" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp*)"3" (rewrite "rows_transpose" )"3" (rewrite "columns_transpose" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"nat" matrix_det nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[nat -> SquareMatrix(pn)]" matrix_det nil )"posnat" matrix_det nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil matrices nil )"odd_int" integers nil )nil matrix_det nil )"(strict_total_order?[real])" real_props nil )nil matrix_det nil )nil matrix_det nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" matrix_det nil )nil matrix_det nil )nil matrices nil )nil matrices nil )nil matrices nil )nil booleans nil )nil booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )"bool" matrix_det nil )"PosFullMatrix" matrices nil ))nil 3615903437"" (skeep)"" "GZ" "LAMBDA (k): form_matrix(lambda (i,j): IF i<=k AND i=j THEN entry(S)(i,j) ELSIF i=j THEN 1 ELSE 0 ENDIF,pn,pn)" )"" case "FORALL (k): k<pn IMPLIES is_simple_prod?(pn,true,include_swaps)(GZ(k))" )"1" (case "S = GZ(pn-1)" )"1" (inst - "pn-1" )"1" (assert ) (("1" (assert ) nil nil )) nil )) nil )"2" (hide (-1 2))"2" (rewrite "full_matrix_eq" )"1" (split +)"1" (expand "GZ" 1)"1" (rewrite "rows_form_matrix" )"1" (assert ) nil nil )) nil ))nil )"2" (expand "GZ" 1)"2" (lemma "columns_form_matrix" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (skosimp*)"3" (expand "GZ" +)"3" (rewrite "entry_form_matrix" )"3" (lift-if)"3" (assert )"3" (ground)"3" (typepred "i!1" )"3" "j!1" )"3" expand "diagonal?" )"3" "i!1" "j!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "form_matrix_square" )"2" "LAMBDA (i, j): IF i <= pn-1 AND i = j THEN entry(S)(i, j)" " pn" " pn") "2" (skosimp*)"2" (assert )"2" (expand "GZ" +)"2" (assert )"2" (inst - "i!1" "j!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (induct "k" )"1" (flatten)"1" (assert )"1" (hide -2)"1" (expand "is_simple_prod?" )"1" (inst + "LAMBDA (i): GZ(0)" "0" )"1" (split)"1" (expand "is_simple_seq?" )"1" (skeep)"1" (inst 4 "0" "entry(S)(0,0)" )"1" assert )"1" "1" rewrite "full_matrix_eq" 2)"1" "1" expand "GZ" )"1" rewrite "rows_form_matrix" )"1" (assert ) nil nil ))nil ))nil )"2" expand "GZ" 1)"2" "columns_form_matrix" )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" "i" )"3" "j" )"3" expand "GZ" )"3" "3" rewrite "entry_form_matrix" )"3" assert )"3" rewrite "entry_Esr" )"3" "3" "3" "3" assert )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "form_matrix_square" )"2" expand "GZ" 2)"2" "2" assert )"2" "1" expand "GZ" 1)"1" nil nil ))nil )"2" "i!1" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "prod_mat" )"2" (propax) nil nil )) nil ))nil )"2" (split +)"1" (flatten)"1" (lemma "form_matrix_square" )"1" (expand "GZ" )"1" "1" assert )"1" "1" "i!1" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "GZ" )"2" (rewrite "rows_form_matrix" )"2" (assert ) nil nil )) nil ))nil )"3" (lemma "columns_form_matrix" )"3" (expand "GZ" )"3" (inst?) (("3" (assert ) nil nil ))nil ))nil ))nil )"4" (expand "GZ" )"4" (rewrite "rows_form_matrix" )"4" (lemma "columns_form_matrix" )"4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" (expand "GZ" )"5" (rewrite "rows_form_matrix" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" case "GZ(j+1) = GZ(j)*Esr(pn)(j+1,entry(S)(j+1,j+1))" )"1" (replaces -1)"1" (rewrite "mult_simple_prod" )"1" (hide 2)"1" (rewrite "Esr_simple_prod" ) nil nil )) nil )"2" (assert )"2" (expand "is_simple_prod?" )"2" (skeep)"2" (assert )"2" (flatten)"2" replace -2)"2" assert )"2" "prod_mat(pn)(FM,k)" )"2" assert )"2" "2" "i!1" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide (-1 2))"2" (expand "GZ" )"2" (expand "Esr" )"2" (rewrite "form_matrix_mult" )"2" (rewrite "full_matrix_eq" )"2" (split)"1" rewrite "rows_form_matrix" )"1" rewrite "rows_form_matrix" )nil nil ))nil )"2" "columns_form_matrix" )"2" "2" assert )"2" "2" "columns_form_matrix" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "entry_form_matrix" )"3" rewrite "entry_form_matrix" )"3" assert )"3" "3" "1" "1" assert )"1" "1" "1" assert )"1" replace -2)"1" assert )"1" "sigma_eq_one_arg2" )"1" "1" "j!1" )"1" assert )"1" "1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "diagonal?" )"2" "2" "2" "2" "2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" assert )"1" "sigma_eq_one_arg2" )"1" "1" "j!1" )"1" assert )"1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" expand "diagonal?" )"2" "i!1" "i!2" )"2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (assert )"3" (split)"1" (lemma "form_matrix_square" )"1" (expand "GZ" )"1" "LAMBDA (i, j): IF i <= k AND i = j THEN entry(S)(i, j)" " pn" " pn") "1" (assert )"1" (flatten)"1" assert )"1" "1" (inst - "i!1" "j!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "GZ" )"2" (rewrite "rows_form_matrix" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (expand "GZ" )"3" (lemma "columns_form_matrix" )"3" (inst?) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (expand "GZ" )"4" (rewrite "rows_form_matrix" )"4" (lemma "columns_form_matrix" )"4" (inst?) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"5" (expand "GZ" )"5" (rewrite "rows_form_matrix" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (assert )"3" (split)"1" (flatten)"1" (expand "GZ" )"1" (lemma "form_matrix_square" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (inst - "i!1" "j!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "GZ" )"2" (rewrite "rows_form_matrix" )"2" (assert ) nil nil )) nil ))nil )"3" (expand "GZ" )"3" (lemma "columns_form_matrix" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil )"4" (expand "GZ" )"4" (rewrite "rows_form_matrix" )"4" (lemma "columns_form_matrix" )"4" (inst?) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"5" (expand "GZ" )"5" (rewrite "rows_form_matrix" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{M: MatrixMN(m, n) | " nil )nil matrices nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"nat" matrices nil )nil matrices nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" matrices nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"Vector" matrices nil )nil matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"nat" list_props nil )"[T, T -> boolean]" equalities nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"FullMatrix" matricesnil )"boolean" notequal nil )nil matrices nil )"real" reals nil )nil integers nil )nil sigma "reals/" )"(divides(m))" divides nil )"nat" sigma_nat "reals/" )"nnreal" sigma_nat "reals/" )"even_int" integersnil )nil sigma "reals/" )"posint" nil )"odd_int" integers nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil matrix_det nil )nil matrix_det nil )"{A: MatrixMN(rows(M), columns(N)) | " nil )"VectorN(rows(M))" matrices nil )nil matrices nil )"real" matrices nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"FullMatrix" matrices nil )"(strict_total_order?[real])" real_props nil )"SquareMatrix(pn)" matrix_det nil )"bool" matrix_det nil )nil matrix_det nil )"SquareMatrix(pn)" matrix_det nil )nil naturalnumbers nil )nil defined_types nil )"SquareMatrix(pn)" matrix_det nil )"posnat" matrix_det nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )nil matrices nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" matrix_det nil )nil matrices nil )"[k: nat -> IF i_1 <= k AND i_1 = j_1 THEN entry(S)(i_1, j_1)" matrix_det nil) nil matrices nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )"bool" matrix_det nil )"bool" booleans nil ))nil 3616751452"" (skeep)"" (expand "is_simple_prod?" )"" (skeep)"" (inst + "FM" "k" )"" (assert )"" (expand "is_simple_seq?" )"" (skeep)"" (inst - "p" ) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil integers nil )nil integers nil )nil matrices nil )"bool" matrix_det nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.565Bemerkung:
(vorverarbeitet am 2026-04-30)
¤ *Bot Zugriff
2026-05-26
