(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
--> --------------------
