| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/matrices/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 935 kB |
|
Quelle matrices.prfSprache: Lisp |
|||||||||||||||
|
(matrices (IMP_sigma_swap_TCC1 0 (IMP_sigma_swap_TCC1-1 nil 3621252270 ("" (assuming-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (length_matrix_eq 0 (length_matrix_eq-1 nil 3618314996 ("" (skeep :but "LL") (("" (induct-and-simplify "LL") nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (list_induction formula-decl nil list_adt 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) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/")) nil)) (nth_matrix_eq_TCC1 0 (nth_matrix_eq_TCC1-2 nil 3618315122 ("" (skeep :preds? t) (("" (rewrite "length_matrix_eq") nil nil)) nil) ((length_matrix_eq formula-decl nil matrices 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) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/")) nil) (nth_matrix_eq_TCC1-1 nil 3618314996 ("" (subtype-tcc) nil nil) nil nil)) (nth_matrix_eq 0 (nth_matrix_eq-1 nil 3618315013 ("" (case "FORALL (i,nn: nat, LL: list[listn[real](nn)]) : i < length[list[real]](LL) IMPLIES nt (("1" (skeep) (("1" (insteep) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "i") (("1" (grind) nil nil) ("2" (skeep*) (("2" (expand "nth" 1) (("2" (inst -1 "nn" "cdr(LL)") (("2" (assert) (("2" (hide 2) (("2" (expand "length" -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (rewrite "length_matrix_eq") nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (rewrite "length_matrix_eq") nil nil)) nil)) nil)) nil) ((length_matrix_eq formula-decl nil matrices nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (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) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil)) nil)) (length_matrix_equiv 0 (length_matrix_equiv-1 nil 3613207327 ("" (skolem 1 ("nn" _)) (("" (induct "LL") (("1" (grind) nil nil) ("2" (skolem 1 ("v" "L")) (("2" (flatten) (("2" (expand "length" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((listn type-eq-decl nil listn "structures/") (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (= const-decl "[T, T -> boolean]" equalities nil) (real nonempty-type-from-decl nil reals nil) (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) (list_induction formula-decl nil list_adt nil)) shostak)) (length_matrix_nth 0 (length_matrix_nth-1 nil 3613210127 ("" (skolem 1 ("nn" _ _)) (("" (induct "LL") (("1" (grind) nil nil) ("2" (skolem 1 ("v" "L")) (("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (expand "length" +) (("2" (lift-if) (("2" (ground) (("1" (typepred "L") (("1" (rewrite "every_nth") (("1" (expand "nth" -2) (("1" (lift-if) (("1" (ground) (("1" (typepred "v") (("1" (grind) nil nil)) nil) ("2" (inst - "i-1") (("1" (flatten) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nth" 2) (("2" (lift-if) (("2" (ground) (("1" (typepred "v") (("1" (expand "length" -2) (("1" (lift-if) (("1" (ground) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "i-1") (("2" (expand "length" -1) (("2" (lift-if) (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (listn type-eq-decl nil listn "structures/") (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (= const-decl "[T, T -> boolean]" equalities nil) (real nonempty-type-from-decl nil reals nil) (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) (list_induction formula-decl nil list_adt nil) (NOT const-decl "[bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt 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) (int_minus_int_is_int application-judgement "int" integers nil) (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nn skolem-const-decl "nat" matrices nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (v skolem-const-decl "listn[real](nn)" matrices nil) (L skolem-const-decl "list[listn[real](nn)]" matrices nil) (i skolem-const-decl "below[length[list[real]](cons(v, L))]" matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (every_nth formula-decl nil list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (matrix_listn_nth_TCC1 0 (matrix_listn_nth_TCC1-2 nil 3618315146 ("" (skeep :preds? t) (("" (hide -2) (("" (rewrite "nth_matrix_eq") nil nil)) nil)) nil) ((below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (listn type-eq-decl nil listn "structures/") (length def-decl "nat" list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nth_matrix_eq formula-decl nil matrices nil)) nil) (matrix_listn_nth_TCC1-1 nil 3613218314 ("" (skeep) (("" (rewrite "length_matrix_equiv" :dir rl) (("" (assert) nil nil)) nil)) nil) ((listn type-eq-decl nil listn "structures/")) nil)) (matrix_listn_nth 0 (matrix_listn_nth-2 nil 3618315031 ("" (skeep) (("" (rewrite "nth_matrix_eq") nil nil)) nil) ((nth_matrix_eq formula-decl nil matrices 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) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil)) nil) (matrix_listn_nth-1 nil 3613218443 ("" (postpone) nil nil) nil shostak)) (length_rows 0 (length_rows-1 nil 3615893404 ("" (skeep) (("" (expand "rows") (("" (propax) nil nil)) nil)) nil) ((rows const-decl "nat" matrices nil)) shostak)) (columns_TCC1 0 (columns_TCC1-1 nil 3613146060 ("" (skeep) (("" (assert) (("" (skosimp*) (("" (typepred "i!1") (("" (hide +) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (length def-decl "nat" list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (columns_TCC2 0 (columns_TCC2-1 nil 3613146060 ("" (termination-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)) nil)) (columns_TCC3 0 (columns_TCC3-1 nil 3613228106 ("" (termination-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) (length def-decl "nat" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (columns_TCC4 0 (columns_TCC4-1 nil 3613228106 ("" (skeep) (("" (assert) (("" (split) (("1" (expand "max") (("1" (case "length[real](car[list[real]](M)) < v(cdr[list[real]](M))") (("1" (assert) (("1" (typepred "v(cdr[list[real]](M))") (("1" (skeep) (("1" (typepred "i") (("1" (case "i = 0") (("1" (expand "nth" 1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst - "i-1") (("1" (assert) (("1" (expand "nth" +) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "length" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (case "i = 0") (("1" (expand "nth" 2) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (typepred "v(cdr[list[real]](M))") (("2" (inst - "i-1") (("1" (assert) (("1" (expand "nth" 3) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "i") (("2" (expand "length" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "length" 1 2) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "max" 1) (("2" (case "length[real](car[list[real]](M)) < v(cdr[list[real]](M))") (("1" (assert) (("1" (typepred "v(cdr[list[real]](M))") (("1" (assert) (("1" (skosimp*) (("1" (inst + "i!1+1") (("1" (expand "nth" 1) (("1" (propax) nil nil)) nil) ("2" (typepred "i!1") (("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst + "0") (("1" (expand "nth" 2) (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "length" 1 2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "below(length(cdr[list[real]](M)))" matrices nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (i skolem-const-decl "below(length(M))" matrices nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (M skolem-const-decl "Matrix" matrices nil) (i skolem-const-decl "below(length(M))" matrices nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (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) (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) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (Matrix type-eq-decl nil matrices nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)) nil)) (row_TCC1 0 (row_TCC1-1 nil 3613147893 ("" (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) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (col_TCC1 0 (col_TCC1-1 nil 3613147893 ("" (grind) 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) (length def-decl "nat" list_props nil) (rows const-decl "nat" matrices nil)) nil)) (col_TCC2 0 (col_TCC2-1 nil 3613147893 ("" (skeep) (("" (expand "rows" +) (("" (expand "length" + 2) (("" (assert) (("" (expand "length" + 1) (("" (typepred "v(cdr[list[real]](M))(i)") (("" (replaces -2) (("" (expand "rows") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rows const-decl "nat" matrices nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (VectorN type-eq-decl nil matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (length def-decl "nat" list_props nil)) nil)) (col_def_TCC1 0 (col_def_TCC1-1 nil 3613306052 ("" (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) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (rows const-decl "nat" matrices nil)) nil)) (col_def_TCC2 0 (col_def_TCC2-1 nil 3613306052 ("" (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) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (rows const-decl "nat" matrices nil)) nil)) (col_def 0 (col_def-1 nil 3613306076 ("" (induct "M") (("1" (skeep) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (skolem 1 ("v" "M")) (("2" (flatten) (("2" (skeep) (("2" (assert) (("2" (splash +) (("1" (skeep) (("1" (typepred "j") (("1" (lift-if) (("1" (ground) (("1" (case "j = 0") (("1" (replace -1) (("1" (assert) (("1" (expand "nth" + 1) (("1" (expand "col" + 1) (("1" (expand "nth" + 2) (("1" (expand "access") (("1" (lift-if) (("1" (ground) (("1" (expand "nth" -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "nth" + 1) (("2" (expand "nth" + 3) (("2" (expand "col" +) (("2" (inst - "i") (("2" (flatten) (("2" (inst - "j-1") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (expand "nth" -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "rows" -2) (("2" (expand "length" -2) (("2" (assert) (("2" (expand "rows" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "i") (("2" (flatten) (("2" (assert) (("2" (expand "col" +) (("2" (expand "nth" 2) (("2" (lift-if) (("2" (ground) (("1" (replaces -1) (("1" (expand "access" 1) (("1" (lift-if) (("1" (ground) (("1" (expand "nth" 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "j-1") (("1" (assert) (("1" (replaces -4) (("1" (lift-if) (("1" (ground) (("1" (expand "nth" 3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rows" (-1 1)) (("2" (expand "length" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "col(cons(v,M))(i)") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (skosimp*) (("3" (typepred "j!1") (("3" (expand "rows") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (typepred "j!1") (("4" (expand "rows") (("4" (propax) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (typepred "j!1") (("5" (expand "rows") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt 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) (v skolem-const-decl "list[real]" matrices nil) (M skolem-const-decl "list[list[real]]" matrices nil) (j skolem-const-decl "below(rows(cons(v, M)))" matrices nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (access const-decl "real" matrices nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (list_induction formula-decl nil list_adt 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) (real nonempty-type-from-decl nil reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (rows const-decl "nat" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil)) shostak)) (col_zero 0 (col_zero-1 nil 3613380700 ("" (skeep) (("" (rewrite "list_extensionality[real]") (("" (splash) (("1" (skeep) (("1" (typepred "n") (("1" (lemma "col_def") (("1" (inst - "M" "i") (("1" (flatten) (("1" (assert) (("1" (inst - "n") (("1" (replaces -2) (("1" (assert) (("1" (typepred "columns(M)") (("1" (inst - "n") (("1" (assert) (("1" (expand "zero" 1) (("1" (typepred "array2list[real](rows(M))(LAMBDA (p: nat): 0)") (("1" (inst - "n") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "col(M)(i)") (("2" (expand "rows") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "col(M)(i)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((list_extensionality formula-decl nil more_list_props "structures/") (list type-decl nil list_adt 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (rows const-decl "nat" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (zero const-decl "VectorN(n)" matrices 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) (col_def formula-decl nil matrices nil) (M skolem-const-decl "Matrix" matrices nil) (i skolem-const-decl "nat" matrices nil) (n skolem-const-decl "below(length(col(M)(i)))" matrices nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (listn type-eq-decl nil listn "structures/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil)) shostak)) (access_zero 0 (access_zero-1 nil 3615738110 ("" (skeep) (("" (expand "access") (("" (lift-if) (("" (ground) (("" (expand "zero" 1) (("" (typepred "array2list[real](n)(LAMBDA (p: nat): 0)") (("" (inst - "i") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((access const-decl "real" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (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) (listn type-eq-decl nil listn "structures/") (length def-decl "nat" list_props nil) (= const-decl "[T, T -> boolean]" equalities 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (zero const-decl "VectorN(n)" matrices nil)) shostak)) (entry_test 0 (entry_test-1 nil 3614700058 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (access_row 0 (access_row-1 nil 3615133327 ("" (skeep) (("" (expand "entry") (("" (propax) nil nil)) nil)) nil) ((entry const-decl "real" matrices nil)) shostak)) (access_col 0 (access_col-1 nil 3615801371 ("" (skeep) (("" (lemma "col_def") (("" (inst?) (("" (flatten) (("" (assert) (("" (expand "access" 1) (("" (lift-if) (("" (ground) (("1" (inst - "i") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (replaces -2) (("1" (expand "entry") (("1" (expand "access") (("1" (expand "row") (("1" (assert) (("1" (copy -3) (("1" (expand "rows" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (expand "entry" 2) (("2" (expand "row" 2) (("2" (copy -2) (("2" (expand "rows" -1) (("2" (assert) (("2" (expand "access" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "entry" 2) (("2" (copy -1) (("2" (expand "rows" -1) (("2" (expand "row" 2) (("2" (assert) (("2" (expand "access" 2) (("2" (expand "length" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((col_def formula-decl nil matrices nil) (access const-decl "real" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (length_null formula-decl nil more_list_props "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (rows const-decl "nat" matrices nil) (< const-decl "bool" reals 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) (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)) shostak)) (coltest 0 (coltest-1 nil 3613147897 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (full_matrix_columns_TCC1 0 (full_matrix_columns_TCC1-1 nil 3613226737 ("" (grind) 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) (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)) nil)) (full_matrix_columns 0 (full_matrix_columns-1 nil 3613226737 ("" (skeep) (("" (case "null?(SM)") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (typepred "columns(SM)") (("2" (assert) (("2" (skosimp*) (("2" (typepred "SM") (("2" (assert) (("2" (inst - "0" "i!1") (("2" (expand "nth" -2 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (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) (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (<= const-decl "bool" reals nil)) shostak)) (rows_mn 0 (rows_mn-1 nil 3614001127 ("" (skeep) (("" (expand "rows") (("" (assert) nil nil)) nil)) nil) ((rows const-decl "nat" matrices nil)) shostak)) (columns_mn 0 (columns_mn-1 nil 3614001169 ("" (skeep) (("" (typepred "M") (("" (typepred "columns(M)") (("" (assert) (("" (split) (("1" (flatten) (("1" (hide-all-but (-1 -5)) (("1" (grind) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((MatrixMN type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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)) (length_row 0 (length_row-1 nil 3614003138 ("" (skeep) (("" (typepred "SM") (("" (assert) (("" (split -) (("1" (hide-all-but (-1 -3)) (("1" (grind) nil nil)) nil) ("2" (expand "row") (("2" (typepred "columns(SM)") (("2" (assert) (("2" (split -) (("1" (hide-all-but (-1 -5)) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "i" "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (row const-decl "Vector" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (length_col 0 (length_col-1 nil 3614003247 ("" (skeep) (("" (lemma "col_def") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((col_def formula-decl nil matrices nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (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)) shostak)) (columns_0_entry 0 (columns_0_entry-1 nil 3614083194 ("" (skeep) (("" (expand "entry") (("" (expand "row") (("" (expand "access") (("" (lift-if) (("" (typepred "columns(M)") (("" (ground) (("1" (inst - "i") (("1" (assert) nil nil)) nil) ("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((entry const-decl "real" matrices nil) (access const-decl "real" 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 "[T, T -> boolean]" equalities nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (length def-decl "nat" list_props 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) (< 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (length_null formula-decl nil more_list_props "structures/") (row const-decl "Vector" matrices nil)) shostak)) (rows_0_entry 0 (rows_0_entry-1 nil 3614083501 ("" (grind) 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) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil) (row const-decl "Vector" matrices nil) (length def-decl "nat" list_props nil) (access const-decl "real" matrices nil) (entry const-decl "real" matrices nil)) shostak)) (entry_eq_0 0 (entry_eq_0-1 nil 3614090600 ("" (skeep) (("" (expand "entry") (("" (expand "rows") (("" (expand "row") (("" (expand "access") (("" (lift-if) (("" (assert) (("" (ground) (("" (typepred "columns(M)") (("" (inst - "i") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((entry const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (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) (length def-decl "nat" list_props nil) (Matrix type-eq-decl nil matrices nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (= const-decl "[T, T -> boolean]" equalities 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) (length_null formula-decl nil more_list_props "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (access const-decl "real" matrices nil) (rows const-decl "nat" matrices nil)) shostak)) (add_TCC1 0 (add_TCC1-1 nil 3613147199 ("" (skeep) (("" (expand "length" + 2) (("" (assert) (("" (expand "max") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((length def-decl "nat" list_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) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)) nil)) (add_TCC2 0 (add_TCC2-1 nil 3613147199 ("" (skeep) (("" (expand "length" + 3) (("" (assert) (("" (expand "max") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((length def-decl "nat" list_props nil) (max const-decl "{p: real | p >= m AND p >= n}" 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)) nil)) (add_TCC3 0 (add_TCC3-1 nil 3613147199 ("" (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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil)) nil)) (add_TCC4 0 (add_TCC4-1 nil 3613147199 ("" (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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil)) nil)) (add_TCC5 0 (add_TCC5-1 nil 3613147199 ("" (termination-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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil) (length def-decl "nat" list_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (add_TCC6 0 (add_TCC6-1 nil 3613147199 ("" (skeep) (("" (expand "length" + 1) (("" (typepred "v(cdr[real](v1), cdr[real](v2))") (("" (assert) (("" (replaces -2) (("" (expand "length" + 3) (("" (expand "length" + 4) (("" (expand "max" +) (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((length def-decl "nat" list_props nil) (posint_plus_nnint_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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (VectorN type-eq-decl nil matrices nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)) nil)) (scal_TCC1 0 (scal_TCC1-1 nil 3613147199 ("" (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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil)) nil)) (scal_TCC2 0 (scal_TCC2-1 nil 3613147199 ("" (termination-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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil) (length def-decl "nat" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (scal_TCC3 0 (scal_TCC3-1 nil 3613147199 ("" (skeep) (("" (typepred "v(r, cdr[real](v2))") (("" (expand "length" + 1) (("" (expand "length" + 2) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (VectorN type-eq-decl nil matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (Vector type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (sub_TCC1 0 (sub_TCC1-1 nil 3613147199 ("" (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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (super_dot_TCC1 0 (super_dot_TCC1-1 nil 3621252270 ("" (grind) 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil) (dot def-decl "real" matrices nil)) nil)) (super_dot_TCC2 0 (super_dot_TCC2-1 nil 3621252270 ("" (grind) 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil) (dot def-decl "real" matrices nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (super_dot_TCC3 0 (super_dot_TCC3-1 nil 3621252270 ("" (grind) 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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil) (dot def-decl "real" matrices nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (super_duper_dot_TCC1 0 (super_duper_dot_TCC1-1 nil 3621961564 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (super_duper_dot_TCC2 0 (super_duper_dot_TCC2-1 nil 3621961564 ("" (termination-tcc) nil nil) nil nil)) (access_sum 0 (access_sum-1 nil 3614958801 ("" (induct "v1") (("1" (grind) nil nil) ("2" (skolem 1 ("r" "v")) (("2" (flatten) (("2" (skeep) (("2" (expand "+") (("2" (expand "access" +) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (expand "add" +) (("1" (lift-if) (("1" (ground) (("1" (grind) nil nil) ("2" (expand "nth" + 1) (("2" (lift-if) (("2" (ground) (("1" (replaces -1) (("1" (expand "nth" +) (("1" (propax) nil nil)) nil)) nil) ("2" (inst - "i-1" "cdr(v2)") (("2" (assert) (("2" (expand "nth" + 2) (("2" (assert) (("2" (expand "access") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil) ("7" (grind) nil nil) ("8" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "add" +) (("2" (lift-if) (("2" (ground) (("2" (expand "nth" + 1) (("2" (lift-if) (("2" (ground) (("1" (replaces -1) (("1" (expand "nth" + 1) (("1" (expand "length" 3) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "i-1" "cdr(v2)") (("2" (expand "access" -) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil) ("7" (grind) nil nil) ("8" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "add" +) (("3" (lift-if) (("3" (ground) (("1" (grind) nil nil) ("2" (expand "nth" + 1) (("2" (lift-if) (("2" (ground) (("1" (grind) nil nil) ("2" (inst - "i-1" "cdr(v2)") (("2" (expand "access") (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (typepred "add(cons(r,v),v2)") (("4" (expand "max") (("4" (lift-if) (("4" (ground) nil nil)) nil)) nil)) nil) ("5" (typepred "add(cons(r,v),v2)") (("5" (expand "max") (("5" (lift-if) (("5" (ground) nil nil)) nil)) nil)) nil) ("6" (typepred "add(cons(r,v),v2)") (("6" (expand "max") (("6" (ground) nil nil)) nil)) nil) ("7" (typepred "add(cons(r,v),v2)") (("7" (expand "max") (("7" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nth def-decl "T" list_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (add def-decl "VectorN(max(length(v1), length(v2)))" matrices nil) (list_induction formula-decl nil list_adt 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "VectorN(max(length(v1), length(v2)))" matrices nil) (VectorN type-eq-decl nil matrices nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (length def-decl "nat" list_props nil) (access const-decl "real" matrices nil) (= const-decl "[T, T -> boolean]" equalities 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) (Vector type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (access_scal 0 (access_scal-1 nil 3614962946 ("" (induct "v") (("1" (grind) nil nil) ("2" (skolem 1 ("r" "v")) (("2" (flatten) (("2" (skosimp*) (("2" (expand "*") (("2" (expand "scal" +) (("2" (expand "access" +) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (expand "nth" + 1) (("1" (lift-if) (("1" (ground) (("1" (replaces -1) (("1" (expand "nth" +) (("1" (propax) nil nil)) nil)) nil) ("2" (inst - "i!1-1" "r!1") (("2" (expand "access") (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (replaces -2) (("1" (expand "nth" + 2) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "scal" 1) (("2" (lift-if) (("2" (ground) (("1" (expand "length" -2) (("1" (assert) nil nil)) nil) ("2" (expand "length" 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" -1) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nth def-decl "T" list_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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_times_real_is_real application-judgement "real" reals nil) (scal def-decl "VectorN(length(v2))" matrices nil) (list_induction formula-decl nil list_adt 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "VectorN(length(v2))" matrices nil) (VectorN type-eq-decl nil matrices nil) (length def-decl "nat" list_props nil) (access const-decl "real" matrices nil) (= const-decl "[T, T -> boolean]" equalities 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) (Vector type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (vect_scal_1 0 (vect_scal_1-1 nil 3615126795 ("" (skeep) (("" (lemma "list_extensionality[real]") (("" (inst?) (("" (assert) (("" (hide 2) (("" (skosimp*) (("" (lemma "access_scal") (("" (inst - "n!1" "1" "v") (("" (expand "access") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (list_extensionality formula-decl nil more_list_props "structures/") (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (real_times_real_is_real application-judgement "real" reals nil) (access const-decl "real" matrices nil) (access_scal formula-decl nil matrices nil) (* const-decl "VectorN(length(v2))" matrices nil) (VectorN type-eq-decl nil matrices nil) (length def-decl "nat" list_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (dot_eq_sigma_TCC1 0 (dot_eq_sigma_TCC1-1 nil 3613318240 ("" (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) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (Vector type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (dot_eq_sigma 0 (dot_eq_sigma-2 nil 3613746369 ("" (induct "v1") (("1" (expand "length" 1 1) (("1" (expand "min") (("1" (assert) (("1" (skeep) (("1" (lift-if) (("1" (ground) (("1" (expand "dot") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("r" "l")) (("2" (flatten) (("2" (skeep) (("2" (expand "dot" +) (("2" (lift-if) (("2" (ground) (("1" (case "NOT v2 = null") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (expand "length" + 2) (("2" (expand "min" +) (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" + 1) (("2" (assert) (("2" (inst - "cdr(v2)") (("2" (expand "length" + 1) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (case "NOT l = null") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (assert) (("2" (expand "dot" 1 1) (("2" (expand "length" 1 1) (("2" (assert) (("2" (expand "min" 1) (("2" (expand "sigma") (("2" (expand "sigma") (("2" (expand "access" + 1) (("2" (expand "length" 1) (("2" (expand "nth" 1 1) (("2" (expand "access") (("2" (lift-if) (("2" (ground) (("1" (expand "nth") (("1" (propax) nil nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" -1 1) (("2" (expand "length" + 2) (("2" (case "NOT min(1 + length[real](cdr(l)), length[real](cdr(v2))) = min(length[real](cdr(l)), l (("1" (hide-all-but 1) (("1" (expand "min") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (invoke (name "S" "%1") (! -2 2 2)) (("2" (replace -1) (("2" (rewrite "sigma_first" +) (("2" (lemma "sigma_shift") (("2" (inst - "LAMBDA (k: nat): access(cons(r, l))(k) * access(v2)(k)" "S" "0" "1") (("2" (assert) (("2" (replaces -1) (("2" (assert) (("2" (expand "access" + 3) (("2" (lift-if) (("2" (ground) (("1" (expand "nth" +) (("1" (expand "access" + 3) (("1" (lift-if) (("1" (ground) (("1" (expand "nth" +) (("1" (assert) (("1" (replaces -5) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skolem 1 "nn") (("1" (expand "access") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "nth" + 3) (("1" (expand "nth" + 4) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil) ("3" (expand "length" 2) (("3" (assert) nil nil)) nil) ("4" (expand "length" 3) (("4" (assert) nil nil)) nil) ("5" (expand "length" -1) (("5" (assert) (("5" (expand "length" 2) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (inst + "min(length[real](v1), length[real](v2)) + 5") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ((cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (nth def-decl "T" list_props nil) (length_null formula-decl nil more_list_props "structures/") (sigma_shift formula-decl nil sigma_nat "reals/") (sigma_eq formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_first formula-decl nil sigma "reals/") (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (list_induction formula-decl nil list_adt 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) (access const-decl "real" matrices nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (dot def-decl "real" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (list type-decl nil list_adt 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) (Vector type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_times_real_is_real application-judgement "real" reals nil)) nil) (dot_eq_sigma-1 nil 3613318241 ("" (induct "v1") (("1" (skeep) (("1" (expand "*" + 1) (("1" (expand "dot") (("1" (expand "length" + 1) (("1" (expand "min") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "access" + 1) (("1" (expand "length" + 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("r" "l")) (("2" (flatten) (("2" (skeep) (("2" (expand "*" + 1) (("2" (expand "dot") (("2" (lift-if) (("2" (ground) (("1" (case "NOT v2 = null") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (expand "length" + 2) (("2" (expand "min" +) (("2" (assert) (("2" (expand "length" + 1) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (expand "sigma" +) (("2" (expand "sigma" +) (("2" (expand "access" + 2) (("2" (expand "length" + 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "cdr(v2)") (("2" (expand "length" + 1) (("2" (expand "length" + 2) (("2" (case "NOT min(1 + length[real](l), 1 + length[real](cdr(v2))) = 1+min(length[real](l), le (("1" (expand "min" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (rewrite "sigma_first" +) (("2" (lemma "sigma_shift") (("2" (inst - "LAMBDA (k: nat): access(cons(r, l))(k) * access(v2)(k)" " min(length[real](l), length[real](cdr(v2)))" "0" "1") (("2" (replaces -1) (("2" (assert) (("2" (expand "access" + 3) (("2" (lift-if) (("2" (ground) (("1" (expand "nth" +) (("1" (expand "access" + 3) (("1" (lift-if) (("1" (ground) (("1" (expand "nth" +) (("1" (assert) (("1" (expand "*" -3 1) (("1" (assert) (("1" (replaces -3) (("1" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skolem 1 "nn") (("1" (expand "access") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "nth" + 3) (("1" (expand "nth" + 4) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil) ("3" (expand "length" 2) (("3" (assert) nil nil)) nil) ("4" (expand "length" 3) (("4" (assert) nil nil)) nil) ("5" (expand "length" -1) (("5" (assert) nil nil)) nil) ("6" (expand "length" -2) (("6" (assert) nil nil)) nil) ("7" (expand "length" -1) (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "length" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (inst + "min(length[real](v1), length[real](v2)) + 5") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ((sigma_first formula-decl nil sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (sigma_shift formula-decl nil sigma_nat "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/")) shostak)) (dot_zero_right 0 (dot_zero_right-1 nil 3613381095 ("" (skeep) (("" (expand "*") (("" (rewrite "dot_eq_sigma") (("" (rewrite "sigma_restrict_eq_0") (("" (hide 2) (("" (skosimp*) (("" (expand "access" + 2) (("" (ground) (("" (expand "zero") (("" (typepred "array2list[real](n)(LAMBDA (p: nat): 0)") (("" (inst - "i!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "real" matrices nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (access const-decl "real" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil sigma "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (listn type-eq-decl nil listn "structures/") (< 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) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (subrange type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (zero const-decl "VectorN(n)" matrices nil) (VectorN type-eq-decl nil matrices nil) (length def-decl "nat" list_props nil) (= const-decl "[T, T -> boolean]" equalities 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) (Vector type-eq-decl nil matrices nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (dot_eq_sigma formula-decl nil matrices nil)) shostak)) (dot_commutes 0 (dot_commutes-1 nil 3613381325 ("" (induct "v1") (("1" (grind) nil nil) ("2" (skolem 1 ("r" "l")) (("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (expand "*") (("2" (expand "dot" +) (("2" (lift-if) (("2" (ground) (("2" (inst - "cdr(v2)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (dot def-decl "real" matrices nil) (list_induction formula-decl nil list_adt 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) (* const-decl "real" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (list type-decl nil list_adt nil)) shostak)) (dot_zero_left 0 (dot_zero_left-1 nil 3613381393 ("" (skeep) (("" (rewrite "dot_commutes") (("" (rewrite "dot_zero_right") nil nil)) nil)) nil) ((dot_commutes formula-decl nil matrices 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) (Vector type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (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) (dot_zero_right formula-decl nil matrices nil)) shostak)) (length_add_vect 0 (length_add_vect-1 nil 3615541943 ("" (skeep) (("" (assert) nil nil)) 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)) shostak)) (length_add_vect_same 0 (length_add_vect_same-1 nil 3615541963 ("" (skeep) (("" (rewrite "length_add_vect") (("" (grind :exclude "length") nil nil)) nil)) nil) ((length_add_vect formula-decl nil matrices 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) (Vector type-eq-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) (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)) shostak)) (length_scal_vect 0 (length_scal_vect-1 nil 3615541978 ("" (skeep) (("" (assert) nil nil)) nil) nil shostak)) (form_matrix_TCC1 0 (form_matrix_TCC1-1 nil 3613150030 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (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) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props 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) (MatrixMN type-eq-decl nil matrices 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) (row const-decl "Vector" matrices nil)) nil)) (form_matrix_TCC2 0 (form_matrix_TCC2-1 nil 3613150030 ("" (case "FORALL (n: nat): EXISTS (x: listn[real](n)): TRUE") (("1" (skeep) (("1" (inst - "n") nil nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (inst + "null") nil nil) ("2" (skeep) (("2" (skeep) (("2" (inst + "cons(0,x)") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (x skolem-const-decl "listn[real](j)" matrices nil) (j skolem-const-decl "nat" matrices nil) (length_null formula-decl nil more_list_props "structures/") (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt 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) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (TRUE const-decl "bool" booleans nil)) nil)) (form_matrix_TCC3 0 (form_matrix_TCC3-1 nil 3613217047 ("" (skeep) (("" (invoke (case "NOT (%1)") (! 1 1 1)) (("1" (hide 2) (("1" (lemma "length_matrix_equiv") (("1" (inst - "n" "array2list[listn[real](n)] (m) (LAMBDA (k: nat): array2list[real](n)(LAMBDA (p: nat): F(k, p)))") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (invoke (case "NOT (%1)") (! 1 1)) (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "length_matrix_nth") (("1" (inst - "n" "array2list[listn[real](n)] (m) (LAMBDA (k: nat): array2list[real](n)(LAMBDA (p: nat): F(k, p)))" "i!1") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (expand "row") (("2" (skeep) (("2" (typepred "array2list[listn[real](n)] (m) (LAMBDA (k: nat): array2list[real](n)(LAMBDA (p: nat): F(k, p)))") (("2" (inst - "i") (("2" (assert) (("2" (lemma "matrix_listn_nth") (("2" (inst - "n" "array2list[listn[real](n)] (m) (LAMBDA (k: nat): array2list[real](n)(LAMBDA (p: nat): F(k, p)))" "i" "j") (("2" (assert) (("2" (replace -4 :dir rl) (("2" (replace -1 :dir rl) (("2" (typepred "array2list[real](n)(LAMBDA (p: nat): F(i, p))") (("2" (inst - "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (= const-decl "[T, T -> boolean]" equalities 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) (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) (listn type-eq-decl nil listn "structures/") (< 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) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (length_matrix_equiv formula-decl nil matrices nil) (length_matrix_nth formula-decl nil matrices nil) (matrix_listn_nth formula-decl nil matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (row const-decl "Vector" matrices nil)) nil)) (columns_form_matrix 0 (columns_form_matrix-1 nil 3613747835 ("" (skeep) (("" (invoke (name "KV" "%1") (! 2 1 1)) (("" (replaces -1) (("" (typepred "KV") (("" (typepred "columns(KV)") (("" (split -) (("1" (flatten) (("1" (case "NOT m = 0") (("1" (hide-all-but (-1 -5 1)) (("1" (grind) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (length def-decl "nat" list_props 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) (MatrixMN type-eq-decl nil matrices nil) (Vector type-eq-decl nil matrices nil) (row const-decl "Vector" 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) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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)) (rows_form_matrix 0 (rows_form_matrix-1 nil 3613750191 ("" (skeep) (("" (expand "rows") (("" (assert) nil nil)) nil)) nil) ((rows const-decl "nat" matrices nil)) shostak)) (form_matrix_empty 0 (form_matrix_empty-1 nil 3615045475 ("" (skosimp*) (("" (replace -1) (("" (expand "form_matrix") (("" (grind) nil nil)) nil)) nil)) nil) ((array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers 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)) shostak)) (form_matrix_test1 0 (form_matrix_test1-1 nil 3613150439 ("" (eval-formula) nil nil) ((TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (full_matrix_eq 0 (full_matrix_eq-1 nil 3613230474 ("" (skeep) (("" (split) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (case "null?(SM1) OR null?(SM2)") (("1" (hide (-3 -4)) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (copy 3) (("2" (label "ans" 4) (("2" (hide "ans") (("2" (rewrite "list_extensionality[list[real]]" 1) (("2" (reveal "ans") (("2" (copy -1) (("2" (expand "rows" -1) (("2" (assert) (("2" (skolem 2 "i") (("2" (rewrite "list_extensionality[real]" 2) (("2" (lemma "full_matrix_columns") (("2" (inst-cp - "SM1") (("2" (inst - "SM2") (("2" (assert) (("2" (typepred "SM1") (("2" (assert) (("2" (hide -1) (("2" (inst - "i" "0") (("2" (typepred "SM2") (("2" (assert) (("2" (hide -1) (("2" (inst - "i" "0") (("2" (expand "nth" -1 2) (("2" (expand "nth" -2 2) (("2" (assert) (("2" (skolem + "j") (("2" (inst - "i" "j") (("1" (expand "entry") (("1" (expand "access") (("1" (expand "row") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "i") (("2" (expand "rows" 1) (("2" (propax) 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)) nil)) nil)) nil)) nil)) nil)) nil) ((FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (Matrix type-eq-decl nil matrices nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (rows const-decl "nat" matrices nil) (full_matrix_columns formula-decl nil matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (SM1 skolem-const-decl "FullMatrix" matrices nil) (i skolem-const-decl "below(length(SM1))" 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) (access const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (entry const-decl "real" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (list_extensionality formula-decl nil more_list_props "structures/")) shostak)) (matrix2array 0 (matrix2array-1 nil 3613232644 ("" (skeep) (("" (case "null?(SM)") (("1" (grind) nil nil) ("2" (rewrite "full_matrix_eq") (("1" (name "FM" "form_matrix(entry(SM), rows(SM), columns(SM))") (("1" (assert) (("1" (replace -1) (("1" (case "NOT (rows(SM) = rows(FM) AND columns(SM) = columns(FM))") (("1" (hide 3) (("1" (split) (("1" (typepred "FM") (("1" (expand "rows") (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "FM") (("2" (typepred "columns(FM)") (("2" (assert) (("2" (case "null?(FM)") (("1" (hide-all-but (-1 -5 2)) (("1" (grind) nil nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (inst -5 "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (typepred "FM") (("2" (skeep) (("2" (inst - "i" "j") (("2" (assert) (("2" (expand "entry") (("2" (expand "row") (("2" (expand "access") (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (copy -5) (("2" (expand "rows" -1) (("2" (assert) (("2" (grind) 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" (assert) (("2" (skosimp*) (("2" (name "FM" "form_matrix(entry(SM), rows(SM), columns(SM))") (("2" (replaces -1) (("2" (typepred "FM") (("2" (inst-cp - "i!1") (("2" (inst - "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (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) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (entry const-decl "real" matrices nil) (access const-decl "real" matrices nil) (row const-decl "Vector" 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) (rows const-decl "nat" 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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (length_null formula-decl nil more_list_props "structures/") (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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (Vector type-eq-decl nil matrices nil) (MatrixMN type-eq-decl nil matrices nil) (full_matrix_eq formula-decl nil matrices nil)) shostak)) (entry_form_matrix 0 (entry_form_matrix-2 nil 3613825301 ("" (skeep) (("" (name "FM" "form_matrix(F,m,n)") (("" (replaces -1) (("" (typepred "FM") (("" (expand "entry") (("" (expand "row") (("" (assert) (("" (expand "access") (("" (assert) (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (ground) (("1" (inst - "i") (("1" (inst - "i" "j") nil nil)) nil) ("2" (inst - "i") (("2" (assert) nil nil)) nil) ("3" (inst - "i") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (MatrixMN type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (access const-decl "real" matrices nil) (length_null formula-decl nil more_list_props "structures/") (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) (entry const-decl "real" matrices nil)) nil) (entry_form_matrix-1 nil 3613290911 ("" (skeep) (("" (name "FM" "form_matrix(F,m,n)") (("" (replaces -1) (("" (typepred "FM") (("" (expand "entry") (("" (expand "row") (("" (assert) (("" (expand "access") (("" (assert) (("" (inst -3 "i") (("" (assert) (("" (inst - "i" "j") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (entry_form_matrix2 0 (entry_form_matrix2-1 nil 3613826303 ("" (skeep) (("" (name "FM" "form_matrix(F,m,n)") (("" (replaces -1) (("" (typepred "FM") (("" (expand "entry") (("" (expand "row") (("" (assert) (("" (expand "access") (("" (assert) (("" (lift-if) (("" (ground) (("1" (inst - "i") (("1" (inst - "i" "j") nil nil)) nil) ("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (MatrixMN type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (access const-decl "real" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (entry const-decl "real" matrices nil)) nil)) (form_matrix_eq 0 (form_matrix_eq-1 nil 3613924751 ("" (skeep) (("" (ground) (("1" (skeep) (("1" (lemma "entry_form_matrix2") (("1" (inst - "F" "i" "j" "m" "n") (("1" (assert) (("1" (lemma "entry_form_matrix2") (("1" (inst - "G" "i" "j" "m" "n") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "f" "form_matrix(F, m, n)") (("2" (replaces -1) (("2" (name "g" "form_matrix(G, m, n)") (("2" (replaces -1) (("2" (rewrite "full_matrix_eq") (("1" (case "NOT rows(f) = rows(g)") (("1" (assert) (("1" (hide 2) (("1" (expand "rows") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (copy -1) (("2" (expand "rows" -1) (("2" (assert) (("2" (case "NOT columns(f)=columns(g)") (("1" (hide 2) (("1" (expand "f" 1) (("1" (expand "g" 1) (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (typepred "form_matrix(F,0,n)") (("1" (case "NOT form_matrix(F,0,n)=null") (("1" (expand "length" -2) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (typepred "form_matrix(G,0,n)") (("2" (case "NOT form_matrix(G,0,n)=null") (("1" (expand "length" -2) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "columns_form_matrix") (("2" (inst - "m" "n" "G") (("2" (assert) (("2" (replace -1) (("2" (typepred "form_matrix(F,0,n)") (("2" (case "NOT form_matrix(F,0,n)=null") (("1" (expand "length" -2) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (typepred "form_matrix(G,0,n)") (("2" (case "NOT form_matrix(G,0,n)=null") (("1" (expand "length" -2) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (copy -3) (("2" (expand "rows" -1) (("2" (skeep) (("2" (expand "f" 1) (("2" (expand "g" 1) (("2" (rewrite "entry_form_matrix2" 1) (("1" (rewrite "entry_form_matrix2" 1) (("1" (inst - "i" "j") (("1" (assert) (("1" (typepred "i") (("1" (expand "rows" -1) (("1" (assert) (("1" (typepred "j") (("1" (expand "f" -1) (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i") (("2" (expand "rows" -1) (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "j") (("3" (expand "f" -1) (("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) (("3" (typepred "i") (("3" (expand "rows" -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i") (("2" (expand "rows" -1) (("2" (assert) nil nil)) nil)) nil) ("3" (typepred "j") (("3" (expand "f" -1) (("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) (("3" (typepred "i") (("3" (expand "rows" -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "g") (("2" (skeep) (("2" (inst-cp - "i") (("2" (inst - "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (typepred "f") (("3" (skeep) (("3" (inst-cp - "i") (("3" (inst - "j") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((entry_form_matrix2 formula-decl nil matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans 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) (f skolem-const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (columns_form_matrix formula-decl nil matrices nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (FALSE const-decl "bool" booleans nil) (length_null formula-decl nil more_list_props "structures/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (null adt-constructor-decl "(null?)" list_adt nil) (g skolem-const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = G(i, j)}" matrices nil) (FullMatrix type-eq-decl nil matrices nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (full_matrix_eq formula-decl nil matrices nil) (list type-decl nil list_adt nil) (= const-decl "[T, T -> boolean]" equalities 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) (length def-decl "nat" list_props 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) (MatrixMN type-eq-decl nil matrices nil) (Vector type-eq-decl nil matrices nil) (row const-decl "Vector" 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)) shostak)) (matrix_reduce_prop 0 (matrix_reduce_prop-1 nil 3613998916 ("" (skeep) (("" (case "m = 0") (("1" (skeep) (("1" (case "NOT M = null") (("1" (typepred "M") (("1" (grind) nil nil)) nil) ("2" (inst - "LAMBDA (i,j): 0") (("2" (case "NOT form_matrix(LAMBDA (i,j):0,m,n)=null") (("1" (replaces -2) (("1" (typepred "form_matrix(LAMBDA (i, j): 0, 0, n)") (("1" (expand "length" -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (case "M = null") (("1" (typepred "M") (("1" (expand "length" -2) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "matrix2array") (("2" (inst - "M") (("1" (case "rows(M) = m and columns(M)=n") (("1" (inst?) (("1" (ground) nil nil)) nil) ("2" (split +) (("1" (expand "rows" 1) (("1" (assert) nil nil)) nil) ("2" (typepred "columns(M)") (("2" (assert) (("2" (skosimp*) (("2" (typepred "M") (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (typepred "M") (("2" (inst-cp - "i") (("2" (inst - "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (MatrixMN type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (array2list_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/") (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (row const-decl "Vector" matrices nil) (Vector type-eq-decl nil matrices nil) (FALSE const-decl "bool" booleans nil) (M skolem-const-decl "MatrixMN(m, n)" matrices nil) (n skolem-const-decl "nat" matrices nil) (m skolem-const-decl "nat" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (FullMatrix type-eq-decl nil matrices nil) (entry const-decl "real" 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) (matrix2array formula-decl nil matrices nil)) shostak)) (mult_TCC1 0 (mult_TCC1-1 nil 3613219504 ("" (skeep) (("" (skosimp*) (("" (rewrite "entry_form_matrix") (("" (expand "*") (("" (lift-if) (("" (ground) (("1" (rewrite "dot_eq_sigma") (("1" (rewrite "sigma_restrict_eq_0") (("1" (skosimp*) (("1" (expand "row" + 1) (("1" (copy 2) (("1" (expand "rows" 1) (("1" (assert) (("1" (expand "access" 2 1) (("1" (expand "length" 2 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "dot_eq_sigma") (("2" (rewrite "sigma_restrict_eq_0") (("2" (skosimp*) (("2" (rewrite "col_zero" 1) (("2" (rewrite "access_zero") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "real" matrices nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (T_high type-eq-decl nil sigma "reals/") (access const-decl "real" matrices nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (dot_eq_sigma formula-decl nil matrices nil) (col_zero formula-decl nil matrices nil) (access_zero formula-decl nil matrices nil) (subrange type-eq-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (length def-decl "nat" list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (row const-decl "Vector" matrices nil) (Matrix type-eq-decl nil matrices nil) (dot def-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (entry_form_matrix formula-decl nil matrices nil)) nil)) (mult_full 0 (mult_full-1 nil 3613231597 ("" (skeep) (("" (skeep) (("" (typepred "M*N") (("" (inst-cp - "i") (("" (inst - "j") (("" (assert) nil nil)) nil)) nil)) nil)) 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) (= const-decl "[T, T -> boolean]" equalities nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil)) nil)) (mult_null_left 0 (mult_null_left-1 nil 3613291665 ("" (skeep) (("" (typepred "null[list[real]]*M") (("" (expand "rows" -2) (("" (hide-all-but (-2 +)) (("" (grind :exclude "*") nil nil)) nil)) nil)) nil)) nil) ((null adt-constructor-decl "(null?)" list_adt nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (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) (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) (mult_full application-judgement "FullMatrix" matrices nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (mult_null_right 0 (mult_null_right-1 nil 3613293057 ("" (skeep) (("" (name "NN" "M*null[list[real]]") (("" (replace -1) (("" (assert) (("" (splash) (("1" (typepred "NN") (("1" (skeep) (("1" (inst - "i") (("1" (hide-all-but (-3 1)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "NN") (("2" (expand "rows" -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((null adt-constructor-decl "(null?)" list_adt nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (VectorN type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (* const-decl "real" matrices nil) (Vector type-eq-decl nil matrices nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (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) (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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (mult_full application-judgement "FullMatrix" matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (columns_mult 0 (columns_mult-1 nil 3613300815 ("" (skeep) (("" (assert) (("" (typepred "columns(M*N)") (("" (typepred "M*N") (("" (assert) (("" (case "null?(M*N)") (("1" (assert) (("1" (case "NOT M = null") (("1" (hide-all-but (-1 -3 1)) (("1" (grind) nil nil)) nil) ("2" (replace -1) (("2" (rewrite "mult_null_left") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mult_full application-judgement "FullMatrix" matrices nil) (null adt-constructor-decl "(null?)" list_adt nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" 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) (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) (access const-decl "real" 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) (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) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (mult_null_left formula-decl nil matrices nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (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) (length def-decl "nat" list_props nil) (Matrix type-eq-decl nil matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (rows const-decl "nat" matrices 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil)) shostak)) (rows_mult 0 (rows_mult-1 nil 3613301627 ("" (skeep) (("" (expand "rows" + 1) (("" (assert) nil nil)) nil)) nil) ((rows const-decl "nat" matrices nil) (mult_full application-judgement "FullMatrix" matrices nil)) shostak)) (columns_append 0 (columns_append-1 nil 3613301930 ("" (skeep) (("" (typepred "columns(append(M,N))") (("" (split -) (("1" (flatten) (("1" (case "NOT (M = null and N = null)") (("1" (lemma "length_append[list[real]]") (("1" (inst - "M" "N") (("1" (hide-all-but (-1 -2 1)) (("1" (grind :exclude "append") nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (replaces -1) (("2" (assert) (("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "i!1") (("2" (rewrite "length_append" -1) (("2" (typepred "columns(M)") (("2" (assert) (("2" (case "null?(M)") (("1" (case "NOT M = null") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (rewrite "append_null_left") (("2" (expand "columns" + 2) (("2" (expand "max") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "null?(N)") (("1" (case "N = null") (("1" (replaces -1) (("1" (rewrite "append_null") (("1" (expand "columns" + 3) (("1" (expand "max") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (typepred "columns(N)") (("2" (assert) (("2" (skolem - ("jn")) (("2" (skolem - ("jm")) (("2" (case "columns(append(M, N)) <= max(columns(M), columns(N))") (("1" (case "columns(append(M, N)) >= max(columns(M), columns(N))") (("1" (assert) nil nil) ("2" (hide (-1 4)) (("2" (inst-cp -7 "jm") (("1" (inst-cp -7 "length(M)+jn") (("1" (rewrite "nth_append" -8) (("1" (rewrite "nth_append" -9) (("1" (assert) (("1" (expand "max" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_append") (("2" (assert) nil nil)) nil)) nil) ("2" (rewrite "length_append") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (case "i!1 < length(M)") (("1" (rewrite "nth_append") (("1" (assert) (("1" (inst -4 "i!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst -1 "i!1-length(M)") (("1" (rewrite "nth_append") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 "[T, T -> boolean]" equalities nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (Matrix type-eq-decl nil matrices nil) (append def-decl "list[T]" list_props nil) (length def-decl "nat" list_props 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) (< 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (append_null formula-decl nil list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (jn skolem-const-decl "below(length(N))" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (nth_append formula-decl nil more_list_props "structures/") (N skolem-const-decl "Matrix" matrices nil) (jm skolem-const-decl "below(length(M))" matrices nil) (M skolem-const-decl "Matrix" matrices nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (i!1 skolem-const-decl "below(length(append(M, N)))" matrices nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (append_null_left formula-decl nil more_list_props "structures/") (max const-decl "{p: real | p >= m AND p >= n}" 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) (length_append formula-decl nil list_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (null adt-constructor-decl "(null?)" list_adt nil)) shostak)) (append_mult 0 (append_mult-2 nil 3613315727 ("" (skeep) (("" (lemma "full_matrix_eq") (("" (inst?) (("1" (assert) (("1" (hide 3) (("1" (case "NOT (rows(append(M, N) * A) = rows(append(M * A, N * A)) AND columns(append(M, N) * A) = columns(append(M * A, N * A)))") (("1" (hide 2) (("1" (split) (("1" (rewrite "rows_mult") (("1" (expand "rows") (("1" (rewrite "length_append") (("1" (rewrite "length_append") (("1" (typepred "M*A") (("1" (typepred "N*A") (("1" (expand "rows") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "columns_mult") (("2" (inst?) (("2" (split -) (("1" (replaces -1) (("1" (assert) (("1" (rewrite "columns_append") (("1" (lemma "columns_mult") (("1" (inst-cp - "M" "A") (("1" (assert) (("1" (replaces -2) (("1" (inst - "N" "A") (("1" (ground) (("1" (grind) nil nil) ("2" (expand "max") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (typepred "i") (("2" (typepred "j") (("2" (lemma "columns_mult") (("2" (inst?) (("2" (ground) (("1" (replaces -1) (("1" (rewrite "rows_mult") (("1" (expand "rows" -2) (("1" (rewrite "length_append") (("1" (expand "*" 1 1) (("1" (expand "mult") (("1" (rewrite "entry_form_matrix") (("1" (expand "entry" 1) (("1" (expand "row") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (rewrite "length_append") (("1" (rewrite "length_append") (("1" (lemma "rows_mult") (("1" (inst-cp - "M" "A") (("1" (inst - "N" "A") (("1" (expand "rows") (("1" (replaces -1) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_append") (("2" (rewrite "length_append") (("2" (lemma "rows_mult") (("2" (inst-cp - "M" "A") (("2" (inst - "N" "A") (("2" (expand "rows") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "length_append") (("3" (rewrite "length_append") (("3" (lemma "rows_mult") (("3" (inst-cp - "M" "A") (("3" (inst - "N" "A") (("3" (expand "rows") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "access") (("4" (lift-if) (("4" (assert) (("4" (ground) (("1" (rewrite "nth_append" 1) (("1" (rewrite "nth_append" 1) (("1" (lemma "rows_mult") (("1" (expand "rows" -1) (("1" (rewrite -1) (("1" (hide -1) (("1" (lift-if) (("1" (ground) (("1" (typepred "M*A") (("1" (hide (-1 -2 -3)) (("1" (inst - "i" "j") (("1" (expand "entry" -1) (("1" (expand "row" -1) (("1" (expand "access") (("1" (lemma "rows_mult") (("1" (expand "rows" -1) (("1" (rewrite -1) (("1" (assert) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "N*A") (("2" (hide (-1 -2 -3)) (("2" (inst - "i-length(M)" "j") (("2" (expand "entry") (("2" (expand "row" -1) (("2" (expand "access") (("2" (lemma "rows_mult") (("2" (expand "rows" -1) (("2" (rewrite -1) (("2" (assert) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "rows_mult") (("2" (expand "rows" -1) (("2" (rewrite -1) (("2" (rewrite -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "nth_append" 1) (("1" (lemma "rows_mult") (("1" (expand "rows" -1) (("1" (rewrite -1) (("1" (hide -1) (("1" (lift-if) (("1" (ground) (("1" (typepred "M*A") (("1" (inst - "i") (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "N*A") (("2" (inst - "i-length(M)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "rows_mult") (("2" (expand "rows" -1) (("2" (rewrite -1) (("2" (rewrite -1) 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" (hide-all-but (-1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (rewrite "nth_append") (("1" (rewrite "nth_append") (("1" (lemma "rows_mult") (("1" (expand "rows" -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (assert) (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (typepred "M*A") (("1" (inst-cp - "i!1") (("1" (inst-cp - "j!1") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (typepred "M*A") (("2" (inst?) (("2" (typepred "N*A") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (typepred "M*A") (("3" (inst?) (("3" (typepred "N*A") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (typepred "N*A") (("4" (inst-cp - "i!1-length(M)") (("4" (inst-cp - "j!1-length(M)") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (rewrite "nth_append") (("1" (typepred "M*A") (("1" (inst?) (("1" (typepred "N*A") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "j!1") (("2" (rewrite "length_append") nil nil)) nil)) nil) ("2" (typepred "j!1") (("2" (rewrite "length_append") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (rewrite "length_append") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((full_matrix_eq formula-decl nil matrices nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (length_append formula-decl nil list_props nil) (rows_mult formula-decl nil matrices nil) (columns_append 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) (int_minus_int_is_int application-judgement "int" integers 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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (mult const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" 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) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (dot def-decl "real" matrices nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (columns_mult formula-decl nil matrices nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nth_append formula-decl nil more_list_props "structures/") (access const-decl "real" matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (entry_form_matrix formula-decl nil matrices nil) (FullMatrix type-eq-decl nil matrices 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) (append def-decl "list[T]" list_props 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) (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) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (M skolem-const-decl "Matrix" matrices nil) (A skolem-const-decl "Matrix" matrices nil) (N skolem-const-decl "Matrix" matrices nil) (mult_full application-judgement "FullMatrix" matrices nil)) nil) (append_mult-1 nil 3613292381 ("" (induct "N") (("1" (skeep) (("1" (rewrite "append_null") (("1" (rewrite "mult_null_left") (("1" (rewrite "append_null") nil nil)) nil)) nil)) nil) ("2" (skolem 1 ("v" "N")) (("2" (flatten) (("2" (induct "A") (("1" (skeep) (("1" (rewrite "cons_append") (("1" (rewrite "append_assoc" :dir rl) (("1" (assert) (("1" (rewrite "list_extensionality[list[real]]" 2) (("1" (splash +) (("1" (assert) (("1" (skeep) (("1" (lemma "mult_null_right") (("1" (inst - "append(append(M, (: v :)), N)") (("1" (assert) (("1" (flatten) (("1" (inst - "n") (("1" (replaces -2) (("1" (assert) (("1" (rewrite "nth_append" +) (("1" (lift-if) (("1" (ground) (("1" (lemma "mult_null_right") (("1" (inst - "M") (("1" (assert) (("1" (flatten) (("1" (inst - "n") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "k" "n - length(M * null)") (("2" (replace -1) (("2" (lemma "mult_null_right") (("2" (inst - "append((: v :), N)") (("2" (assert) (("2" (flatten) (("2" (inst - "k") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "append((: v :), N) * null") (("2" (hide (-1 -3 -4 -5)) (("2" (replaces -1) (("2" (expand "rows" 1) (("2" (typepred "n") (("2" (typepred "append(append(M, (: v :)), N) * null") (("2" (hide (-1 -3 -4 -5)) (("2" (replaces -1) (("2" (expand "rows" -1) (("2" (rewrite "length_append" -1) (("2" (rewrite "length_append" -1) (("2" (rewrite "length_append" 1) (("2" (assert) (("2" (typepred "M*null") (("2" (hide (-1 -3 -4 -5)) (("2" (assert) (("2" (replaces -1) (("2" (expand "rows" 1) (("2" (propax) 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" (assert) (("2" (rewrite "length_append") (("2" (typepred "append((: v :), N) * null") (("2" (hide (-1 -3 -4 -5)) (("2" (replaces -1) (("2" (typepred "append(append(M, (: v :)), N) * null") (("2" (hide (-1 -3 -4 -5)) (("2" (replaces -1) (("2" (expand "rows") (("2" (rewrite "length_append") (("2" (rewrite "length_append") (("2" (rewrite "length_append") (("2" (assert) (("2" (typepred "M*null") (("2" (expand "rows" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("l" "AA")) (("2" (flatten) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (matrix_mult_assoc 0 (matrix_mult_assoc-3 nil 3613826341 ("" (induct "M") (("1" (skeep) (("1" (rewrite "mult_null_left") (("1" (rewrite "mult_null_left") (("1" (rewrite "mult_null_left") nil nil)) nil)) nil)) nil) ("2" (skolem 1 ("v" "M")) (("2" (flatten) (("2" (skeep) (("2" (rewrite "cons_append") (("2" (lemma "append_mult") (("2" (inst - "N" "(: v :)" "M") (("2" (assert) (("2" (replaces -1) (("2" (lemma "append_mult") (("2" (inst - "A" "(: v :) * N" "M*N") (("2" (assert) (("2" (split -) (("1" (replaces -1) (("1" (lemma "append_mult") (("1" (inst - "N*A" "(: v :)" "M") (("1" (assert) (("1" (replaces -1) (("1" (assert) (("1" (inst-cp - "A" "N") (("1" (replaces -2) (("1" (assert) (("1" (case "FORALL (X,Y:Matrix): null?(X) OR LET K = (: v :) IN (K*X)*Y = K*(X*Y)") (("1" (inst - "N" "A") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (assert) (("2" (name "K" "(: v :)") (("2" (replace -1) (("2" (case "NOT length(K) = 1") (("1" (expand "K" 1) (("1" (grind) nil nil)) nil) ("2" (rewrite "full_matrix_eq" 2) (("2" (case "NOT (rows((K * X) * Y) = rows(K * (X * Y)) AND columns((K * X) * Y) = columns(K * (X * Y)))") (("1" (hide 3) (("1" (split) (("1" (assert) (("1" (rewrite "rows_mult") (("1" (rewrite "rows_mult") (("1" (rewrite "rows_mult") nil nil)) nil)) nil)) nil) ("2" (lemma "columns_mult") (("2" (inst?) (("2" (split -) (("1" (replaces -1) (("1" (lemma "columns_mult") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (lemma "columns_mult") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "K*X") (("2" (expand "rows") (("2" (assert) (("2" (replace -7) (("2" (hide-all-but (-2 -5)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (typepred "i") (("2" (typepred "j") (("2" (copy -2) (("2" (expand "rows" -1) (("2" (assert) (("2" (expand "*" +) (("2" (expand "mult" +) (("2" (rewrite "entry_form_matrix2") (("1" (rewrite "entry_form_matrix2") (("1" (case "NOT i = 0") (("1" (assert) (("1" (rewrite "rows_mult") (("1" (rewrite "rows_mult") (("1" (expand "rows") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (expand "row" + 1) (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (typepred "form_matrix(LAMBDA (i, j: nat): dot(row(K)(i),col(X)(j)), rows(K), columns(X))") (("1" (expand "rows") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "row" + 2) (("2" (case "NOT rows(K) = 1") (("1" (expand "rows" 1) (("1" (propax) nil nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (name "FKXM" "form_matrix(LAMBDA (i, j: nat): dot(row(K)(i),col(X)(j)), 1, columns(X))") (("2" (replace -1) (("2" (name "FXYM" "form_matrix(LAMBDA (i, j: nat): dot(row(X)(i) , col(Y)(j)), rows(X), columns(Y))") (("2" (replace -1) (("2" (typepred "FKXM") (("2" (case "nth(K,0) = v") (("1" (replace -1) (("1" (assert) (("1" (typepred "FKXM") (("1" (inst -4 "0" _) (("1" (expand "row" -4 1) (("1" (hide (-1 -6)) (("1" (rewrite "dot_eq_sigma" 2) (("1" (inst-cp - "0") (("1" (replaces -3) (("1" (assert) (("1" (typepred "col(Y)(j)") (("1" (hide -1) (("1" (replaces -1) (("1" (case "NOT (LAMBDA (k: nat): access(nth(FKXM, 0))(k) * access(col(Y)(j))(k))=(LAMBDA (k:nat):dot(row(K)(0) , col(X) (("1" (hide 3) (("1" (decompose-equality 1) (("1" (inst -3 "x!1") (("1" (assert) (("1" (expand "access" 1 1) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (inst-cp -6 "0") (("1" (replace -7) (("1" (assert) (("1" (lemma "col_zero") (("1" (inst - "X" "x!1") (("1" (assert) (("1" (replaces -1) (("1" (lemma "dot_zero_right") (("1" (expand "*" -1) (("1" (rewrite -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "col_zero") (("2" (inst - "X" "x!1") (("2" (assert) (("2" (replaces -1) (("2" (lemma "dot_zero_right") (("2" (expand "*" -1) (("2" (rewrite -1) (("2" (assert) (("2" (expand "access" + 1) (("2" (lift-if) (("2" (ground) (("2" (inst - "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (case "NOT row(K)(0) = v") (("1" (expand "row" 1) (("1" (propax) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (lemma "dot_eq_sigma") (("2" (case "NOT (LAMBDA (k: nat): dot(v , col(X)(k)) * access(col(Y)(j))(k)) = (LAMBDA (k: nat): sigma(0 LAMBDA (i: nat): (access(v)(i) * access(col(X)(k))(i))*access(col(Y)(j))(k)))") (("1" (decompose-equality 1) (("1" (inst - "v" "col(X)(x!1)") (("1" (replaces -1) (("1" (rewrite "sigma_scal_right" :dir rl) (("1" (typepred "col(X)(x!1)") (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst + "2") (("2" (hide-all-but (1 2)) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (rewrite "sigma_swap") (("2" (hide (-1 -2 -3 -4 -5 -6 -7 -8 -9 -10)) (("2" (typepred "FXYM") (("2" (hide -1) (("2" (rewrite "dot_eq_sigma" 2) (("2" (typepred "col(FXYM)(j)") (("2" (hide -1) (("2" (replace -1) (("2" (expand "rows" + 3) (("2" (replace -2) (("2" (rewrite "sigma_eq") (("1" (hide 3) (("1" (skosimp*) (("1" (typepred "n!1") (("1" (expand "access" + 5) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "col_def") (("1" (inst - "FXYM" "j") (("1" (flatten) (("1" (assert) (("1" (inst - "n!1") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (replaces -2) (("1" (inst -9 "n!1" "j") (("1" (expand "row" -9) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (typepred "col(FXYM)(j)") (("1" (replaces -2) (("1" (assert) (("1" (expand "rows") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "rows") (("2" (assert) (("2" (replaces -1) (("2" (rewrite "dot_eq_sigma" 2) (("2" (rewrite "sigma_scal" :dir rl) (("2" (typepred "col(Y)(j)") (("2" (hide -1) (("2" (replaces -1) (("2" (expand "rows" 2) (("2" (invoke (name "K1" "%1") (! 2 1 2)) (("2" (replace -1) (("2" (invoke (name "K2" "%1") (! 2 2 2)) (("2" (replace -1) (("2" (invoke (name "F1" "%1") (! 2 1 3)) (("2" (replace -1) (("2" (invoke (name "F2" "%1") (! 2 2 3)) (("2" (replace -1) (("2" (hide (-1 -2 -3 -4)) (("2" (case "NOT K1>=K2") (("1" (expand "K1" 1) (("1" (expand "K2" 1) (("1" (typepred "columns(X)") (("1" (inst - "n!1") (("1" (assert) (("1" (expand "min" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_split") (("2" (inst - "F1" "K1" "0" "K2") (("2" (assert) (("2" (replaces -1) (("2" (case "NOT -1<=K2") (("1" (expand "K2" 1) (("1" (expand "min") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -1) (("2" (replaces -1) (("2" (case "NOT sigma(1+K2,K1,F1)=0") (("1" (hide 3) (("1" (rewrite "sigma_restrict_eq_0") (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "K2") (("1" (expand "min" -1) (("1" (lift-if) (("1" (ground) (("1" (expand "F1" 2) (("1" (case "access(col(X)(i!1))(n!1)=0") (("1" (assert) nil nil) ("2" (expand "access" 1) (("2" (lift-if) (("2" (ground) (("2" (lemma "col_def") (("2" (inst - "X" "i!1") (("2" (flatten) (("2" (replaces -1) (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (rewrite "sigma_eq" 2) (("2" (skosimp*) (("2" (expand "F1" 1) (("2" (expand "F2" 1) (("2" (lemma "col_def") (("2" (inst - "X" "n!2") (("2" (flatten) (("2" (inst - "n!1") (("2" (assert) (("2" (expand "access" 1 1) (("2" (replaces -2) (("2" (assert) (("2" (expand "access" + 4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "n!1") (("2" (assert) (("2" (typepred "j") (("2" (lemma "columns_mult") --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.572 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26