(matrix_upper_triang
(upper_triangulate_TCC1 0
(upper_triangulate_TCC1-1 nil 3615110328
("" (skeep)
(("" (typepred "j")
(("" (expand "ut_point1")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
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)
(ut_point1 const-decl "bool" matrix_upper_triang 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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(upper_triangulate_TCC2 0
(upper_triangulate_TCC2-1 nil 3615110328
("" (skeep)
(("" (typepred "z`7")
(("" (expand "ut_point1")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((ut_point2 const-decl "bool" matrix_upper_triang 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)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(SquareMatrix type-eq-decl nil matrices nil)
(ut_point1 const-decl "bool" matrix_upper_triang 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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(upper_triangulate_TCC3 0
(upper_triangulate_TCC3-1 nil 3615110328
("" (skeep)
(("" (typepred "j")
(("" (expand "ut_point1")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
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)
(ut_point1 const-decl "bool" matrix_upper_triang 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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(upper_triangulate_TCC4 0
(upper_triangulate_TCC4-2 nil 3615121606
("" (skeep)
(("" (assert)
(("" (flatten)
(("" (split)
(("1" (expand "upper_triangular?")
(("1" (skeep)
(("1" (typepred "j")
(("1" (expand "ut_point1")
(("1" (assert)
(("1" (inst - "i!1" "j!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "T") (("2" (propax) nil nil)) nil)
("3" (typepred "R") (("3" (propax) nil nil)) nil)
("4" (typepred "R") (("4" (propax) nil nil)) nil)
("5" (typepred "Q") (("5" (propax) nil nil)) nil))
nil))
nil))
nil))
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)
(int_minus_int_is_int application-judgement "int" integers 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)
(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)
(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)
(Square type-eq-decl nil matrices nil)
(ut_point1 const-decl "bool" matrix_upper_triang 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(is_simple_prod? const-decl "bool" matrix_det nil)
(FALSE const-decl "bool" booleans 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))
nil)
(upper_triangulate_TCC4-1 nil 3615110328 ("" (subtype-tcc) nil nil)
nil nil))
(upper_triangulate_TCC5 0
(upper_triangulate_TCC5-1 nil 3615110328
("" (skeep)
(("" (assert)
(("" (expand "ut_point1")
(("" (assert)
(("" (case "j = pn-1")
(("1" (assert) nil nil)
("2" (assert)
(("2" (hide 3)
(("2" (split 3)
(("1" (typepred "j")
(("1" (expand "ut_point1")
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skeep)
(("2" (case "p = j")
(("1" (typepred "i")
(("1" (expand "ut_point2")
(("1" (flatten)
(("1" (inst - "k!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (typepred "j")
(("2" (expand "ut_point1")
(("2" (flatten)
(("2" (inst - "k!1" "p")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ut_point2 const-decl "bool" matrix_upper_triang nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(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)
(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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(SquareMatrix type-eq-decl nil matrices nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(ut_point1 const-decl "bool" matrix_upper_triang nil))
nil))
(upper_triangulate_TCC6 0
(upper_triangulate_TCC6-1 nil 3615110328
("" (skeep)
(("" (assert)
(("" (case "j = pn-1")
(("1" (assert) nil nil)
("2" (hide 3)
(("2" (expand "ut_point2")
(("2" (assert)
(("2" (split 3)
(("1" (typepred "j")
(("1" (expand "ut_point1")
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skeep) (("2" (assert) nil nil)) 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ut_point2 const-decl "bool" matrix_upper_triang nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(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)
(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)
(ut_point1 const-decl "bool" matrix_upper_triang 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(upper_triangulate_TCC7 0
(upper_triangulate_TCC7-1 nil 3615110328
("" (skeep) (("" (assert) (("" (postpone) nil 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))
(upper_triangulate_TCC8 0
(upper_triangulate_TCC8-1 nil 3615110328
("" (termination-tcc) nil nil)
((row const-decl "Vector" matrices nil)
(length def-decl "nat" list_props nil)
(access const-decl "real" matrices nil)
(nth def-decl "T" list_props nil)
(entry const-decl "real" matrices nil)
(lex2 const-decl "ordinal" lex2 nil)
(lex3 const-decl "ordinal" lex3 "orders/")
(< def-decl "bool" ordinals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(upper_triangulate_TCC9 0
(upper_triangulate_TCC9-1 nil 3615110328
("" (skeep)
(("" (typepred "i")
(("" (expand "ut_point2")
(("" (flatten)
(("" (assert)
(("" (skeep)
(("" (inst - "k!1") (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((ut_point1 const-decl "bool" matrix_upper_triang 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)
(ut_point2 const-decl "bool" matrix_upper_triang 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_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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(upper_triangulate_TCC10 0
(upper_triangulate_TCC10-1 nil 3615110328
("" (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))
(upper_triangulate_TCC11 0
(upper_triangulate_TCC11-1 nil 3615110328
("" (skeep)
(("" (lemma "lex3_lt_2")
(("" (inst?)
(("1" (replace 4) (("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (typepred "i")
(("2" (expand "ut_point2") (("2" (propax) nil nil)) nil))
nil))
nil)
("3" (assert)
(("3" (typepred "j")
(("3" (expand "ut_point1") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((lex3_lt_2 formula-decl nil lex3 "orders/")
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(entry const-decl "real" matrices nil)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(ut_point2 const-decl "bool" matrix_upper_triang nil)
(i skolem-const-decl "{i | ut_point2(S, j)(i)}" matrix_upper_triang
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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(pn skolem-const-decl "posnat" matrix_upper_triang nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(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)
(ut_point1 const-decl "bool" matrix_upper_triang nil)
(SquareMatrix type-eq-decl nil matrices nil)
(S skolem-const-decl "SquareMatrix(pn)" matrix_upper_triang nil)
(j skolem-const-decl "{j | ut_point1(S)(j)}" matrix_upper_triang
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(upper_triangulate_TCC12 0
(upper_triangulate_TCC12-1 nil 3615110328
("" (skeep)
(("" (typepred "row(S)(j) + row(S)(i)")
(("" (replaces -2)
(("" (rewrite "matrix_props.length_row")
(("" (rewrite "matrix_props.length_row")
(("" (assert)
(("" (lift-if)
(("" (lift-if)
(("" (lift-if)
(("" (typepred "i")
(("" (typepred "j")
(("" (expand "ut_point2")
(("" (expand "ut_point1")
(("" (flatten)
((""
(assert)
((""
(expand "max")
(("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ut_point2 const-decl "bool" matrix_upper_triang nil)
(ut_point1 const-decl "bool" matrix_upper_triang 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)
(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(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)
(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)
(real nonempty-type-from-decl nil reals 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)
(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)
(nonneg_rat_max application-judgement
"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
(nat_max application-judgement "{k: nat | i <= k AND j <= k}"
real_defs 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))
nil))
(upper_triangulate_TCC13 0
(upper_triangulate_TCC13-1 nil 3615110328
("" (skeep)
(("" (rewrite "rows_replace_row")
(("1" (rewrite "columns_replace_row") (("1" (assert) nil nil))
nil)
("2" (typepred "row(S)(j) + row(S)(i)")
(("2" (replaces -2)
(("2" (rewrite "matrix_props.length_row")
(("2" (rewrite "matrix_props.length_row")
(("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "ut_point2")
(("2" (expand "ut_point1") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rows_replace_row formula-decl nil matrix_props 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)
(Square type-eq-decl nil matrices 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)
(ut_point1 const-decl "bool" matrix_upper_triang nil)
(Vector type-eq-decl nil matrices nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(VectorN type-eq-decl nil matrices nil)
(+ const-decl "VectorN(max(length(v1), length(v2)))" matrices nil)
(row const-decl "Vector" matrices nil)
(ut_point2 const-decl "bool" matrix_upper_triang nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(columns_replace_row formula-decl nil matrix_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(length_row formula-decl nil matrix_props nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(upper_triangulate_TCC14 0
(upper_triangulate_TCC14-1 nil 3615110328
("" (skeep)
(("" (typepred "row(Q)(j) + row(Q)(i)")
(("" (replaces -2)
(("" (rewrite "matrix_props.length_row")
(("" (rewrite "matrix_props.length_row")
(("" (typepred "i")
(("" (typepred "j")
(("" (expand "ut_point1")
(("" (expand "ut_point2")
(("" (flatten)
(("" (assert)
(("" (expand "max") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ut_point2 const-decl "bool" matrix_upper_triang nil)
(ut_point1 const-decl "bool" matrix_upper_triang 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)
(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(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)
(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)
(real nonempty-type-from-decl nil reals 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)
(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)
(int_minus_int_is_int application-judgement "int" integers nil)
(nat_max application-judgement "{k: nat | i <= k AND j <= k}"
real_defs nil)
(nonneg_rat_max application-judgement
"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil))
nil))
(upper_triangulate_TCC15 0
(upper_triangulate_TCC15-1 nil 3615110328
("" (skeep)
(("" (rewrite "rows_replace_row")
(("1" (rewrite "columns_replace_row")
(("1" (assert)
(("1" (rewrite "replace_row_sum_to_scal")
(("1" (lemma "mult_Easr_left")
(("1" (inst?)
(("1" (inst - "pn")
(("1" (assert)
(("1" (case "j < pn AND i < pn")
(("1" (flatten)
(("1" (assert)
(("1" (replace -3 :dir rl)
(("1" (split 5)
(("1"
(rewrite "mult_simple_prod")
(("1"
(rewrite "Easr_simple_prod")
nil
nil))
nil)
("2"
(rewrite "upper_triangular_mult")
(("2"
(rewrite "upper_triangular_Easr")
(("2"
(typepred "i")
(("2"
(expand "ut_point2")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "ut_point2")
(("2" (expand "ut_point1")
(("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (typepred "j")
(("2" (expand "ut_point1") (("2" (propax) nil nil))
nil))
nil))
nil)
("3" (typepred "i")
(("3" (typepred "j")
(("3" (expand "ut_point2") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_add_vect")
(("2" (rewrite "length_row")
(("1" (rewrite "length_row")
(("1" (expand "max") (("1" (propax) nil nil)) nil)
("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "ut_point2")
(("2" (flatten)
(("2" (assert)
(("2" (typepred "Q")
(("2" (expand "rows")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "Q")
(("2" (expand "rows")
(("2" (assert)
(("2" (typepred "j")
(("2" (expand "ut_point1") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "length_add_vect")
(("2" (rewrite "length_row")
(("1" (rewrite "length_row")
(("1" (expand "max") (("1" (propax) nil nil)) nil)
("2" (typepred "Q")
(("2" (expand "rows")
(("2" (assert)
(("2" (typepred "i")
(("2" (expand "ut_point2") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "Q")
(("2" (expand "rows")
(("2" (assert)
(("2" (typepred "j")
(("2" (expand "ut_point1") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rows_replace_row formula-decl nil matrix_props 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)
(Square type-eq-decl nil matrices 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)
(is_simple_prod? const-decl "bool" matrix_det nil)
(FALSE const-decl "bool" booleans nil)
(ut_point1 const-decl "bool" matrix_upper_triang nil)
(Vector type-eq-decl nil matrices nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(VectorN type-eq-decl nil matrices nil)
(+ const-decl "VectorN(max(length(v1), length(v2)))" matrices nil)
(row const-decl "Vector" matrices nil)
(ut_point2 const-decl "bool" matrix_upper_triang nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(nat_max application-judgement "{k: nat | i <= k AND j <= k}"
real_defs nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(length_row formula-decl nil matrices nil)
(mult_Easr_left formula-decl nil matrix_det nil)
(Easr const-decl "SquareMatrix(pn)" matrix_det nil)
(mult_simple_prod formula-decl nil matrix_det nil)
(mult_full application-judgement "FullMatrix" matrices nil)
(Easr_simple_prod formula-decl nil matrix_det nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(replace_row_sum_to_scal formula-decl nil matrix_props nil)
(columns_replace_row formula-decl nil matrix_props nil))
nil))
(upper_triangulate_TCC16 0
(upper_triangulate_TCC16-1 nil 3615110328
("" (skeep)
(("" (rewrite "Id_simple_prod")
(("" (rewrite "upper_triangular_Id") nil nil)) nil))
nil)
((Id_simple_prod formula-decl nil matrix_det nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(FALSE const-decl "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)
(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)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil))
nil))
(upper_triangulate_TCC17 0
(upper_triangulate_TCC17-1 nil 3615110328
("" (skeep)
(("" (case "null?(R) OR null?(S) OR null?(Q)")
(("1" (split -1)
(("1" (typepred "R")
(("1" (expand "rows")
(("1" (expand "length") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (typepred "S")
(("2" (expand "rows")
(("2" (expand "length") (("2" (assert) nil nil)) nil))
nil))
nil)
("3" (typepred "Q")
(("3" (expand "rows")
(("3" (expand "length") (("3" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (case "i < pn AND j < pn AND i>j")
(("1" (flatten)
(("1" (assert)
(("1" (split 8)
(("1" (rewrite "mult_simple_prod")
(("1" (rewrite "Easr_simple_prod") nil nil)) nil)
("2" (rewrite "replace_row_sum_to_scal")
(("2" (lemma "mult_Easr_left")
(("2" (inst - _ _ _ _ "1")
(("2" (inst?)
(("2" (inst - "pn")
(("2" (assert)
(("2" (replaces -1 :dir rl)
(("2"
(rewrite "matrix_mult_assoc")
(("1"
(rewrite "matrix_mult_assoc" :dir rl)
(("1"
(rewrite "mult_Easr_Easr_inv")
(("1"
(rewrite "mult_Id_left")
(("1"
(assert)
(("1"
(typepred "R")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (rewrite "Easr_null") nil nil))
nil)
("2" (rewrite "Easr_null") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (rewrite "replace_row_sum_to_scal")
(("3" (lemma "mult_Easr_left")
(("3" (inst - _ _ _ _ "1")
(("3" (inst?)
(("3" (inst?)
(("3" (assert)
(("3" (replaces -1 :dir rl)
(("3"
(rewrite "matrix_mult_assoc")
(("3"
(rewrite "matrix_mult_assoc" :dir rl)
(("3"
(typepred "R")
(("3"
(assert)
(("3"
(flatten)
(("3"
(assert)
(("3"
(replace -9)
(("3"
(rewrite "mult_Id_left")
(("3"
(rewrite
"mult_Easr_Easr_inv")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (rewrite "rows_mult") (("4" (assert) nil nil))
nil)
("5" (assert)
(("5" (rewrite "rows_mult")
(("5" (rewrite "columns_mult")
(("5" (assert) nil nil)) nil))
nil))
nil)
("6" (rewrite "rows_mult") (("6" (assert) nil nil))
nil)
("7" (rewrite "columns_mult") (("7" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (typepred "i")
(("2" (typepred "j")
(("2" (expand "ut_point2")
(("2" (expand "ut_point1")
(("2" (hide 9)
(("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
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)
(* 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)
(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)
(Matrix type-eq-decl nil matrices nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt 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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(number nonempty-type-decl nil numbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(mult_full application-judgement "FullMatrix" matrices nil)
(ut_point2 const-decl "bool" matrix_upper_triang nil)
(ut_point1 const-decl "bool" matrix_upper_triang nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(columns_mult formula-decl nil matrices nil)
(rows_mult formula-decl nil matrices nil)
(replace_row_sum_to_scal formula-decl nil matrix_props nil)
(mult_Id_left formula-decl nil matrices nil)
(mult_Easr_Easr_inv formula-decl nil matrix_det nil)
(Easr_null formula-decl nil matrix_det nil)
(matrix_mult_assoc formula-decl nil matrices nil)
(mult_Easr_left formula-decl nil matrix_det nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Easr const-decl "SquareMatrix(pn)" matrix_det nil)
(mult_simple_prod formula-decl nil matrix_det nil)
(Easr_simple_prod formula-decl nil matrix_det nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(upper_triangulate_TCC18 0
(upper_triangulate_TCC18-1 nil 3615110328
("" (skeep)
(("" (assert)
(("" (replace 1) (("" (rewrite "Id_simple_prod") nil nil)) nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(Id_simple_prod formula-decl nil matrix_det nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(FALSE const-decl "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)
(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)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil))
nil))
(upper_triangulate_TCC19 0
(upper_triangulate_TCC19-1 nil 3615110328
("" (skeep)
(("" (case "NOT (i < pn AND j)
(("1" (typepred "i")
(("1" (typepred "j")
(("1" (expand "ut_point2")
(("1" (expand "ut_point1") (("1" (ground) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (assert)
(("2" (typepred "T")
(("2" (assert)
(("2" (replace -7 + :dir rl)
(("2" (lemma "vect_scal_1")
(("2" (inst - "row(Q)(i)")
(("2" (replaces -1 :dir rl)
(("2" (lemma "vect_scal_1")
(("2" (inst - "row(Q*T)(i)")
(("2" (replaces -1 :dir rl)
(("2" (assert)
(("2"
(lemma "mult_Easr_left")
(("2"
(inst?)
(("2"
(inst - "pn")
(("2"
(assert)
(("2"
(replaces -1 :dir rl)
(("2"
(lemma "mult_Easr_left")
(("2"
(inst
-
"Q*T"
"j"
"i"
"pn"
"1")
(("2"
(assert)
(("2"
(replaces -1 :dir rl)
(("2"
(lemma
"matrix_mult_assoc")
(("2"
(inst?)
(("2"
(assert)
(("2"
(typepred "Q")
(("2"
(expand
"rows")
(("2"
(expand
"length")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ut_point1 const-decl "bool" matrix_upper_triang 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)
(ut_point2 const-decl "bool" matrix_upper_triang 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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.75 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.
|
