Impressum linear_dependence.prf

(linear_dependence
 (zerow_TCC1 0
  (zerow_TCC1-1 nil 3620493442
   ("" (skeep)
    (("" (splash +)
      (("1" (grind) nil nil) ("2" (grind) nil nil)
       ("3" (flatten)
        (("3" (skeep)
          (("3" (case "i=0")
            (("1" (case "j=0")
              (("1" (grind) nil nil)
               ("2" (typepred (j)) (("2" (grind) nil nil)) nil))
              nil)
             ("2" (grind)
              (("2" (typepred (i)) (("2" (grind) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, 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)
    (real nonempty-type-from-decl nil reals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" 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 "[T, T -> boolean]" equalities nil)
    (length def-decl "nat" list_props nil)
    (VectorN type-eq-decl nil matrices nil)
    (zero const-decl "VectorN(n)" matrices nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (null adt-constructor-decl "(null?)" 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)
    (rows const-decl "nat" matrices nil)
    (Matrix type-eq-decl nil 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (array2list_it def-decl
                   "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}"
                   array2list "structures/")
    (array2list const-decl
                "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
                array2list "structures/")
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil))
 (zerow_dim 0
  (zerow_dim-1 nil 3620567942
   ("" (skeep)
    (("" (split 1)
      (("1" (expand "rows")
        (("1" (ground) (("1" (grind) nil nil)) nil)) nil)
       ("2" (expand "zerow") (("2" (grind) nil nil)) nil))
      nil))
    nil)
   ((array2list_it def-decl
                   "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}"
                   array2list "structures/")
    (array2list const-decl
                "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
                array2list "structures/")
    (zero const-decl "VectorN(n)" matrices nil)
    (zerow const-decl "PosFullMatrix" linear_dependence nil)
    (length def-decl "nat" list_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (rows const-decl "nat" matrices nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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))
   shostak))
 (zecolumn_dim 0
  (zecolumn_dim-1 nil 3620568042
   ("" (skeep)
    (("" (expand "zecolumn")
      (("" (rewrite "rows_transpose")
        (("" (rewrite "columns_transpose")
          (("" (lemma "zerow_dim")
            (("" (inst?) (("" (ground) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((zecolumn const-decl "PosFullMatrix" linear_dependence nil)
    (columns_transpose formula-decl nil matrices nil)
    (zerow_dim formula-decl nil linear_dependence nil)
    (zerow const-decl "PosFullMatrix" linear_dependence nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (columns def-decl "{c: nat |
         (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
          (null?(M) AND c = 0 OR
            (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
             matrices nil)
    (<= const-decl "bool" reals nil)
    (rows const-decl "nat" matrices nil)
    (> const-decl "bool" reals nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (real nonempty-type-from-decl nil reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (Matrix type-eq-decl nil matrices nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil)
    (rows_transpose formula-decl nil matrices nil))
   shostak))
 (row2mat_TCC1 0
  (row2mat_TCC1-1 nil 3620493442
   ("" (skeep)
    (("" (splash)
      (("1" (typepred (A))
        (("1" (expand "columns")
          (("1" (ground)
            (("1" (expand "columns")
              (("1" (ground)
                (("1" (case "length(row(A)(j)) = columns(A)")
                  (("1" (ground) nil nil)
                   ("2" (ground)
                    (("2" (rewrite "length_row")
                      (("2" (typepred (j))
                        (("2" (expand "rows") (("2" (propax) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (ground) (("2" (grind) nil nil)) nil)
       ("3" (flatten)
        (("3" (skeep)
          (("3" (case "i=0")
            (("1" (case-replace "j_1=0")
              (("1" (replace -2) (("1" (propax) nil nil)) nil)
               ("2" (typepred (j_1)) (("2" (ground) nil nil)) nil))
              nil)
             ("2" (typepred (i)) (("2" (ground) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, 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)
    (real nonempty-type-from-decl nil reals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Vector type-eq-decl nil matrices nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (Matrix type-eq-decl nil matrices 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)
    (row const-decl "Vector" matrices 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)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length_row formula-decl nil matrices nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_max application-judgement "{k: int | i <= k AND j <= k}"
     real_defs 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_singleton formula-decl nil more_list_props "structures/"))
   nil))
 (row2mat_dim 0
  (row2mat_dim-1 nil 3620568149
   ("" (skeep)
    (("" (typepred (A))
      (("" (split 1)
        (("1" (grind) nil nil)
         ("2" (typepred "row2mat(A, j)")
          (("2" (lemma "matrices.length_row")
            (("2" (inst-cp -1 "A" "j")
              (("2" (split -2)
                (("1" (replace -1 :dir rl)
                  (("1" (typepred "columns(row2mat(A,j))")
                    (("1" (split -2)
                      (("1" (flatten) (("1" (ground) nil nil)) nil)
                       ("2" (skeep)
                        (("2" (case "i=0")
                          (("1" (replace -1)
                            (("1" (replace -2 :dir rl)
                              (("1" (grind) nil nil)) nil))
                            nil)
                           ("2" (typepred (i))
                            (("2" (hide-all-but (-1 1))
                              (("2"
                                (ground)
                                (("2" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (typepred (j))
                  (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_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)
    (length_row formula-decl nil matrices nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (row2mat const-decl "PosFullMatrix" linear_dependence nil)
    (row const-decl "Vector" matrices nil))
   shostak))
 (sum_rows_TCC1 0
  (sum_rows_TCC1-1 nil 3620493442
   ("" (skeep)
    (("" (splash +)
      (("1" (rewrite "columns_add")
        (("1" (rewrite "columns_scal") (("1" (ground) nil nil)) nil))
        nil)
       ("2" (rewrite "rows_add")
        (("2" (rewrite "rows_scal") (("2" (ground) nil nil)) nil)) nil)
       ("3" (flatten)
        (("3" (typepred "(M + f(j) * row2mat(A, j))")
          (("3" (skeep)
            (("3" (inst-cp - "i")
              (("3" (inst - "j_1") (("3" (ground) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, 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)
    (real nonempty-type-from-decl nil reals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Matrix type-eq-decl nil matrices 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)
    (rows const-decl "nat" matrices 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) (<= 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)
    (MatrixMN type-eq-decl nil matrices nil)
    (entry const-decl "real" matrices nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
       matrices nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (> const-decl "bool" reals nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "{A: MatrixMN(rows(M), columns(M)) |
         FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
       nil)
    (row2mat const-decl "PosFullMatrix" linear_dependence nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (columns_scal 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)
    (columns_add formula-decl nil matrices nil)
    (rows_scal formula-decl nil matrices nil)
    (rows_add formula-decl nil matrices nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil))
 (sum_rows_TCC2 0
  (sum_rows_TCC2-1 nil 3620493442 ("" (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)
    (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) (<= 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)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (rows const-decl "nat" matrices nil))
   nil))
 (sum_rows_TCC3 0
  (sum_rows_TCC3-2 nil 3620570095
   ("" (skeep)
    (("" (splash +)
      (("1" (rewrite "columns_add")
        (("1" (rewrite "columns_scal") (("1" (ground) nil nil)) nil))
        nil)
       ("2" (rewrite "rows_add")
        (("2" (rewrite "rows_scal") (("2" (ground) nil nil)) nil)) nil)
       ("3" (flatten)
        (("3" (typepred "(M + f(j) * row2mat(A, j))")
          (("3" (skeep)
            (("3" (inst-cp - "i")
              (("3" (inst - "j_1") (("3" (ground) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, 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)
    (real nonempty-type-from-decl nil reals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Matrix type-eq-decl nil matrices 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)
    (rows const-decl "nat" matrices 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) (<= 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)
    (MatrixMN type-eq-decl nil matrices nil)
    (entry const-decl "real" matrices nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
       matrices nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (> const-decl "bool" reals nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "{A: MatrixMN(rows(M), columns(M)) |
         FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
       nil)
    (row2mat const-decl "PosFullMatrix" linear_dependence nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (columns_scal 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)
    (columns_add formula-decl nil matrices nil)
    (rows_scal formula-decl nil matrices nil)
    (rows_add formula-decl nil matrices nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil)
  (sum_rows_TCC3-1 nil 3620493442 ("" (subtype-tcc) nil nil) nil nil))
 (sum_rows_TCC4 0
  (sum_rows_TCC4-1 nil 3620493442 ("" (termination-tcc) nil nil) nil
   nil))
 (sum_rows_TCC5 0
  (sum_rows_TCC5-1 nil 3620493442 ("" (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)
    (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) (<= 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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (rows const-decl "nat" matrices nil))
   nil))
 (sum_rows_TCC6 0
  (sum_rows_TCC6-1 nil 3620493442 ("" (subtype-tcc) nil nil) nil nil))
 (sum_rows_eq 0
  (sum_rows_eq-2 "alt-proof" 3620557971
   (""
    (case "FORALL (n:nat, A,M: PosFullMatrix, f, g: [nat -> real], j: below(rows(A))):
                             n=j IMPLIES ((FORALL (k: subrange(0, j)): f(k) = g(k)) IMPLIES
                              sum_rows(A, f, j, M) =
                               sum_rows(A, g, j, M))")
    (("1" (skeep)
      (("1" (inst -1 "j" "A" "M" "f" "g" "j")
        (("1" (split -1)
          (("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (induct "n")
        (("1" (skeep)
          (("1" (replace -1 :dir rl)
            (("1" (expand "sum_rows")
              (("1" (inst -2 "0")
                (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil))
              nil))
            nil))
          nil)
         ("2" (skeep)
          (("2" (skeep)
            (("2" (expand "sum_rows" 1)
              (("2" (lift-if 1)
                (("2" (split 1)
                  (("1" (flatten)
                    (("1" (inst -4 "j")
                      (("1" (replace -4) (("1" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (flatten)
                    (("2" (inst-cp -3 "j")
                      (("2" (replace -4)
                        (("2"
                          (inst -1 "A" "M + g(j) * row2mat(A, j)" "f"
                           "g" "j-1")
                          (("1" (split -1)
                            (("1" (propax) nil nil)
                             ("2" (skeep) (("2" (inst -2 "k") nil nil))
                              nil)
                             ("3" (ground) nil nil))
                            nil)
                           ("2" (ground) nil nil))
                          nil))
                        nil))
                      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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (A skolem-const-decl "PosFullMatrix" linear_dependence nil)
    (j skolem-const-decl "below(rows(A))" linear_dependence nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (MatrixMN type-eq-decl nil matrices nil)
    (entry const-decl "real" matrices nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
       matrices nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "{A: MatrixMN(rows(M), columns(M)) |
         FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
       nil)
    (row2mat const-decl "PosFullMatrix" linear_dependence nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (Matrix type-eq-decl nil matrices nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (< const-decl "bool" reals nil)
    (length def-decl "nat" list_props nil)
    (below type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (> const-decl "bool" reals nil)
    (rows const-decl "nat" matrices nil)
    (<= const-decl "bool" reals nil)
    (columns def-decl "{c: nat |
         (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
          (null?(M) AND c = 0 OR
            (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
             matrices nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (sum_rows def-decl "PosFullMatrix" linear_dependence nil))
   shostak)
  (sum_rows_eq-1 nil 3620555529
   (""
    (case "FORALL (n:nat, A: PosFullMatrix, f, g: [nat -> real], j: below(rows(A))):
                      n=j IMPLIES ((FORALL (k: subrange(0, j)): f(k) = g(k)) IMPLIES
                       sum_rows(A, f, j, zerow(columns(A))) =
                        sum_rows(A, g, j, zerow(columns(A))))")
    (("1" (skeep)
      (("1" (inst -1 "j" "A" "f" "g" "j")
        (("1" (split -1)
          (("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (induct "n")
        (("1" (skeep)
          (("1" (replace -1 :dir rl)
            (("1" (expand "sum_rows")
              (("1" (inst -2 "0")
                (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil))
              nil))
            nil))
          nil)
         ("2" (skeep)
          (("2" (skeep)
            (("2" (expand "sum_rows" 1)
              (("2" (lift-if 1)
                (("2" (split 1)
                  (("1" (flatten)
                    (("1" (inst -4 "j")
                      (("1" (replace -4) (("1" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (flatten)
                    (("2" (inst -3 "j")
                      (("2" (replace -3)
                        (("2" (inst -1 "A" "f" "g" "j-1")
                          (("1" (split -1)
                            (("1" (ground) (("1" (postpone) nil nil))
                              nil)
                             ("2" (postpone) nil nil)
                             ("3" (postpone) nil nil))
                            nil)
                           ("2" (ground) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (sum_rows_add_start_TCC1 0
  (sum_rows_add_start_TCC1-2 nil 3620570216
   ("" (skeep)
    (("" (splash +)
      (("1" (rewrite "columns_add") (("1" (ground) nil nil)) nil)
       ("2" (rewrite "rows_add") (("2" (ground) nil nil)) nil)
       ("3" (flatten)
        (("3" (typepred "(M + N)")
          (("3" (skeep)
            (("3" (inst-cp - "i")
              (("3" (inst - "j_1") (("3" (ground) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, 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)
    (real nonempty-type-from-decl nil reals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (Matrix type-eq-decl nil matrices 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)
    (rows const-decl "nat" matrices 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) (<= 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)
    (MatrixMN type-eq-decl nil matrices nil)
    (entry const-decl "real" matrices nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
       matrices nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (> const-decl "bool" reals nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (columns_add formula-decl nil matrices nil)
    (rows_add formula-decl nil matrices nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil)
  (sum_rows_add_start_TCC1-1 nil 3620563385 ("" (subtype-tcc) nil nil)
   nil nil))
 (sum_rows_add_start 0
  (sum_rows_add_start-1 nil 3620563440
   (""
    (case "FORALL (n:nat, A, M, N: PosFullMatrix, f: [nat -> real], j: below(rows(A))):
        n=j IMPLIES
        sum_rows(A, f, j, M + N) = sum_rows(A, f, j, M) + N")
    (("1" (skeep) (("1" (inst -1 "j" "A" "M" "N" "f" "j") nil nil))
      nil)
     ("2" (hide 2)
      (("2" (induct "n")
        (("1" (skeep)
          (("1" (replace -1 :dir rl)
            (("1" (expand "sum_rows")
              (("1" (ground)
                (("1" (lemma "matrix_add_comm")
                  (("1" (inst -1 "N" "f(0) * row2mat(A, 0)")
                    (("1" (ground)
                      (("1" (rewrite "matrix_add_assoc" 1)
                        (("1" (rewrite "matrix_add_assoc" 1)
                          (("1" (ground) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skeep)
          (("2" (skeep)
            (("2" (expand "sum_rows" 1)
              (("2" (lift-if 1)
                (("2" (split 1)
                  (("1" (flatten) (("1" (ground) nil nil)) nil)
                   ("2" (flatten)
                    (("2" (hide -2)
                      (("2" (rewrite "matrix_add_assoc" 2)
                        (("2" (rewrite "matrix_add_comm" (2 2))
                          (("2" (rewrite "matrix_add_assoc" 2 :dir rl)
                            (("2"
                              (inst -1 "A" "M + f(j) * row2mat(A, j)"
                               "N" "f" "j-1")
                              (("1"
                                (split -1)
                                (("1" (propax) nil nil)
                                 ("2"
                                  (reveal -2)
                                  (("2" (ground) nil nil))
                                  nil))
                                nil)
                               ("2" (ground) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (hide 2)
          (("3" (skeep)
            (("3" (splash +)
              (("1" (rewrite "columns_add") (("1" (ground) nil nil))
                nil)
               ("2" (rewrite "rows_add") (("2" (ground) nil nil)) nil)
               ("3" (flatten)
                (("3" (skeep)
                  (("3" (typepred "M+N")
                    (("3" (inst-cp - "i")
                      (("3" (inst - "j_1") (("3" (ground) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skeep)
      (("3" (typepred "M + N")
        (("3" (split 1)
          (("1" (flatten)
            (("1" (skeep)
              (("1" (inst-cp -3 "i")
                (("1" (inst-cp - "j_1") (("1" (ground) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (ground)
            (("2" (rewrite "rows_add") (("2" (ground) nil nil)) nil))
            nil)
           ("3" (rewrite "columns_add") (("3" (ground) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (columns_add formula-decl nil matrices nil)
    (rows_add formula-decl nil matrices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (A skolem-const-decl "PosFullMatrix" linear_dependence nil)
    (j skolem-const-decl "below(rows(A))" linear_dependence nil)
    (matrix_add_comm formula-decl nil matrices nil)
    (matrix_add_assoc formula-decl nil matrices nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "{A: MatrixMN(rows(M), columns(M)) |
         FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
       nil)
    (row2mat const-decl "PosFullMatrix" linear_dependence nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (Matrix type-eq-decl nil matrices nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (< const-decl "bool" reals nil)
    (length def-decl "nat" list_props nil)
    (below type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (> const-decl "bool" reals nil)
    (rows const-decl "nat" matrices nil)
    (<= const-decl "bool" reals nil)
    (columns def-decl "{c: nat |
         (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
          (null?(M) AND c = 0 OR
            (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
             matrices nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sum_rows def-decl "PosFullMatrix" linear_dependence nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (MatrixMN type-eq-decl nil matrices nil)
    (entry const-decl "real" matrices nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
       matrices nil))
   shostak))
 (subtract_same_scal 0
  (subtract_same_scal-1 nil 3620554565
   ("" (skeep)
    (("" (typepred "f(j) * row2mat(A, j) - f(j) * row2mat(A, j)")
      (("" (typepred "0 * row2mat(A, j)")
        (("" (lemma "matrix2array" ("SM" "0*row2mat(A,j)"))
          (("1" (replace -1 1)
            (("1" (hide -1)
              (("1"
                (lemma "matrix2array"
                 ("SM"
                  "(f(j) * row2mat(A, j) - f(j) * row2mat(A, j))"))
                (("1" (replace -1 1)
                  (("1" (hide -1)
                    (("1" (rewrite "rows_sub")
                      (("1" (rewrite "columns_sub")
                        (("1" (expand "max")
                          (("1" (rewrite "rows_scal")
                            (("1" (rewrite "rows_scal")
                              (("1"
                                (rewrite "columns_scal")
                                (("1"
                                  (rewrite "columns_scal")
                                  (("1"
                                    (lemma "form_matrix_eq")
                                    (("1"
                                      (inst?)
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (split -1)
                                            (("1" (propax) nil nil)
                                             ("2"
                                              (skeep)
                                              (("2"
                                                (inst -6 "i" "j_1")
                                                (("2"
                                                  (inst -10 "i" "j_1")
                                                  (("2"
                                                    (ground)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (skeep)
                    (("2" (inst-cp -7 "i")
                      (("2" (inst -7 "j_1") (("2" (ground) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (flatten)
            (("2" (ground)
              (("2" (skeep)
                (("2" (inst-cp -3 "i")
                  (("2" (inst -3 "j_1") (("2" (ground) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((row2mat const-decl "PosFullMatrix" linear_dependence nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (> const-decl "bool" reals nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (* const-decl "{A: MatrixMN(rows(M), columns(M)) |
         FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
       nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) - entry(N)(i, j)}"
       matrices nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (entry const-decl "real" matrices nil)
    (MatrixMN 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)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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)
    (rows const-decl "nat" 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)
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (matrix2array formula-decl nil matrices nil)
    (rows_sub 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_times_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (form_matrix_eq formula-decl nil matrices nil)
    (columns_scal formula-decl nil matrices nil)
    (rows_scal formula-decl nil matrices nil)
    (columns_sub formula-decl nil matrices nil))
   shostak))
 (sum_lem_prep_TCC1 0
  (sum_lem_prep_TCC1-1 nil 3620563013 ("" (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)
    (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) (<= 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (rows const-decl "nat" matrices nil))
   nil))
 (sum_lem_prep 0
  (sum_lem_prep-1 nil 3620565983
   (""
    (case "FORALL (n:nat, A, M: PosFullMatrix, f: [nat -> real], j: below(rows(A)),
              k: below(1 + j)):
        n=j IMPLIES
        sum_rows(A, f WITH [k := 0], j, M) =
         sum_rows(A, f, j, M) - f(k) * row2mat(A, k)")
    (("1" (skeep) (("1" (inst -1 "j" "A" "M" "f" "j" "k") nil nil))
      nil)
     ("2" (hide 2)
      (("2" (induct "n")
        (("1" (skeep)
          (("1" (replace -1 :dir rl)
            (("1" (expand "sum_rows")
              (("1" (typepred (k))
                (("1" (case-replace "k=0")
                  (("1" (simplify 1)
                    (("1" (expand "-")
                      (("1" (expand "sub")
                        (("1" (rewrite "matrix_add_assoc" 1)
                          (("1" (lemma "subtract_same_scal")
                            (("1" (inst?)
                              (("1"
                                (expand "-")
                                (("1"
                                  (expand "sub")
                                  (("1" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (ground) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skeep)
          (("2" (skeep)
            (("2" (expand "sum_rows" 1)
              (("2" (lift-if 1)
                (("2" (split 1)
                  (("1" (flatten) (("1" (ground) nil nil)) nil)
                   ("2" (flatten)
                    (("2" (split 2)
                      (("1" (flatten)
                        (("1" (lemma "sum_rows_eq")
                          (("1"
                            (inst -1 "A" "M + 0 * row2mat(A, j)"
                             "f WITH [k := 0]" "f" "j-1")
                            (("1" (split -1)
                              (("1"
                                (replace -1)
                                (("1"
                                  (replace -2 1 :dir rl)
                                  (("1"
                                    (expand "-" 1)
                                    (("1"
                                      (expand "sub")
                                      (("1"
                                        (rewrite
                                         "sum_rows_add_start"
                                         1
                                         :dir
                                         rl)
                                        (("1"
                                          (rewrite
                                           "matrix_add_assoc"
                                           1)
                                          (("1"
                                            (lemma
                                             "subtract_same_scal")
                                            (("1"
                                              (inst -1 "A" "f" "j")
                                              (("1"
                                                (expand "-")
                                                (("1"
                                                  (expand "sub")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide (2 3))
                                          (("2"
                                            (splash +)
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (typepred
                                                 "-1 * (f(j) * row2mat(A, j))")
                                                (("1"
                                                  (skeep)
                                                  (("1"
                                                    (inst-cp - "i")
                                                    (("1"
                                                      (inst - "j_1!1")
                                                      (("1"
                                                        (ground)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (rewrite "columns_scal")
                                              (("2"
                                                (rewrite
                                                 "columns_scal")
                                                (("2"
                                                  (lemma "row2mat_dim")
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (rewrite "rows_scal")
                                              (("3"
                                                (rewrite "rows_scal")
                                                (("3"
                                                  (lemma "row2mat_dim")
                                                  (("3"
                                                    (inst?)
                                                    (("3"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("4"
                                              (flatten)
                                              (("4"
                                                (typepred
                                                 "-1 * (f(j) * row2mat(A, j))")
                                                (("4"
                                                  (skeep)
                                                  (("4"
                                                    (inst-cp - "i")
                                                    (("4"
                                                      (inst - "j_1!1")
                                                      (("4"
                                                        (ground)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (skeep)
                                (("2"
                                  (typepred (k_1))
                                  (("2"
                                    (ground)
                                    (("2"
                                      (replace -3)
                                      (("2" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (ground) nil nil))
                            nil))
                          nil))
                        nil)
                       ("2" (flatten)
                        (("2" (inst?)
                          (("1" (split -1)
                            (("1" (propax) nil nil)
                             ("2" (ground) nil nil))
                            nil)
                           ("2" (ground) nil nil)
                           ("3" (ground) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (sum_rows_eq formula-decl nil linear_dependence nil)
    (rows_scal formula-decl nil matrices nil)
    (columns_scal formula-decl nil matrices nil)
    (row2mat_dim formula-decl nil linear_dependence nil)
    (sum_rows_add_start formula-decl nil linear_dependence nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (subrange type-eq-decl nil integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (+ const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) + entry(N)(i, j)}"
       matrices nil)
    (j skolem-const-decl "below(rows(A))" linear_dependence nil)
    (A skolem-const-decl "PosFullMatrix" linear_dependence nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (k skolem-const-decl "below(1 + j)" linear_dependence nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (matrix_add_assoc formula-decl nil matrices nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (subtract_same_scal formula-decl nil linear_dependence nil)
    (sub const-decl
         "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) - entry(N)(i, j)}"
         matrices nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (Matrix type-eq-decl nil matrices nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (< const-decl "bool" reals nil)
    (length def-decl "nat" list_props nil)
    (below type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (> const-decl "bool" reals nil)
    (rows const-decl "nat" matrices nil)
    (<= const-decl "bool" reals nil)
    (columns def-decl "{c: nat |
         (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
          (null?(M) AND c = 0 OR
            (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
             matrices nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sum_rows def-decl "PosFullMatrix" linear_dependence nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (MatrixMN type-eq-decl nil matrices nil)
    (entry const-decl "real" matrices nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) - entry(N)(i, j)}"
       matrices nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "{A: MatrixMN(rows(M), columns(M)) |
         FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
       nil)
    (row2mat const-decl "PosFullMatrix" linear_dependence nil))
   shostak))
 (sum_lem 0
  (sum_lem-1 nil 3620494148
   ("" (expand "sum_rows")
    (("" (skeep)
      (("" (lemma "sum_lem_prep")
        (("" (inst -1 "A" "zerow(columns(A))" "f" "rows(A)-1" "j") 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)
    (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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (zerow const-decl "PosFullMatrix" linear_dependence nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sum_lem_prep formula-decl nil linear_dependence nil)
    (sum_rows const-decl "PosFullMatrix" linear_dependence nil))
   shostak))
 (row_dependence_lem 0
  (row_dependence_lem-1 nil 3620493681
   ("" (skeep)
    (("" (expand "row_dependent")
      (("" (rewrite "sum_lem")
        (("" (typepred (f))
          (("" (replace -1)
            (("" (replace -2)
              ((""
                (typepred "(zerow(columns(A)) - -1 * row2mat(A, j))")
                ((""
                  (case-replace
                   "(zerow(columns(A)) - -1 * row2mat(A, j)) = row2mat(A,j)")
                  (("" (hide 2)
                    ((""
                      (lemma "matrix2array"
                       ("SM"
                        "(zerow(columns(A)) - -1 * row2mat(A, j))"))
                      (("1" (replace -1 1)
                        (("1" (hide -1)
                          (("1"
                            (lemma "matrix2array"
                             ("SM" "row2mat(A,j)"))
                            (("1"
                              (name-replace "FMB"
                               "form_matrix(entry((zerow(columns(A)) - -1 * row2mat(A, j))),
                  rows((zerow(columns(A)) - -1 * row2mat(A, j))),
                  columns((zerow(columns(A)) - -1 * row2mat(A, j))))")
                              (("1"
                                (replace -1 1)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (expand "FMB")
                                    (("1"
                                      (rewrite "rows_sub")
                                      (("1"
                                        (rewrite "columns_sub")
                                        (("1"
                                          (rewrite "rows_scal")
                                          (("1"
                                            (rewrite "columns_scal")
                                            (("1"
                                              (lemma "zerow_dim")
                                              (("1"
                                                (inst -1 "columns(A)")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (replace -2)
                                                      (("1"
                                                        (lemma
                                                         "row2mat_dim")
                                                        (("1"
                                                          (inst
                                                           -1
                                                           "A"
                                                           "j")
                                                          (("1"
                                                            (flatten)
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (replace
                                                                 -2)
                                                                (("1"
                                                                  (expand
                                                                   "max"
                                                                   1)
                                                                  (("1"
                                                                    (rewrite
                                                                     "form_matrix_eq")
                                                                    (("1"
                                                                      (skeep)
                                                                      (("1"
                                                                        (inst
                                                                         -10
                                                                         "i"
                                                                         "j_1")
                                                                        (("1"
                                                                          (replace
                                                                           -10)
                                                                          (("1"
                                                                            (case-replace
                                                                             "entry(zerow(columns(A)))(i,j_1) = 0")
                                                                            (("1"
                                                                              (simplify
                                                                               1)
                                                                              (("1"
                                                                                (typepred
                                                                                 "-1 * entry(-1 * row2mat(A, j))(i, j_1)")
                                                                                (("1"
                                                                                  (typepred
                                                                                   "-1 * row2mat(A, j)")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -4
                                                                                     "i"
                                                                                     "j_1")
                                                                                    (("1"
                                                                                      (replace
                                                                                       -4)
                                                                                      (("1"
                                                                                        (ground)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (hide
                                                                               2)
                                                                              (("2"
                                                                                (case-replace
                                                                                 "i=0")
                                                                                (("1"
                                                                                  (case
                                                                                   "row(zerow(columns(A)))(0) = zero(columns(A))")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "entry")
                                                                                    (("1"
                                                                                      (replace
                                                                                       -1)
                                                                                      (("1"
                                                                                        (rewrite
                                                                                         "access_zero")
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (expand
                                                                                     "row")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "zerow")
                                                                                      (("2"
                                                                                        (lift-if
                                                                                         1)
                                                                                        (("2"
                                                                                          (split
                                                                                           1)
                                                                                          (("1"
                                                                                            (flatten)
                                                                                            (("1"
                                                                                              (ground)
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (flatten)
                                                                                            (("2"
                                                                                              (ground)
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "nth")
                                                                                                (("2"
                                                                                                  (propax)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (ground)
                                                                                  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)
                       ("2" (flatten)
                        (("2" (ground)
                          (("2" (skeep)
                            (("2" (inst-cp -3 "i")
                              (("2"
                                (inst -3 "j_1")
                                (("2" (ground) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((row_dependent const-decl "bool" linear_dependence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (matrix2array formula-decl nil matrices nil)
    (form_matrix const-decl "{M: MatrixMN(m, n) |
         FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}"
                 matrices nil)
    (row const-decl "Vector" matrices nil)
    (Vector type-eq-decl nil matrices nil)
    (form_matrix_square application-judgement "FullMatrix" matrices
     nil)
    (rows_sub 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)
    (rows_scal formula-decl nil matrices nil)
    (zerow_dim formula-decl nil linear_dependence nil)
    (VectorN type-eq-decl nil matrices nil)
    (zero const-decl "VectorN(n)" matrices nil)
    (access_zero formula-decl nil matrices nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (length_singleton formula-decl nil more_list_props "structures/")
    (posint_max application-judgement "{k: posint | i <= k AND j <= k}"
     real_defs nil)
    (nzint_max application-judgement "{k: nzint | i <= k AND j <= k}"
     real_defs nil)
    (posrat_max application-judgement "{s: posrat | s >= q AND s >= r}"
     real_defs nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (form_matrix_eq formula-decl nil matrices nil)
    (row2mat_dim formula-decl nil linear_dependence nil)
    (columns_scal formula-decl nil matrices nil)
    (columns_sub formula-decl nil matrices nil)
    (FMB skolem-const-decl "{M:
   MatrixMN(rows((zerow(columns(A)) - -1 * row2mat(A, j))),
            columns((zerow(columns(A)) - -1 * row2mat(A, j)))) |
         FORALL (i: below(rows((zerow(columns(A)) - -1 * row2mat(A, j)))),
                 j_1:
                   below(columns((zerow(columns(A)) -
                                   -1 * row2mat(A, j))))):
           nth(row(M)(i), j_1) =
            entry((zerow(columns(A)) - -1 * row2mat(A, j)))(i, j_1)}"
     linear_dependence nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (MatrixMN type-eq-decl nil matrices nil)
    (entry const-decl "real" matrices nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl
       "{A: MatrixMN(max(rows(M), rows(N)), max(columns(M), columns(N))) |
         FORALL (i, j): entry(A)(i, j) = entry(M)(i, j) - entry(N)(i, j)}"
       matrices nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (zerow const-decl "PosFullMatrix" linear_dependence nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "{A: MatrixMN(rows(M), columns(M)) |
         FORALL (i, j): entry(A)(i, j) = r * entry(M)(i, j)}" matrices
       nil)
    (row2mat const-decl "PosFullMatrix" linear_dependence nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (PosFullMatrix type-eq-decl nil matrices nil)
    (columns def-decl "{c: nat |
         (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND
          (null?(M) AND c = 0 OR
            (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}"
             matrices nil)
    (<= const-decl "bool" reals nil)
    (rows const-decl "nat" matrices nil)
    (> const-decl "bool" reals nil)
    (FullMatrix type-eq-decl nil matrices nil)
    (nth def-decl "T" list_props nil)
    (below type-eq-decl nil nat_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil naturalnumbers nil)
    (length def-decl "nat" list_props nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (real nonempty-type-from-decl nil reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (Matrix type-eq-decl nil matrices nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (number nonempty-type-decl nil numbers nil)
    (sum_lem formula-decl nil linear_dependence nil))
   shostak)))