|
(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 nth[listn[real](nn)](LL, i) = nth[list[real]](LL, i)")
(("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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.80 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
