|
(matrix_det
(Esr_TCC1 0
(Esr_TCC1-1 nil 3615028556
("" (skeep)
(("" (assert)
(("" (split)
(("1" (rewrite "rows_form_matrix") nil nil)
("2" (lemma "columns_form_matrix")
(("2" (assert)
(("2" (inst?)
(("2" (assert)
(("2" (rewrite "rows_form_matrix")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (rewrite "rows_form_matrix") (("3" (assert) nil nil))
nil)
("4" (lemma "columns_form_matrix")
(("4" (inst?) (("4" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((form_matrix_square application-judgement "FullMatrix" matrices
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(columns_form_matrix formula-decl nil matrices nil)
(rows_form_matrix formula-decl nil matrices nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(/= const-decl "boolean" notequal nil))
nil))
(entry_Esr 0
(entry_Esr-1 nil 3615030016
("" (skeep)
(("" (expand "Esr")
(("" (rewrite "entry_form_matrix")
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Esr const-decl "SquareMatrix(pn)" matrix_det nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(entry_form_matrix formula-decl nil matrices nil))
shostak))
(rows_Esr 0
(rows_Esr-1 nil 3615028664
("" (skeep)
(("" (expand "Esr") (("" (rewrite "rows_form_matrix") nil nil))
nil))
nil)
((Esr const-decl "SquareMatrix(pn)" matrix_det nil)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(rows_form_matrix formula-decl nil matrices nil))
shostak))
(columns_Esr 0
(columns_Esr-1 nil 3615028700
("" (skeep)
(("" (expand "Esr")
(("" (lemma "columns_form_matrix")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((Esr const-decl "SquareMatrix(pn)" matrix_det nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(/= const-decl "boolean" notequal nil)
(form_matrix_square application-judgement "FullMatrix" matrices
nil)
(columns_form_matrix formula-decl nil matrices nil))
shostak))
(det_Esr 0
(det_Esr-1 nil 3615047615
("" (skeep)
(("" (lemma "det_replace_row_scal")
(("" (inst - "Id(pn)" "i" "r" "row(Id(pn))(i)")
(("" (assert)
(("" (split -)
(("1" (rewrite "replace_row_id")
(("1" (rewrite "det_Id")
(("1" (assert)
(("1"
(case "replace_row(i, r * row(Id(pn))(i))(Id(pn)) = Esr(pn)(i,r)")
(("1" (assert) nil nil)
("2" (hide (-1 2))
(("2" (rewrite "full_matrix_eq")
(("2" (skosimp*)
(("2" (rewrite "entry_replace_row")
(("1" (rewrite "entry_Esr")
(("1"
(rewrite "entry_Id")
(("1"
(rewrite "access_scal")
(("1"
(lemma "entry_Id")
(("1"
(inst - "i" "j!1" "pn")
(("1"
(expand "entry" -1)
(("1"
(assert)
(("1"
(replaces -1)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "columns_Id")
(("2"
(typepred "r*row(Id(pn))(i)")
(("2"
(replaces -2)
(("2"
(rewrite "length_row")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_row") nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((det_replace_row_scal formula-decl nil matrix_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(replace_row_id formula-decl nil matrix_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(columns_Id formula-decl nil matrices nil)
(length_row formula-decl nil matrix_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(entry_Esr formula-decl nil matrix_det nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(access_scal formula-decl nil matrices nil)
(entry_Id formula-decl nil matrices nil)
(entry_replace_row formula-decl nil matrix_props nil)
(full_matrix_eq formula-decl nil matrices nil)
(Esr const-decl "SquareMatrix(pn)" matrix_det nil)
(* const-decl "VectorN(length(v2))" matrices nil)
(replace_row def-decl "{PFM |
rows(PFM) = rows(D) AND
columns(PFM) = columns(D) AND
(FORALL (j):
row(PFM)(j) =
IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)
AND
(FORALL (j, k):
entry(PFM)(j, k) =
IF j < rows(D) AND j = i THEN access(v)(k)
ELSE entry(D)(j, k)
ENDIF)}" matrix_props nil)
(access const-decl "real" matrices nil)
(det_Id formula-decl nil matrix_props nil)
(Id const-decl "{M: SquareMatrix(pm) |
(FORALL (i, j):
entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)
AND
(FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND
(FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}"
matrices nil)
(* const-decl "{A: MatrixMN(rows(M), columns(N)) |
FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}"
matrices nil)
(col def-decl "VectorN(rows(M))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(row const-decl "Vector" matrices nil)
(* const-decl "real" matrices nil)
(Vector type-eq-decl nil matrices nil)
(MatrixMN type-eq-decl nil matrices nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(entry const-decl "real" matrices nil)
(SquareMatrix type-eq-decl nil matrices nil)
(Square type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(transpose_Esr 0
(transpose_Esr-1 nil 3615817279
("" (skeep)
(("" (rewrite "full_matrix_eq")
(("" (split)
(("1" (rewrite "rows_transpose") (("1" (assert) nil nil)) nil)
("2" (rewrite "columns_transpose" +) (("2" (assert) nil nil))
nil)
("3" (skosimp*)
(("3" (rewrite "entry_transpose")
(("3" (rewrite "entry_Esr")
(("3" (rewrite "entry_Esr")
(("3" (lift-if)
(("3" (lift-if)
(("3" (lift-if)
(("3" (lift-if) (("3" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((full_matrix_eq formula-decl nil matrices nil)
(number nonempty-type-decl nil numbers nil)
(list type-decl nil list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(Matrix type-eq-decl nil matrices nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(length def-decl "nat" list_props nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(FullMatrix type-eq-decl nil matrices nil)
(> const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(<= const-decl "bool" reals nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(transpose const-decl "PosFullMatrix" matrices nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(Square type-eq-decl nil matrices nil)
(SquareMatrix type-eq-decl nil matrices nil)
(Esr const-decl "SquareMatrix(pn)" matrix_det nil)
(entry_Esr formula-decl nil matrix_det nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(entry_transpose formula-decl nil matrices nil)
(columns_transpose formula-decl nil matrices nil)
(rows_transpose formula-decl nil matrices nil))
shostak))
(mult_Esr_left_TCC1 0
(mult_Esr_left_TCC1-1 nil 3615028556
("" (skeep)
(("" (typepred "r*row(D)(i)")
(("" (replace -2)
(("" (rewrite "length_row" 1)
(("" (assert)
(("" (lift-if)
(("" (ground) (("" (postpone) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(row const-decl "Vector" matrices nil)
(Matrix type-eq-decl nil matrices nil)
(* const-decl "VectorN(length(v2))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil matrices nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(list type-decl nil list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(length_row formula-decl nil matrix_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(mult_Esr_left 0
(mult_Esr_left-1 nil 3615028557
("" (skeep)
(("" (rewrite "full_matrix_eq")
(("" (split)
(("1" (rewrite "rows_mult")
(("1" (rewrite "rows_Esr")
(("1" (rewrite "rows_replace_row") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (lemma "columns_mult")
(("2" (inst?)
(("2" (assert) (("2" (hide 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (rewrite "entry_mult")
(("3" (assert)
(("3" (expand "*" + 1)
(("3" (lift-if)
(("3" (ground)
(("1" (lemma "rows_Esr")
(("1" (inst?)
(("1" (rewrite "entry_replace_row")
(("1" (lift-if)
(("1" (ground)
(("1"
(rewrite "dot_eq_sigma")
(("1"
(rewrite "length_row")
(("1"
(rewrite "length_col")
(("1"
(rewrite "columns_Esr")
(("1"
(expand "min")
(("1"
(lemma "sigma_eq_one_arg")
(("1"
(inst?)
(("1"
(inst - "i!1")
(("1"
(assert)
(("1"
(split -)
(("1"
(replaces -1)
(("1"
(rewrite
"access_scal")
(("1"
(lemma
"entry_Esr")
(("1"
(inst?)
(("1"
(inst
-
"i!1"
"i!1")
(("1"
(assert)
(("1"
(expand
"entry"
-1)
(("1"
(replaces
-1)
(("1"
(rewrite
"access_col")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(hide 2)
(("2"
(lemma
"entry_Esr")
(("2"
(inst
-
"i"
"i!2"
"i!1"
"pn"
"r")
(("2"
(assert)
(("2"
(expand
"entry"
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(skosimp*)
(("3"
(lemma
"entry_Esr")
(("3"
(inst
-
"i"
"i!2"
"i!1"
"pn"
"r")
(("3"
(assert)
(("3"
(expand
"entry"
-1)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "dot_eq_sigma")
(("2"
(rewrite "length_row")
(("2"
(rewrite "length_col")
(("2"
(rewrite "columns_Esr")
(("2"
(replace -4)
(("2"
(assert)
(("2"
(expand "min")
(("2"
(lemma
"sigma_eq_one_arg")
(("2"
(inst?)
(("2"
(inst - "i!1")
(("2"
(assert)
(("2"
(split -)
(("1"
(replaces -1)
(("1"
(lemma
"entry_Esr")
(("1"
(inst?)
(("1"
(inst
-
"i!1"
"i!1")
(("1"
(assert)
(("1"
(expand
"entry"
-1)
(("1"
(replaces
-1)
(("1"
(rewrite
"access_col")
(("1"
(expand
"entry")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(skosimp*)
(("2"
(lemma
"entry_Esr")
(("2"
(inst
-
"i"
"i!2"
"i!1"
"pn"
"r")
(("2"
(assert)
(("2"
(expand
"entry")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide 3)
(("3"
(skosimp*)
(("3"
(lemma
"entry_Esr")
(("3"
(inst
-
"i"
"i!2"
"i!1"
"pn"
"r")
(("3"
(assert)
(("3"
(expand
"entry")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "r*row(D)(i)")
(("2"
(replaces -2)
(("2" (rewrite "length_row") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "rows_Esr")
(("2" (rewrite "entry_replace_row")
(("1" (expand "entry")
(("1" (expand "row")
(("1" (lift-if)
(("1"
(ground)
(("1"
(expand "rows")
(("1"
(assert)
(("1"
(expand "access")
(("1"
(lift-if)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil)
("2"
(expand "rows")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "r*row(D)(i)")
(("2" (replace -2)
(("2" (rewrite "length_row") nil nil))
nil))
nil))
nil))
nil)
("3" (typepred "j!1")
(("3" (lemma "columns_mult")
(("3" (inst?)
(("3" (assert)
(("3" (typepred "Esr(pn)(i,r)")
(("3"
(expand "rows")
(("3"
(expand "length")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((mult_full application-judgement "FullMatrix" matrices nil)
(full_matrix_eq formula-decl nil matrices nil)
(number nonempty-type-decl nil numbers nil)
(list type-decl nil list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(Matrix type-eq-decl nil matrices nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(length def-decl "nat" list_props nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(FullMatrix type-eq-decl nil matrices nil)
(rows const-decl "nat" matrices nil)
(<= const-decl "bool" reals nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(MatrixMN type-eq-decl nil matrices nil)
(entry const-decl "real" matrices nil)
(Vector type-eq-decl nil matrices nil)
(* const-decl "real" matrices nil)
(row const-decl "Vector" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(col def-decl "VectorN(rows(M))" matrices nil)
(* const-decl "{A: MatrixMN(rows(M), columns(N)) |
FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}"
matrices nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(Square type-eq-decl nil matrices nil)
(SquareMatrix type-eq-decl nil matrices nil)
(Esr const-decl "SquareMatrix(pn)" matrix_det nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(access const-decl "real" matrices nil)
(replace_row def-decl "{PFM |
rows(PFM) = rows(D) AND
columns(PFM) = columns(D) AND
(FORALL (j):
row(PFM)(j) =
IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)
AND
(FORALL (j, k):
entry(PFM)(j, k) =
IF j < rows(D) AND j = i THEN access(v)(k)
ELSE entry(D)(j, k)
ENDIF)}" matrix_props nil)
(* const-decl "VectorN(length(v2))" matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(entry_replace_row formula-decl nil matrix_props nil)
(length_row formula-decl nil matrix_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(columns_Esr formula-decl nil matrix_det nil)
(sigma_eq_one_arg formula-decl nil sigma "reals/")
(access_scal formula-decl nil matrices nil)
(access_col formula-decl nil matrix_props nil)
(entry_Esr formula-decl nil matrix_det nil)
(subrange type-eq-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_high type-eq-decl nil sigma "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_low type-eq-decl nil sigma "reals/")
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(length_col formula-decl nil matrices nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(dot_eq_sigma formula-decl nil matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(entry_mult formula-decl nil matrices nil)
(columns_mult formula-decl nil matrices nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(array2list_it def-decl
"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}"
array2list "structures/")
(array2list const-decl
"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
array2list "structures/")
(form_matrix const-decl "{M: MatrixMN(m, n) |
FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}"
matrices nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(form_matrix_square application-judgement "FullMatrix" matrices
nil)
(rows_mult formula-decl nil matrices nil)
(rows_replace_row formula-decl nil matrix_props nil)
(rows_Esr formula-decl nil matrix_det nil))
shostak))
(mult_Esr_Esr_inv 0
(mult_Esr_Esr_inv-1 nil 3615053212
("" (skeep)
(("" (rewrite "mult_Esr_left")
(("" (rewrite "full_matrix_eq")
(("" (split)
(("1" (rewrite "rows_replace_row")
(("1" (rewrite "rows_Esr")
(("1" (rewrite "rows_Id") nil nil)) nil))
nil)
("2" (rewrite "columns_replace_row")
(("2" (rewrite "columns_Esr")
(("2" (rewrite "columns_Id") nil nil)) nil))
nil)
("3" (skosimp*)
(("3" (rewrite "entry_replace_row")
(("1" (rewrite "entry_Id")
(("1" (rewrite "access_scal")
(("1" (lemma "entry_Esr")
(("1" (inst - "i" "j!1" "i" "pn" "1/r")
(("1" (assert)
(("1" (expand "entry" -1)
(("1" (replaces -1)
(("1" (rewrite "entry_Esr")
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (rewrite "columns_Esr")
(("2" (typepred "r * row(Esr(pn)(i, 1 / r))(i)")
(("2" (replace -2)
(("2" (rewrite "length_row")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(mult_Esr_left formula-decl nil matrix_det nil)
(number nonempty-type-decl nil numbers nil)
(list type-decl nil list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(Matrix type-eq-decl nil matrices nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(length def-decl "nat" list_props nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(FullMatrix type-eq-decl nil matrices nil)
(> const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(<= const-decl "bool" reals nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(Square type-eq-decl nil matrices nil)
(SquareMatrix type-eq-decl nil matrices nil)
(Esr const-decl "SquareMatrix(pn)" matrix_det nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(rows_Esr formula-decl nil matrix_det nil)
(rows_Id formula-decl nil matrices nil)
(rows_replace_row formula-decl nil matrix_props nil)
(columns_Esr formula-decl nil matrix_det nil)
(columns_Id formula-decl nil matrices nil)
(columns_replace_row formula-decl nil matrix_props nil)
(entry_replace_row formula-decl nil matrix_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(access_scal formula-decl nil matrices nil)
(real_times_real_is_real application-judgement "real" reals nil)
(r skolem-const-decl "real" matrix_det nil)
(entry_Esr formula-decl nil matrix_det nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(entry_Id formula-decl nil matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(length_row formula-decl nil matrix_props nil)
(Id const-decl "{M: SquareMatrix(pm) |
(FORALL (i, j):
entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)
AND
(FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND
(FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}"
matrices nil)
(* const-decl "{A: MatrixMN(rows(M), columns(N)) |
FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}"
matrices nil)
(col def-decl "VectorN(rows(M))" matrices nil)
(* const-decl "real" matrices nil)
(MatrixMN type-eq-decl nil matrices nil)
(* const-decl "VectorN(length(v2))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(replace_row def-decl "{PFM |
rows(PFM) = rows(D) AND
columns(PFM) = columns(D) AND
(FORALL (j):
row(PFM)(j) =
IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF)
AND
(FORALL (j, k):
entry(PFM)(j, k) =
IF j < rows(D) AND j = i THEN access(v)(k)
ELSE entry(D)(j, k)
ENDIF)}" matrix_props nil)
(access const-decl "real" matrices nil)
(entry const-decl "real" matrices nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(row const-decl "Vector" matrices nil)
(Vector type-eq-decl nil matrices nil)
(full_matrix_eq formula-decl nil matrices nil))
shostak))
(Ers_TCC1 0
(Ers_TCC1-1 nil 3615034417
("" (skeep)
((""
(name "FM" "form_matrix(LAMBDA (k, p: nat):
IF k = i AND p = j THEN 1
ELSIF k = j AND p = i THEN 1
ELSIF k /= i AND k /= j AND k = p THEN 1
ELSE 0
ENDIF,
pn, pn)")
(("" (replace -1)
(("" (split)
(("1" (rewrite "full_matrix_eq")
(("1" (split)
(("1" (expand "FM" 1)
(("1" (rewrite "rows_form_matrix")
(("1" (assert) nil nil)) nil))
nil)
("2" (expand "FM" 1)
(("2" (lemma "columns_form_matrix")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (skosimp*)
(("3" (expand "FM" 1)
(("3" (rewrite "entry_form_matrix")
(("3" (rewrite "entry_swap")
(("3" (expand "swap")
(("3" (lift-if)
(("3" (lift-if)
(("3" (lift-if)
(("3"
(lift-if)
(("3"
(lift-if)
(("3"
(lift-if)
(("3"
(assert)
(("3"
(expand "Id" +)
(("3"
(rewrite -1)
(("3"
(rewrite
"entry_form_matrix")
(("3"
(rewrite
"entry_form_matrix")
(("3"
(rewrite
"entry_form_matrix")
(("3"
(assert)
(("3"
(rewrite
"rows_form_matrix")
(("3"
(lemma
"columns_form_matrix")
(("3"
(inst?)
(("3"
(assert)
(("3"
(replaces
-1)
(("3"
(lift-if)
(("3"
(lift-if)
(("3"
(lift-if)
(("3"
(lift-if)
(("3"
(lift-if)
(("3"
(lift-if)
(("3"
(assert)
(("3"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "FM")
(("2" (rewrite "rows_form_matrix") nil nil)) nil)
("3" (assert)
(("3" (expand "FM")
(("3" (rewrite "rows_form_matrix")
(("3" (lemma "columns_form_matrix")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("4" (expand "FM" 1)
(("4" (rewrite "rows_form_matrix") (("4" (assert) nil nil))
nil))
nil)
("5" (expand "FM" 1)
(("5" (lemma "columns_form_matrix")
(("5" (inst?) (("5" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(form_matrix const-decl "{M: MatrixMN(m, n) |
FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}"
matrices nil)
(row const-decl "Vector" matrices nil)
(Vector type-eq-decl nil matrices nil)
(MatrixMN type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(length def-decl "nat" list_props nil)
(Matrix type-eq-decl nil matrices nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(form_matrix_square application-judgement "FullMatrix" matrices
nil)
(rows_form_matrix formula-decl nil matrices nil)
(FM skolem-const-decl "{M: MatrixMN(pn, pn) |
FORALL (i_1: below(pn), j_1: below(pn)):
nth(row(M)(i_1), j_1) =
IF i_1 = i AND j_1 = j THEN 1
ELSIF i_1 = j AND j_1 = i THEN 1
ELSIF i_1 /= i AND i_1 /= j AND i_1 = j_1 THEN 1
ELSE 0
ENDIF}" matrix_det nil)
(columns_form_matrix formula-decl nil matrices nil)
(entry_swap formula-decl nil matrix_props nil)
(swap const-decl "real" matrix_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(entry_form_matrix formula-decl nil matrices nil)
(Id const-decl "{M: SquareMatrix(pm) |
(FORALL (i, j):
entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)
AND
(FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND
(FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}"
matrices nil)
(* const-decl "{A: MatrixMN(rows(M), columns(N)) |
FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}"
matrices nil)
(col def-decl "VectorN(rows(M))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(* const-decl "real" matrices nil)
(SquareMatrix type-eq-decl nil matrices nil)
(Square type-eq-decl nil matrices nil)
(swap const-decl "{PFM |
rows(PFM) = rows(D) AND
columns(PFM) = columns(D) AND
(FORALL (k, p):
i < rows(D) AND j < rows(D) IMPLIES
entry(PFM)(k, p) =
(IF k = i THEN entry(D)(j, p)
ELSIF k = j THEN entry(D)(i, p)
ELSE entry(D)(k, p)
ENDIF))}" matrix_props nil)
(entry const-decl "real" matrices nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(FullMatrix type-eq-decl nil matrices nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(full_matrix_eq formula-decl nil matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(entry_Ers 0
(entry_Ers-1 nil 3615034417
("" (skeep)
(("" (expand "Ers")
(("" (rewrite "entry_form_matrix")
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (assert) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Ers const-decl "{M: SquareMatrix(pn) | M = swap(i, j)(Id(pn))}"
matrix_det nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.90 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
