|
(ordered_subset
(emptyset_is_prefix 0
(emptyset_is_prefix-1 nil 3318613436 ("" (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)
(T formal-type-decl nil ordered_subset nil)
(set type-eq-decl nil sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(prefix? const-decl "bool" ordered_subset nil))
shostak))
(fullset_is_prefix 0
(fullset_is_prefix-1 nil 3318613441 ("" (grind) nil nil)
((fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(prefix? const-decl "bool" ordered_subset nil))
shostak))
(emptyset_is_suffix 0
(emptyset_is_suffix-1 nil 3318613448 ("" (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)
(T formal-type-decl nil ordered_subset nil)
(set type-eq-decl nil sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(suffix? const-decl "bool" ordered_subset nil))
shostak))
(fullset_is_suffix 0
(fullset_is_suffix-1 nil 3318613451 ("" (grind) nil nil)
((fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(suffix? const-decl "bool" ordered_subset nil))
shostak))
(upto_TCC1 0
(upto_TCC1-1 nil 3318613417
("" (grind :if-match nil)
(("" (inst - "t!2" "r!1" "t!1") (("" (assert) nil nil)) nil)) nil)
((transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(prefix? const-decl "bool" ordered_subset nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(T formal-type-decl nil ordered_subset nil))
nil))
(below_TCC1 0
(below_TCC1-1 nil 3318613417
("" (grind :if-match nil)
(("1" (inst - "r!1" "t!1") (("1" (assert) nil nil)) nil)
("2" (inst - "t!2" "r!1" "t!1") (("2" (assert) nil nil)) nil))
nil)
((transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(prefix? const-decl "bool" ordered_subset nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(T formal-type-decl nil ordered_subset nil))
nil))
(upfrom_TCC1 0
(upfrom_TCC1-1 nil 3318613417
("" (grind :if-match nil)
(("" (inst - "t!1" "r!1" "t!2") (("" (assert) nil nil)) nil)) nil)
((transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(suffix? const-decl "bool" ordered_subset nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(T formal-type-decl nil ordered_subset nil))
nil))
(above_TCC1 0
(above_TCC1-1 nil 3318613417
("" (grind :if-match nil)
(("1" (inst - "t!2" "r!1") (("1" (assert) nil nil)) nil)
("2" (inst - "t!1" "r!1" "t!2") (("2" (assert) nil nil)) nil))
nil)
((transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(suffix? const-decl "bool" ordered_subset nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(T formal-type-decl nil ordered_subset nil))
nil))
(add_below_is_upto 0
(add_below_is_upto-1 nil 3318613549 ("" (grind-with-ext) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(set type-eq-decl nil sets nil)
(order_to_partial_order application-judgement "(partial_order?)"
ordered_subset nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" ordered_subset nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" ordered_subset nil)
(order_to_strict_order application-judgement "(strict_order?)"
ordered_subset nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(union const-decl "set" sets nil)
(transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(prefix? const-decl "bool" ordered_subset nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil))
shostak))
(remove_upto_is_below 0
(remove_upto_is_below-1 nil 3318613559 ("" (grind-with-ext) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(order_to_strict_order application-judgement "(strict_order?)"
ordered_subset nil)
(order_to_partial_order application-judgement "(partial_order?)"
ordered_subset nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" ordered_subset nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" ordered_subset nil)
(/= const-decl "boolean" notequal nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(difference const-decl "set" sets nil)
(transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(prefix? const-decl "bool" ordered_subset nil)
(remove const-decl "set" sets nil) (set type-eq-decl nil sets nil))
shostak))
(add_above_is_upfrom 0
(add_above_is_upfrom-1 nil 3318613566 ("" (grind-with-ext) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(set type-eq-decl nil sets nil)
(order_to_partial_order application-judgement "(partial_order?)"
ordered_subset nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" ordered_subset nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" ordered_subset nil)
(order_to_strict_order application-judgement "(strict_order?)"
ordered_subset nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(union const-decl "set" sets nil)
(transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(upfrom const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(suffix? const-decl "bool" ordered_subset nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil))
shostak))
(remove_upfrom_is_above 0
(remove_upfrom_is_above-1 nil 3318613575
("" (grind-with-ext) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(order_to_strict_order application-judgement "(strict_order?)"
ordered_subset nil)
(order_to_partial_order application-judgement "(partial_order?)"
ordered_subset nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" ordered_subset nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" ordered_subset nil)
(/= const-decl "boolean" notequal nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(difference const-decl "set" sets nil)
(transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(upfrom const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(suffix? const-decl "bool" ordered_subset nil)
(remove const-decl "set" sets nil) (set type-eq-decl nil sets nil))
shostak))
(upto_above_related 0
(upto_above_related-1 nil 3318613579 ("" (grind-with-ext) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(order_to_strict_order application-judgement "(strict_order?)"
ordered_subset nil)
(order_to_partial_order application-judgement "(partial_order?)"
ordered_subset nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" ordered_subset nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" ordered_subset nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(difference const-decl "set" sets nil)
(transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(unrelated const-decl "set[T]" ordered_subset nil)
(complement const-decl "set" sets nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(suffix? const-decl "bool" ordered_subset nil)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(prefix? const-decl "bool" ordered_subset nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil))
shostak))
(below_upfrom_related 0
(below_upfrom_related-1 nil 3318613588 ("" (grind-with-ext) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(order_to_partial_order application-judgement "(partial_order?)"
ordered_subset nil)
(reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" ordered_subset nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" ordered_subset nil)
(order_to_strict_order application-judgement "(strict_order?)"
ordered_subset nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(transitive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(unrelated const-decl "set[T]" ordered_subset nil)
(complement const-decl "set" sets nil)
(upfrom const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(suffix? const-decl "bool" ordered_subset nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(prefix? const-decl "bool" ordered_subset nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil))
shostak))
(down_TCC1 0
(down_TCC1-2 nil 3406647229
("" (skosimp)
(("" (typepred "tr!1")
(("" (expand "reflexive_closure")
(("" (expand "union")
(("" (expand "member")
(("" (expand "prefix?")
(("" (skosimp)
(("" (expand "member")
(("" (flatten)
(("" (typepred "r!1")
(("" (split)
(("1" (expand "transitive?")
(("1" (inst - "t!2" "r!1" "t!1")
(("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(union const-decl "set" sets nil)
(prefix? const-decl "bool" ordered_subset nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil))
nil)
(down_TCC1-1 nil 3406647177 ("" (subtype-tcc) nil nil) nil nil))
(up_TCC1 0
(up_TCC1-2 nil 3406647254
("" (skosimp)
(("" (typepred "tr!1")
(("" (expand "reflexive_closure")
(("" (expand "union")
(("" (expand "suffix?")
(("" (skosimp*)
(("" (expand "member")
(("" (flatten)
(("" (typepred "r!1")
(("" (expand "member")
(("" (split)
(("1" (expand "transitive?")
(("1" (inst - "t!1" "r!1" "t!2")
(("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(union const-decl "set" sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(member const-decl "bool" sets nil)
(suffix? const-decl "bool" ordered_subset nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil))
nil)
(up_TCC1-1 nil 3406647177 ("" (subtype-tcc) nil nil) nil nil))
(down_subset 0
(down_subset-1 nil 3406647291
("" (skolem 1 ("lt" "x" "y"))
(("" (expand "subset?")
(("" (expand "reflexive_closure")
(("" (expand "union")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "lt")
(("" (expand "transitive?")
(("" (inst - "x!1" "x" "y") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(PRED type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil))
nil))
(up_subset 0
(up_subset-1 nil 3406647310
("" (expand "reflexive_closure")
(("" (expand "union")
(("" (expand "member")
(("" (expand "subset?")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "tr!1")
(("" (expand "transitive?")
(("" (inst - "x!1" "y!1" "x!2")
(("" (split -3)
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((union const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(PRED type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil))
nil))
(complement_lower_set 0
(complement_lower_set-1 nil 3406647692
("" (skosimp)
(("" (typepred "X!1")
(("" (expand "suffix?")
(("" (skosimp*)
(("" (expand "member")
(("" (expand "complement")
(("" (expand "member")
(("" (expand "prefix?")
(("" (typepred "r!1")
(("" (expand "complement")
(("" (expand "member")
(("" (inst - "r!1" "t!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((prefix? const-decl "bool" ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(complement const-decl "set" sets nil)
(lessp!1 skolem-const-decl "pred[[T, T]]" ordered_subset nil)
(X!1 skolem-const-decl "(LAMBDA (S): prefix?(S, lessp!1))"
ordered_subset nil)
(t!1 skolem-const-decl "T" ordered_subset nil)
(member const-decl "bool" sets nil)
(suffix? const-decl "bool" ordered_subset nil))
nil))
(complement_upper_set 0
(complement_upper_set-1 nil 3406647708
("" (skosimp)
(("" (typepred "X!1")
(("" (expand "complement")
(("" (expand "member")
(("" (expand "prefix?")
(("" (expand "suffix?")
(("" (expand "member")
(("" (skosimp)
(("" (typepred "r!1")
(("" (inst - "r!1" "t!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((suffix? const-decl "bool" ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(lessp!1 skolem-const-decl "pred[[T, T]]" ordered_subset nil)
(X!1 skolem-const-decl "(LAMBDA (S): suffix?(S, lessp!1))"
ordered_subset nil)
(t!1 skolem-const-decl "T" ordered_subset nil)
(prefix? const-decl "bool" ordered_subset nil)
(complement const-decl "set" sets nil))
nil))
(lower_set_def 0
(lower_set_def-1 nil 3406647530
("" (skosimp)
(("" (typepred "tr!1")
(("" (split)
(("1" (flatten)
(("1" (expand "reflexive_closure")
(("1" (expand "union")
(("1" (expand "member")
(("1" (expand "image")
(("1" (expand "extend")
(("1" (apply-extensionality 1 :hide? t)
(("1" (case-replace "X!1(x!1)")
(("1" (expand "Union")
(("1" (inst + "down(tr!1)(x!1)")
(("1" (expand "reflexive_closure")
(("1"
(expand "union")
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (split)
(("1"
(flatten)
(("1"
(inst + "x!1")
(("1"
(expand "reflexive_closure")
(("1"
(expand "union")
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "prefix?")
(("2"
(skosimp)
(("2"
(expand "reflexive_closure")
(("2"
(expand "union")
(("2"
(expand "member")
(("2"
(flatten)
(("2"
(expand "transitive?")
(("2"
(typepred "r!1")
(("2"
(expand
"reflexive_closure")
(("2"
(expand "union")
(("2"
(expand "member")
(("2"
(split -1)
(("1"
(inst
-5
"t!1"
"r!1"
"x!1")
(("1"
(assert)
nil
nil))
nil)
("2"
(replace -1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2)
(("2" (assert)
(("2" (expand "Union")
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "x!2")
(("2"
(replace -2)
(("2"
(assert)
(("2"
(expand "prefix?")
(("2"
(expand "member")
(("2"
(inst -5 "x!1" "x!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "prefix?")
(("2" (skosimp)
(("2" (expand "member")
(("2"
(flatten)
(("2"
(typepred "x!1")
(("2"
(typepred "r!1")
(("2"
(split -1)
(("1"
(expand "transitive?")
(("1"
(inst -6 "t!2" "r!1" "x!1")
(("1" (assert) nil nil))
nil))
nil)
("2"
(replace -1)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2" (hide -1)
(("2" (expand "reflexive_closure")
(("2" (expand "union")
(("2" (expand "member")
(("2" (expand "image")
(("2" (expand "extend")
(("2" (expand "Union")
(("2" (expand "prefix?")
(("2" (expand "member")
(("2"
(skosimp)
(("2"
(typepred "r!1")
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "r!1")
(("2"
(skosimp)
(("2"
(typepred "a!2")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "x!2")
(("2"
(inst + "a!2")
(("2"
(expand
"prefix?"
-3)
(("2"
(inst
-
"t!1"
"r!1")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(union const-decl "set" sets nil)
(image const-decl "set[R]" function_image nil)
(FALSE const-decl "bool" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(Union const-decl "set" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(prefix? const-decl "bool" ordered_subset nil)
(tr!1 skolem-const-decl "(transitive?[T])" ordered_subset nil)
(X!1 skolem-const-decl "set[T]" ordered_subset nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(x!1 skolem-const-decl "T" ordered_subset nil)
(reflexive? const-decl "bool" relations nil)
(extend const-decl "R" extend nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil))
nil))
(upper_set_def 0
(upper_set_def-1 nil 3406647552
("" (skosimp)
(("" (expand "reflexive_closure")
(("" (expand "union")
(("" (expand "member")
(("" (expand "image")
(("" (expand "extend")
(("" (split)
(("1" (flatten)
(("1" (apply-extensionality 1 :hide? t)
(("1" (case-replace "X!1(x!1)")
(("1" (expand "Union")
(("1" (inst + "up(tr!1)(x!1)")
(("1" (expand "reflexive_closure")
(("1" (expand "union")
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (assert)
(("2" (prop)
(("1"
(inst + "x!1")
(("1"
(expand "reflexive_closure")
(("1"
(expand "union")
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(expand "reflexive_closure")
(("2"
(expand "union")
(("2"
(expand "member")
(("2"
(expand "suffix?")
(("2"
(skosimp)
(("2"
(expand "member")
(("2"
(flatten)
(("2"
(typepred "r!1")
(("2"
(split)
(("1"
(typepred "tr!1")
(("1"
(expand
"transitive?")
(("1"
(inst
-
"x!1"
"r!1"
"t!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2)
(("2" (assert)
(("2" (expand "Union")
(("2" (skosimp)
(("2"
(typepred "a!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "x!2")
(("2"
(expand "suffix?")
(("2"
(replace -2)
(("2"
(assert)
(("2"
(inst -5 "x!1" "x!2")
(("2"
(expand "member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "suffix?")
(("2" (skosimp)
(("2" (expand "member")
(("2" (flatten)
(("2"
(typepred "x!1")
(("2"
(typepred "r!1")
(("2"
(split -1)
(("1"
(typepred "tr!1")
(("1"
(expand "transitive?")
(("1"
(inst - "x!1" "r!1" "t!2")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2" (hide -1)
(("2" (expand "Union")
(("2" (expand "suffix?")
(("2" (expand "member")
(("2" (skosimp*)
(("2"
(typepred "r!1")
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "x!1")
(("2"
(inst + "a!1")
(("2"
(expand "suffix?")
(("2"
(inst - "t!1" "r!1")
(("2"
(expand "member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(extend const-decl "R" extend nil)
(reflexive? const-decl "bool" relations nil)
(x!1 skolem-const-decl "T" ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(X!1 skolem-const-decl "set[T]" ordered_subset nil)
(tr!1 skolem-const-decl "(transitive?[T])" ordered_subset nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(suffix? const-decl "bool" ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setofsets type-eq-decl nil sets nil)
(Union const-decl "set" sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(FALSE const-decl "bool" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(boolean nonempty-type-decl nil booleans nil)
(image const-decl "set[R]" function_image nil)
(union const-decl "set" sets nil))
nil))
(Union_lower_set 0
(Union_lower_set-1 nil 3406647579
("" (skosimp)
(("" (expand "every")
(("" (expand "prefix?")
(("" (skosimp)
(("" (expand "member")
(("" (expand "Union")
(("" (typepred "r!1")
(("" (expand "Union")
(("" (skosimp)
(("" (inst + "a!1")
(("" (inst - "a!1")
(("" (inst - "t!1" "r!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((every const-decl "bool" sets nil)
(Union const-decl "set" sets nil)
(U!1 skolem-const-decl "setofsets[T]" ordered_subset nil)
(a!1 skolem-const-decl "(U!1)" ordered_subset nil)
(r!1 skolem-const-decl "(Union(U!1))" ordered_subset nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil ordered_subset nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
(prefix? const-decl "bool" ordered_subset nil))
nil))
(Union_upper_set 0
(Union_upper_set-1 nil 3406647751
("" (expand "every")
(("" (expand "Union")
(("" (expand "suffix?")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "r!1")
(("" (skosimp)
(("" (typepred "a!1")
(("" (inst - "a!1")
(("" (inst - "t!1" "r!1")
(("" (inst + "a!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(U!1 skolem-const-decl "setofsets[T]" ordered_subset nil)
(a!1 skolem-const-decl "(U!1)" ordered_subset nil)
(r!1 skolem-const-decl "({x | EXISTS (a: (U!1)): a(x)})"
ordered_subset nil)
(suffix? const-decl "bool" ordered_subset nil)
(every const-decl "bool" sets nil))
nil))
(union_lower_set 0
(union_lower_set-1 nil 3406647775
("" (skosimp)
((""
(lemma "Union_lower_set"
("U" "add(X!1,singleton(Y!1))" "tr" "tr!1"))
(("" (split -1)
(("1"
(lemma "extensionality"
("f" "Union(extend
[setof[T], (LAMBDA (S): prefix?(S, tr!1)), bool,
FALSE]
(add(X!1, singleton(Y!1))))" "g"
"union(X!1,Y!1)"))
(("1" (split -1)
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (skosimp)
(("2" (expand "union")
(("2" (expand "singleton")
(("2" (expand "add")
(("2" (expand "extend")
(("2" (expand "Union")
(("2" (expand "member")
(("2" (case-replace "X!1(x!1)")
(("1" (inst + "X!1") nil nil)
("2"
(assert)
(("2"
(case-replace "Y!1(x!1)")
(("1"
(inst + "Y!1")
(("1"
(assert)
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(assert)
(("2"
(expand "member")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "singleton")
(("2" (expand "add")
(("2" (expand "member")
(("2" (expand "extend")
(("2" (expand "every") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(prefix? const-decl "bool" ordered_subset nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil ordered_subset nil)
(Union_lower_set formula-decl nil ordered_subset nil)
(nonempty_add_finite application-judgement "non_empty_finite_set"
finite_sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(every const-decl "bool" sets nil)
(nonempty_extend application-judgement "(nonempty?[T])"
extend_set_props nil)
(finite_extend application-judgement "finite_set[T]"
extend_set_props nil)
(extensionality formula-decl nil functions nil)
(Union const-decl "set" sets nil) (union const-decl "set" sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Y!1 skolem-const-decl "(LAMBDA (S): prefix?(S, tr!1))"
ordered_subset nil)
(X!1 skolem-const-decl "(LAMBDA (S): prefix?(S, tr!1))"
ordered_subset nil)
(tr!1 skolem-const-decl "(transitive?[T])" ordered_subset nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil))
nil))
(union_upper_set 0
(union_upper_set-1 nil 3406647799
("" (skosimp)
((""
(lemma "Union_upper_set"
("U" "add(X!1,singleton(Y!1))" "<" "lessp!1"))
(("" (split -1)
(("1"
(lemma "extensionality"
("f" "Union(extend
[setof[T], (LAMBDA (S): suffix?(S, lessp!1)), bool,
FALSE]
(add(X!1, singleton(Y!1))))" "g"
"union(X!1, Y!1)"))
(("1" (split -1)
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (skosimp)
(("2" (expand "union")
(("2" (expand "member")
(("2" (expand "singleton")
(("2" (expand "add")
(("2" (expand "member")
(("2" (expand "extend")
(("2" (expand "Union")
(("2"
(case-replace "X!1(x!1)")
(("1" (inst + "X!1") nil nil)
("2"
(case-replace "Y!1(x!1)")
(("1" (inst + "Y!1") nil nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "singleton")
(("2" (expand "add")
(("2" (expand "member")
(("2" (expand "extend")
(("2" (expand "every") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(suffix? const-decl "bool" ordered_subset nil)
(set type-eq-decl nil sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil ordered_subset nil)
(Union_upper_set formula-decl nil ordered_subset nil)
(nonempty_add_finite application-judgement "non_empty_finite_set"
finite_sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(every const-decl "bool" sets nil)
(nonempty_extend application-judgement "(nonempty?[T])"
extend_set_props nil)
(finite_extend application-judgement "finite_set[T]"
extend_set_props nil)
(extensionality formula-decl nil functions nil)
(Union const-decl "set" sets nil) (union const-decl "set" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(member const-decl "bool" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil))
nil))
(Intersection_lower_set 0
(Intersection_lower_set-1 nil 3406647819
("" (expand "every")
(("" (expand "Intersection")
(("" (expand "prefix?")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "a!1")
(("" (typepred "r!1")
(("" (inst - "a!1")
(("" (inst - "a!1")
(("" (inst - "t!1" "r!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(U!1 skolem-const-decl "setofsets[T]" ordered_subset nil)
(a!1 skolem-const-decl "(U!1)" ordered_subset nil)
(r!1 skolem-const-decl "({x | FORALL (a: (U!1)): a(x)})"
ordered_subset nil)
(prefix? const-decl "bool" ordered_subset nil)
(every const-decl "bool" sets nil))
nil))
(Intersection_upper_set 0
(Intersection_upper_set-1 nil 3406647838
("" (skosimp)
(("" (lemma "Union_lower_set" ("tr" "tr!1" "U" "Complement(U!1)"))
(("" (split -1)
(("1" (rewrite "Demorgan2" -1 :dir rl)
(("1" (lemma "complement_lower_set" ("<" "tr!1"))
(("1" (inst - "complement(Intersection(U!1))")
(("1" (rewrite "complement_complement") nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "every")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2" (expand "Complement")
(("2" (skosimp)
(("2" (replace -1)
(("2" (typepred "b!1")
(("2" (hide -2)
(("2" (inst - "b!1")
(("2"
(lemma "complement_upper_set"
("<" "tr!1" "X" "b!1"))
(("1" (propax) nil nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(Complement const-decl "setofsets[T]" sets_lemmas nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil ordered_subset nil)
(Union_lower_set formula-decl nil ordered_subset nil)
(suffix? const-decl "bool" ordered_subset nil)
(complement_upper_set formula-decl nil ordered_subset nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(every const-decl "bool" sets nil)
(Demorgan2 formula-decl nil sets_lemmas nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(tr!1 skolem-const-decl "(transitive?[T])" ordered_subset nil)
(U!1 skolem-const-decl "setofsets[T]" ordered_subset nil)
(Intersection const-decl "set" sets nil)
(complement const-decl "set" sets nil)
(prefix? const-decl "bool" ordered_subset nil)
(set type-eq-decl nil sets nil)
(complement_complement formula-decl nil sets_lemmas nil)
(pred type-eq-decl nil defined_types nil)
(complement_lower_set formula-decl nil ordered_subset nil))
nil))
(intersection_lower_set 0
(intersection_lower_set-1 nil 3406647858
("" (skosimp)
((""
(lemma "Intersection_lower_set"
("<" "lessp!1" "U" "add(X!1,singleton(Y!1))"))
(("" (split -1)
(("1"
(lemma "extensionality"
("f" "Intersection(extend
[setof[T],
(LAMBDA (S): prefix?(S, lessp!1)), bool,
FALSE]
(add(X!1, singleton(Y!1))))" "g"
"intersection(X!1, Y!1)"))
(("1" (split -1)
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (skosimp)
(("2" (expand "intersection")
(("2" (expand "member")
(("2" (expand "singleton")
(("2" (expand "add")
(("2" (expand "member")
(("2" (expand "extend")
(("2" (expand "Intersection")
(("2"
(case-replace "X!1(x!1)")
(("1"
(case-replace "Y!1(x!1)")
(("1"
(skosimp)
(("1"
(typepred "a!1")
(("1" (assert) nil nil))
nil))
nil)
("2"
(assert)
(("2" (inst - "Y!1") nil nil))
nil))
nil)
("2"
(assert)
(("2" (inst - "X!1") nil nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.124 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.
|
