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