| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/matrices/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 207 kB |
|
Quelle matrix_upper_triang.prfSprache: Lisp |
|||||||||||||||
|
(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<pn)") (("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) (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) (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) (int_minus_int_is_int application-judgement "int" integers nil) (mult_full application-judgement "FullMatrix" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (vect_scal_1 formula-decl nil matrices nil) (matrix_mult_assoc formula-decl nil matrices nil) (Easr const-decl "SquareMatrix(pn)" matrix_det nil) (mult_Easr_left formula-decl nil 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)) nil)) (upper_triangulate_TCC20 0 (upper_triangulate_TCC20-1 nil 3615110328 ("" (skeep) (("" (case "NOT i>j") (("1" (typepred "i") (("1" (expand "ut_point2") (("1" (ground) nil nil)) nil)) nil) ("2" (assert) (("2" (hide 4) (("2" (hide 3) (("2" (hide 2) (("2" (case "NOT (i < pn AND j<pn)") (("1" (typepred "i") (("1" (typepred "j") (("1" (expand "ut_point1") (("1" (expand "ut_point2") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "ut_point1") (("2" (split +) (("1" (rewrite "rows_replace_row") (("1" (assert) nil nil)) nil) ("2" (skeep) (("2" (rewrite "entry_replace_row") (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (typepred "j") (("1" (expand "ut_point1") (("1" (inst-cp - "j" "p") (("1" (assert) (("1" (inst - "i" "p") (("1" (assert) (("1" (rewrite "access_sum") (("1" (expand "entry") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "k!1") (("2" (typepred "j") (("2" (expand "ut_point1") (("2" (inst-cp - "k!1" "p") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "row(S)(j) + row(S)(i)") (("2" (replace -2) (("2" (rewrite "matrix_props.length_row") (("2" (rewrite "matrix_props.length_row") (("2" (expand "max" 1) (("2" (propax) 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) (rows const-decl "nat" matrices 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) (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) (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_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (rows_replace_row formula-decl nil matrix_props nil) (entry_replace_row formula-decl nil matrix_props nil) (entry const-decl "real" matrices nil) (real_plus_real_is_real application-judgement "real" reals nil) (access_sum formula-decl nil matrices nil) (length_row formula-decl nil matrix_props nil)) nil)) (upper_triangulate_TCC21 0 (upper_triangulate_TCC21-1 nil 3615110328 ("" (skeep) (("" (assert) (("" (case "NOT (i < pn AND j<pn)") (("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" (expand "ut_point2") (("2" (hide 4) (("2" (assert) (("2" (case "NOT i > j") (("1" (typepred "i") (("1" (expand "ut_point2") (("1" (ground) nil nil)) nil)) nil) ("2" (assert) (("2" (hide 3) (("2" (skeep) (("2" (rewrite "entry_replace_row") (("1" (lift-if) (("1" (ground) (("1" (typepred "i") (("1" (expand "ut_point2") (("1" (inst - "k!1") (("1" (assert) nil nil)) nil)) nil)) 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" (expand "max" 1) (("2" (propax) nil nil)) nil)) 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry_replace_row formula-decl nil matrix_props nil) (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) (length_row formula-decl nil matrix_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, 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) (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) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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_point2 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) (ut_point1 const-decl "bool" matrix_upper_triang nil)) nil)) (upper_triangulate_TCC22 0 (upper_triangulate_TCC22-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_TCC23 0 (upper_triangulate_TCC23-1 nil 3615110328 ("" (skeep) (("" (case "NOT (i < pn AND j<pn)") (("1" (typepred "i") (("1" (typepred "j") (("1" (expand "ut_point1") (("1" (expand "ut_point2") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "lex3_lt_2") (("2" (inst?) (("1" (replace 5) (("1" (assert) (("1" (hide 6) (("1" (lift-if) (("1" (hide (4 5)) (("1" (split +) (("1" (flatten) (("1" (rewrite "entry_replace_row") (("1" (rewrite "entry_replace_row") (("1" (assert) (("1" (rewrite "access_sum") (("1" (rewrite "access_row") (("1" (rewrite "access_row") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "row(S)(j) + row(S)(i)") (("2" (replace -2) (("2" (rewrite "matrix_props.length_row") (("2" (rewrite "matrix_props.length_row") (("2" (expand "max" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "row(S)(j) + row(S)(i)") (("2" (replace -2) (("2" (rewrite "matrix_props.length_row") (("2" (rewrite "matrix_props.length_row") (("2" (expand "max" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 6) (("2" (flatten) (("2" (typepred "row(S)(j) + row(S)(i)") (("2" (replace -2) (("2" (rewrite "matrix_props.length_row") (("2" (rewrite "matrix_props.length_row") (("2" (assert) (("2" (expand "max") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "row(S)(j) + row(S)(i)") (("3" (replace -2) (("3" (rewrite "matrix_props.length_row") (("3" (rewrite "matrix_props.length_row") (("3" (expand "max" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) 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) (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) (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) (int_minus_int_is_int application-judgement "int" integers nil) (lex3_lt_2 formula-decl nil lex3 "orders/") (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) (access_sum formula-decl nil matrices nil) (real_plus_real_is_real application-judgement "real" reals nil) (access_row formula-decl nil matrices nil) (length_row formula-decl nil matrix_props nil) (entry_replace_row formula-decl nil matrix_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (entry const-decl "real" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (access const-decl "real" matrices nil) (replace_row def-decl "{PFM | rows(PFM) = rows(D) AND columns(PFM) = columns(D) AND (FORALL (j): row(PFM)(j) = IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF) AND (FORALL (j, k): entry(PFM)(j, k) = IF j < rows(D) AND j = i THEN access(v)(k) ELSE entry(D)(j, k) ENDIF)}" matrix_props nil) (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) (i skolem-const-decl "{i | ut_point2(S, j)(i)}" matrix_upper_triang nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (pn skolem-const-decl "posnat" matrix_upper_triang nil) (S skolem-const-decl "SquareMatrix(pn)" matrix_upper_triang nil) (j skolem-const-decl "{j | ut_point1(S)(j)}" matrix_upper_triang nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (upper_triangulate_TCC24 0 (upper_triangulate_TCC24-1 nil 3615110328 ("" (skeep) (("" (case "i < pn AND j < pn AND i>j") (("1" (case "NOT (null?(Q) OR null?(R) OR null?(S))") (("1" (flatten) (("1" (case "length[real](row(S)(j) + 1 * row(S)(i)) = pn") (("1" (case "columns(S)=pn") (("1" (name "GG" "v(pn) (comp_matrix, comp_inverse, replace_row(j, row(S)(j) + row(S)(i))(S), IF comp_matrix THEN replace_row(j, row(Q)(j) + row(Q)(i))(Q) ELSE Id(pn) ENDIF, IF comp_matrix AND comp_inverse THEN R * Easr(pn)(j, i, -1) ELSE Id(pn) ENDIF, T, j, i, stop_rec, max(k - 1, 0))") (("1" (replaces -1) (("1" (assert) (("1" (typepred "GG") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (split 9) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (assert) (("3" (replace -4 1) (("3" (rewrite "replace_row_sum_to_scal") (("3" (rewrite "det_replace_row_sum_scal") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 10) (("2" (rewrite "replace_row_sum_to_scal") (("2" (rewrite "lex3_lt_2") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (rewrite "entry_replace_row") (("2" (rewrite "entry_replace_row") (("2" (assert) (("2" (split 1) (("1" (rewrite "access_sum") (("1" (rewrite "access_scal") (("1" (rewrite "access_row") (("1" (rewrite "access_row") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 10) (("3" (assert) nil nil)) nil) ("4" (hide 10) (("4" (typepred "i") (("4" (typepred "j") (("4" (expand "ut_point1") (("4" (expand "ut_point2") (("4" (flatten) (("4" (assert) (("4" (rewrite "rows_replace_row") (("4" (assert) (("4" (skeep) (("4" (rewrite "entry_replace_row") (("4" (lift-if) (("4" (assert) (("4" (inst - "k!1" "j") (("4" (inst - "k!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 10) (("5" (typepred "j") (("5" (typepred "i") (("5" (expand "ut_point1") (("5" (expand "ut_point2") (("5" (flatten) (("5" (rewrite "rows_replace_row") (("5" (assert) (("5" (skeep) (("5" (rewrite "entry_replace_row") (("5" (lift-if) (("5" (assert) (("5" (split 1) (("1" (flatten) (("1" (rewrite "access_sum") (("1" (rewrite "access_row") (("1" (rewrite "access_row") (("1" (assert) (("1" (inst - "i") (("1" (inst-cp - "i" "p") (("1" (inst - "j" "p") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("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)) nil) ("6" (hide 10) (("6" (flatten) (("6" (assert) (("6" (lemma "mult_Easr_left") (("6" (inst-cp - "Q" "j" "i" "pn" "1") (("6" (inst - "S" "j" "i" "pn" "1") (("6" (rewrite "replace_row_sum_to_scal") (("6" (rewrite "replace_row_sum_to_scal") (("6" (assert) (("6" (replaces -1 :dir rl) (("6" (replaces -1 :dir rl) (("6" (rewrite "matrix_mult_assoc") (("6" (typepred "Q") (("6" (assert) (("6" (typepred "T") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (hide 10) (("7" (flatten) (("7" (assert) (("7" (replace 1) (("7" (rewrite "Id_simple_prod") nil nil)) nil)) nil)) nil)) nil) ("8" (hide 10) (("8" (flatten) (("8" (assert) (("8" (assert) (("8" (split 1) (("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 - "Q" "j" "i" "pn" "1") (("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) ("3" (rewrite "replace_row_sum_to_scal") (("3" (lemma "mult_Easr_left") (("3" (inst - "Q" "j" "i" "pn" "1") (("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" (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) ("4" (rewrite "rows_mult") (("4" (assert) nil nil)) nil) ("5" (rewrite "rows_mult") (("5" (rewrite "columns_mult") (("5" (rewrite "columns_Easr") (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (rewrite "rows_mult") (("6" (assert) nil nil)) nil) ("7" (rewrite "columns_mult") (("7" (rewrite "columns_Easr") (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("9" (hide 10) (("9" (flatten) (("9" (assert) (("9" (rewrite "Id_simple_prod") nil nil)) nil)) nil)) nil) ("10" (hide 10) (("10" (flatten) (("10" (assert) (("10" (split 1) (("1" (rewrite "rows_replace_row") (("1" (rewrite "columns_replace_row") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "rows_replace_row") (("2" (assert) nil nil)) nil) ("3" (rewrite "replace_row_sum_to_scal") (("3" (lemma "mult_Easr_left") (("3" (inst - "Q" "j" "i" "pn" "1") (("3" (assert) (("3" (replaces -1 :dir rl) (("3" (rewrite "mult_simple_prod") (("3" (rewrite "Easr_simple_prod") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("11" (hide 10) (("11" (flatten) (("11" (assert) (("11" (rewrite "length_add_vect") (("11" (rewrite "length_row") (("1" (rewrite "length_row") (("1" (expand "max") (("1" (propax) nil nil)) nil) ("2" (typepred "Q") (("2" (expand "rows") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "Q") (("2" (expand "rows") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("12" (hide 10) (("12" (rewrite "rows_replace_row") (("12" (rewrite "columns_replace_row") (("12" (assert) nil nil)) nil)) nil)) nil) ("13" (hide 10) (("13" (lemma "vect_scal_1") (("13" (inst?) (("13" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 10) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 10) (("2" (assert) (("2" (rewrite "length_add_vect") (("2" (rewrite "length_scal_vect") (("2" (rewrite "length_row") (("1" (rewrite "length_row") (("1" (expand "max") (("1" (assert) nil nil)) nil) ("2" (typepred "S") (("2" (expand "rows") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "S") (("2" (expand "rows") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 6) (("2" (split -) (("1" (typepred "Q") (("1" (expand "rows") (("1" (expand "length") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (typepred "S") (("3" (expand "rows") (("3" (expand "length") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 7) (("2" (typepred "i") (("2" (typepred "j") (("2" (expand "ut_point1") (("2" (expand "ut_point2") (("2" (flatten) (("2" (assert) 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) (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_scal_vect formula-decl nil matrices nil) (vect_scal_1 formula-decl nil matrices nil) (length_row formula-decl nil matrices 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) (length_add_vect formula-decl nil matrices nil) (columns_replace_row formula-decl nil matrix_props nil) (Easr_simple_prod formula-decl nil matrix_det nil) (mult_simple_prod formula-decl nil matrix_det nil) (Easr_null formula-decl nil matrix_det nil) (mult_Easr_Easr_inv formula-decl nil matrix_det nil) (mult_Id_left formula-decl nil matrices nil) (rows_mult formula-decl nil matrices nil) (columns_mult formula-decl nil matrices nil) (columns_Easr formula-decl nil matrix_det nil) (Id_simple_prod formula-decl nil matrix_det nil) (matrix_mult_assoc formula-decl nil matrices nil) (mult_Easr_left formula-decl nil matrix_det nil) (rows_replace_row formula-decl nil matrix_props nil) (lex3_lt_2 formula-decl nil lex3 "orders/") (entry_replace_row formula-decl nil matrix_props 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_times_real_is_real application-judgement "real" reals nil) (access_scal formula-decl nil matrices nil) (det_replace_row_sum_scal formula-decl nil matrix_props nil) (replace_row_sum_to_scal formula-decl nil matrix_props 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mult_full application-judgement "FullMatrix" matrices nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (ordstruct type-decl nil ordstruct_adt nil) (< def-decl "bool" ordinals nil) (ordinal? def-decl "bool" ordinals nil) (ordinal nonempty-type-eq-decl nil ordinals nil) (lex3 const-decl "ordinal" lex3 "orders/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (upper_triangular? const-decl "bool" matrix_det nil) (det def-decl "real" matrix_props nil) (access const-decl "real" matrices nil) (replace_row def-decl "{PFM | rows(PFM) = rows(D) AND columns(PFM) = columns(D) AND (FORALL (j): row(PFM)(j) = IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF) AND (FORALL (j, k): entry(PFM)(j, k) = IF j < rows(D) AND j = i THEN access(v)(k) ELSE entry(D)(j, k) ENDIF)}" matrix_props nil) (Easr const-decl "SquareMatrix(pn)" matrix_det nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "VectorN(length(v2))" matrices nil) (+ const-decl "VectorN(max(length(v1), length(v2)))" matrices nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (NOT const-decl "[bool -> bool]" booleans 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) (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) (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_TCC25 0 (upper_triangulate_TCC25-1 nil 3615110328 ("" (skeep) (("" (skeep) (("" (typepred "row(S)(i) + pivnum * row(S)(j)") (("" (replaces -2) (("" (expand "max") (("" (lift-if) (("" (split 6) (("1" (flatten) (("1" (typepred "pivnum * row(S)(j)") (("1" (replaces -2) (("1" (assert) (("1" (rewrite "matrix_props.length_row" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "matrix_props.length_row" 2) (("2" (lift-if) (("2" (hide 1) (("2" (split 1) (("1" (flatten) (("1" (typepred "i") (("1" (expand "ut_point2") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals 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) (real_div_nzreal_is_real application-judgement "real" reals 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (Vector type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities 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) (length def-decl "nat" list_props 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) (Matrix type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (< const-decl "bool" reals 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) (ut_point2 const-decl "bool" matrix_upper_triang nil) (ut_point1 const-decl "bool" matrix_upper_triang nil) (* const-decl "VectorN(length(v2))" matrices nil)) nil)) (upper_triangulate_TCC26 0 (upper_triangulate_TCC26-1 nil 3615110328 ("" (skeep) (("" (skeep) (("" (split 6) (("1" (rewrite "rows_replace_row") (("1" (rewrite "columns_replace_row") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "rows_replace_row") (("2" (assert) 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_point2 const-decl "bool" matrix_upper_triang 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) (* const-decl "VectorN(length(v2))" matrices nil) (minus_real_is_real application-judgement "real" reals nil) (columns_replace_row formula-decl nil matrix_props nil)) nil)) (upper_triangulate_TCC27 0 (upper_triangulate_TCC27-1 nil 3615110328 ("" (skeep) (("" (skeep) (("" (rewrite "length_add_vect_same") (("1" (rewrite "matrix_props.length_row") (("1" (typepred "i") (("1" (expand "ut_point2") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "matrix_props.length_row") (("2" (typepred "i") (("2" (expand "ut_point2") (("2" (flatten) (("2" (assert) (("2" (rewrite "length_scal_vect") (("2" (rewrite "matrix_props.length_row") 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_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) (int_minus_int_is_int application-judgement "int" integers nil) (* const-decl "VectorN(length(v2))" matrices nil) (VectorN type-eq-decl nil matrices nil) (ut_point1 const-decl "bool" matrix_upper_triang nil) (ut_point2 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) (= 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)) (upper_triangulate_TCC28 0 (upper_triangulate_TCC28-1 nil 3615110328 ("" (skeep) (("" (case "i<pn aND j<pn") (("1" (flatten) (("1" (skeep) (("1" (assert) (("1" (rewrite "rows_replace_row") (("1" (lemma "mult_Easr_left") (("1" (inst?) (("1" (inst - "pn") (("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) ("2" (rewrite "length_add_vect") (("2" (rewrite "length_scal_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) nil nil)) nil)) nil)) nil) ("2" (rewrite "length_rows") (("2" (assert) 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" (flatten) (("2" (assert) 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) (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) (rows_replace_row formula-decl nil matrix_props nil) (is_simple_prod? const-decl "bool" matrix_det nil) (FALSE const-decl "bool" booleans 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) (* const-decl "VectorN(length(v2))" matrices 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) (mult_Easr_left formula-decl nil matrix_det nil) (length_scal_vect formula-decl nil matrices nil) (length_rows formula-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (length_row formula-decl nil matrices 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) (length_add_vect formula-decl nil matrices 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) (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_TCC29 0 (upper_triangulate_TCC29-1 nil 3615110328 ("" (skeep) (("" (skeep) (("" (rewrite "Id_simple_prod") nil nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "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) (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) (FALSE const-decl "bool" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Id_simple_prod formula-decl nil matrix_det nil)) nil)) (upper_triangulate_TCC30 0 (upper_triangulate_TCC30-1 nil 3615110328 ("" (skeep) (("" (skeep) (("" (assert) (("" (case "NOT (i<pn AND j<pn AND i>j)") (("1" (typepred "i") (("1" (typepred "j") (("1" (expand "ut_point2") (("1" (expand "ut_point1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split 6) (("1" (rewrite "mult_simple_prod") (("1" (rewrite "Easr_simple_prod") nil nil)) nil) ("2" (lemma "mult_Easr_left") (("2" (inst - "Q" "i" "j" "pn" "pivnum") (("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" (typepred "R") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "Easr_null") nil nil)) nil) ("2" (rewrite "Easr_null") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "mult_Easr_left") (("3" (inst - "Q" "i" "j" "pn" "pivnum") (("3" (assert) (("3" (replaces -1 :dir rl) (("3" (rewrite "matrix_mult_assoc") (("1" (rewrite "matrix_mult_assoc" :dir rl) (("1" (typepred "R") (("1" (assert) (("1" (flatten) (("1" (replace -9) (("1" (rewrite "mult_Id_left") (("1" (rewrite "mult_Easr_Easr_inv") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "Q") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (rewrite "rows_mult") (("4" (assert) nil nil)) nil) ("5" (rewrite "rows_mult") (("5" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (rewrite "rows_mult") (("6" (assert) nil nil)) nil) ("7" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) 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) (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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (real_gt_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) (mult_Easr_left formula-decl nil matrix_det nil) (matrix_mult_assoc formula-decl nil matrices nil) (Easr_null formula-decl nil matrix_det nil) (mult_Easr_Easr_inv formula-decl nil matrix_det nil) (mult_Id_left formula-decl nil matrices nil) (mult_simple_prod formula-decl nil matrix_det nil) (FALSE const-decl "bool" booleans nil) (is_simple_prod? 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) (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) (Easr const-decl "SquareMatrix(pn)" matrix_det nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Easr_simple_prod formula-decl nil matrix_det nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_full application-judgement "FullMatrix" matrices nil)) nil)) (upper_triangulate_TCC31 0 (upper_triangulate_TCC31-1 nil 3615110328 ("" (skeep) (("" (skeep) (("" (assert) (("" (replace 6) (("" (rewrite "Id_simple_prod") nil nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "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) (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) (FALSE const-decl "bool" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Id_simple_prod formula-decl nil matrix_det nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (upper_triangulate_TCC32 0 (upper_triangulate_TCC32-1 nil 3615110328 ("" (skeep) (("" (assert) (("" (skeep) (("" (assert) (("" (lemma "mult_Easr_left") (("" (inst?) (("" (inst - "pn") (("" (assert) (("" (split -) (("1" (replaces -1 :dir rl) (("1" (rewrite "matrix_mult_assoc") (("1" (lemma "mult_Easr_left") (("1" (inst - "S" _ _ _ _) (("1" (inst?) (("1" (assert) (("1" (split -1) (("1" (replaces -1 :dir rl) (("1" (assert) (("1" (typepred "T") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (typepred "i") (("2" (typepred "j") (("2" (expand "ut_point1") (("2" (expand "ut_point2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "i") (("3" (typepred "j") (("3" (expand "ut_point1") (("3" (expand "ut_point2") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "Q") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (typepred "i") (("2" (typepred "j") (("2" (expand "ut_point1") (("2" (expand "ut_point2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "i") (("3" (typepred "j") (("3" (expand "ut_point1") (("3" (expand "ut_point2") (("3" (flatten) (("3" (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) (minus_real_is_real application-judgement "real" reals nil) (mult_full application-judgement "FullMatrix" matrices nil) (real_div_nzreal_is_real application-judgement "real" reals 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_point2 const-decl "bool" matrix_upper_triang nil) (ut_point1 const-decl "bool" matrix_upper_triang 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) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Easr const-decl "SquareMatrix(pn)" 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) (matrix_mult_assoc formula-decl nil matrices nil) (mult_Easr_left formula-decl nil matrix_det nil)) nil)) (upper_triangulate_TCC33 0 (upper_triangulate_TCC33-1 nil 3615111640 ("" (skeep) (("" (skeep) (("" (assert) (("" (typepred "j") (("" (expand "ut_point1") (("" (flatten) (("" (assert) (("" (skeep 6) (("" (inst-cp - "k!1" "p") (("" (assert) (("" (rewrite "entry_replace_row" +) (("1" (assert) (("1" (lift-if) (("1" (split 6) (("1" (flatten) (("1" (replace -1) (("1" (assert) (("1" (rewrite "access_sum") (("1" (rewrite "access_scal") (("1" (rewrite "access_row") (("1" (rewrite "access_row") (("1" (inst - "j" "p") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) ("2" (rewrite "length_add_vect_same") (("1" (rewrite "matrix_props.length_row") (("1" (typepred "i") (("1" (typepred "j") (("1" (expand "ut_point1") (("1" (expand "ut_point2") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_scal_vect") (("2" (rewrite "matrix_props.length_row") (("2" (rewrite "matrix_props.length_row") (("2" (typepred "i") (("2" (typepred "j") (("2" (expand "ut_point1") (("2" (expand "ut_point2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_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_times_real_is_real application-judgement "real" reals nil) (access_scal formula-decl nil matrices 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) (ut_point2 const-decl "bool" matrix_upper_triang nil) (entry_replace_row formula-decl nil matrix_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (upper_triangulate_TCC34 0 (upper_triangulate_TCC34-1 nil 3615111640 ("" (skeep) (("" (skeep) (("" (case "i = 0") (("1" (typepred "i") (("1" (expand "ut_point2") (("1" (ground) nil nil)) nil)) nil) ("2" (assert) (("2" (typepred "i") (("2" (expand "ut_point2") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (rewrite "entry_replace_row" +) (("1" (lift-if) (("1" (split 6) (("1" (flatten) (("1" (assert) (("1" (rewrite "access_sum") (("1" (rewrite "access_scal") (("1" (rewrite "access_row") (("1" (rewrite "access_row") (("1" (inst-cp - "i") (("1" (inst - "j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (inst - "k!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_add_vect_same") (("1" (rewrite "matrix_props.length_row") nil nil) ("2" (rewrite "length_scal_vect") (("2" (rewrite "matrix_props.length_row" 1) (("2" (rewrite "matrix_props.length_row" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (length_add_vect_same formula-decl nil matrices 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_times_real_is_real application-judgement "real" reals nil) (access_scal formula-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (entry_replace_row formula-decl nil matrix_props nil) (NOT const-decl "[bool -> bool]" booleans 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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_point2 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) (ut_point1 const-decl "bool" matrix_upper_triang nil)) nil)) (upper_triangulate_TCC35 0 (upper_triangulate_TCC35-1 nil 3615111640 ("" (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) (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) (ut_point1 const-decl "bool" matrix_upper_triang nil) (ut_point2 const-decl "bool" matrix_upper_triang nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (/= const-decl "boolean" notequal nil) (Easr const-decl "SquareMatrix(pn)" matrix_det nil) (is_simple_seq? const-decl "bool" matrix_det 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) (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) (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) (real_div_nzreal_is_real application-judgement "real" reals nil) (entry const-decl "real" matrices nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (upper_triangulate_TCC36 0 (upper_triangulate_TCC36-1 nil 3615121566 ("" (skeep) (("" (skeep) (("" (rewrite "lex3_lt_2") (("1" (hide 7) (("1" (flatten) (("1" (rewrite "length_add_vect_same") (("1" (rewrite "matrix_props.length_row") (("1" (typepred "i") (("1" (typepred "j") (("1" (expand "ut_point1") (("1" (expand "ut_point2") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_scal_vect") (("2" (rewrite "matrix_props.length_row") (("2" (rewrite "matrix_props.length_row") (("2" (typepred "i") (("2" (typepred "j") (("2" (expand "ut_point1") (("2" (expand "ut_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 "matrix_props.length_row") (("1" (typepred "i") (("1" (typepred "j") (("1" (expand "ut_point1") (("1" (expand "ut_point2") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_scal_vect") (("2" (rewrite "matrix_props.length_row") (("2" (rewrite "matrix_props.length_row") (("2" (typepred "i") (("2" (typepred "j") (("2" (expand "ut_point1") (("2" (expand "ut_point2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (case "i = 0") (("1" (typepred "i") (("1" (expand "ut_point2") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("4" (typepred "j") (("4" (assert) (("4" (expand "ut_point1") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((length_add_vect_same formula-decl nil matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (length_row formula-decl nil matrix_props nil) (length_scal_vect formula-decl nil matrices nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (* const-decl "VectorN(length(v2))" 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) (replace_row def-decl "{PFM | rows(PFM) = rows(D) AND columns(PFM) = columns(D) AND (FORALL (j): row(PFM)(j) = IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF) AND (FORALL (j, k): entry(PFM)(j, k) = IF j < rows(D) AND j = i THEN access(v)(k) ELSE entry(D)(j, k) ENDIF)}" matrix_props nil) (access const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (Vector type-eq-decl nil matrices 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) (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) (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) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (lex3_lt_2 formula-decl nil lex3 "orders/") (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)) nil)) (upper_triangulate_TCC37 0 (upper_triangulate_TCC37-1 nil 3615121566 ("" (skeep) (("" (case "i<pn aND j<pn AND i>j") (("1" (flatten) (("1" (case "NOT (null?(S) OR null?(Q) OR null?(R))") (("1" (flatten) (("1" (skeep) (("1" (case "NOT length(row(S)(i) + pivnum * row(S)(j)) = pn") (("1" (hide 11) (("1" (rewrite "length_add_vect") (("1" (rewrite "length_scal_vect") (("1" (rewrite "length_row") (("1" (rewrite "length_row") (("1" (expand "max") (("1" (assert) nil nil)) nil) ("2" (rewrite "length_rows") (("2" (assert) nil nil)) nil)) nil) ("2" (rewrite "length_rows") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT length(row(Q)(i) + pivnum * row(Q)(j)) = pn") (("1" (hide 11) (("1" (rewrite "length_add_vect") (("1" (rewrite "length_scal_vect") (("1" (rewrite "length_row") (("1" (rewrite "length_row") (("1" (expand "max") (("1" (assert) nil nil)) nil) ("2" (rewrite "length_rows") (("2" (assert) nil nil)) nil)) nil) ("2" (rewrite "length_rows") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "GG" "v(pn) (comp_matrix, comp_inverse, replace_row(i, row(S)(i) + pivnum * row(S)(j))(S), IF comp_matrix THEN replace_row(i, row(Q)(i) + pivnum * row(Q)(j))(Q) ELSE Id(pn) ENDIF, IF comp_matrix AND comp_inverse THEN R * Easr(pn)(i, j, -pivnum) ELSE Id(pn) ENDIF, T, j, i - 1, stop_rec, max(k - 1, 0))") (("1" (replaces -1) (("1" (typepred "GG") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (split 10) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (replace -4) (("3" (rewrite "det_replace_row_sum_scal") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 11) (("2" (rewrite "lex3_lt_2") nil nil)) nil) ("3" (hide 11) (("3" (assert) nil nil)) nil) ("4" (hide 11) (("4" (assert) (("4" (typepred "i") (("4" (typepred "j") (("4" (expand "ut_point1") (("4" (expand "ut_point2") (("4" (assert) (("4" (rewrite "rows_replace_row") (("4" (assert) (("4" (skeep) (("4" (rewrite "entry_replace_row") (("4" (lift-if) (("4" (assert) (("4" (split 1) (("1" (flatten) (("1" (rewrite "access_sum") (("1" (rewrite "access_scal") (("1" (rewrite "access_row") (("1" (rewrite "access_row") (("1" (inst-cp - "i" "j") (("1" (inst - "j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst - "k!1" "j") (("2" (inst - "k!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 11) (("5" (typepred "j") (("5" (typepred "i") (("5" (expand "ut_point1") (("5" (expand "ut_point2") (("5" (flatten) (("5" (assert) (("5" (rewrite "rows_replace_row") (("5" (assert) (("5" (skeep) (("5" (rewrite "entry_replace_row") (("5" (lift-if) (("5" (split 1) (("1" (flatten) (("1" (rewrite "access_sum") (("1" (rewrite "access_scal") (("1" (rewrite "access_row") (("1" (rewrite "access_row") (("1" (assert) (("1" (inst-cp - "i" "p") (("1" (inst - "j" "p") (("1" (assert) (("1" (inst - "i") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("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)) nil) ("6" (hide 11) (("6" (flatten) (("6" (assert) (("6" (lemma "mult_Easr_left") (("6" (inst - "Q" "i" "j" "pn" "pivnum") (("6" (assert) (("6" (replaces -1 :dir rl) (("6" (lemma "mult_Easr_left") (("6" (inst - "S" "i" "j" "pn" "pivnum") (("6" (assert) (("6" (replaces -1 :dir rl) (("6" (rewrite "matrix_mult_assoc") (("6" (typepred "T") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (hide 11) (("7" (flatten) (("7" (assert) (("7" (replace 1) (("7" (rewrite "Id_simple_prod") nil nil)) nil)) nil)) nil)) nil) ("8" (hide 11) (("8" (flatten) (("8" (assert) (("8" (split 1) (("1" (rewrite "mult_simple_prod") (("1" (rewrite "Easr_simple_prod") nil nil)) nil) ("2" (lemma "mult_Easr_left") (("2" (inst - "Q" "i" "j" "pn" "pivnum") (("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" (typepred "R") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "Easr_null") nil nil)) nil) ("2" (rewrite "Easr_null") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "mult_Easr_left") (("3" (inst - "Q" "i" "j" "pn" "pivnum") (("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" (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) ("4" (rewrite "rows_mult") (("4" (assert) nil nil)) nil) ("5" (rewrite "rows_mult") (("5" (rewrite "columns_mult") (("5" (assert) 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)) nil) ("9" (hide 11) (("9" (flatten) (("9" (rewrite "Id_simple_prod") nil nil)) nil)) nil) ("10" (hide 11) (("10" (flatten) (("10" (assert) (("10" (rewrite "rows_replace_row") (("10" (rewrite "columns_replace_row") (("10" (assert) (("10" (lemma "mult_Easr_left") (("10" (inst?) (("10" (inst - "pn") (("10" (assert) (("10" (replaces -1 :dir rl) (("10" (rewrite "mult_simple_prod") (("10" (rewrite "Easr_simple_prod") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("11" (hide 11) (("11" (assert) nil nil)) nil) ("12" (hide 11) (("12" (rewrite "rows_replace_row") (("12" (rewrite "columns_replace_row") (("12" (assert) nil nil)) nil)) nil)) nil) ("13" (hide 11) (("13" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 6) (("2" (label "igz" -1) (("2" (typepred "S") (("2" (typepred "Q") (("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (split "igz") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 7) (("2" (typepred "i") (("2" (typepred "j") (("2" (expand "ut_point2") (("2" (expand "ut_point1") (("2" (flatten) (("2" (assert) 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) (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) (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) (NOT const-decl "[bool -> bool]" booleans nil) (columns_replace_row formula-decl nil matrix_props nil) (columns_mult formula-decl nil matrices nil) (rows_mult formula-decl nil matrices nil) (Easr_null formula-decl nil matrix_det nil) (mult_Easr_Easr_inv formula-decl nil matrix_det nil) (mult_Id_left formula-decl nil matrices nil) (mult_simple_prod formula-decl nil matrix_det nil) (Easr_simple_prod formula-decl nil matrix_det nil) (Id_simple_prod formula-decl nil matrix_det nil) (matrix_mult_assoc formula-decl nil matrices nil) (mult_Easr_left formula-decl nil matrix_det nil) (entry_replace_row formula-decl nil matrix_props nil) (access_scal formula-decl nil matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (access_row formula-decl nil matrices nil) (real_plus_real_is_real application-judgement "real" reals nil) (access_sum formula-decl nil matrices nil) (rows_replace_row formula-decl nil matrix_props nil) (lex3_lt_2 formula-decl nil lex3 "orders/") (det_replace_row_sum_scal formula-decl nil matrix_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (mult_full application-judgement "FullMatrix" matrices 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) (ordstruct type-decl nil ordstruct_adt nil) (< def-decl "bool" ordinals nil) (ordinal? def-decl "bool" ordinals nil) (ordinal nonempty-type-eq-decl nil ordinals nil) (lex3 const-decl "ordinal" lex3 "orders/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (upper_triangular? const-decl "bool" matrix_det nil) (det def-decl "real" matrix_props nil) (access const-decl "real" matrices nil) (replace_row def-decl "{PFM | rows(PFM) = rows(D) AND columns(PFM) = columns(D) AND (FORALL (j): row(PFM)(j) = IF j < rows(D) AND j = i THEN v ELSE row(D)(j) ENDIF) AND (FORALL (j, k): entry(PFM)(j, k) = IF j < rows(D) AND j = i THEN access(v)(k) ELSE entry(D)(j, k) ENDIF)}" matrix_props nil) (Easr const-decl "SquareMatrix(pn)" matrix_det nil) (- const-decl "[numfield -> numfield]" number_fields nil) (length_scal_vect formula-decl nil matrices nil) (length_rows formula-decl nil matrices 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (length_row formula-decl nil matrices 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) (minus_real_is_real application-judgement "real" reals nil) (length_add_vect formula-decl nil matrices nil) (* const-decl "VectorN(length(v2))" matrices nil) (+ const-decl "VectorN(max(length(v1), length(v2)))" matrices nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) nil)) (upper_triangulate_TCC38 0 (upper_triangulate_TCC38-1 nil 3615121566 ("" (skeep) nil nil) nil nil)))
¤ Dauer der Verarbeitung: 0.240 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26