|
(elementary_matrices
(zero_or_nonzero 0
(zero_or_nonzero-1 nil 3522729752 ("" (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)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(Matrix type-eq-decl nil matrices nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero_row? const-decl "bool" elementary_matrices nil)
(/= const-decl "boolean" notequal nil)
(nonzero_row? const-decl "bool" elementary_matrices nil))
shostak))
(zero_isnt_nonzero 0
(zero_isnt_nonzero-1 nil 3522729758 ("" (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)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(Matrix type-eq-decl nil matrices nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero_row? const-decl "bool" elementary_matrices nil)
(/= const-decl "boolean" notequal nil)
(nonzero_row? const-decl "bool" elementary_matrices nil))
shostak))
(nonzero_isnt_zero 0
(nonzero_isnt_zero-1 nil 3522729771 ("" (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)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(Matrix type-eq-decl nil matrices nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(nonzero_row? const-decl "bool" elementary_matrices nil)
(zero_row? const-decl "bool" elementary_matrices nil))
shostak))
(elemM1?_TCC1 0
(elemM1?_TCC1-1 nil 3492633163 ("" (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)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices 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)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(/= const-decl "boolean" notequal nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(elemM1?_TCC2 0
(elemM1?_TCC2-1 nil 3492633163 ("" (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)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices 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)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(/= const-decl "boolean" notequal nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(elemM2?_TCC1 0
(elemM2?_TCC1-1 nil 3492633163 ("" (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)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices 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)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(elemM2?_TCC2 0
(elemM2?_TCC2-1 nil 3492633163 ("" (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)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices 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)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(elemM3?_TCC1 0
(elemM3?_TCC1-1 nil 3492633163 ("" (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)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices 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)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(elemM3?_TCC2 0
(elemM3?_TCC2-1 nil 3492633163 ("" (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)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices 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)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(elemM3?_TCC3 0
(elemM3?_TCC3-1 nil 3492633163 ("" (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)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(real nonempty-type-from-decl nil reals nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices 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)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(elm1_judgement 0
(elm1_judgement-1 nil 3500317945 ("" (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)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices nil)
(squareMat? const-decl "bool" matrices nil)
(SquareMat type-eq-decl nil matrices nil)
(elemMat1? const-decl "bool" elementary_matrices nil)
(ElemMat1 type-eq-decl nil elementary_matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(elemM1? const-decl "bool" elementary_matrices nil)
(elemM1? const-decl "bool" elementary_matrices nil))
nil))
(elm2_judgement 0
(elm2_judgement-1 nil 3500318534 ("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices nil)
(squareMat? const-decl "bool" matrices nil)
(SquareMat type-eq-decl nil matrices nil)
(elemMat2? const-decl "bool" elementary_matrices nil)
(ElemMat2 type-eq-decl nil elementary_matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(elemM2? const-decl "bool" elementary_matrices nil)
(elemM2? const-decl "bool" elementary_matrices nil))
nil))
(elm3_judgement 0
(elm3_judgement-1 nil 3500318534 ("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices nil)
(squareMat? const-decl "bool" matrices nil)
(SquareMat type-eq-decl nil matrices nil)
(elemMat3? const-decl "bool" elementary_matrices nil)
(ElemMat3 type-eq-decl nil elementary_matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(elemM3? const-decl "bool" elementary_matrices nil)
(elemM3? const-decl "bool" elementary_matrices nil))
nil))
(elm_judgement 0
(elm_judgement-1 nil 3500318534 ("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(Matrix type-eq-decl nil matrices nil)
(square? const-decl "bool" matrices nil)
(Square type-eq-decl nil matrices nil)
(squareMat? const-decl "bool" matrices nil)
(SquareMat type-eq-decl nil matrices nil)
(elemMat? const-decl "bool" elementary_matrices nil)
(ElemMat type-eq-decl nil elementary_matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(elemMat1? const-decl "bool" elementary_matrices nil)
(elemMat2? const-decl "bool" elementary_matrices nil)
(elemMat3? const-decl "bool" elementary_matrices nil)
(elemM1? const-decl "bool" elementary_matrices nil)
(elemM1? const-decl "bool" elementary_matrices nil)
(/= const-decl "boolean" notequal nil)
(elemM2? const-decl "bool" elementary_matrices nil)
(elemM2? const-decl "bool" elementary_matrices nil)
(elemM3? const-decl "bool" elementary_matrices nil)
(elemM3? const-decl "bool" elementary_matrices nil)
(elemM? const-decl "bool" elementary_matrices nil))
nil))
(elemM1_TCC1 0
(elemM1_TCC1-1 nil 3492635698
("" (skolem-typepred)
(("" (prop)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind)
(("3" (inst 1 "i!1" "j!1")
(("3" (skolem-typepred)
(("3" (prop)
(("1" (lift-if) (("1" (assert) nil nil)) nil)
("2" (lift-if) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((square? const-decl "bool" matrices nil)
(squareMat? const-decl "bool" matrices nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(elemM1? const-decl "bool" elementary_matrices nil)
(elemMat1? const-decl "bool" elementary_matrices nil)
(/= const-decl "boolean" notequal nil)
(below type-eq-decl nil naturalnumbers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(> 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))
nil))
(elemM2_TCC1 0
(elemM2_TCC1-1 nil 3492635698
("" (skolem-typepred)
(("" (prop)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (expand "elemMat2?")
(("3" (inst 1 "i!1" "j!1") (("3" (grind) nil nil)) nil)) nil))
nil))
nil)
((square? const-decl "bool" matrices nil)
(squareMat? const-decl "bool" matrices nil)
(elemM2? const-decl "bool" elementary_matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(elemMat2? const-decl "bool" elementary_matrices nil)
(/= const-decl "boolean" notequal nil)
(below type-eq-decl nil naturalnumbers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(> 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))
nil))
(elemM3_TCC1 0
(elemM3_TCC1-1 nil 3492635698
("" (skolem-typepred)
(("" (prop)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (expand "elemMat3?")
(("3" (inst 1 "i!1") (("3" (grind) nil nil)) nil)) nil))
nil))
nil)
((square? const-decl "bool" matrices nil)
(squareMat? const-decl "bool" matrices nil)
(elemM3? const-decl "bool" elementary_matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(elemMat3? const-decl "bool" elementary_matrices nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(below type-eq-decl nil naturalnumbers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(> 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))
nil))
(elemM1_invertible 0
(elemM1_invertible-2 "" 3520306768
("" (skolem-typepred)
(("" (expand "invertible?")
(("" (expand "elemM1?")
(("" (skolem-typepred)
((""
(inst 1
"elemM1(M!1`rows)(i!1, j!1)(-(M!1`matrix(i!1, j!1)))")
(("1" (prop)
(("1" (grind) nil nil)
("2" (expand "inverse?")
(("2" (prop)
(("1" (expand "elemM1?")
(("1" (expand "elemM1")
(("1" (expand "*")
(("1" (apply-extensionality :hide? t)
(("1" (grind) nil nil)
("2" (apply-extensionality :hide? t)
(("1" (expand "I")
(("1"
(lift-if)
(("1"
(prop)
(("1"
(lemma
"sigma_middle[below(M!1`cols)]")
(("1"
(inst?
:subst
("low"
"0"
"high"
"M!1`cols-1"
"i"
"x!1"))
(("1"
(prop)
(("1"
(replace -1 :hide? t)
(("1"
(lemma
"sigma_eq[below(M!1`cols)]")
(("1"
(inst-cp
-1
"LAMBDA (k_1: below(M!1`cols)):
(M!1`matrix(x!1, k_1) *
IF (k_1 = x!2) THEN 1
ELSIF ((k_1 = i!1) AND (x!2 = j!1))
THEN -(M!1`matrix(i!1, j!1))
ELSE 0
ENDIF)"
"LAMBDA (k_1: below(M!1`cols)): 0"
"x!1-1"
"0")
(("1"
(prop)
(("1"
(replace -1 :hide? t)
(("1"
(use
"sigma_zero[below(M!1`cols)]")
(("1"
(replace
-1
:hide?
t)
(("1"
(inst
-1
"LAMBDA (k_1: below(M!1`cols)):
(M!1`matrix(x!1, k_1) *
IF (k_1 = x!2) THEN 1
ELSIF ((k_1 = i!1) AND (x!2 = j!1))
THEN -(M!1`matrix(i!1, j!1))
ELSE 0
ENDIF)"
"LAMBDA (k_1: below(M!1`cols)): 0"
"M!1`cols-1"
"x!1+1")
(("1"
(prop)
(("1"
(replace
-1
:hide?
t)
(("1"
(use
"sigma_zero[below(M!1`cols)]")
(("1"
(replace
-1
:hide?
t)
(("1"
(assert)
(("1"
(inst
-5
"x!1"
"x!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(assert)
(("2"
(inst
-5
"x!1"
"n!1")
(("1"
(assert)
(("1"
(prop)
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(lift-if)
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(lift-if)
(("3"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(lift-if)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -5 2)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(hide -1)
(("2"
(skolem-typepred)
(("2"
(inst
-7
"x!1"
"n!1")
(("2"
(assert)
(("2"
(assert)
(("2"
(prop)
(("1"
(lift-if)
(("1"
(assert)
nil
nil))
nil)
("2"
(lift-if)
(("2"
(assert)
nil
nil))
nil)
("3"
(lift-if)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -5 2)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide -5 2)
(("2" (grind) nil nil))
nil)
("3"
(hide -5 2)
(("3" (grind) nil nil))
nil))
nil)
("2"
(hide -5 2)
(("2" (grind) nil nil))
nil)
("3"
(hide -5 2)
(("3" (grind) nil nil))
nil)
("4"
(hide -6 2)
(("4" (grind) nil nil))
nil))
nil)
("2"
(hide -5 2)
(("2" (grind) nil nil))
nil))
nil)
("2"
(case-replace "x!1 = i!1")
(("1"
(inst -5 "i!1" _)
(("1"
(case "x!2 = j!1")
(("1"
(replace -1)
(("1"
(lemma
"sigma_middle[below(M!1`cols)]")
(("1"
(inst?
:subst
("low"
"0"
"high"
"M!1`cols-1"
"i"
"min(i!1,j!1)"))
(("1"
(prop)
(("1"
(replace -1 :hide? t)
(("1"
(lemma
"sigma_middle[below(M!1`cols)]")
(("1"
(inst?
:subst
("low"
"min(i!1,j!1)+1"
"high"
"M!1`cols-1"
"i"
"max(i!1, j!1)"))
(("1"
(prop)
(("1"
(replace
-1
:hide?
t)
(("1"
(lemma
"sigma_eq[below(M!1`cols)]")
(("1"
(inst-cp
-1
"LAMBDA (k_1: below(M!1`cols)):
(M!1`matrix(i!1, k_1) *
IF (k_1 = j!1) THEN 1
ELSIF (k_1 = i!1) THEN -(M!1`matrix(i!1, j!1))
ELSE 0
ENDIF)"
"LAMBDA (k_1: below(M!1`cols)): 0"
"min(i!1,j!1)-1"
"0")
(("1"
(prop)
(("1"
(replace
-1
:hide?
t)
(("1"
(use
"sigma_zero[below(M!1`cols)]")
(("1"
(replace
-1
:hide?
t)
(("1"
(assert)
(("1"
(inst-cp
-1
"LAMBDA (k_1: below(M!1`cols)):
(M!1`matrix(i!1, k_1) *
IF (k_1 = j!1) THEN 1
ELSIF (k_1 = i!1) THEN -(M!1`matrix(i!1, j!1))
ELSE 0
ENDIF)"
"LAMBDA (k_1: below(M!1`cols)): 0"
"max(i!1,j!1)-1"
"min(i!1,j!1)+1")
(("1"
(prop)
(("1"
(replace
-1
:hide?
t)
(("1"
(use
"sigma_zero[below(M!1`cols)]")
(("1"
(replace
-1
:hide?
t)
(("1"
(assert)
(("1"
(inst
-1
"LAMBDA (k_1: below(M!1`cols)):
(M!1`matrix(i!1, k_1) *
IF (k_1 = j!1) THEN 1
ELSIF (k_1 = i!1) THEN -(M!1`matrix(i!1, j!1))
ELSE 0
ENDIF)"
"LAMBDA (k_1: below(M!1`cols)): 0"
"M!1`cols-1"
"max(i!1,j!1)+1")
(("1"
(prop)
(("1"
(replace
-1
:hide?
t)
(("1"
(use
"sigma_zero[below(M!1`cols)]")
(("1"
(replace
-1
:hide?
t)
(("1"
(assert)
(("1"
(expand
"min")
(("1"
(lift-if)
(("1"
(prop)
(("1"
(expand
"max")
(("1"
(assert)
(("1"
(inst
-7
"i!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"max")
(("2"
(assert)
(("2"
(assert)
(("2"
(inst
-6
"i!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
3)
(("2"
(skolem-typepred)
(("2"
(expand
"max")
(("2"
(lift-if)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-6
3)
(("2"
(flatten)
(("2"
(inst
2
"max(i!1,j!1)")
(("1"
(grind)
nil
nil)
("2"
(grind)
nil
nil))
nil))
nil))
nil)
("3"
(hide
-6
3)
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
3)
(("2"
(hide
-1)
(("2"
(skolem-typepred)
(("2"
(expand
"min")
(("2"
(lift-if)
(("2"
(bddsimp
-1)
(("1"
(assert)
(("1"
(expand
"max")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"max")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-6
3)
(("2"
(flatten)
(("2"
(inst
2
"min(i!1,j!1)")
(("1"
(grind)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.79 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
