(matrix_diag
(diagonalize_TCC1 0
(diagonalize_TCC1-1 nil 3615559416
("" (skeep)
(("" (typepred "i")
(("" (expand "d_point2")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((d_point1 const-decl "bool" matrix_diag nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(d_point2 const-decl "bool" matrix_diag nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(diagonalize_TCC2 0
(diagonalize_TCC2-1 nil 3615559416
("" (skeep)
(("" (typepred "z`8")
(("" (expand "d_point2")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((d_point1 const-decl "bool" matrix_diag nil)
(Id const-decl "{M: SquareMatrix(pm) |
(FORALL (i, j):
entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)
AND
(FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND
(FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}"
matrices nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(* const-decl "{A: MatrixMN(rows(M), columns(N)) |
FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}"
matrices nil)
(col def-decl "VectorN(rows(M))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(row const-decl "Vector" matrices nil)
(* const-decl "real" matrices nil)
(Vector type-eq-decl nil matrices nil)
(entry const-decl "real" matrices nil)
(MatrixMN type-eq-decl nil matrices nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(FALSE const-decl "bool" booleans nil)
(is_simple_prod? const-decl "bool" matrix_det nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(d_point2 const-decl "bool" matrix_diag nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(diagonalize_TCC3 0
(diagonalize_TCC3-1 nil 3615559416
("" (skeep)
(("" (typepred "i")
(("" (expand "d_point2") (("" (ground) nil nil)) nil)) nil))
nil)
((d_point1 const-decl "bool" matrix_diag nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(d_point2 const-decl "bool" matrix_diag nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_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))
(diagonalize_TCC4 0
(diagonalize_TCC4-1 nil 3615559416
("" (skeep)
(("" (assert)
(("" (split +)
(("1" (typepred "T") (("1" (propax) nil nil)) nil)
("2" (flatten)
(("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "d_point2")
(("2" (flatten)
(("2" (expand "d_point1")
(("2" (flatten)
(("2" (replace -6)
(("2" (replace -7)
(("2" (assert)
(("2" (skosimp*)
(("2"
(inst - "k!1" "p!1")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (typepred "T") (("3" (propax) nil nil)) nil)
("4" (typepred "R") (("4" (propax) nil nil)) nil)
("5" (typepred "R") (("5" (propax) nil nil)) nil)
("6" (typepred "Q") (("6" (propax) nil nil)) nil))
nil))
nil))
nil)
((Id const-decl "{M: SquareMatrix(pm) |
(FORALL (i, j):
entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)
AND
(FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND
(FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}"
matrices nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(d_point2 const-decl "bool" matrix_diag nil)
(d_point1 const-decl "bool" matrix_diag nil)
(FALSE const-decl "bool" booleans nil)
(is_simple_prod? const-decl "bool" matrix_det nil)
(* const-decl "{A: MatrixMN(rows(M), columns(N)) |
FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}"
matrices nil)
(col def-decl "VectorN(rows(M))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(row const-decl "Vector" matrices nil)
(* const-decl "real" matrices nil)
(Vector type-eq-decl nil matrices nil)
(entry const-decl "real" matrices nil)
(MatrixMN type-eq-decl nil matrices nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(diagonalize_TCC5 0
(diagonalize_TCC5-1 nil 3615559416
("" (skeep)
(("" (case "i = j")
(("1" (hide -2)
(("1" (case "j = 0")
(("1" (ground) nil nil)
("2" (assert)
(("2" (typepred "j")
(("2" (expand "d_point1")
(("2" (hide 3)
(("2" (flatten)
(("2" (assert)
(("2" (skeep)
(("2" (case "NOT p = j")
(("1" (assert)
(("1" (inst - "k!1" "p")
(("1" (ground) nil nil)) nil))
nil)
("2" (assert)
(("2" (replace -1)
(("2"
(assert)
(("2"
(typepred "i")
(("2"
(expand "d_point2")
(("2"
(inst - "k!1")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "j = 0")
(("1" (replace -1)
(("1" (assert)
(("1" (typepred "i")
(("1" (expand "d_point2") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "d_point1")
(("2" (typepred "j")
(("2" (expand "d_point1")
(("2" (flatten)
(("2" (assert)
(("2" (skeep)
(("2" (case "NOT k!1 = p")
(("1" (inst - "k!1" "p")
(("1" (ground) nil nil)) nil)
("2" (replace -1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((d_point1 const-decl "bool" matrix_diag nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(d_point2 const-decl "bool" matrix_diag nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(list type-decl nil list_adt 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)
(number nonempty-type-decl nil numbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil))
nil))
(diagonalize_TCC6 0
(diagonalize_TCC6-1 nil 3615559416
("" (skeep)
(("" (typepred "j")
(("" (typepred "i")
(("" (expand "d_point2")
(("" (assert)
(("" (typepred "i")
(("" (expand "d_point2") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(d_point1 const-decl "bool" matrix_diag nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(d_point2 const-decl "bool" matrix_diag nil))
nil))
(diagonalize_TCC7 0
(diagonalize_TCC7-1 nil 3615559416 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(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)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(list type-decl nil list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt 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)
(PosFullMatrix type-eq-decl nil matrices nil)
(Square type-eq-decl nil matrices nil)
(SquareMatrix type-eq-decl nil matrices nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(is_simple_prod? const-decl "bool" matrix_det nil)
(FALSE const-decl "bool" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(MatrixMN type-eq-decl nil matrices nil)
(Vector type-eq-decl nil matrices nil)
(* const-decl "real" matrices nil)
(row const-decl "Vector" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(col def-decl "VectorN(rows(M))" matrices nil)
(* const-decl "{A: MatrixMN(rows(M), columns(N)) |
FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}"
matrices nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(Id const-decl "{M: SquareMatrix(pm) |
(FORALL (i, j):
entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF)
AND
(FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND
(FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}"
matrices nil)
(d_point1 const-decl "bool" matrix_diag nil)
(d_point2 const-decl "bool" matrix_diag nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(is_simple_seq? const-decl "bool" matrix_det nil)
(Easr const-decl "SquareMatrix(pn)" matrix_det nil)
(/= const-decl "boolean" notequal 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)
(array2list const-decl
"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
array2list "structures/")
(entry const-decl "real" matrices nil))
nil))
(diagonalize_TCC8 0
(diagonalize_TCC8-1 nil 3615559416
("" (skeep)
(("" (rewrite "lex2_lt")
(("1" (typepred "i")
(("1" (expand "d_point2") (("1" (propax) nil nil)) nil)) nil)
("2" (assert)
(("2" (typepred "j")
(("2" (typepred "i")
(("2" (expand "d_point2") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(lex2_lt formula-decl nil lex2 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(list type-decl nil list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(< const-decl "bool" reals nil)
(length def-decl "nat" list_props nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(FullMatrix type-eq-decl nil matrices nil)
(> const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(<= const-decl "bool" reals nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(Square type-eq-decl nil matrices nil)
(d_point1 const-decl "bool" matrix_diag nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(SquareMatrix type-eq-decl nil matrices nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(d_point2 const-decl "bool" matrix_diag nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(diagonalize_TCC9 0
(diagonalize_TCC9-1 nil 3615559416
("" (skeep)
(("" (typepred "i")
(("" (expand "d_point2")
(("" (assert)
(("" (flatten)
(("" (assert)
(("" (case "i = rows(S)-1")
(("1" (typepred "i")
(("1" (typepred "j")
(("1" (expand "d_point2")
(("1" (expand "d_point1")
(("1" (ground) nil nil)) nil))
nil))
nil))
nil)
("2" (assert)
(("2" (skeep)
(("2" (case "NOT k!1 = i")
(("1" (inst - "k!1") (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((d_point1 const-decl "bool" matrix_diag nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(d_point2 const-decl "bool" matrix_diag nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(diagonalize_TCC10 0
(diagonalize_TCC10-1 nil 3615559416
("" (skeep) (("" (assert) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(diagonalize_TCC11 0
(diagonalize_TCC11-1 nil 3615559416
("" (skeep)
(("" (assert)
(("" (rewrite "lex2_lt")
(("1" (typepred "i")
(("1" (expand "d_point2") (("1" (propax) nil nil)) nil)) nil)
("2" (typepred "i")
(("2" (expand "d_point2") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(d_point2 const-decl "bool" matrix_diag nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(d_point1 const-decl "bool" matrix_diag nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(list type-decl nil list_adt 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)
(lex2_lt formula-decl nil lex2 nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(diagonalize_TCC12 0
(diagonalize_TCC12-1 nil 3615559416
("" (skeep)
(("" (skeep)
(("" (rewrite "length_add_vect_same")
(("1" (rewrite "length_row")
(("1" (typepred "i")
(("1" (typepred "j")
(("1" (expand "d_point1")
(("1" (expand "d_point2")
(("1" (flatten) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_scal_vect")
(("2" (rewrite "length_row")
(("2" (rewrite "length_row")
(("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "d_point1")
(("2" (expand "d_point2")
(("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((length_scal_vect formula-decl nil matrices nil)
(length_row formula-decl nil matrix_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_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)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(* const-decl "VectorN(length(v2))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(d_point1 const-decl "bool" matrix_diag nil)
(d_point2 const-decl "bool" matrix_diag nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(row const-decl "Vector" matrices nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(Vector 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)
(length_add_vect_same formula-decl nil matrices nil))
nil))
(diagonalize_TCC13 0
(diagonalize_TCC13-1 nil 3615559416
("" (skeep)
(("" (skeep)
(("" (rewrite "rows_replace_row")
(("1" (rewrite "columns_replace_row")
(("1" (assert)
(("1" (expand "upper_triangular?")
(("1" (skosimp*)
(("1" (copy -3)
(("1" (label "igz" -1)
(("1" (hide "igz")
(("1" (rewrite "rows_replace_row")
(("1" (reveal "igz")
(("1" (rewrite "entry_replace_row")
(("1" (lift-if)
(("1"
(assert)
(("1"
(split 6)
(("1"
(flatten)
(("1"
(replace -1)
(("1"
(typepred "S")
(("1"
(hide -2)
(("1"
(expand
"upper_triangular?")
(("1"
(rewrite "access_sum")
(("1"
(rewrite "access_scal")
(("1"
(rewrite
"access_row")
(("1"
(rewrite
"access_row")
(("1"
(inst-cp
-
"i"
"j!1")
(("1"
(inst
-
"j"
"j!1")
(("1"
(assert)
(("1"
(assert)
(("1"
(typepred
"i")
(("1"
(typepred
"j")
(("1"
(expand
"d_point1")
(("1"
(expand
"d_point2")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(typepred "S")
(("2"
(expand "upper_triangular?")
(("2"
(inst - "i!1" "j!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_add_vect_same")
(("1"
(rewrite "length_row")
(("1"
(typepred "i")
(("1"
(typepred "j")
(("1"
(expand "d_point1")
(("1"
(expand "d_point2")
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "length_scal_vect")
(("2"
(rewrite "length_row")
(("2"
(rewrite "length_row")
(("2"
(typepred "i")
(("2"
(typepred "j")
(("2"
(expand "d_point1")
(("2"
(expand "d_point2")
(("2"
(flatten)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_add_vect_same")
(("1" (rewrite "length_row")
(("1" (typepred "i")
(("1"
(typepred "j")
(("1"
(expand "d_point1")
(("1"
(expand "d_point2")
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_scal_vect")
(("2" (rewrite "length_row")
(("2"
(rewrite "length_row")
(("2"
(typepred "i")
(("2"
(typepred "j")
(("2"
(expand "d_point1")
(("2"
(expand "d_point2")
(("2"
(flatten)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_add_vect_same")
(("1" (rewrite "length_row")
(("1" (typepred "i")
(("1" (typepred "j")
(("1" (expand "d_point1")
(("1" (expand "d_point2")
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_scal_vect")
(("2" (rewrite "length_row")
(("2" (rewrite "length_row")
(("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "d_point1")
(("2" (expand "d_point2")
(("2" (flatten) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_add_vect_same")
(("1" (rewrite "length_row")
(("1" (typepred "i")
(("1" (typepred "j")
(("1" (expand "d_point1")
(("1" (expand "d_point2")
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_scal_vect")
(("2" (rewrite "length_row")
(("2" (rewrite "length_row")
(("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "d_point1")
(("2" (expand "d_point2")
(("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((columns_replace_row formula-decl nil matrix_props nil)
(length_add_vect_same formula-decl nil matrices nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(length_row formula-decl nil matrix_props nil)
(length_scal_vect formula-decl nil matrices nil)
(access_sum formula-decl nil matrices nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(access_row formula-decl nil matrices nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(access_scal formula-decl nil matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(entry_replace_row formula-decl nil matrix_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(* const-decl "VectorN(length(v2))" matrices nil)
(row const-decl "Vector" matrices nil)
(+ const-decl "VectorN(max(length(v1), length(v2)))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(Vector type-eq-decl nil matrices nil)
(d_point1 const-decl "bool" matrix_diag nil)
(d_point2 const-decl "bool" matrix_diag nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(real nonempty-type-from-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(rows_replace_row formula-decl nil matrix_props nil))
nil))
(diagonalize_TCC14 0
(diagonalize_TCC14-1 nil 3615559416
("" (skeep)
(("" (skeep)
(("" (rewrite "length_add_vect_same")
(("1" (rewrite "length_row")
(("1" (typepred "i")
(("1" (typepred "j")
(("1" (expand "d_point1")
(("1" (expand "d_point2")
(("1" (flatten) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_scal_vect")
(("2" (rewrite "length_row")
(("2" (rewrite "length_row")
(("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "d_point1")
(("2" (expand "d_point2")
(("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((length_scal_vect formula-decl nil matrices nil)
(length_row formula-decl nil matrix_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_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)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(* const-decl "VectorN(length(v2))" matrices nil)
(VectorN type-eq-decl nil matrices nil)
(d_point1 const-decl "bool" matrix_diag nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(d_point2 const-decl "bool" matrix_diag nil)
(FALSE const-decl "bool" booleans nil)
(is_simple_prod? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(row const-decl "Vector" matrices nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(Vector 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)
(length_add_vect_same formula-decl nil matrices nil))
nil))
(diagonalize_TCC15 0
(diagonalize_TCC15-1 nil 3615559416
("" (skeep)
(("" (case "i)
(("1" (flatten)
(("1" (skeep)
(("1" (case "length(row(Q)(i) + pivnum*row(Q)(j)) = rows(S)")
(("1" (rewrite "rows_replace_row")
(("1" (assert)
(("1" (rewrite "columns_replace_row")
(("1" (assert)
(("1" (lemma "mult_Easr_left")
(("1" (inst?)
(("1" (assert)
(("1" (inst?)
(("1" (assert)
(("1"
(replaces -1 :dir rl)
(("1"
(rewrite "mult_simple_prod")
(("1"
(rewrite "Easr_simple_prod")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide 7)
(("2" (rewrite "length_add_vect")
(("2" (rewrite "length_scal_vect")
(("2" (rewrite "length_row")
(("2" (rewrite "length_row")
(("2" (expand "max") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 7)
(("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "d_point1")
(("2" (expand "d_point2")
(("2" (flatten) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((d_point1 const-decl "bool" matrix_diag nil)
(upper_triangular? const-decl "bool" matrix_det nil)
(SquareMatrix type-eq-decl nil matrices nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(d_point2 const-decl "bool" matrix_diag nil)
(Square type-eq-decl nil matrices nil)
(PosFullMatrix type-eq-decl nil matrices nil)
(columns def-decl "{c: nat |
(FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
(null?(M) AND c = 0 OR
(EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
matrices nil)
(<= const-decl "bool" reals nil)
(rows const-decl "nat" matrices nil)
(> const-decl "bool" reals nil)
(FullMatrix type-eq-decl nil matrices nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Matrix type-eq-decl nil matrices nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt 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 "bool" reals 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)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(length_add_vect formula-decl nil matrices nil)
(nonneg_rat_max application-judgement
"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.366 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.
|
