Quelle matrix_props.prf
Sprache: Lisp
(matrix_propsnil 3615814158"" (skeep)"" (rewrite "full_matrix_eq" )"1" (split)"1" (grind :exclude "entry" ) nil nil )"2" (grind :exclude "entry" ) nil nil )"3" (skosimp*)"3" (case "(i!1=0 OR i!1=1) AND (j!1 = 0 OR j!1=1)" )"1" (ground)"1" (replaces -1)"1" (replaces -1)"1" (expand "entry" + 2)"1" (grind :exclude "entry" ) nil nil )) nil ))nil ))nil )"2" (replaces -1)"2" (replaces -1)"2" (expand "entry" + 2)"2" (grind :exclude "entry" ) nil nil )) nil ))nil ))nil )"3" (replaces -1)"3" (replaces -1)"3" (expand "entry" + 2)"3" (grind :exclude "entry" ) nil nil )) nil ))nil ))nil )"4" (replaces -1)"4" (replaces -1)"4" (expand "entry" + 2)"4" (grind :exclude "entry" ) nil nil )) nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (case "(i!1=0 OR i!1=1) AND (j!1 = 0 OR j!1=1)" )"1" (ground)"1" (replaces -1)"1" (replaces -1)"1" (expand "entry" + 2)"1" (grind :exclude "entry" ) nil nil )) nil ))nil ))nil )"2" (replaces -1)"2" (replaces -1)"2" (expand "entry" + 2)"2" (grind :exclude "entry" ) nil nil )) nil ))nil ))nil ))nil )"2" (replaces -1)"2" (replaces -1)"2" (expand "entry" + 2)"2" (typepred "i!1" )"2" (typepred "j!1" )"2" (hide 2)"2" (grind :exclude "entry" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"real" matrices nil )"(null?)" list_adt nil )"(total_order?[real])" nil )"real" matrices nil )"Vector" matrices nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3614701537"" (skeep)"" (expand "row" )"" (expand "rows" )"" (lift-if)"" (ground)"" (typepred "columns(SM)" )"" (assert )"" (split -)"1" (grind) nil nil )"2" (skosimp*)"2" (typepred "SM" )"2" (split -)"1" (grind) nil nil )"2" (inst - "i" "i!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Vector" matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )"nat" list_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ) (< const-decl "bool" reals nil )nil naturalnumbers 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 )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )nil more_list_props "structures/" )"nat" matrices nil ))nil 3614702183"" (skeep)"" (lemma "length_row" )"" (inst - "SM" "i" )"" (assert )"" (expand "rows" )"" (assert )"" (expand "row" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil matrix_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"Vector" matrices nil )"nat" matrices nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )nil naturalnumbers nil )"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 3614702658 ("" (grind) 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 )"(strict_total_order?[real])" real_props nil )"nat" matrices nil ))nil ))nil 3614702658"" (skeep)"" (typepred "columns(cdr(D))" )"" (assert )"" (split -)"1" (grind) nil nil )"2" (skosimp*)"2" (typepred "columns(D)" )"2" (split -)"1" (grind) nil nil )"2" (skosimp*)"2" (typepred "D" )"2" (split -)"1" (grind) nil nil )"2" (inst - "i!1+1" "i!2" )"1" (assert )"1" (expand "nth" -1 1)"1" (ground) nil nil )) nil ))nil )"2" (expand "length" 1)"2" (assert )"2" (lift-if)"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )"{c: nat | AND AND c = 0 OR " nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )nil matrices nil )"T" list_props nil )nil nat_types nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )"[(cons?) -> list]" list_adt nil )"[list -> boolean]" list_adt nil )"nat" list_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ) (< const-decl "bool" reals nil )nil naturalnumbers 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 )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"posint" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"PosFullMatrix" matrix_props nil )"below(length(cdr(D)))" matrix_props nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil ))nil 3614939393"" (induct "M" )"1" (grind) nil nil )"2" (skolem 1 ("m1" "M" ))"2" (flatten) (("2" (grind) nil nil )) nil )) nil ))nil )nil list_adt 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 reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"{c: nat | AND AND c = 0 OR " nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"T" list_props nil )nil nat_types nil )"bool" reals 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 )"[T, T -> boolean]" equalities nil )nil matrices nil )nil matrices nil ))nil 3615029745"" (skeep)"" (expand "access" )"" (lift-if)"" (lift-if)"" (lift-if)"" (ground)"1" (lemma "col_def" )"1" (inst?)"1" (assert )"1" (inst - "j" )"1" (replaces -1)"1" (lift-if)"1" (ground)"1" (expand "row" 1)"1" "1" "1" rewrite "length_col" )"1" expand "rows" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_nth_row" )"1" (rewrite "length_row" ) nil nil )"2" rewrite "length_col" )"2" expand "rows" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "length_row" )"2" (rewrite "length_col" )"2" (assert )"2" (lemma "col_def" )"2" (inst?)"2" (assert )"2" (inst?)"2" (assert )"2" "2" "2" rewrite "length_nth_row" )"2" expand "rows" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (rewrite "length_col" )"3" (rewrite "length_row" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" matrices nil )"(strict_total_order?[real])" real_props nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"nat" matrices nil )nil matrix_props nil )nil matrix_props nil )"Vector" matrices nil )"(total_order?[real])" nil )nil matrices nil )nil matrices nil ))nil 3614083040"" (skeep)"" (ground)"1" (grind) nil nil )"2" (skeep 1)"2" (rewrite "columns_0_entry" )"1" (rewrite "columns_0_entry" ) nil nil )"2" (expand "columns" 1) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil )"nat" list_props nil )"Vector" matrices nil )"real" matrices nil )"real" matrices nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )nil reals nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"posint" nil )"(total_order?[real])" nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"{c: nat | AND AND c = 0 OR " nil ))nil ))nil 3614083040 ("" (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 )"int" integers nil )"(total_order?[real])" nil )"nat" matrices nil ))nil ))nil 3614083040 ("" (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 )"int" integers nil )"(total_order?[real])" nil )"nat" matrices nil ))nil ))nil 3614083040"" (skeep)"" (assert )"" (ground)"1" (rewrite "rows_form_matrix" 1) nil nil )"2" (lemma "columns_form_matrix" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil )"3" (skosimp*)"3" (rewrite "entry_form_matrix" )"3" (lift-if)"3" (split)"1" (propax) nil nil )"2" (flatten)"2" (rewrite "entry_eq_0" )"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (assert ) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"FullMatrix" matricesnil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )nil matrices nil )"(total_order?[real])" nil )"posint" nil )nil matrices nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil 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 )"nat" matrices nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"[T, T -> boolean]" equalities nil )"{c: nat | AND AND c = 0 OR " nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3614602887"" (skeep)"" (skosimp*)"" (name "R" "remove(D,i,j)" )"" (replace -1)"" (assert )"" (expand "remove" -1)"" (invoke (name "FZ" "%1" ) (! -1 1))"" (replaces -1)"" (typepred "FZ" )"" (assert )"" (copy -5)"" (inst - "i!1" "j!1" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"int" integers nil )"FullMatrix" matricesnil )nil matrices nil )nil matrices nil )"Vector" matrices nil )"{M: MatrixMN(m, n) | " nil )"(total_order?[real])" nil )nil numbers nil )nil list_adt nil )nil booleans nil )"[T, T -> boolean]" equalities 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 )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"{c: nat | AND AND c = 0 OR " nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )nil matrices nil )nil matrices nil ))nil ))nil 3615024326"" (skeep)"" (expand "remove" )"" (lift-if)"" (ground)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (rewrite "rows_form_matrix" ) nil nil ))nil ))nil ))nil ))nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )"FullMatrix" matricesnil )"int" integers nil )"posint" nil )"nat" matrices nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"{c: nat | AND AND c = 0 OR " nil )"[T, T -> boolean]" equalities nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"T" list_props nil )nil nat_types nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrices nil )"posint" nil )"(total_order?[real])" nil ))nil 3615024543"" (skeep)"" (expand "remove" )"" (lift-if)"" (ground)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (lemma "columns_form_matrix" )"3" (inst?)"3" (assert )"3" (lift-if)"3" (ground)"1" (replace -2)"1" (expand "form_matrix" 1)"1" (expand "array2list" + 1)"1" (expand "array2list_it" )"1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (case "rows(M)=1" )"1" (replaces -1)"1" (assert )"1" (expand "form_matrix" 1)"1" (expand "array2list" + 1)"1" expand "array2list_it" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )"FullMatrix" matricesnil )"int" integers nil )"(total_order?[real])" nil )"{c: nat | AND AND c = 0 OR " nil )"nat" matrices nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(total_order?[real])" nil )"posint" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil 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 )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"[T, T -> boolean]" equalities nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integersnil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" "structures/" )"{M: MatrixMN(m, n) | " nil )nil matrices nil ))nil 3614609488"" (skeep)"" (lemma "full_matrix_eq" )"" (inst?)"1" (assert )"1" (hide 2)"1" (invoke (case "NOT %1" ) (! 1 1))"1" (hide 2)"1" (assert )"1" (typepred "remove(D,1,1+n)" )"1" (assert )"1" (assert )"1" (flatten)"1" (typepred "remove(D,0,m)" )"1" (assert )"1" "1" assert )"1" "remove(remove(D, 1, 1 + n), 0, m)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 0, m), 0, n)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (invoke (case "NOT %1" ) (! 1 1))"1" (hide 2)"1" (assert )"1" (typepred "remove(D,1,1+n)" )"1" (assert )"1" (assert )"1" (flatten)"1" "remove(D,0,m)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 1, 1 + n), 0, m)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 0, m), 0, n)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skosimp*)"2" "remove(remove(D, 1, 1 + n), 0, m)" )"2" (assert )"2" (hide (-1 -2))"2" (inst?)"2" "2" assert )"2" "remove(remove(D, 0, m), 0, n)" )"2" "2" "2" "2" assert )"2" "remove(D,1,1+n)" )"2" "2" "2" "2" "remove(D,0,m)" )"2" "2" "2" "2" assert )"2" "2" "remove(D,1,1+n)" )"2" "2" assert )"2" "2" "remove(D,0,m)" )"2" "2" assert )"2" "2" "remove(remove(D, 1, 1 + n), 0, m)" )"2" "2" assert )"2" "2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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" (lemma "remove_posfullmatrix" )"2" (inst?)"1" (split -)"1" (propax) nil nil ) ("2" (propax) nil nil )) nil )"2" (typepred "remove(D,0,m)" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"3" (flatten)"3" (lemma "remove_posfullmatrix" )"3" (inst?)"1" (assert ) nil nil )"2" (typepred "remove(D,1,1+n)" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil matrix_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )OR const-decl "[bool, 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 reals nil )"[list -> boolean]" list_adt nil )nil matrices nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )"[T, T -> boolean]" equalities nil )"{c: nat | AND AND c = 0 OR " nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )nil matrices nil )nil matrices nil )"PosFullMatrix" matrix_props nil )"nat" matrix_props nil )"nat" matrix_props nil )"posint" nil )"FullMatrix" nil ))nil 3614612404"" (skeep)"" (lemma "full_matrix_eq" )"" (inst?)"1" (assert )"1" (hide 2)"1" (invoke (case "NOT %1" ) (! 1 1))"1" (hide 2)"1" (assert )"1" (typepred "remove(D,1,0)" )"1" (assert )"1" (assert )"1" (flatten)"1" (typepred "remove(D,0,1+n)" )"1" (assert )"1" "1" assert )"1" "remove(remove(D, 1, 0), 0, n)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 0, 1+n), 0, 0)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (invoke (case "NOT %1" ) (! 1 1))"1" (hide 2)"1" (assert )"1" (typepred "remove(D,1,0)" )"1" (assert )"1" (assert )"1" (flatten)"1" "remove(D,0,1+n)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 1, 0), 0, n)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 0, 1+n), 0, 0)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skosimp*)"2" (typepred "remove(remove(D, 1, 0), 0, n)" )"2" (assert )"2" (hide (-1 -2))"2" (inst?)"2" "2" assert )"2" "remove(remove(D, 0, 1 + n), 0, 0)" )"2" "2" "2" "2" assert )"2" "remove(D,1,0)" )"2" "2" "2" "2" "remove(D,0,1+n)" )"2" "2" "2" "2" assert )"2" "2" "remove(D,1,0)" )"2" "2" assert )"2" "remove(D,0,1+n)" )"2" "2" "2" assert )"2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "remove_posfullmatrix" )"2" (inst?)"1" (split -)"1" (propax) nil nil ) ("2" (propax) nil nil )) nil )"2" (typepred "remove(D,0,1+n)" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"3" (flatten)"3" (lemma "remove_posfullmatrix" )"3" (inst?)"1" (assert ) nil nil )"2" (typepred "remove(D,1,0)" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil matrix_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )OR const-decl "[bool, 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 reals nil )"[list -> boolean]" list_adt nil )nil matrices nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )"[T, T -> boolean]" equalities nil )"{c: nat | AND AND c = 0 OR " nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )nil matrices nil )nil matrices nil )"PosFullMatrix" matrix_props nil )"nat" matrix_props nil )"posint" nil )"FullMatrix" nil ))nil ))nil 3614614465"" (skeep)"" (lemma "full_matrix_eq" )"" (inst?)"1" (assert )"1" (hide 2)"1" (invoke (case "NOT %1" ) (! 1 1))"1" (hide 2)"1" (assert )"1" (typepred "remove(D,1,n)" )"1" (assert )"1" (assert )"1" (flatten)"1" (typepred "remove(D,0,1+m+n)" )"1" (assert )"1" "1" assert )"1" "remove(remove(D, 1, n), 0, m + n)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 0, 1 + m + n), 0, n)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (invoke (case "NOT %1" ) (! 1 1))"1" (hide 2)"1" (assert )"1" (typepred "remove(D,1,n)" )"1" (assert )"1" (assert )"1" (flatten)"1" "remove(D,0,1+m+n)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 1, n), 0, m + n)" )"1" assert )"1" "1" assert )"1" "remove(remove(D, 0, 1 + m + n), 0, n)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skosimp*)"2" "remove(remove(D, 1, n), 0, m + n)" )"2" (assert )"2" (hide (-1 -2))"2" (inst?)"2" "2" assert )"2" "remove(remove(D, 0, 1 + m + n), 0, n)" )"2" "2" "2" "2" assert )"2" "remove(D,1,n)" )"2" "2" "2" "2" "remove(D,0,1+m+n)" )"2" "2" "2" "2" assert )"2" "2" "remove(D,1,n)" )"2" "2" assert )"2" "2" "remove(D,0,1+m+n)" )"2" "2" assert )"2" "2" "remove(remove(D, 1, n), 0, m + n)" )"2" "2" assert )"2" "2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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" (lemma "remove_posfullmatrix" )"2" (inst?)"1" (split -)"1" (propax) nil nil ) ("2" (propax) nil nil )) nil )"2" (typepred "remove(D,0,1+m+n)" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"3" (flatten)"3" (lemma "remove_posfullmatrix" )"3" (inst?)"1" (assert ) nil nil )"2" (typepred "remove(D,1,n)" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil matrix_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )OR const-decl "[bool, 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 reals nil )"[list -> boolean]" list_adt nil )nil matrices nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )"[T, T -> boolean]" equalities nil )"{c: nat | AND AND c = 0 OR " nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )nil matrices nil )nil matrices nil )"PosFullMatrix" matrix_props nil )"nat" matrix_props nil )"nat" matrix_props nil )"nonneg_int" nil )"FullMatrix" nil )"posint" nil ))nil ))nil 3614961120"" (skeep)"" (assert )"" (typepred "remove(M,i,j)" ) (("" (inst?) nil nil )) nil ))nil ))nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"[T, T -> boolean]" equalities nil )"{c: nat | AND AND c = 0 OR " nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil ))nil 3615047099 ("" (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 )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3615047100"" (skeep)"" (rewrite "full_matrix_eq" )"" (split)"1" (rewrite "rows_remove" ) (("1" (assert ) nil nil )) nil )"2" (rewrite "columns_remove" ) (("2" (assert ) nil nil )) nil )"3" (skosimp*)"3" (rewrite "entry_remove" )"3" (rewrite "entry_Id" )"3" (rewrite "entry_Id" )"3" (lift-if) (("3" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"FullMatrix" nil )"int" integers nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )nil integers nil )nil integers nil )nil matrices nil )nil matrices nil )nil matrices 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 matrices nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil matrix_props nil )nil matrix_props nil )"(total_order?[real])" nil )nil matrix_props nil ))nil 3614091324 ("" (eval-formula) nil nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil 3614091064 ("" (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 )"(total_order?[real])" nil )"int" integers nil )"nat" matrices nil ))nil ))nil 3614091064"" (skeep)"" (skeep)"" (typepred "remove(M,0,k)" )"" (case "rows(M)=0" )"1" (hide-all-but (-1 2)) (("1" (grind) nil nil )) nil )"2" (hide -1)"2" (assert )"2" (flatten)"2" (expand "rows" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"[T, T -> boolean]" equalities nil )"{c: nat | AND AND c = 0 OR " nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil ))nil ))nil 3614096607 ("" (grind) nil nil )"nat" list_props nil )"nat" matrices nil )"{c: nat | AND AND c = 0 OR " nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" exponentiation nil )"T" list_props nil )"Vector" matrices nil )"real" matrices nil )"real" matrices nil )"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" "structures/" )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"{M: MatrixMN(m, n) | " nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )"real" matrix_props nil )"real" exponentiation 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 )"real" sigma "reals/" )"real" reals nil )"posint" nil )"int" integers nil ))nil 3614958230"" (skeep) (("" (expand "det" ) (("" (assert ) nil nil )) nil )) nil )"real" matrix_props nil )) shostak))nil 3614700165 ("" (eval-formula) nil nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil 3614443657"" (skeep)"" (assert )"" (rewrite "rows_form_matrix" )"" (assert )"" (lemma "columns_form_matrix" )"" (inst?)"" (assert )"" "FM" "form_matrix(swap(i, j)(entry(D)), rows(D), columns(D))" )"" (replaces -1)"" (skeep)"" (expand "FM" 1)"" (rewrite "entry_form_matrix" )"" (lift-if)"" (lift-if)"" "" assert )"" expand "swap" 1)"" "entry_eq_0" )"" "D" "k" "p" )"" assert )"" "D" "i" "p" )"" "D" "j" "p" )"" (ground) 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" matricesnil )"{M: MatrixMN(m, n) | " nil )"Vector" matrices nil )nil matrices nil )nil matrices nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )nil matrices nil )"(total_order?[real])" nil )"{M: MatrixMN(rows(D), columns(D)) | " nil )nil matrices nil )"real" matrices nil )"real" matrix_props 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 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 matrices nil ))nil ))nil 3615020687"" (skeep)"" (expand "swap" + 1)"" (rewrite "entry_form_matrix" ) nil nil )) nil ))nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props 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 )"real" matrices nil )nil matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"real" matrix_props nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil matrices nil ))nil 3614697478"" (assert )"" (split)"1" (eval-formula) nil nil ) ("2" (eval-formula) nil nil )"3" (eval-formula) nil nil ))nil ))nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil ))nil 3614697479 ("" (eval-formula) nil nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil ))nil 3614602382"" (skeep)"" (name "S" "swap(0,1)(D)" )"" (replace -1)"" (name "RS" "remove(S,0,n)" )"" (replace -1)"" (name "RD" "remove(D,1,n)" )"" (replace -1)"" (lemma "full_matrix_eq" )"" (inst - "RS" "RD" )"1" (assert )"1" (hide 2)"1" (case "NOT rows(RS)=rows(RD)" )"1" (hide 2)"1" (typepred "RS" )"1" assert )"1" "1" "RD" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "NOT columns(RS)=columns(RD)" )"1" "RS" )"1" "RD" )"1" assert )"1" "S" )"1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "i!1" )"2" "j!1" )"2" "RS" )"2" "2" "2" "2" "RD" )"2" "2" "2" "2" assert )"2" "S" )"2" assert )"2" "2" "2" "2" "2" "2" "2" "2" assert )"2" "2" "2" assert )"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 )"2" (flatten)"2" (skosimp*)"2" (typepred "RS" )"2" (lemma "remove_posfullmatrix" )"2" (inst - "S" "0" "n" )"2" assert )"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 )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )"{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 naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil list_adt nil )nil numbers nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"FullMatrix" nil )nil matrices nil )nil matrix_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"PosFullMatrix" matrix_props nil )"{PFM | AND AND AND 1 < rows(D) IMPLIESIF k = 0 THEN entry(D)(1, p)" matrix_props nil) "nat" matrix_props nil )"{N | AND columns(S) > 1 IMPLIESAND columns(N) = columns(S) - 1))AND IF n_1 >= n OR n >= columns(S) THEN 1 + n_1" matrix_props nil)) nil 3614689741"" (skeep)"" (typepred "remove(D,0,n)" )"" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil matrices nil )nil matrices nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"{c: nat | AND AND c = 0 OR " nil )"[T, T -> boolean]" equalities nil )"[list -> boolean]" list_adt nil )OR const-decl "[bool, bool -> bool]" booleans nil )"T" list_props nil )nil nat_types nil )"bool" reals nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"[bool, bool -> bool]" booleans 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 list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"FullMatrix" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3614689741 ("" (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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nat" matrices nil )"boolean" notequal nil ))nil ))nil 3614689741 ("" (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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nat" matrices nil )"boolean" notequal nil ))nil ))nil 3614689742"" (skeep)"" (rewrite "full_matrix_eq" )"" (assert )"" (invoke (case "NOT %1" ) (! 3 1))"1" (hide 4)"1" (typepred "remove(swap(i, j)(D), 0, n)" )"1" (assert )"1" (flatten)"1" (assert )"1" (replaces -2)"1" (typepred "remove(D,0,n)" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (invoke (case "NOT %1" ) (! 3 1))"1" (hide 4)"1" (typepred "remove(swap(i, j)(D), 0, n)" )"1" (assert )"1" (flatten)"1" (assert )"1" (typepred "remove(D,0,n)" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skosimp*)"2" (typepred "remove(swap(i, j)(D), 0, n)" )"2" (assert )"2" (flatten)"2" (hide (-1 -5))"2" (inst?)"2" (replaces -3)"2" assert )"2" "swap(i - 1, j - 1)(remove(D, 0, n))" )"2" "2" assert )"2" "2" "2" assert )"2" "remove(D,0,n)" )"2" rewrite -3)"2" rewrite -3)"2" rewrite -3)"2" assert )"2" "2" "2" "swap(i,j)(D)" )"2" assert )"2" "2" rewrite "2" "2" "2" "2" assert )"2" "2" "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 ))nil ))nil ))nil )"(total_order?[real])" nil )"FullMatrix" nil )"int" integers nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )nil matrices nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) "(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil 3614688578"" (skeep)"" (rewrite "full_matrix_eq" )"" (assert )"" (skosimp*)"" (expand "swap" +)"" (rewrite "entry_form_matrix" )"" (rewrite "entry_form_matrix" )"" (expand "swap" )"" (lift-if)"" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) nil matrices nil )"real" matrix_props nil )"(strict_total_order?[real])" real_props nil ))nil 3614509198"" (skeep)"" (case "rows(D)/=columns(D)" )"1" (flatten)"1" (expand "det" + 2)"1" (assert )"1" (expand "det" +) (("1" (propax) nil nil )) nil )) nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (case "rows(D) = 2" )"1" case "EXISTS (a,b,c,d:real): D = (:(:a,b:),(:c,d:):)" )"1" (skeep)"1" (replaces -1) (("1" (grind) nil nil )) nil )) nil )"2" (hide (-3 2))"2" (typepred "D" )"2" "entry(D)(0,0)" "entry(D)(0,1)" "entry(D)(1,0)" "entry(D)(1,1)" )"2" (rewrite "list_extensionality[list[real]]" )"2" (splash +)"1" (skosimp*)"1" (case "NOT (n!1 = 0 OR n!1=1)" )"1" (typepred "n!1" )"1" expand "rows" )"1" assert )"1" (ground) nil nil ))nil ))nil ))nil )"2" rewrite "list_extensionality[real]" 1)"2" "1" assert )"1" "1" (grind) nil nil )"2" case "NOT columns(D)=2" )"1" (assert ) nil nil )"2" "columns(D)" )"2" "1" (grind) nil nil )"2" "2" "n!1" "i!1" )"2" assert )"2" replace -4)"2" replace -1)"2" replace -3)"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "NOT (n!2 = 0 OR n!2 = 1)" )"1" "1" "n!2" )"1" "columns(D)" )"1" "1" (grind) nil nil )"2" "2" "1" (grind) nil nil )"2" "n!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT (rows(D)=2 AND columns(D)=2)" )"1" (assert ) nil nil )"2" expand "entry" )"2" expand "access" )"2" expand "row" )"2" rewrite "length_null" )"2" assert )"2" case "NOT length(D)=2" )"1" expand "rows" )"1" nil nil ))nil )"2" assert )"2" "2" case "null?(D)" )"1" nil nil )"2" assert )"2" "1" "1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil )"3" "3" "3" "3" nil nil ))nil ))nil ))nil )"4" "4" "4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 -2 -4))"2" (hide -3) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "NOT rows(D)>=3" )"1" (assert ) nil nil )"2" (hide (-3 1))"2" (copy -2)"2" (hide -3)"2" (name "S" "swap(0,1)(D)" )"2" (replaces -1)"2" (expand "det" )"2" (assert )"2" (lift-if)"2" "2" "2" "2" assert )"2" "1" "S" )"1" (grind) nil nil ))nil )"2" "S" )"2" (grind) nil nil ))nil )"3" "S" )"3" "3" case "NOT FORALL (rr:real): -rr = (-1)*rr" )"1" (assert ) nil nil )"2" "%1" )"2" "2" rewrite "sigma_scal" "2" expand "det" "2" case "NOT (%1 = (sigma(0, columns(D) - 1, LAMBDA (i: nat):LAMBDA (k):") "1" "1" rewrite "sigma_eq" )"1" "1" "1" "1" "1" "remove(D,0,n!1)" )"1" assert )"1" "1" "remove" )nil nil ))nil ))nil ))nil )"2" "remove(D,0,n!1)" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "remove(D,0,n!1)" )"3" assert )nil nil ))nil )"4" rewrite "sigma_scal" "4" rewrite "sigma_scal" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "10" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" "3" "10" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" assert )"2" case "NOT (LAMBDA (i: nat): LAMBDA (k):LAMBDA (i: nat):LAMBDA (k):") "1" "1" "1" "remove(D,0,x!1)" )"1" assert )nil nil ))nil )"2" "2" "remove(D,0,i!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_swap" )"2" "H" "LAMBDA (j:nat): LAMBDA (i_1:nat): -1 * ") "2" case "NOT %1 = sigma(0,columns(D)-2,LAMBDA (j:nat): sigma(0,columns(D)-1,H(j)))" )"1" "1" expand "H" "1" nil nil ))nil ))nil )"2" "2" "H1" "LAMBDA (j:nat): LAMBDA (i_1:nat): IF j<i_1 THEN H(j)(i_1) ELSE 0 ENDIF" )"2" "H2" "LAMBDA (j:nat): LAMBDA (i_1:nat): IF j>=i_1 THEN H(j)(i_1) ELSE 0 ENDIF" )"2" case "NOT (LAMBDA (j: nat): sigma(0, columns(D) - 1, H(j))) = (LAMBDA (j: nat): sigma(0, columns(D) - 1, H1(j)) + sigma(0,columns(D)-1,H2(j)))" )"1" "1" "1" rewrite "sigma_sum" )"1" rewrite "sigma_eq" )"1" "1" "1" expand "H1" )"1" expand "H2" )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "K1" "LAMBDA (j:nat): sigma(0, columns(D) - 1, H1(j))" )"2" "K2" "LAMBDA (j:nat): sigma(0, columns(D) - 1, H2(j))" )"2" case "NOT %1 = K1+K2" )"1" "1" expand "+" "1" expand "K1" "1" expand "K2" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "H3" "LAMBDA (j:nat): IF j>=1 THEN H2(j-1) ELSE (LAMBDA (kj:nat): 0) ENDIF" )"1" "K3" "LAMBDA (j:nat): sigma(0, columns(D) - 1, H3(j))" )"1" expand "+" "1" rewrite "sigma_sum" "1" case "NOT sigma(0, columns(D) - 2, K2) = sigma(0,columns(D)-1,K3)" )"1" "1" "sigma_split" )"1" "K3" "1" "1" "0" )"1" assert )"1" "1" expand "sigma" "1" expand "sigma" "1" expand "K3" "1" expand "H3" "1" case "NOT %1 = 0" )"1" rewrite "sigma_restrict_eq_0" nil nil )"2" "2" assert )"2" rewrite "sigma_shift_fun_eq" )"2" "2" expand "K3" "2" expand "K2" "2" rewrite "sigma_eq" "2" "2" expand "H3" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "D8" "LAMBDA (k:nat): IF k<=columns(D)-2 THEN K1(k) ELSE 0 ENDIF" )"2" case "NOT sigma(0,columns(D)-2,K1)=sigma(0,columns(D)-1,D8)" )"1" expand "sigma" "1" expand "D8" "1" rewrite "sigma_eq" )"1" "1" expand "D8" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_sum" )"2" rewrite "sigma_eq" "2" "2" "2" "n!1" )"2" expand "D8" "2" assert )"2" expand "K3" "2" "S" )"2" "2" "0" "n!1" )"2" assert )"2" "2" expand "S" "2" rewrite "remove_swap_1" )"2" case "n!1 = columns(D)-1" )"1" assert )"1" expand "H3" "1" expand "H2" "1" expand "H" "1" expand "det" "1" "1" assert )"1" "1" "1" assert )"1" "1" case "NOT rows(remove(D,1,n!1))=0" )"1" expand "rows" "1" expand "length" "1" "remove(D,1,n!1)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "remove(D,1,n!1)" )"2" assert )nil nil ))nil ))nil )"2" "remove(D,1,n!1)" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "remove(D,1,n!1)" )"1" assert )nil nil ))nil ))nil )"2" "2" rewrite "sigma_scal" "2" case "NOT columns(remove(D,1,n!1))=columns(D)-1" )"1" "remove(D,1,n!1)" )"1" assert )nil nil ))nil )"2" replace "2" assert )"2" expand "sigma" "2" rewrite "sigma_eq" "2" "2" "2" case "(-1)^(n!1)=-(-1)^(n!1-1)" )"1" "1" "remove(D,0,n!2)" )"1" "1" "1" replace "1" assert )"1" "remove(D,1,n!1)" )"1" "1" "1" "1" assert )"1" "remove_remove_1_0" )"1" "D" "n!2" "n!1-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "n!1 = 0" )"1" "1" expand "K1" "1" expand "^" "1" expand "expt" "1" rewrite "sigma_first" "1" expand "H1" "1" case "NOT %1 = 0" )"1" rewrite "sigma_restrict_eq_0" "1" "1" expand "H3" "1" nil nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "det" "2" "2" assert )"2" "1" "remove(D,1,0)" )"1" assert )"1" "1" expand "rows" )"1" expand "length" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "remove(D,1,0)" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "remove(D,1,0)" )"3" assert )nil nil ))nil )"4" "remove(D,1,0)" )"4" assert )"4" "4" replace "4" assert )"4" rewrite "sigma_scal_right" "4" rewrite "sigma_shift_fun_eq" "4" "4" "4" "i!1" )"4" expand "H1" "4" expand "H" "4" "remove(D,1,0)" )"4" "4" "4" "4" assert )"4" "remove(D,0,1+i!1)" )"4" "4" "4" "4" assert )"4" case "NOT (-1)^0=1" )"1" "1" nil nil ))nil )"2" case "NOT (-1)^(1+i!1) = -(-1)^i!1" )"1" "1" nil nil ))nil )"2" "2" assert )"2" rewrite "remove_remove_1_0_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "H3" "2" case "NOT sigma(0, columns(D) - 1, H2(n!1 - 1)) = sigma(0, n!1-1, H(n!1 - 1))" )"1" "sigma_split" )"1" "1" "n!1-1" )"1" assert )"1" "1" case "NOT %1 = 0" )"1" rewrite "sigma_restrict_eq_0" )"1" "1" expand "H2" )"1" nil nil ))nil ))nil ))nil )"2" "2" "sigma_eq" )"2" "H2(n!1-1)" "H(n!1-1)" "n!1-1" "0" )"2" assert )"2" "2" expand "H2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "K1" "2" case "NOT sigma(0, columns(D) - 1, H1(n!1)) = sigma(n!1+1, columns(D) - 1, H(n!1))" )"1" "sigma_split" )"1" "1" "n!1" )"1" assert )"1" case "NOT %1 = 0" )"1" rewrite "sigma_restrict_eq_0" )"1" "1" expand "H1" "1" nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" rewrite "sigma_eq" "2" "2" expand "H1" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "det" "2" "2" assert )"2" "1" "remove(D,1,n!1)" )"1" assert )"1" "1" expand "rows" )"1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "remove(D,1,n!1)" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "remove(D,1,n!1)" )"3" assert )nil nil ))nil )"4" "remove(D,1,n!1)" )"4" "4" assert )"4" "4" "4" assert )"4" rewrite "sigma_scal" "4" "sigma_split" )"4" "4" "n!1-1" )"4" assert )"4" "4" case "FORALL (aa,bb,cc,dd:real): aa=cc AND bb=dd IMPLIES aa+bb=cc+dd" )"1" rewrite "1" "1" "1" rewrite "sigma_eq" "1" "1" "1" expand "H" "1" case "NOT (-1)^n!1 = -(-1)^(n!1-1)" )"1" "1" nil nil ))nil )"2" "2" assert )"2" "remove_remove_1_0" )"2" "D" "n!2" "n!1-1" )"2" assert )"2" "2" assert )"2" "remove(D,1,n!1)" )"2" "2" "2" assert )"2" "2" "remove(D,0,n!2)" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma_shift_fun_eq" )"2" "2" assert )"2" "2" "2" "i!1" )"2" expand "H" "2" "remove_remove_1_0" )"2" "remove_remove_1_n" )"2" rewrite "2" "remove(D,1,n!1)" )"2" "2" "2" assert )"2" "2" "remove(D,0,1+i!1+n!1)" )"2" "2" "2" assert )"2" "2" case "(-1)^(1+i!1+n!1) = -(-1)^(i!1+n!1)" )"1" assert )nil nil )"2" "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 )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "remove(D,0,i!1)" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "10" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" "4" "10" )"4" 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 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 list_adt nil )"boolean" notequal nil )nil booleans nil )nil numbers nil )"real" matrix_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"nzreal" exponentiation nil )"int" exponentiation nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[nat -> real]" matrix_props nil )nil matrix_props nil )nil matrix_props nil )nil sigma "reals/" )"odd_int" integers nil )nil sigma "reals/" )nil matrix_props nil )"nzrat" rationalsnil )"nzint" integers nil )nil matrix_props nil )"odd_int" integers nil )"nzrat" rationals nil )"{PFM | AND AND AND 1 < rows(D) IMPLIESIF k = 0 THEN entry(D)(1, p)" matrix_props nil) "[nat -> [nat -> real]]" matrix_props nil )nil sigma "reals/" )"int" integers nil )nil sigma "reals/" )"nnreal" sigma_nat "reals/" )"nat" sigma_nat "reals/" )"[nat -> real]" matrix_props nil )"odd_int" integersnil )nil sigma "reals/" )"[nat -> real]" matrix_props nil )"[nat -> real]" matrix_props nil )"[T -> real]" real_fun_ops "reals/" )nil sigma "reals/" )"[nat -> [nat -> real]]" matrix_props nil )"even_int" integersnil )"nonneg_int" nil )"[nat -> [nat -> real]]" matrix_props nil )"[nat -> [nat -> real]]" matrix_props nil )nil sigma_swap "reals/" )"PosFullMatrix" matrix_props nil )nil integers nil )"rat" exponentiation nil )nil sigma "reals/" )"FullMatrix" nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil sigma "reals/" )"(total_order?[real])" nil )"(null?)" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"posint" nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"(strict_total_order?[real])" real_props nil )"FullMatrix" matricesnil )"int" integers nil )"posint" nil )"real" reals nil )"real" reals nil )"int" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"nzint" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(total_order?[real])" nil )"real" reals nil )"real" sigma "reals/" )"real" exponentiation nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )"real" exponentiation nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) "{M: MatrixMN(m, n) | " nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" "structures/" )"real" matrix_props nil )"real" matrices nil )"real" matrices nil )"Vector" matrices nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )NOT const-decl "[bool -> bool]" booleans nil )nil more_list_props"structures/" )nil more_list_props "structures/" )"[bool, bool -> bool]" booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil ))nil 3614444971"" (skeep)"" (lemma "full_matrix_eq" )"" (inst?)"" (assert )"" (hide 2)"" (skosimp*)"" (typepred "i!1" )"" (typepred "j!1" )"" (typepred "swap(i, j)(swap(i, j)(D))" )"" (hide (-1 -2 -3 -4 -7))"" (copy -3)"" (copy -5)"" (replace -4)"" (replace -3)"" "swap(i,j)(D)" )"" "" "" "" replace -4)"" replace -3)"" assert )"" "swap(i, j)(swap(i, j)(D))" )"" "" "i!1" "j!1" )"" case "%1" )"1" "1" assert )"1" "1" assert )"1" "1" "1" "1" "swap(i,j)(D)" )"1" "1" "j" "j!1" )"1" assert )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "swap(i,j)(D)" )"2" "2" "i" "j!1" )"2" nil nil ))nil ))nil ))nil )"3" "swap(i,j)(D)" )"3" "3" "i!1" "j!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" assert )nil nil )"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 matrices nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )"{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 3614695692"" (skeep)"" (rewrite "full_matrix_eq" )"" (assert )"" (skosimp*)"" (expand "swap" + 1)"" (rewrite "entry_form_matrix" )"" (expand "swap" + 2)"" (rewrite "entry_form_matrix" )"" (expand "swap" + 3)"" (expand "swap" + 1)"" (expand "swap" + 1)"" (assert )"" (lift-if)"" (lift-if)"" "" "" "1" rewrite "entry_form_matrix" )"1" expand "swap" + 1)"1" "1" expand "swap" + 1)"1" rewrite "entry_form_matrix" )"1" expand "swap" +)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "swap" + 1)"2" rewrite "entry_form_matrix" )"2" expand "swap" +)"2" rewrite "entry_form_matrix" )"2" expand "swap" +)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "entry_form_matrix" )"3" expand "swap" +)"3" rewrite "entry_form_matrix" )"3" expand "swap" +)"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" rewrite "entry_form_matrix" )"4" expand "swap" +)"4" rewrite "entry_form_matrix" )"4" expand "swap" +)"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices nil )"bool" reals nil )"nat" matrices nil )"bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"[bool, bool -> bool]" booleans nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) nil matrices nil )"real" matrix_props nil )"FullMatrix" matricesnil )"(strict_total_order?[real])" real_props nil ))nil 3614688092"" case "FORALL (D: PosFullMatrix, i, j, n: nat): AND i < rows(D) AND j < rows(D) AND rows(D)=columns(D) AND rows(D)=n+2 IMPLIES") "1" (skeep)"1" (case "rows(D)/=columns(D)" )"1" (flatten)"1" (assert )"1" (expand "det" +) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (flatten)"2" (case "i < j" )"1" (inst - "D" "i" "j" "rows(D)-2" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (inst - "D" "j" "i" "rows(D)-2" )"1" (assert ) (("1" (rewrite "swap_sym" -) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skeep)"1" (assert )"1" (lemma "det_swap_0_1" )"1" (inst - "D" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (skolem 1 "n" )"2" (flatten)"2" (assert )"2" case "NOT FORALL (D: PosFullMatrix, i, j: nat): AND i < j AND i < rows(D) AND j < rows(D) AND rows(D) = columns(D)AND rows(D) = 3 + n") "1" (hide 2)"1" (skeep)"1" (expand "det" +)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" assert )"1" assert )"1" "1" "swap(i,j)(D)" )"1" expand "rows" )"1" expand "length" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "D" )"2" expand "rows" )"2" expand "length" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" case "FORALL (rr:real): -rr=(-1)*rr" )"1" "%1" )"1" "1" rewrite "sigma_scal" "1" "swap(i,j)(D)" )"1" "1" "1" assert )"1" rewrite "sigma_eq" "1" "1" "1" case "entry(swap(i, j)(D))(0, n!1) = entry(D)(0, n!1)" )"1" "1" assert )"1" case "remove(swap(i, j)(D), 0, n!1) = swap(i-1,j-1)(remove(D,0,n!1))" )"1" "1" "1" assert )"1" "remove(D,0,n!1)" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "remove_swap_2" )nil nil ))nil ))nil )"3" assert )"3" "3" "remove(D,0,n!1)" )"3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "swap(i,j)(D)" )"2" rewrite nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (case "NOT i = 0" )"1" (inst - "D" "i" "j" ) (("1" (assert ) nil nil ))nil )"2" (replaces -1)"2" (assert )"2" (lemma "swap_similar" )"2" (inst - "D" "1" "j" "0" )"2" (assert )"2" case "j = 1" )"1" "1" "det_swap_0_1" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "swap(0, 1)(swap(1, j)(D))" "1" "j" )"2" assert )"2" "2" rewrite "det_swap_0_1" +)"2" "D" "1" "j" )"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 matrix_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"rat" exponentiation nil )nil matrix_props nil )"FullMatrix" nil )nil integers nil )nil sigma "reals/" )"odd_int" integers nil )"real" exponentiation nil )"{N | AND columns(M) > 1 IMPLIESAND columns(N) = columns(M) - 1))AND LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF,IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF" nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"(total_order?[real])" nil )"real" reals nil )"int" exponentiation nil )"nzreal" exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )"even_int" integersnil )nil naturalnumbers nil )nil defined_types nil )nil matrix_props nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"PosFullMatrix" matrix_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"posint" nil )"real" reals 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 )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" matrix_props nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) "[numfield -> numfield]" number_fields nil ))nil 3614963731"" (skeep)"" (rewrite "list_extensionality[real]" )"" (split)"1" (rewrite "length_row" )"1" (rewrite "length_row" )"1" (rewrite "length_row" )"1" (rewrite "length_row" )"1" (lift-if) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (skeep)"2" (lemma "entry_swap" )"2" (inst - "D" "i" "j" "k" "n" )"2" (expand "entry" )"2" (expand "access" -1)"2" (replaces -1)"2" (expand "swap" )"2" (lift-if)"2" (lift-if)"2" (assert )"2" (rewrite "length_row" )"2" rewrite "length_row" )"2" rewrite "length_row" )"2" assert )"2" "1" expand "row" 2)"1" expand "rows" )"1" assert )"1" "n" )"1" rewrite "length_row" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "n" )"2" rewrite "length_row" )"2" (assert ) nil nil ))nil ))nil )"3" "n" )"3" rewrite "length_row" )"3" (assert ) nil nil ))nil ))nil )"4" "n" )"4" rewrite "length_row" )"4" "4" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil more_list_props"structures/" )nil list_adt nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil matrices nil )"Vector" 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 )"[bool, bool -> bool]" booleans nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" matrices nil )"real" matrix_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrix_props nil )nil matrix_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3615053514"" (skeep)"" (expand "swap" ) (("" (rewrite "rows_form_matrix" ) nil nil ))nil ))nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) "real" matrices nil )"real" matrix_props 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 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 matrices nil ))nil 3615053542"" (skeep)"" (expand "swap" )"" (lemma "columns_form_matrix" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props 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 )"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 ) (<= const-decl "bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"real" matrix_props nil )"real" matrices nil )"FullMatrix" matricesnil )nil matrices nil ))nil 3614445784"" (skeep)"" (lemma "full_matrix_eq" )"" (inst?)"" (assert )"" (skosimp*)"" (typepred "swap(i,i)(D)" )"" (hide (-1 -2 -3 -4 -5 -6))"" (inst - "i!1" "j!1" )"" (assert )"" (case "i < rows(D)" )"1" (assert )"1" (replaces -2)"1" (assert )"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil ))nil )"2" (hide -)"2" (expand "swap" )"2" (rewrite "entry_form_matrix" )"2" (expand "swap" 2)"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )NOT const-decl "[bool -> bool]" booleans nil )nil matrices nil )"real" matrix_props nil )"(strict_total_order?[real])" real_props nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices nil )"[bool, bool -> bool]" booleans nil )nil matrices nil )"{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 3615027356"" (skeep)"" (rewrite "full_matrix_eq" )"" (split)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (rewrite "entry_swap" )"3" (expand "swap" )"3" (expand "entry" )"3" (lift-if) (("3" (ground) 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 )"[bool, bool -> bool]" booleans nil )"real" matrices nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{PFM | AND AND AND j < rows(D) IMPLIESIF k = i THEN entry(D)(j, p)" matrix_props nil) "real" matrix_props nil )"(strict_total_order?[real])" real_props nil )nil matrix_props nil ))nil 3615027482"" (skeep)"" (lemma "swap_eq" )"" (inst?)"" (assert )"" (lemma "det_swap" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil matrix_props nil )"(strict_total_order?[real])" real_props nil )nil matrix_props 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 3614701196 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices 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 ) (<= const-decl "bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"{D | columns(D) = length(v!1)}" nil )"Vector" matrix_props nil )"nat" matrix_props nil )"nat" matrix_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil )"real" matrices nil ))nil ))nil 3614701196 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices nil )nil matrices nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )nil matrices nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"(null?)" list_adt nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil )"nat" list_props nil )"{c: nat | AND AND c = 0 OR " nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"T" list_props nil )"Vector" matrices nil )"real" matrices nil )"real" matrices nil ))nil ))nil 3614701196 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil matrices 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 ) (<= const-decl "bool" reals nil )"{c: nat | AND AND c = 0 OR " nil )nil matrices nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" matrices nil ))nil ))nil 3614701196"" (skeep)"" (replace -1)"" (assert )"" (split)"1" (skosimp*)"1" (expand "nth" )"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" (ground)"1" (replaces -1)"1" (typepred "D" )"1" (assert )"1" (split -)"1" (grind) nil nil )"2" "columns(D)" )"2" assert )"2" "2" "i!2" "j!1" )"1" expand "nth" -3 2)"1" (assert ) nil nil ))nil )"2" "j!1" )"2" expand "length" -1)"2" expand "length" 1)"2" assert )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "columns(D)" )"2" (ground)"2" (skosimp*)"2" (typepred "D" )"2" "1" (grind) nil nil )"2" "i!1" "i!2" )"1" expand "nth" -1)"1" "1" "1" case "length(car(D)) = columns(D)" )"1" (assert ) nil nil )"2" "D" )"2" "1" (grind) nil nil )"2" "0" "i!2" )"2" expand "nth" -1 1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "length" -6)"2" "2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" expand "length" -1)"2" expand "length" 1)"2" "2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "D" )"3" (ground)"1" (grind) nil nil )"2" (inst - "i!1" "j!1" )"1" (assert )"1" expand "nth" -1)"1" (propax) nil nil ))nil ))nil )"2" (typepred "j!1" )"2" expand "length" (-1 1))"2" "2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"3" (typepred "i!1" )"3" expand "length" (-1 1))"3" "3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ) ("3" (grind) nil nil )"4" (grind)"4" (expand "length" 1 2)"4" (lift-if) (("4" (ground) nil nil )) nil )) nil ))nil )"5" (name "KD" "cons[Vector](v, cdr[list[real]](D))" )"5" (replace -1)"5" (typepred "columns(KD)" )"5" (ground)"1" (grind) nil nil )"2" (skosimp*)"2" (replaces -1 1 :dir rl)"2" (typepred "columns(D)" )"2" (ground)"2" (skosimp*)"2" (replace -1 :dir rl)"2" case "i!1 = 0" )"1" "1" expand "nth" 1 1)"1" expand "KD" 1)"1" (assert ) nil nil ))nil ))nil ))nil )"2" "D" )"2" "1" (grind) nil nil )"2" "i!1" "i!2" )"1" expand "KD" 2)"1" expand "nth" + 1)"1" "1" expand "nth" + 2)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" assert )"2" expand "KD" -1)"2" expand "length" -1)"2" expand "length" 1)"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (skosimp*)"6" (expand "row" 1 1)"6" (lift-if)"6" (lift-if)"6" (lift-if)"6" (assert )"6" (ground)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (expand "row" )"3" (lift-if)"3" (ground)"3" expand "length" -1 1)"3" expand "length" 1)"3" "3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "nth" ) (("4" (propax) nil nil ))nil )"5" (expand "rows" )"5" (expand "length" (1 3))"5" (lift-if)"5" "5" (grind) nil nil ))nil ))nil ))nil ))nil )"6" (expand "nth" 2)"6" (expand "row" 2)"6" (lift-if)"6" "1" expand "length" (-1 3))"1" "1" "1" (grind) nil nil ))nil ))nil ))nil )"2" expand "nth" 2 2)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" (assert )"7" (skeep)"7" (expand "entry" )"7" (expand "row" )"7" (expand "access" )"7" (lift-if)"7" (lift-if)"7" (lift-if)"7" (lift-if)"7" (lift-if)"7" assert )"7" case "null?(D)" )"1" "1" (grind) nil nil ))nil )"2" assert )"2" case "null?(v)" )"1" "1" "D" )"1" (grind) nil nil ))nil ))nil )"2" "1" expand "length" -4)"1" expand "rows" -2)"1" expand "length" -2)"1" (assert ) nil nil ))nil ))nil ))nil )"2" expand "length" -2)"2" expand "length" 2)"2" (propax) nil nil ))nil ))nil )"3" expand "length" (-2 2))"3" (propax) nil nil ))nil )"4" expand "nth" + 2)"4" (propax) nil nil ))nil )"5" expand "nth" -3 1)"5" (propax) nil nil ))nil )"6" expand "length" (-1 3))"6" (propax) nil nil ))nil )"7" expand "rows" +)"7" (assert ) nil nil ))nil )"8" expand "rows" +)"8" (assert ) nil nil ))nil )"9" (grind) nil nil )"10" (grind) nil nil )"11" (grind) nil nil )"12" (grind) nil nil )"13" (grind) nil nil )"14" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" list_props nil )"int" 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 )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 )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.773 Sekunden
(vorverarbeitet am 2026-05-01)
¤ *© Formatika GbR, Deutschland
2026-05-26
