|
(bags
(delete_TCC1 0
(delete_TCC1-1 nil 3286291749
("" (ground)
(("" (skolem!) (("" (apply (then (ground) (assert))) nil nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(emptybag_is_empty? 0
(emptybag_is_empty?-1 nil 3286291749
("" (skosimp*)
(("" (split)
(("1" (flatten)
(("1" (expand "empty?")
(("1" (expand "emptybag")
(("1" (apply-extensionality 1) (("1" (inst?) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2" (expand "empty?")
(("2" (expand "emptybag") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" bags nil) (bag type-eq-decl nil bags nil)
(T formal-type-decl nil bags 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)
(emptybag const-decl "bag" bags nil))
nil))
(delete_purge 0
(delete_purge-1 nil 3286291749
("" (skosimp*)
(("" (expand "delete")
(("" (expand "purge")
(("" (apply-extensionality 1)
(("" (hide 2) (("" (lift-if) (("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((delete const-decl "bag" bags nil)
(T formal-type-decl nil bags 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(purge const-decl "bag" bags nil))
nil))
(insert_unique 0
(insert_unique-1 nil 3286291749
("" (skosimp*)
(("" (expand "insert")
(("" (apply-extensionality 1)
((""
(case "(LAMBDA (t: T): IF x!1 = t THEN 1 + a!1(t) ELSE a!1(t) ENDIF)(x!2)
= (LAMBDA (t: T): IF x!1 = t THEN 1 + b!1(t) ELSE b!1(t) ENDIF)(x!2)")
(("1" (hide -2)
(("1" (beta -1)
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (replace -1) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((insert const-decl "bag" bags nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(bag type-eq-decl nil bags 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)
(T formal-type-decl nil bags nil))
nil))
(insert_exchange 0
(insert_exchange-1 nil 3286291749
("" (skosimp*)
(("" (expand "insert")
(("" (apply-extensionality :hide? t)
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((insert const-decl "bag" bags nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bag type-eq-decl nil bags 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)
(T formal-type-decl nil bags nil))
nil))
(delete_insert_TCC1 0
(delete_insert_TCC1-1 nil 3286291749 ("" (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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(delete_insert 0
(delete_insert-1 nil 3286291749
("" (skosimp*)
(("" (expand "insert")
(("" (expand "delete")
(("" (apply-extensionality 1 :hide? t)
(("" (case "x!1 = x!2")
(("1" (lift-if) (("1" (assert) nil nil)) nil)
("2" (lift-if) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((insert const-decl "bag" bags nil)
(T formal-type-decl nil bags 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(delete const-decl "bag" bags nil))
nil))
(insert_delete 0
(insert_delete-1 nil 3286291749
("" (skosimp*)
(("" (apply-extensionality 1)
(("" (expand "insert")
(("" (expand "delete") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((T formal-type-decl nil bags 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)
(delete const-decl "bag" bags nil)
(insert const-decl "bag" bags nil) (bag type-eq-decl nil bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(delete_insert_diff 0
(delete_insert_diff-1 nil 3286291749
("" (skosimp*)
(("" (expand "delete")
(("" (expand "insert")
(("" (apply-extensionality 2 :hide? t)
(("" (lift-if) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((delete const-decl "bag" bags nil)
(T formal-type-decl nil bags 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bag type-eq-decl nil bags nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(insert const-decl "bag" bags nil))
nil))
(decomposition 0
(decomposition-1 nil 3286291749
("" (skosimp*)
(("" (expand "empty?")
(("" (skosimp*)
((""
(inst 2
"(LAMBDA t: IF t = x!1 THEN b!1(t) - 1 ELSE b!1(t) ENDIF)"
"x!1")
(("1" (expand "insert")
(("1" (apply-extensionality 2) nil nil)) nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" bags nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(b!1 skolem-const-decl "bag" bags nil)
(bag type-eq-decl nil bags nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(x!1 skolem-const-decl "T" bags nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil bags nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(insert const-decl "bag" bags nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(bag_equality 0
(bag_equality-1 nil 3286291749
("" (skosimp*)
(("" (split 1)
(("1" (flatten)
(("1" (expand "eqmult")
(("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (skosimp*)
(("2" (expand "eqmult")
(("2" (apply-extensionality 1) nil nil)) nil))
nil))
nil))
nil)
((eqmult const-decl "bool" bags 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)
(T formal-type-decl nil bags nil) (bag type-eq-decl nil bags nil))
nil))
(subbag_empty 0
(subbag_empty-1 nil 3286291749
("" (skosimp*)
(("" (expand "subbag?")
(("" (expand "emptybag")
(("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((subbag? const-decl "bool" bags nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(emptybag const-decl "bag" bags nil))
nil))
(subbag_equality 0
(subbag_equality-1 nil 3286291749
("" (skosimp*)
(("" (expand "subbag?")
(("" (split 1)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (flatten)
(("2" (apply-extensionality 1)
(("2" (hide 2)
(("2" (inst?)
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subbag? const-decl "bool" bags nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bag type-eq-decl nil bags 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)
(T formal-type-decl nil bags nil))
nil))
(subbag_trans 0
(subbag_trans-1 nil 3288965621 ("" (grind) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T formal-type-decl nil bags nil)
(subbag? const-decl "bool" bags nil))
shostak))
(bag_plus_union 0
(bag_plus_union-1 nil 3286291749
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("" (expand "union")
(("" (expand "plus")
(("" (expand "intersection")
(("" (expand "max")
(("" (expand "min")
(("" (lift-if)
(("" (lift-if)
(("" (ground)
(("" (lift-if) (("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil bags 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)
(intersection const-decl "bag" bags nil)
(union const-decl "bag" bags nil) (plus const-decl "bag" bags nil)
(bag type-eq-decl nil bags 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
nil))
(bag_plus_comm 0
(bag_plus_comm-1 nil 3286291749
("" (skosimp*) (("" (expand "plus") (("" (propax) nil nil)) nil))
nil)
((plus const-decl "bag" bags nil)) nil))
(plus_emptybag 0
(plus_emptybag-1 nil 3286291749
("" (skosimp*)
(("" (expand "plus")
(("" (expand "emptybag") (("" (apply-eta "a!1") nil nil)) nil))
nil))
nil)
((plus const-decl "bag" bags nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bag type-eq-decl nil bags 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)
(T formal-type-decl nil bags nil)
(emptybag const-decl "bag" bags nil))
nil))
(bag_plus_insert 0
(bag_plus_insert-1 nil 3286291749
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("" (expand "plus")
(("" (expand "insert")
(("" (lift-if) (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((T formal-type-decl nil bags 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)
(insert const-decl "bag" bags nil) (plus const-decl "bag" bags nil)
(bag type-eq-decl nil bags nil))
nil))
(bag_distributive 0
(bag_distributive-1 nil 3286291749
("" (skosimp*)
(("" (expand "union")
(("" (expand "intersection")
(("" (apply-extensionality 1)
(("1" (hide 2) (("1" (grind) nil nil)) nil)
("2" (hide 2) (("2" (skosimp*) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((union const-decl "bag" bags nil) (T formal-type-decl nil bags 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)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(bag type-eq-decl nil bags nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(a!1 skolem-const-decl "bag" bags nil)
(b!1 skolem-const-decl "bag" bags nil)
(c!1 skolem-const-decl "bag" bags 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)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(intersection const-decl "bag" bags nil))
nil))
(extract_subbag 0
(extract_subbag-1 nil 3286291771
("" (skosimp*)
(("" (expand "subbag?")
(("" (skosimp*)
(("" (expand "extract")
(("" (lift-if)
(("" (split)
(("1" (flatten) (("1" (assert) nil)))
("2" (flatten) (("2" (assert) nil))))))))))))))
nil)
((subbag? const-decl "bool" bags nil)
(extract const-decl "bag" bags nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(extract_disj 0
(extract_disj-1 nil 3286292091 ("" (skosimp*) (("" (grind) nil)) nil)
((disjoint? const-decl "bool" bags nil)
(empty? const-decl "bool" bags nil)
(intersection const-decl "bag" bags nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(extract const-decl "bag" bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(bag_disj_comm 0
(bag_disj_comm-1 nil 3286292236 ("" (grind) nil nil)
((T formal-type-decl nil bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(intersection const-decl "bag" bags nil)
(empty? const-decl "bool" bags nil)
(disjoint? const-decl "bool" bags nil))
nil))
(bag_union_comm 0
(bag_union_comm-1 nil 3286292266
("" (skosimp*)
(("" (decompose-equality +)
(("" (expand "union")
(("" (expand "max")
(("" (lift-if)
(("" (split)
(("1" (flatten)
(("1" (lift-if)
(("1" (split)
(("1" (flatten) (("1" (assert) nil)))
("2" (propax) nil)))))))
("2" (flatten)
(("2" (lift-if)
(("2" (split)
(("1" (propax) nil)
("2" (flatten)
(("2" (assert) nil))))))))))))))))))))
nil)
((bag type-eq-decl nil bags nil) (union const-decl "bag" bags 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)
(T formal-type-decl nil bags 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))
nil))
(bag_union_fix_pt 0
(bag_union_fix_pt-1 nil 3286292546
("" (skosimp*)
(("" (decompose-equality +)
(("" (expand "union")
(("" (expand "max") (("" (propax) nil))))))))
nil)
((bag type-eq-decl nil bags nil) (union const-decl "bag" bags 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)
(T formal-type-decl nil bags nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
nil))
(bag_purge_extract 0
(bag_purge_extract-1 nil 3286292562
("" (skosimp*)
(("" (decompose-equality +)
(("" (expand "union")
(("" (expand "max")
(("" (expand "purge")
(("" (lift-if)
(("" (lift-if)
(("" (expand "extract")
(("" (lift-if)
(("" (split)
(("1" (prop) (("1" (assert) nil nil)) nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bag type-eq-decl nil bags nil) (union const-decl "bag" bags nil)
(purge const-decl "bag" bags nil)
(extract const-decl "bag" bags 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)
(T formal-type-decl nil bags nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
nil))
(bag_disj_extract_perge 0
(bag_disj_extract_perge-1 nil 3286292587 ("" (grind) nil nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(extract const-decl "bag" bags nil)
(purge const-decl "bag" bags nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(intersection const-decl "bag" bags nil)
(empty? const-decl "bool" bags nil)
(disjoint? const-decl "bool" bags nil))
nil))
(bag_extract_union_subbag 0
(bag_extract_union_subbag-1 nil 3286292609
("" (skosimp*)
(("" (lemma "extract_disj")
(("" (inst - "a!1" "x!1" "y!1")
(("" (assert)
(("" (expand "subbag?")
(("" (skosimp*)
(("" (expand "union")
(("" (expand "max")
(("" (lift-if)
(("" (expand "disjoint?")
(("" (expand "intersection")
(("" (expand "empty?")
(("" (inst?)
(("" (expand "min")
((""
(lift-if)
((""
(grind)
nil))))))))))))))))))))))))))))))
nil)
((extract_disj formula-decl nil bags nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(disjoint? const-decl "bool" bags nil)
(empty? const-decl "bool" bags nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(extract const-decl "bag" bags nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(intersection const-decl "bag" bags nil)
(union const-decl "bag" bags nil)
(subbag? const-decl "bool" bags nil)
(bag type-eq-decl nil bags 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)
(T formal-type-decl nil bags nil))
nil))
(union_upper_bound 0
(union_upper_bound-1 nil 3287522217 ("" (grind) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T formal-type-decl nil bags nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(subbag? const-decl "bool" bags nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(union const-decl "bag" bags nil))
shostak)))
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
