Quellcode-Bibliothek matrix_diag.prf
Sprache: Lisp
(matrix_diagnil 3615559416"" (skeep)"" (typepred "i" )"" (expand "d_point2" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"bool" matrix_diag nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 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 )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3615559416"" (skeep)"" (typepred "z`8" )"" (expand "d_point2" )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"bool" matrix_diag nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )IF const-decl "[boolean, T, T -> T]" if_def 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 )"[bool, bool -> bool]" booleans nil )"bool" booleans nil )"bool" matrix_det nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 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 )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3615559416"" (skeep)"" (typepred "i" )"" (expand "d_point2" ) (("" (ground) nil nil )) nil )) nil ))nil )"bool" matrix_diag nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3615559416"" (skeep)"" (assert )"" (split +)"1" (typepred "T" ) (("1" (propax) nil nil )) nil )"2" (flatten)"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point2" )"2" (flatten)"2" (expand "d_point1" )"2" (flatten)"2" (replace -6)"2" (replace -7)"2" (assert )"2" (skosimp*)"2" "k!1" "p!1" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "T" ) (("3" (propax) nil nil )) nil )"4" (typepred "R" ) (("4" (propax) nil nil )) nil )"5" (typepred "R" ) (("5" (propax) nil nil )) nil )"6" (typepred "Q" ) (("6" (propax) nil nil )) nil ))nil ))nil ))nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" matrix_diag nil )"bool" matrix_diag nil )"bool" booleans nil )"bool" 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 )"[bool, bool -> bool]" booleans nil )"bool" 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 )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 list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3615559416"" (skeep)"" (case "i = j" )"1" (hide -2)"1" (case "j = 0" )"1" (ground) nil nil )"2" (assert )"2" (typepred "j" )"2" (expand "d_point1" )"2" (hide 3)"2" (flatten)"2" (assert )"2" (skeep)"2" (case "NOT p = j" )"1" (assert )"1" (inst - "k!1" "p" )"1" (ground) nil nil )) nil ))nil )"2" (assert )"2" (replace -1)"2" assert )"2" "i" )"2" expand "d_point2" )"2" "k!1" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "j = 0" )"1" (replace -1)"1" (assert )"1" (typepred "i" )"1" (expand "d_point2" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "d_point1" )"2" (typepred "j" )"2" (expand "d_point1" )"2" (flatten)"2" (assert )"2" (skeep)"2" (case "NOT k!1 = p" )"1" (inst - "k!1" "p" )"1" (ground) nil nil )) nil )"2" (replace -1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_diag nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 )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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil ))nil ))nil 3615559416"" (skeep)"" (typepred "j" )"" (typepred "i" )"" (expand "d_point2" )"" (assert )"" (typepred "i" )"" (expand "d_point2" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" matrix_diag nil ))nil ))nil 3615559416 ("" (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 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" matrix_det nil )"bool" matrix_det nil )"bool" booleans nil )"[bool, bool -> bool]" booleans 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 )IF const-decl "[boolean, T, T -> T]" if_def nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"bool" matrix_diag nil )"bool" matrix_diag nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"bool" matrix_det nil )"SquareMatrix(pn)" matrix_det nil )"boolean" notequal nil )"{M: MatrixMN(m, n) | " nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"real" matrices nil ))nil ))nil 3615559416"" (skeep)"" (rewrite "lex2_lt" )"1" (typepred "i" )"1" (expand "d_point2" ) (("1" (propax) nil nil )) nil )) nil )"2" (assert )"2" (typepred "j" )"2" (typepred "i" )"2" (expand "d_point2" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil lex2 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields 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 )"bool" matrix_diag nil )nil integers nil )nil integers nil )nil matrices nil )"bool" matrix_det nil )"bool" matrix_diag nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3615559416"" (skeep)"" (typepred "i" )"" (expand "d_point2" )"" (assert )"" (flatten)"" (assert )"" (case "i = rows(S)-1" )"1" (typepred "i" )"1" (typepred "j" )"1" (expand "d_point2" )"1" (expand "d_point1" )"1" (ground) nil nil )) nil ))nil ))nil ))nil )"2" (assert )"2" (skeep)"2" (case "NOT k!1 = i" )"1" (inst - "k!1" ) (("1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_diag nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil ))nil ))nil 3615559416"" (skeep) (("" (assert ) nil nil )) nil )"int" integers nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(total_order?[real])" nil ))nil ))nil 3615559416"" (skeep)"" (assert )"" (rewrite "lex2_lt" )"1" (typepred "i" )"1" (expand "d_point2" ) (("1" (propax) nil nil )) nil )) nil )"2" (typepred "i" )"2" (expand "d_point2" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"int" integers nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"bool" matrix_diag nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 lex2 nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3615559416"" (skeep)"" (skeep)"" (rewrite "length_add_vect_same" )"1" (rewrite "length_row" )"1" (typepred "i" )"1" (typepred "j" )"1" (expand "d_point1" )"1" (expand "d_point2" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" (rewrite "length_row" )"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point1" )"2" (expand "d_point2" )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil matrix_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"VectorN(length(v2))" matrices nil )nil matrices nil )"bool" matrix_diag nil )"bool" matrix_diag nil )"bool" 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 )"Vector" matrices nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )nil matrices 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 matrices nil ))nil ))nil 3615559416"" (skeep)"" (skeep)"" (rewrite "rows_replace_row" )"1" (rewrite "columns_replace_row" )"1" (assert )"1" (expand "upper_triangular?" )"1" (skosimp*)"1" (copy -3)"1" (label "igz" -1)"1" (hide "igz" )"1" (rewrite "rows_replace_row" )"1" (reveal "igz" )"1" (rewrite "entry_replace_row" )"1" (lift-if)"1" assert )"1" "1" "1" replace -1)"1" "S" )"1" "1" expand "upper_triangular?" )"1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "access_row" )"1" rewrite "access_row" )"1" "i" "j!1" )"1" "j" "j!1" )"1" assert )"1" assert )"1" "i" )"1" "j" )"1" expand "d_point1" )"1" expand "d_point2" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "S" )"2" expand "upper_triangular?" )"2" "i!1" "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_add_vect_same" )"1" rewrite "length_row" )"1" "i" )"1" "j" )"1" expand "d_point1" )"1" expand "d_point2" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "length_scal_vect" )"2" rewrite "length_row" )"2" rewrite "length_row" )"2" "i" )"2" "j" )"2" expand "d_point1" )"2" expand "d_point2" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_add_vect_same" )"1" (rewrite "length_row" )"1" (typepred "i" )"1" "j" )"1" expand "d_point1" )"1" expand "d_point2" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" rewrite "length_row" )"2" "i" )"2" "j" )"2" expand "d_point1" )"2" expand "d_point2" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_add_vect_same" )"1" (rewrite "length_row" )"1" (typepred "i" )"1" (typepred "j" )"1" (expand "d_point1" )"1" (expand "d_point2" )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" (rewrite "length_row" )"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point1" )"2" (expand "d_point2" )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_add_vect_same" )"1" (rewrite "length_row" )"1" (typepred "i" )"1" (typepred "j" )"1" (expand "d_point1" )"1" (expand "d_point2" )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" (rewrite "length_row" )"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point1" )"2" (expand "d_point2" )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrix_props nil )nil matrices nil )"(total_order?[real])" nil )nil matrix_props nil )nil matrices nil )nil matrices nil )"real" reals nil )nil matrices nil )"(total_order?[real])" nil )"real" reals nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"VectorN(length(v2))" matrices nil )"Vector" 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 )nil matrices nil )"bool" matrix_diag nil )"bool" matrix_diag nil )"bool" 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 )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 matrix_props nil ))nil ))nil 3615559416"" (skeep)"" (skeep)"" (rewrite "length_add_vect_same" )"1" (rewrite "length_row" )"1" (typepred "i" )"1" (typepred "j" )"1" (expand "d_point1" )"1" (expand "d_point2" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" (rewrite "length_row" )"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point1" )"2" (expand "d_point2" )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil matrix_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"VectorN(length(v2))" matrices nil )nil matrices nil )"bool" matrix_diag nil )"bool" matrix_det nil )"bool" matrix_diag nil )"bool" booleans nil )"bool" 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 )"Vector" matrices nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )nil matrices 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 matrices nil ))nil ))nil 3615559416"" (skeep)"" (case "i<pn anD j < pn AND i<j" )"1" (flatten)"1" (skeep)"1" (case "length(row(Q)(i) + pivnum*row(Q)(j)) = rows(S)" )"1" (rewrite "rows_replace_row" )"1" (assert )"1" (rewrite "columns_replace_row" )"1" (assert )"1" (lemma "mult_Easr_left" )"1" (inst?)"1" (assert )"1" (inst?)"1" (assert )"1" "1" rewrite "mult_simple_prod" )"1" rewrite "Easr_simple_prod" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide 7)"2" (rewrite "length_add_vect" )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" (rewrite "length_row" )"2" (expand "max" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 7)"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point1" )"2" (expand "d_point2" )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrix_diag nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil matrices nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )nil matrix_props nil )"(total_order?[real])" nil )nil matrices nil )nil matrix_props nil )"real" reals nil )nil matrix_props nil )nil matrix_det nil )"SquareMatrix(pn)" matrix_det nil )nil matrix_det nil )"FullMatrix" matrices nil )nil matrix_det nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil matrices nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil matrices nil )"VectorN(max(length(v1), length(v2)))" matrices nil )"Vector" matrices nil )"bool" matrix_det nil )"bool" booleans nil )"VectorN(length(v2))" matrices nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil ))nil ))nil 3615559416"" (skeep)"" (skeep) (("" (rewrite "Id_simple_prod" ) nil nil )) nil )) 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 )nil numbers nil )"bool" booleans nil )nil booleans nil )nil booleans nil )nil matrix_det nil ))nil ))nil 3615559416"" (skeep)"" (assert )"" (case "i<pn anD j < pn AND i<j" )"1" (flatten)"1" (case "NOT (null?(R) OR null?(S) OR null?(Q))" )"1" (flatten)"1" (assert )"1" (skeep)"1" case "length(row(Q)(i) + pivnum*row(Q)(j)) = pn" )"1" (assert )"1" (split 9)"1" (rewrite "mult_simple_prod" )"1" (rewrite "Easr_simple_prod" ) nil nil ))nil )"2" (lemma "mult_Easr_left" )"2" (inst - "Q" "i" "j" "pn" "pivnum" )"2" (assert )"2" "2" rewrite "matrix_mult_assoc" )"1" rewrite "matrix_mult_assoc" "1" rewrite "mult_Easr_Easr_inv" )"1" rewrite "mult_Id_left" )"1" assert )"1" "R" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" rewrite "Easr_null" )nil nil ))nil )"2" (rewrite "Easr_null" ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "mult_Easr_left" )"3" (inst - "Q" "i" "j" "pn" "pivnum" )"3" (assert )"3" "3" rewrite "matrix_mult_assoc" )"3" rewrite "matrix_mult_assoc" "3" "R" )"3" assert )"3" "3" replace -9)"3" rewrite "mult_Id_left" )"3" rewrite "mult_Easr_Easr_inv" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (rewrite "rows_mult" )"4" (assert ) nil nil )) nil )"5" (rewrite "rows_mult" )"5" (rewrite "columns_mult" )"5" (assert ) nil nil )) nil ))nil )"6" (rewrite "rows_mult" )"6" (assert ) nil nil )) nil )"7" (rewrite "columns_mult" )"7" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 10)"2" (rewrite "length_add_vect" )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" (rewrite "length_row" )"2" expand "max" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 6)"2" (label "igz" -1)"2" (typepred "R" )"2" (typepred "S" )"2" (typepred "Q" )"2" (expand "rows" )"2" (expand "length" )"2" (split "igz" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 7)"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point2" )"2" (expand "d_point1" )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"FullMatrix" matrices nil )"real" reals nil )"(total_order?[real])" nil )nil matrices nil )"(total_order?[real])" nil )nil matrix_props nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )nil matrices nil )"real" reals nil )nil matrices nil )nil matrices nil )nil matrix_det nil )nil matrices nil )nil matrix_det nil )nil matrix_det nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"SquareMatrix(pn)" matrix_det nil )nil matrix_det nil )nil matrix_det 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 )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" matrix_det nil )"bool" booleans nil )"[bool, bool -> bool]" booleans 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 )IF const-decl "[boolean, T, T -> T]" if_def nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, 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 naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt 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" matrix_diag nil )nil integers nil )nil integers nil )nil matrices nil )"bool" matrix_det nil )"bool" matrix_diag nil ))nil ))nil 3615559416"" (skeep)"" (skeep)"" (replace 6) (("" (rewrite "Id_simple_prod" ) nil nil )) nil ))nil ))nil )nil matrix_det nil )nil booleans nil )nil booleans nil )"bool" 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 ))nil 3615559416"" (skeep)"" (skeep)"" (assert )"" (split 6)"1" (flatten)"1" (assert )"1" (lemma "mult_Easr_left" )"1" (inst-cp - "Q" "i" "j" "pn" "pivnum" )"1" (inst - "S" "i" "j" "pn" "pivnum" )"1" (assert )"1" (case "i < pn AND j < pn" )"1" (flatten)"1" (assert )"1" (replaces -3 :dir rl)"1" "1" rewrite "matrix_mult_assoc" )"1" "T" )"1" (assert ) nil nil ))nil )"2" "Q" )"2" expand "rows" )"2" expand "length" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point1" )"2" expand "d_point2" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (rewrite "entry_replace_row" )"1" (lift-if)"1" (split 1)"1" (flatten)"1" (rewrite "access_sum" )"1" (rewrite "access_scal" )"1" (assert )"1" (typepred "T" )"1" (inst-cp - "i!1" )"1" assert )"1" rewrite "access_row" )"1" rewrite "access_row" )"1" assert )"1" "S" )"1" expand "upper_triangular?" )"1" "j" "i!1" )"1" assert )"1" "i" )"1" expand "d_point2" )"1" "1" assert )"1" case "j < rows(S)" )"1" assert )"1" assert )nil nil ))nil )"2" "2" "j" )"2" expand "d_point1" )"2" 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" (flatten)"2" (typepred "T" )"2" (inst - "i!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_add_vect_same" )"1" (rewrite "length_row" )"1" (typepred "i" )"1" (typepred "j" )"1" (expand "d_point1" )"1" (expand "d_point2" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" (rewrite "length_row" )"2" (typepred "i" )"2" (typepred "j" )"2" (expand "d_point1" )"2" (expand "d_point2" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"FullMatrix" 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 )"bool" matrix_det nil )"bool" booleans nil )"bool" matrix_diag nil )"bool" matrix_det nil )"bool" matrix_diag nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil matrices nil )"[bool, bool -> bool]" booleans 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 )"SquareMatrix(pn)" matrix_det nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_det nil )nil 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 )"real" reals nil )nil matrices nil )"real" reals nil )nil matrices nil )nil matrices nil )nil matrix_props nil )"(total_order?[real])" nil )nil matrices nil )"real" reals nil )"real" reals nil ))nil ))nil 3615559416"" (skeep)"" (assert )"" (skeep)"" (typepred "j" )"" (expand "d_point1" )"" (assert )"" (flatten)"" (assert )"" (skeep)"" (rewrite "entry_replace_row" )"1" (rewrite "entry_replace_row" )"1" (lift-if)"1" (split 6)"1" (assert )"1" "1" assert )"1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "access_row" )"1" rewrite "access_row" )"1" "k!1" "p" )"1" assert )"1" replace -2)"1" replace -4)"1" assert )"1" "i" )"1" expand "d_point2" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" assert )"2" "1" "1" replace -1)"1" assert )"1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "access_row" )"1" rewrite "access_row" )"1" assert )"1" "i" "p" )"1" assert )"1" replace -3)"1" assert )"1" "j" )"1" expand "d_point1" )"1" "j" "p" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "j" )"2" expand "d_point1" )"2" "k!1" "p" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_add_vect_same" )"1" (rewrite "length_row" )"1" (typepred "i" )"1" "j" )"1" expand "d_point1" )"1" expand "d_point2" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" rewrite "length_row" )"2" "i" )"2" "j" )"2" expand "d_point1" )"2" expand "d_point2" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_add_vect_same" )"1" (rewrite "length_row" )"1" (typepred "i" )"1" (typepred "j" )"1" expand "d_point1" )"1" expand "d_point2" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_scal_vect" )"2" (rewrite "length_row" )"2" (rewrite "length_row" )"2" "i" )"2" "j" )"2" expand "d_point1" )"2" expand "d_point2" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 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 )"real" reals nil )nil matrix_props nil )"bool" matrix_diag nil )nil matrices nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil matrices nil )"VectorN(max(length(v1), length(v2)))" matrices nil )"Vector" matrices nil )"VectorN(length(v2))" matrices nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil matrix_props nil )nil matrices nil )nil matrices nil )"real" reals nil )nil matrices nil )"real" reals nil )nil matrices nil ))nil ))nil 3615559416"" (skeep)"" (skeep)"" (typepred "i" )"" (expand "d_point2" )"" (flatten)"" (assert )"" (assert )"" (case "NOT j < pn" )"1" (typepred "j" )"1" (expand "d_point1" )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (split 6)"1" (rewrite "rows_replace_row" )"1" (assert ) nil nil )) nil )"2" (skeep)"2" (case "NOT k!1 = i" )"1" (inst - "k!1" )"1" (assert )"1" (rewrite "entry_replace_row" )"1" rewrite "entry_replace_row" 3)"1" rewrite "length_add_vect_same" 1)"1" (rewrite "length_row" ) nil nil )"2" rewrite "length_scal_vect" 1)"2" rewrite "length_row" )"2" rewrite "length_row" )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "length_add_vect_same" 1)"1" (rewrite "length_row" ) nil nil )"2" rewrite "length_scal_vect" 1)"2" rewrite "length_row" )"2" rewrite "length_row" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (replace -1)"2" (assert )"2" rewrite "entry_replace_row" 1)"1" rewrite "entry_replace_row" 2)"1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "access_row" )"1" rewrite "access_row" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" rewrite "length_add_vect_same" 1)"1" rewrite "length_row" )nil nil )"2" rewrite "length_scal_vect" 1)"2" rewrite "length_row" )"2" rewrite "length_row" )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "length_add_vect_same" 1)"1" (rewrite "length_row" ) nil nil )"2" rewrite "length_scal_vect" 1)"2" rewrite "length_row" )"2" rewrite "length_row" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"real" reals nil )nil matrices nil )"real" reals nil )nil matrices nil )nil matrix_props nil )nil matrices nil )nil matrix_props nil )"(total_order?[real])" nil )nil matrices nil )nil matrix_props nil )nil matrices nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil matrices nil )"VectorN(max(length(v1), length(v2)))" matrices nil )"Vector" matrices nil )"VectorN(length(v2))" matrices 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 )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" matrix_diag nil )nil integers nil )nil integers nil )nil matrices nil )"bool" matrix_det nil )"bool" matrix_diag nil ))nil ))nil 3615559416"" (skeep)"" (assert ) (("" (skeep) (("" (assert ) nil nil )) nil )) nil )) nil )"real" reals nil )"int" integers nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(total_order?[real])" nil )"real" reals nil ))nil ))nil 3615559416"" (skeep)"" (skeep)"" (assert )"" (rewrite "lex2_lt" )"1" (typepred "i" )"1" (expand "d_point2" ) (("1" (propax) nil nil )) nil ))nil )"2" (typepred "i" )"2" (expand "d_point2" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil lex2 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 )"bool" matrix_diag nil )nil integers nil )nil integers nil )nil matrices nil )"bool" matrix_det nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" matrix_diag nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"posint" nil )"int" integers nil ))nil ))nil 3615559416"" (skeep)"" (label "answ" 6)"" (hide "answ" )"" (case "NOT (i<pn AND j < pn AND i<j)" )"1" (typepred "j" )"1" (typepred "i" )"1" (expand "d_point1" )"1" (expand "d_point2" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (case "(null?(R) OR null?(S) OR null?(Q))" )"1" (label "igz" -1)"1" (typepred "R" )"1" (typepred "S" )"1" (typepred "Q" )"1" (expand "rows" )"1" (expand "length" )"1" (split "igz" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (reveal "answ" )"2" (skeep)"2" (hide "answ" )"2" case "NOT length(row(S)(i) + pivnum * row(S)(j)) = pn" )"1" (rewrite "length_add_vect" )"1" (rewrite "length_scal_vect" )"1" (rewrite "length_row" )"1" rewrite "length_row" )"1" assert )"1" expand "max" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT length(row(Q)(i) + pivnum * row(Q)(j)) = pn" )"1" (assert )"1" (rewrite "length_add_vect" )"1" rewrite "length_scal_vect" )"1" rewrite "length_row" )"1" rewrite "length_row" )"1" expand "max" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (reveal "answ" )"2" "GG" "v(pn) IF comp_matrixIF comp_matrix AND comp_inversemax (k - 1, 0))") "1" "1" "1" "GG" )"1" assert )"1" "1" assert )"1" "1" (propax) nil nil )"2" (propax) nil nil )"3" (propax) nil nil )"4" (propax) nil nil )"5" replace -6)"5" rewrite "det_replace_row_sum_scal" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (rewrite "lex2_lt" ) nil nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" assert )"4" "i" )"4" "j" )"4" expand "d_point2" )"4" expand "d_point1" )"4" assert )"4" rewrite "rows_replace_row" )"4" assert )"4" "4" rewrite "entry_replace_row" )"4" rewrite "entry_replace_row" )"4" "4" assert )"4" "1" "1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "access_row" )"1" rewrite "access_row" )"1" "i" "j" )"1" "j" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "k!1" "j" )"2" assert )"2" "k!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" "i" )"5" "j" )"5" expand "d_point2" )"5" expand "d_point1" )"5" rewrite "rows_replace_row" )"5" assert )"5" "5" rewrite "entry_replace_row" )"5" rewrite "entry_replace_row" )"5" assert )"5" "5" "1" "1" replace "1" assert )"1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "access_row" )"1" rewrite "access_row" )"1" assert )"1" "i" "p" )"1" "j" "p" )"1" assert )"1" "i" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "k!1" "p" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" "6" assert )"6" "1" "1" assert )"1" "mult_Easr_left" )"1" "Q" "i" "j" "pn" "pivnum" )"1" assert )"1" "1" "mult_Easr_left" )"1" "S" "i" "j" "pn" "pivnum" )"1" assert )"1" "1" rewrite "matrix_mult_assoc" )"1" "T" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "entry_replace_row" )"2" assert )"2" "2" "T" )"2" "1" "1" "1" assert )"1" rewrite "access_sum" )"1" rewrite "access_scal" )"1" rewrite "access_row" )"1" rewrite "access_row" )"1" "S" )"1" expand "upper_triangular?" )"1" "j" "i" )"1" "i" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" "7" "7" replace 1)"7" rewrite "Id_simple_prod" )nil nil ))nil ))nil ))nil )"8" "8" "8" assert )"8" "mult_Easr_left" )"8" "Q" "i" "j" "pn" "pivnum" )"8" assert )"8" "8" assert )"8" "1" rewrite "mult_simple_prod" )"1" rewrite "Easr_simple_prod" )nil nil ))nil )"2" rewrite "matrix_mult_assoc" )"1" rewrite "matrix_mult_assoc" "1" rewrite "mult_Easr_Easr_inv" )"1" rewrite "mult_Id_left" )"1" "R" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "Easr_null" )nil nil ))nil )"2" rewrite "Easr_null" )nil nil ))nil )"3" rewrite "matrix_mult_assoc" )"3" rewrite "matrix_mult_assoc" "3" "R" )"3" assert )"3" "3" replace "3" rewrite "mult_Id_left" )"3" assert )"3" rewrite "mult_Easr_Easr_inv" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" rewrite "rows_mult" )"4" assert )nil nil ))nil )"5" rewrite "rows_mult" )"5" assert )"5" rewrite "columns_mult" )"5" assert )nil nil ))nil ))nil ))nil )"6" rewrite "rows_mult" )"6" assert )nil nil ))nil )"7" rewrite "columns_mult" )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" "9" "9" rewrite "Id_simple_prod" )nil nil ))nil ))nil )"10" "10" "10" assert )"10" rewrite "rows_replace_row" )"10" rewrite "columns_replace_row" )"10" assert )"10" "mult_Easr_left" )"10" "Q" "i" "j" "pn" "pivnum" )"10" assert )"10" "10" rewrite "mult_simple_prod" )"10" rewrite "Easr_simple_prod" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" "11" rewrite "rows_replace_row" )"11" rewrite "columns_replace_row" )"11" assert )"11" "mult_Easr_left" )"11" "S" "i" "j" "pn" "pivnum" )"11" assert )"11" "11" rewrite "upper_triangular_mult" )"11" rewrite "upper_triangular_Easr" )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 )"bool" matrix_diag nil )"bool" matrix_det nil )nil matrices nil )nil integers nil )nil integers nil )"bool" matrix_diag 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 )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )IF const-decl "[boolean, T, T -> T]" if_def 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 )"[bool, bool -> bool]" booleans nil )"bool" booleans nil )"bool" matrix_det nil )"(strict_total_order?[real])" real_props nil )nil matrix_det nil )nil matrix_det nil )nil matrix_props nil )nil matrix_det nil )nil matrix_det nil )nil matrices nil )nil matrix_det nil )nil matrix_det nil )nil matrices nil )nil matrices nil )nil matrix_det nil )nil matrices nil )nil matrix_det nil )nil matrix_props nil )nil matrices nil )"real" reals nil )nil matrices nil )"real" reals nil )nil matrices nil )nil matrix_props nil )nil lex2 nil )"int" integers nil )nil matrix_props nil )"real" reals nil )"posint" nil )"FullMatrix" matrices nil )"real" reals nil )"posint" nil )"int" integers nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )nil ordstruct_adt nil )"bool" ordinals nil )"bool" ordinals nil )nil ordinals nil )"ordinal" lex2 nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrix_props 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) "SquareMatrix(pn)" matrix_det nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil matrices nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )nil matrix_props nil )"(total_order?[real])" nil )nil matrices 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 ))nil ))nil 3615559416 ("" (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 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" matrix_det nil )"bool" matrix_det nil )"bool" booleans nil )"[bool, bool -> bool]" booleans 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 )IF const-decl "[boolean, T, T -> T]" if_def nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"bool" matrix_diag nil )"bool" matrix_diag nil )"real" matrices nil ))nil ))nil 3615632440 ("" (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 )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 ) (<= const-decl "bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil ))nil ))nil 3615632440"" (skeep) (("" (rewrite "Id_simple_prod" ) nil nil )) nil )nil matrix_det nil )nil booleans nil )nil booleans nil )"bool" 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 )nil naturalnumbers nil )"nat" 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 )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil ))nil ))nil 3615632440"" (skeep)"" (rewrite "Id_simple_prod" )"" (flatten) (("" (rewrite "mult_Id_left" ) nil nil )) nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )nil matrix_det nil )nil booleans nil )nil booleans nil )"bool" 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 )nil naturalnumbers nil )"nat" 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 )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil matrices nil )nil matrices nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def 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 ))nil ))nil 3615632440"" (skeep) (("" (rewrite "mult_Id_left" ) 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 ))nil 3615632440 ("" (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 )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 ) (<= const-decl "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 )"nat" matrices nil )"real" matrices nil )"bool" matrix_upper_triang nil ))nil ))nil 3615632440 ("" (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 )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 ) (<= const-decl "bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil )"real" matrices nil )"bool" matrix_upper_triang nil )"int" integers nil ))nil ))nil 3615632440 ("" (skeep) (("" (assert ) nil nil )) nil )"int" integers nil ))nil ))nil 3615632440"" (skeep)"" "ut" "upper_triangulate(rows(S)) ") "" (replaces -1)"" (typepred "ut" )"" (ground)"1" (rewrite "mult_Id_left" ) nil nil )"2" (rewrite "mult_Id_left" ) nil nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"{SGI: [SquareMatrix(pn), SquareMatrix(pn), SquareMatrix(pn)] | NOT stop_rec) IMPLIESLET (S2, Q2, R2) = SGI INAND AND is_simple_prod?(pn, FALSE, FALSE)(Q2))AND AND comp_inverse IMPLIESAND AND AND det(S2) = det(S))}" matrix_upper_triang nil) "real" matrix_props nil )"bool" matrix_det nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" matrix_upper_triang nil )"bool" matrix_upper_triang nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )IF const-decl "[boolean, T, T -> T]" if_def 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 )"[bool, bool -> bool]" booleans nil )"bool" booleans nil )"bool" matrix_det nil )nil integers nil )nil integers nil )nil matrices 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 )"int" integers nil )"(total_order?[real])" nil )nil matrices nil )"FullMatrix" matrices nil ))nil ))nil 3615632440"" (skeep)"" (assert )"" (hide -)"" (typepred "S2" )"" (expand "d_point1" )"" (skosimp*) (("" (rewrite "entry_eq_0" 1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil matrices 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 list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" matrix_diag nil ))nil ))nil 3615632440 ("" (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 )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 ) (<= const-decl "bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )nil matrices nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"{M: MatrixMN(m, n) | " nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"real" matrices nil )"bool" matrix_diag nil ))nil ))nil 3615632440"" (skeep)"" (skeep)"" (assert )"" (rewrite "rows_mult" )"" (rewrite "columns_mult" )"1" (assert ) nil nil )"2" (typepred "R2" )"2" (expand "rows" )"2" (expand "length" ) (("2" (assert ) 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 )nil matrices nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"int" integers nil )"FullMatrix" matrices nil ))nil ))nil 3615632440"" (skeep)"" (skeep)"" (rewrite "rows_mult" )"" (rewrite "columns_mult" )"1" (assert ) nil nil )"2" (typepred "Q3" )"2" (expand "rows" )"2" (expand "length" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )"int" integers nil )"FullMatrix" matrices nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[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 )"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 matrices nil ))nil ))nil 3615632440"" (skeep)"" (skeep)"" "ut" "upper_triangulate(rows(S)) ") "" (replace -1)"" "dt" "diagonalize(rows(S)) ") "" (replaces -1)"" (hide -1)"" (assert )"" (typepred "ut" )"" (typepred "dt" )"" (assert )"" (replace -11 :dir rl)"" (replace -12 :dir rl)"" (replace -13 :dir rl)"" replace -14 :dir rl)"" replace -15 :dir rl)"" replace -16 :dir rl)"" "1" assert )"1" "1" assert )"1" "k" "p" )"1" assert )"1" case "k < p" )"1" assert )nil nil )"2" expand "upper_triangular?" )"2" "k" "p" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" rewrite "matrix_mult_assoc" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" "Q2" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" rewrite "mult_simple_prod" )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" rewrite "matrix_mult_assoc" )"1" rewrite "matrix_mult_assoc" )"1" rewrite "matrix_mult_assoc" "1" "1" replace -8)"1" rewrite "mult_Id_left" )"1" rewrite "matrix_mult_assoc" "1" replace -16)"1" rewrite "mult_Id_left" )"1" assert )"1" rewrite "mult_simple_prod" )nil nil ))nil ))nil ))nil )"2" "R2" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "Q3" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "Q2" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "R3" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" assert )"4" "4" assert )"4" "1" "1" "det_upper_triangular_zero" )"1" "S3" )"1" assert )"1" "p" )"1" assert )"1" "k" "p" )"1" assert )"1" expand "upper_triangular?" )"1" "k" "p" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "det_upper_triangular_zero" )"2" "S3" )"2" assert )"2" "k" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" "det_upper_triangular_zero" )"5" "S3" )"5" assert )"5" "5" "i!1" "i!1" )"5" 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 )"FullMatrix" matrices nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil matrix_det nil )nil matrices nil )nil matrices nil )nil matrix_det nil )"{SGI: [SquareMatrix(pn), SquareMatrix(pn), SquareMatrix(pn)] | NOT stop_rec) IMPLIESLET (S2, Q2, R2) = SGI INAND (FORALL (k):AND (FORALL (k, p):AND k < rows(S2) AND k < p IMPLIESOR entry(S2)(k, p) = 0))AND (comp_matrix IMPLIESAND is_simple_prod?(pn, FALSE, FALSE)(Q2))AND (comp_matrix AND comp_inverse IMPLIESAND AND AND det(S2) = det(S))}" matrix_diag nil) "bool" matrix_diag nil )"bool" matrix_diag nil )"(total_order?[real])" nil )"int" integers 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 matrices nil )nil integers nil )nil integers nil )"bool" matrix_det nil )"bool" booleans nil )"[bool, bool -> bool]" booleans 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 )IF const-decl "[boolean, T, T -> T]" if_def nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )"bool" matrix_upper_triang nil )"bool" matrix_upper_triang nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" matrix_det nil )"real" matrix_props nil )"{SGI: [SquareMatrix(pn), SquareMatrix(pn), SquareMatrix(pn)] | NOT stop_rec) IMPLIESLET (S2, Q2, R2) = SGI INAND AND is_simple_prod?(pn, FALSE, FALSE)(Q2))AND AND comp_inverse IMPLIESAND AND AND det(S2) = det(S))}" matrix_upper_triang nil) nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3615715272"" (skeep)"" (name "DD" "diag(comp_matrix, comp_inverse, S)" )"" (replaces -1)"" (typepred "DD" )"" (assert )"" (hide -6)"" (name "AA" "DD`ans" )"" (replaces -1)"" (name "QQ" "DD`multip" )"" (replaces -1)"" (assert )"" (lemma "det_upper_triangular_zero" )"" (inst - "AA" )"" (assert )"" case "EXISTS (i): i<rows(AA) AND entry(AA)(i,i)=0 AND (FORALL (j): j<rows(AA) AND j>i IMPLIES entry(AA)(j,j)/=0)" )"1" "1" "1" "i" )"1" assert )"1" "1" case "NOT j < rows(S)" )"1" assert )"1" rewrite "entry_eq_0" nil nil ))nil )"2" assert )"2" case "j = i" )"1" (assert ) nil nil )"2" case "j < i" )"1" expand "upper_triangular?" )"1" "i" "j" )"1" assert )nil nil ))nil ))nil )"2" "j" )"2" assert )"2" "2" "i" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (k): LET z = rows(AA)-1-k IN (k<=rows(AA)-1 AND (EXISTS (i): i<rows(AA) AND i>=z AND entry(AA)(i,i)=0)) IMPLIES (EXISTS (i): i<rows(AA) AND i>=z AND entry(AA)(i,i)=0 AND (FORALL (j): j<rows(AA) AND j>i IMPLIES entry(AA)(j,j)/=0))" )"1" "rows(AA)-1" )"1" assert )"1" replace -2)"1" (propax) nil nil ))nil ))nil ))nil )"2" "2" "2" "k" )"1" assert )"1" (ground) nil nil ))nil )"2" (assert ) nil nil )"3" assert )"3" (ground) nil nil ))nil )"4" (assert ) nil nil )"5" "5" "i!1" )"5" assert )"5" "5" assert )nil nil ))nil ))nil ))nil ))nil )"6" "k" )"6" assert )"6" "6" assert )"6" "6" case "NOT i!1 = rows(AA)-2-k" )"1" "1" assert )"1" "1" "i!2" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" case "(EXISTS (i): AND i >= rows(AA) - 1 - k AND entry(AA)(i, i) = 0)") "1" assert )"1" replace "1" assert )"1" "1" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{SGI: AND (FORALL (k, p):AND p < rows(S) AND entry(SGI`ans)(k, p) /= 0OR (k < p AND entry(SGI`ans)(p, p) = 0)))AND (comp_matrix IMPLIESAND AND (comp_matrix AND comp_inverse IMPLIESAND AND AND det(SGI`ans) = det(S)AND (det(S) /= 0 IFFAND p < rows(S) IMPLIES" nil )"[bool, bool -> bool]" booleans nil )"real" matrix_props nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" booleans nil )"bool" matrix_det nil )nil integers nil )nil integers 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 )"real" matrices nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )"bool" matrix_det nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil ) (> const-decl "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 )"nat" matrices nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 defined_types nil )nil booleans nil )nil booleans nil )nil list_adt nil )nil numbers nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_det nil )nil defined_types nil )nil naturalnumbers nil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"FullMatrix" matrices nil ))nil 3615720345"" (skeep)"" (name "DD" "diag(true, true, S)" )"" (label "DDname" -1)"" (typepred "DD" )"" (name "QQ" "DD`multip" )"" (replaces -1)"" (assert )"" (name "AA" "DD`ans" )"" (lemma "diag_det_zero_row" )"" (inst - "S" "true" "true" )"" (replace -2)"" (assert )"" (replace "DDname" )"" (replace -2)"" "sz" -1)"" "sz" )"" "" "II" "DD`inv" )"" "" case "NOT S = II*AA" )"1" case "NOT II*(QQ*S)=II*AA" )"1" (assert ) nil nil )"2" rewrite "matrix_mult_assoc" "1" replace -6)"1" rewrite "mult_Id_left" )nil nil ))nil )"2" "QQ" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "det(AA*R)=det(AA)*det(R)" )"1" replace -2 1)"1" rewrite "matrix_mult_assoc" "1" rewrite "det_mult_simple_prod_left" "1" "det_mult_simple_prod_left" )"1" "rows(S)" "II" "AA" )"1" assert )nil nil ))nil ))nil )"2" rewrite "rows_mult" )"2" rewrite "columns_mult" )"1" assert )nil nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "det(AA)=0" )"1" replace -1)"1" assert )"1" "1" "sz" )"1" assert )"1" "det_replace_row_scal" )"1" "1" "AA*R" "i" "0" "zero(rows(S))" )"1" case "AA*R = replace_row(i, 0 * zero(rows(S)))(AA * R)" )"1" assert )"1" rewrite "columns_mult" "1" assert )"1" rewrite "rows_mult" "1" assert )nil nil ))nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" rewrite "full_matrix_eq" "2" "2" case "NOT (i!1 < rows(S) AND j!1 < rows(S))" )"1" "i!1" )"1" "j!1" )"1" rewrite "columns_mult" )"1" rewrite "rows_mult" )"1" assert )nil nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "entry_replace_row" )"1" "1" "1" "1" replace "1" assert )"1" rewrite "access_scal" )"1" assert )"1" case "FORALL (rrrrr:real): 0*rrrrr=0" )"1" rewrite "1" "1" rewrite "entry_mult" "1" expand "*" "1" rewrite "dot_eq_sigma" "1" rewrite "sigma_restrict_eq_0" )"1" "1" "1" rewrite "access_row" )"1" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" rewrite "columns_mult" )"1" rewrite "length_scal_vect" )"1" assert )nil nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "columns_mult" "1" rewrite "rows_mult" "1" assert )nil nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "rows_mult" )"2" rewrite "columns_mult" )"1" assert )nil nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "isdiag" "LAMBDA (k): (LAMBDA (SQ): (FORALL (i): i<rows(SQ) AND i>=k IMPLIES entry(SQ)(i,i)=1) AND (FORALL (i,j): i<rows(SQ) AND j<rows(SQ) AND entry(SQ)(i,j)/=0 IMPLIES i=j))" )"2" case "FORALL (k,SQ,DQ): k<=rows(SQ) AND isdiag(k)(SQ) AND rows(SQ)=rows(DQ) IMPLIES det(SQ*DQ)=det(SQ)*det(DQ)" )"1" "rows(AA)" "AA" "R" )"1" assert )"1" "1" expand "isdiag" )"1" "1" "1" assert )nil nil ))nil )"2" "2" "det_upper_triangular_zero" )"2" "AA" )"2" assert )"2" "i" "j" )"2" assert )"2" "2" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "k" )"1" "1" case "SQ = Id(rows(SQ))" )"1" replace "1" rewrite "mult_Id_left" )"1" rewrite "det_Id" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "full_matrix_eq" )"2" assert )"2" "2" "i" )"2" "j" )"2" assert )"2" rewrite "entry_Id" )"2" expand "isdiag" )"2" "2" "2" "1" "1" "i" "j" )"1" assert )nil nil ))nil ))nil )"2" "2" "i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" assert )"2" "rr" "entry(SQ)(j,j)" )"2" "newSQ" "form_matrix(lambda (k,p): IF k=p AND k<j THEN entry(SQ)(k,k) ELSIF k=p THEN 1 ELSE 0 ENDIF,rows(SQ),columns(SQ))" )"2" case "SQ = Esr(rows(SQ))(j,rr)*newSQ" )"1" replace "1" rewrite "matrix_mult_assoc" )"1" rewrite "mult_Esr_left" )"1" rewrite "mult_Esr_left" )"1" rewrite "det_replace_row_scal" )"1" rewrite "det_replace_row_scal" )"1" rewrite "replace_row_id" )"1" rewrite "replace_row_id" )"1" "newSQ" "DQ" )"1" assert )"1" "1" expand "isdiag" )"1" "1" case "rows(newSQ)=rows(SQ) AND columns(newSQ)=columns(SQ)" )"1" "1" assert )"1" "1" "1" expand "newSQ" "1" rewrite "entry_form_matrix" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "newSQ" "2" rewrite "entry_form_matrix" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "newSQ" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" rewrite "rows_mult" "2" assert )nil nil ))nil ))nil )"2" rewrite "length_row" )nil nil ))nil )"2" rewrite "length_row" )"2" rewrite "columns_mult" )"1" rewrite "rows_mult" )"1" assert )nil nil ))nil )"2" "newSQ" )"2" expand "rows" )"2" nil nil ))nil ))nil ))nil ))nil )"3" rewrite "rows_mult" )"3" assert )nil nil ))nil ))nil )"2" rewrite "rows_mult" )"2" assert )nil nil ))nil )"3" rewrite "rows_mult" )"3" rewrite "columns_mult" )"1" assert )nil nil )"2" "newSQ" )"2" "rows_form_matrix" )"2" "2" expand "rows" "2" assert )"2" case "NOT rows(SQ) = 0" )"1" replace "1" expand "length" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "newSQ" )"2" rewrite "rows_form_matrix" )nil nil ))nil )"3" "1" assert )"1" expand "newSQ" "1" rewrite "rows_form_matrix" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "newSQ" "2" assert )"2" "columns_form_matrix" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "newSQ" )"2" "rows_form_matrix" )"2" "2" expand "length" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "full_matrix_eq" "2" assert )"2" "1" rewrite "rows_mult" )"1" rewrite "rows_Esr" )nil nil ))nil )"2" rewrite "columns_mult" )"1" expand "newSQ" "1" "columns_form_matrix" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "Esr(rows(SQ))(j,rr)" )"2" expand "rows" "2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" rewrite "mult_Esr_left" )"1" rewrite "entry_replace_row" )"1" rewrite "access_scal" )"1" "1" "1" "1" replace "1" assert )"1" rewrite "access_row" )"1" expand "newSQ" "1" rewrite "entry_form_matrix" )"1" assert )"1" "1" expand "isdiag" "1" "1" "1" "1" "1" replace "1" assert )nil nil ))nil ))nil )"2" "2" "j" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "newSQ" "2" rewrite "rows_form_matrix" )"2" rewrite "entry_form_matrix" )"2" "2" "2" "2" assert )"2" "1" nil nil )"2" "2" "1" "1" "1" assert )"1" "1" expand "isdiag" "1" "1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "isdiag" "2" "2" "i!1" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "newSQ" "2" "columns_form_matrix" )"2" "2" assert )"2" "2" rewrite "length_scal_vect" )"2" rewrite "length_row" )"2" rewrite "rows_form_matrix" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "newSQ" "2" rewrite "rows_form_matrix" )nil nil ))nil )"3" expand "newSQ" "3" rewrite "rows_form_matrix" )"3" assert )"3" "columns_form_matrix" )"3" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" booleans nil )"{SGI: AND (FORALL (k, p):AND p < rows(S) AND entry(SGI`ans)(k, p) /= 0OR (k < p AND entry(SGI`ans)(p, p) = 0)))AND (comp_matrix IMPLIESAND AND (comp_matrix AND comp_inverse IMPLIESAND AND AND det(SGI`ans) = det(S)AND (det(S) /= 0 IFFAND p < rows(S) IMPLIES" nil )"[bool, bool -> bool]" booleans nil )"real" matrix_props nil )"{M: SquareMatrix(pm) | IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)AND AND " nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" booleans nil )"bool" matrix_det nil )nil integers nil )nil integers 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 )"real" matrices nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )"bool" matrix_det nil )nil matrices nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil ) (> const-decl "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 )"nat" matrices nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 defined_types nil )nil booleans nil )nil booleans nil )nil list_adt nil )nil numbers nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrices nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"SquareMatrix(pn)" matrix_det nil )nil matrices nil )nil matrices nil )"{M: MatrixMN(rows(SQ), columns(SQ)) | IF i = j_1 AND i < j THEN entry(SQ)(i, i)" matrix_diag nil) "nat" matrix_diag nil )"Square" matrix_diag nil )nil matrix_props nil )nil matrix_props nil )nil matrices nil )nil matrix_det nil )nil matrix_det nil )"{M: MatrixMN(m, n) | " nil )"FullMatrix" matricesnil )"posint" nil )nil matrices nil )nil matrix_props nil )nil naturalnumbers nil )nil defined_types nil )nil matrix_det nil )"[nat -> [Square -> boolean]]" 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 matrices nil )nil matrices nil )nil matrices nil )"(total_order?[real])" nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(total_order?[real])" nil )nil integers nil )nil matrices nil )nil sigma "reals/" )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/" )nil matrices nil )nil matrix_props nil )nil matrices nil )"VectorN(n)" matrices nil )"Square" matrix_diag nil )"SquareMatrix(rows(S))" matrix_diag nil )"Square" matrix_diag nil )nil matrix_props nil )nil matrix_det nil )nil matrices nil )nil matrices nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil matrix_diag nil )"FullMatrix" matrices nil )"real" reals nil ))nil )nil 3614353622"" (skeep)"" (name "DD" "diag(true, true, S)" )"" (label "DDname" -1)"" (typepred "DD" )"" (name "QQ" "DD`multip" )"" (replaces -1)"" (assert )"" (name "AA" "DD`ans" )"" (lemma "diag_det_zero_row" )"" (inst - "S" "true" "true" )"" (replace -2)"" (assert )"" (replace "DDname" )"" (replace -2)"" "sz" -1)"" "sz" )"" "" "II" "DD`inv" )"" "" case "NOT S = II*AA" )"1" case "NOT II*(QQ*S)=II*AA" )"1" (assert ) nil nil )"2" rewrite "matrix_mult_assoc" "1" replace -6)"1" rewrite "mult_Id_left" )nil nil ))nil )"2" "QQ" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "det(AA*R)=det(AA)*det(R)" )"1" replace -2 1)"1" rewrite "matrix_mult_assoc" "1" rewrite -10 1)"1" rewrite -10 1)nil nil )"2" rewrite "rows_mult" )"2" rewrite "columns_mult" "1" assert )nil nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "det(AA)=0" )"1" replace -1)"1" assert )"1" "1" "sz" )"1" assert )"1" "det_replace_row_scal" )"1" "1" "AA*R" "i" "0" "zero(rows(S))" )"1" case "AA*R = replace_row(i, 0 * zero(rows(S)))(AA * R)" )"1" assert )"1" rewrite "columns_mult" "1" assert )"1" rewrite "rows_mult" "1" assert )nil nil ))nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" rewrite "full_matrix_eq" "2" "2" case "NOT (i!1 < rows(S) AND j!1 < rows(S))" )"1" "i!1" )"1" "j!1" )"1" rewrite "columns_mult" )"1" rewrite "rows_mult" )"1" assert )nil nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "entry_replace_row" )"1" "1" "1" "1" replace "1" assert )"1" rewrite "access_scal" )"1" assert )"1" case "FORALL (rrrrr:real): 0*rrrrr=0" )"1" rewrite "1" "1" rewrite "entry_mult" "1" rewrite "dot_eq_sigma" "1" rewrite "sigma_restrict_eq_0" )"1" "1" "1" rewrite "access_row" )"1" "i!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" rewrite "columns_mult" )"1" rewrite "length_scal_vect" )"1" assert )nil nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "columns_mult" "1" rewrite "rows_mult" "1" assert )nil nil ))nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "rows_mult" )"2" rewrite "columns_mult" )"1" assert )nil nil )"2" "AA" )"2" expand "rows" )"2" expand "length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "isdiag" "LAMBDA (k): (LAMBDA (SQ): (FORALL (i): i<rows(SQ) AND i>=k IMPLIES entry(SQ)(i,i)=1) AND (FORALL (i,j): i<rows(SQ) AND j<rows(SQ) AND entry(SQ)(i,j)/=0 IMPLIES i=j))" )"2" case "FORALL (k,SQ,DQ): k<=rows(SQ) AND isdiag(k)(SQ) AND rows(SQ)=rows(DQ) IMPLIES det(SQ*DQ)=det(SQ)*det(DQ)" )"1" "rows(AA)" "AA" "R" )"1" assert )"1" "1" expand "isdiag" )"1" "1" "1" assert )nil nil ))nil )"2" "2" "det_upper_triangular_zero" )"2" "AA" )"2" assert )"2" "i" "j" )"2" assert )"2" "2" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "k" )"1" "1" case "SQ = Id(rows(SQ))" )"1" replace "1" rewrite "mult_Id_left" )"1" rewrite "det_Id" )"1" assert )nil nil ))nil ))nil ))nil )"2" rewrite "full_matrix_eq" )"2" assert )"2" "2" "i" )"2" "j" )"2" assert )"2" rewrite "entry_Id" )"2" expand "isdiag" )"2" "2" "2" "1" "1" "i" "j" )"1" assert )nil nil ))nil ))nil )"2" "2" "i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" assert )"2" "rr" "entry(SQ)(j,j)" )"2" "newSQ" "form_matrix(lambda (k,p): IF k=p AND k<j THEN entry(SQ)(k,k) ELSIF k=p THEN 1 ELSE 0 ENDIF,rows(SQ),columns(SQ))" )"2" case "SQ = Esr(rows(S))(j,rr)*newSQ" )"1" replace "1" rewrite "matrix_mult_assoc" )"1" rewrite "mult_Esr_left" )"1" rewrite "mult_Esr_left" )"1" rewrite "det_replace_row_scal" )"1" rewrite "det_replace_row_scal" )"1" rewrite "replace_row_id" )"1" rewrite "replace_row_id" )"1" "newSQ" "DQ" )"1" assert )"1" "1" expand "isdiag" )"1" "1" case "rows(newSQ)=rows(SQ) AND columns(newSQ)=columns(SQ)" )"1" "1" assert )"1" "1" "1" expand "newSQ" "1" rewrite "entry_form_matrix" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "newSQ" "2" rewrite "entry_form_matrix" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "newSQ" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" rewrite "rows_mult" "2" assert )nil nil ))nil ))nil )"2" rewrite "length_row" )nil nil ))nil )"2" rewrite "length_row" )"2" rewrite "columns_mult" )"1" rewrite "rows_mult" )"1" assert )nil nil ))nil )"2" "newSQ" )"2" expand "rows" )"2" nil nil ))nil ))nil ))nil ))nil )"3" rewrite "rows_mult" )"3" assert )nil nil ))nil ))nil )"2" rewrite "rows_mult" )"2" assert )"2" expand "newSQ" "2" rewrite "rows_form_matrix" )"2" nil nil ))nil ))nil ))nil ))nil )"3" nil nil )"4" nil nil ))nil )"2" nil nil )"3" nil nil )"4" nil nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak)))
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.554Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
