|
(closure_ops
(reflexive_closure_TCC1 0
(reflexive_closure_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(reflexive? const-decl "bool" relations nil))
nil))
(irreflexive_kernel_TCC1 0
(irreflexive_kernel_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(irreflexive? const-decl "bool" relations nil))
nil))
(symmetric_closure_TCC1 0
(symmetric_closure_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(union const-decl "set" sets nil)
(symmetric? const-decl "bool" relations nil))
nil))
(symmetric_kernel_TCC1 0
(symmetric_kernel_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(intersection const-decl "set" sets nil)
(symmetric? const-decl "bool" relations nil))
nil))
(asymmetric_kernel_TCC1 0
(asymmetric_kernel_TCC1-1 nil 3315150742 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(difference const-decl "set" sets nil)
(T formal-type-decl nil closure_ops nil)
(asymmetric? const-decl "bool" relations_extra nil))
nil))
(transitive_closure_TCC1 0
(transitive_closure_TCC1-1 nil 3315150742
("" (expand* "transitive?" "IUnion")
(("" (skosimp*)
(("" (forward-chain "iterate_add_applied") (("" (inst?) nil nil))
nil))
nil))
nil)
((numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(T formal-type-decl nil closure_ops nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(iterate_add_applied formula-decl nil relation_iterate nil)
(transitive? const-decl "bool" relations nil)
(IUnion const-decl "set[T]" indexed_sets nil))
nil))
(preorder_closure_TCC1 0
(preorder_closure_TCC1-1 nil 3315150742
("" (expand "preorder?")
(("" (skolem!)
(("" (split)
(("1" (expand* "reflexive?" "IUnion")
(("1" (skolem!)
(("1" (inst + "0")
(("1" (expand "iterate") (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (expand* "transitive?" "IUnion")
(("2" (skosimp*)
(("2" (forward-chain "iterate_add_applied")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((transitive? const-decl "bool" relations nil)
(iterate_add_applied formula-decl nil relation_iterate nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(reflexive? const-decl "bool" relations 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)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(preorder? const-decl "bool" orders nil))
nil))
(reflexive_irreflexive 0
(reflexive_irreflexive-1 nil 3315150906 ("" (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 closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(member const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(difference const-decl "set" sets nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil))
shostak))
(irreflexive_reflexive 0
(irreflexive_reflexive-1 nil 3315150924 ("" (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 closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(irreflexive? const-decl "bool" relations nil)
(member const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(union const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil))
shostak))
(reflexive_closure_preserves_transitive 0
(reflexive_closure_preserves_transitive-1 nil 3315150742
("" (skolem-typepred)
((""
(expand* "preorder?" "transitive?" "reflexive_closure" "union"
"member")
(("" (skosimp)
(("" (inst - "x!1" "y!1" "z!1") (("" (ground) nil nil)) nil))
nil))
nil))
nil)
((union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(reflexive_closure_preserves_antisymmetric 0
(reflexive_closure_preserves_antisymmetric-1 nil 3315150742
("" (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)
(T formal-type-decl nil closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(antisymmetric? const-decl "bool" relations nil))
nil))
(order_to_partial_order 0
(order_to_partial_order-1 nil 3315150742
("" (skolem-typepred)
((""
(expand* "partial_order?" "preorder?" "antisymmetric?"
"reflexive_closure" "union" "member")
nil nil))
nil)
((reflexive_closure_preserves_antisymmetric application-judgement
"(antisymmetric?)" closure_ops nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" closure_ops nil)
(partial_order? const-decl "bool" orders nil)
(order? const-decl "bool" relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(reflexive_closure_dichotomous 0
(reflexive_closure_dichotomous-1 nil 3315150742
("" (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)
(T formal-type-decl nil closure_ops nil)
(pred type-eq-decl nil defined_types nil)
(trichotomous? const-decl "bool" orders nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(dichotomous? const-decl "bool" orders nil))
nil))
(linear_order_to_total_order 0
(linear_order_to_total_order-1 nil 3315150742
("" (skolem-typepred)
((""
(expand* "linear_order?" "order?" "total_order?"
"partial_order?")
(("" (flatten)
(("" (assert)
((""
(lemma "reflexive_closure_preserves_transitive"
("R" "R!1"))
((""
(lemma "reflexive_closure_preserves_antisymmetric"
("R" "R!1"))
(("" (lemma "reflexive_closure_dichotomous" ("R" "R!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((order? const-decl "bool" relations_extra nil)
(partial_order? const-decl "bool" orders nil)
(total_order? const-decl "bool" orders nil)
(reflexive_closure_preserves_antisymmetric judgement-tcc nil
closure_ops nil)
(antisymmetric? const-decl "bool" relations nil)
(trichotomous? const-decl "bool" orders nil)
(reflexive_closure_dichotomous judgement-tcc nil closure_ops nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive_closure_preserves_transitive judgement-tcc nil
closure_ops nil)
(linear_order? const-decl "bool" relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(order_to_strict_order 0
(order_to_strict_order-1 nil 3315150742
("" (skolem-typepred)
((""
(expand* "order?" "antisymmetric?" "strict_order?" "transitive?"
"irreflexive_kernel" "difference" "member")
(("" (skosimp)
(("" (inst - "x!1" "y!1" "z!1")
(("" (inst - "y!1" "z!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((antisymmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(strict_order? const-decl "bool" orders nil)
(order? const-decl "bool" relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(irreflexive_kernel_of_antisymmetric 0
(irreflexive_kernel_of_antisymmetric-1 nil 3315150742
("" (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)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(T formal-type-decl nil closure_ops nil)
(asymmetric? const-decl "bool" relations_extra nil))
nil))
(irreflexive_kernel_trichotomous 0
(irreflexive_kernel_trichotomous-1 nil 3315150742
("" (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)
(T formal-type-decl nil closure_ops nil)
(pred type-eq-decl nil defined_types nil)
(dichotomous? const-decl "bool" orders nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(trichotomous? const-decl "bool" orders nil))
nil))
(linear_order_to_strict_total_order 0
(total_order_to_strict_total_order-1 nil 3315150742
("" (skolem!)
(("" (expand "strict_total_order?") (("" (propax) nil nil)) nil))
nil)
((irreflexive_kernel_trichotomous application-judgement
"(trichotomous?)" closure_ops nil)
(irreflexive_kernel_of_antisymmetric application-judgement
"(asymmetric?)" closure_ops nil)
(order_to_strict_order application-judgement "(strict_order?)"
closure_ops nil)
(strict_total_order? const-decl "bool" orders nil))
nil))
(symmetric_kernel_of_preorder 0
(symmetric_kernel_of_preorder-1 nil 3315150742
("" (skolem-typepred)
(("" (expand "equivalence?")
(("" (split)
(("1"
(expand* "preorder?" "reflexive?" "symmetric_kernel"
"intersection" "converse" "member")
(("1" (skosimp) (("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil)
("2"
(expand* "preorder?" "transitive?" "symmetric_kernel"
"intersection" "converse" "member")
(("2" (skosimp)
(("2" (inst-cp - "x!1" "y!1" "z!1")
(("2" (inst - "z!1" "y!1" "x!1") (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((equivalence? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(symmetric_kernel const-decl "(symmetric?)" closure_ops nil)
(preorder? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(asymmetric_kernel_of_preorder 0
(asymmetric_kernel_of_preorder-1 nil 3315150742
("" (skolem-typepred)
(("" (expand "strict_order?")
(("" (rewrite "asymmetric_is_irreflexive")
((""
(expand* "preorder?" "transitive?" "asymmetric_kernel"
"difference" "converse" "member")
(("" (skosimp)
(("" (inst-cp - "x!1" "y!1" "z!1")
(("" (inst - "z!1" "x!1" "y!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((strict_order? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(asymmetric_kernel const-decl "(asymmetric?)" closure_ops nil)
(asymmetric? const-decl "bool" relations_extra nil)
(asymmetric_is_irreflexive judgement-tcc nil relations_extra nil)
(preorder? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(preorder_closure_converse 0
(preorder_closure_converse-1 nil 3315151634
("" (skolem!)
(("" (expand "preorder_closure")
(("" (decompose-equality)
(("" (expand "IUnion")
(("" (iff)
(("" (prop)
(("1" (skolem!)
(("1" (rewrite "iterate_converse")
(("1" (expand "converse") (("1" (inst?) nil nil))
nil))
nil))
nil)
("2" (expand "converse" -)
(("2" (skolem!)
(("2" (inst?)
(("2" (rewrite "iterate_converse")
(("2" (expand "converse")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((preorder_closure const-decl "(preorder?)" closure_ops nil)
(iterate_converse formula-decl nil relation_iterate nil)
(T formal-type-decl nil closure_ops nil)
(boolean nonempty-type-decl nil booleans nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(pred type-eq-decl nil defined_types nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(set type-eq-decl nil sets 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)
(number nonempty-type-decl nil numbers nil))
shostak))
(symmetry_char 0
(symmetry_char-1 nil 3315151700
("" (skolem!)
(("" (expand* "subset?" "member" "converse" "symmetric?") nil nil))
nil)
((subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(symmetric? const-decl "bool" relations nil))
shostak))
(transitive_closure_of_reflexive 0
(transitive_closure_of_reflexive-1 nil 3315150742
("" (skolem-typepred)
((""
(expand* "preorder?" "reflexive?" "transitive_closure" "IUnion")
(("" (skolem!)
(("" (inst + 1)
(("" (assert)
(("" (inst?)
(("" (expand* "iterate" "o" "iterate")
(("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IUnion const-decl "set[T]" indexed_sets nil)
(transitive_closure const-decl "(transitive?)" closure_ops nil)
(preorder? const-decl "bool" orders nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(O const-decl "bool" relation_props nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(transitive_closure_is_monotone 0
(transitive_closure_is_monotone-1 nil 3315151790
("" (skosimp)
(("" (expand "transitive_closure")
(("" (rewrite "IUnion_is_monotone")
(("" (skolem!) (("" (rewrite "iterate_is_monotone") nil nil))
nil))
nil))
nil))
nil)
((transitive_closure const-decl "(transitive?)" closure_ops nil)
(iterate_is_monotone formula-decl nil relation_iterate nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(T formal-type-decl nil closure_ops nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(IUnion_is_monotone formula-decl nil indexed_sets_extra nil))
shostak))
(preorder_closure_is_monotone 0
(preorder_closure_is_monotone-1 nil 3315151831
("" (skosimp)
(("" (expand "preorder_closure")
(("" (rewrite "IUnion_is_monotone")
(("" (skolem!) (("" (rewrite "iterate_is_monotone") nil nil))
nil))
nil))
nil))
nil)
((preorder_closure const-decl "(preorder?)" closure_ops nil)
(iterate_is_monotone formula-decl nil relation_iterate nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(T formal-type-decl nil closure_ops 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)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(IUnion_is_monotone formula-decl nil indexed_sets_extra nil))
shostak))
(preorder_closure_preserves_symmetry 0
(preorder_closure_preserves_symmetry-1 nil 3315150742
("" (skolem-typepred)
(("" (expand "equivalence?")
(("" (typepred "preorder_closure(R!1)")
(("" (expand "preorder?")
(("" (prop)
(("" (rewrite "symmetry_char")
(("" (rewrite "symmetry_char")
(("" (rewrite "preorder_closure_converse" :dir rl)
(("" (rewrite "preorder_closure_is_monotone") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((equivalence? const-decl "bool" relations nil)
(symmetry_char formula-decl nil closure_ops nil)
(reflexive_converse application-judgement "(reflexive?[T])"
relation_converse_props nil)
(transitive_converse application-judgement "(transitive?[T])"
relation_converse_props nil)
(preorder_converse application-judgement "(preorder?[T])"
relation_converse_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(preorder_closure_converse formula-decl nil closure_ops nil)
(preorder_closure_is_monotone formula-decl nil closure_ops nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(symmetric_converse application-judgement "(symmetric?[T])"
relation_converse_props nil)
(pred type-eq-decl nil defined_types nil)
(preorder? const-decl "bool" orders nil)
(preorder_closure const-decl "(preorder?)" closure_ops nil)
(symmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(transitive_closure_step_r 0
(transitive_closure_step_r-1 nil 3315151963
("" (skolem!)
(("" (decompose-equality)
(("" (expand* "transitive_closure" "preorder_closure" "IUnion")
(("" (expand "iterate" 1 1)
(("" (expand "o")
(("" (iff)
(("" (prop)
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert) (("1" (inst?) nil nil)) nil)) nil))
nil)
("2" (skosimp*)
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(transitive_closure const-decl "(transitive?)" closure_ops nil)
(O const-decl "bool" relation_props nil)
(preorder? const-decl "bool" orders nil)
(preorder_closure const-decl "(preorder?)" closure_ops 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 closure_ops nil)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IUnion const-decl "set[T]" indexed_sets nil))
shostak))
(transitive_closure_step_l 0
(transitive_closure_step_l-1 nil 3315152043
("" (skolem!)
(("" (decompose-equality)
(("" (expand* "transitive_closure" "preorder_closure" "IUnion")
(("" (iff)
(("" (prop)
(("1" (skolem!)
(("1" (rewrite "iterate_add_one")
(("1" (expand "o")
(("1" (skosimp)
(("1" (inst?)
(("1" (assert) (("1" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "o")
(("2" (skosimp*)
(("2" (inst + "i!1 + 1")
(("2" (rewrite "iterate_add_one")
(("2" (expand "o")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(transitive_closure const-decl "(transitive?)" closure_ops nil)
(O const-decl "bool" relation_props nil)
(preorder? const-decl "bool" orders nil)
(preorder_closure const-decl "(preorder?)" closure_ops 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 closure_ops nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(iterate_add_one formula-decl nil relation_iterate nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(IUnion const-decl "set[T]" indexed_sets nil))
shostak))
(preorder_closure_reflexive_transitive 0
(preorder_closure_reflexive_transitive-1 nil 3315152113
("" (skolem!)
(("" (decompose-equality)
((""
(expand* "preorder_closure" "reflexive_closure"
"transitive_closure" "union" "member" "IUnion")
(("" (iff)
(("" (prop)
(("1" (skolem!)
(("1" (inst?)
(("1" (assert)
(("1" (expand "iterate") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (skolem!) (("2" (inst?) nil nil)) nil)
("3" (inst + 0)
(("3" (expand "iterate") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((reflexive_closure_preserves_transitive application-judgement
"(preorder?)" closure_ops nil)
(preorder? const-decl "bool" orders nil)
(preorder_closure const-decl "(preorder?)" closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(transitive? const-decl "bool" relations nil)
(transitive_closure const-decl "(transitive?)" closure_ops 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 closure_ops nil)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(i!1 skolem-const-decl "nat" closure_ops nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals 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)
(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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(member const-decl "bool" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(union const-decl "set" sets nil))
shostak))
(preorder_closure_transitive_reflexive 0
(preorder_closure_transitive_reflexive-1 nil 3315152170
("" (skolem!)
(("" (decompose-equality)
(("" (iff)
(("" (prop)
(("1" (rewrite "preorder_closure_reflexive_transitive")
(("1" (expand "reflexive_closure" -)
(("1" (expand* "union" "member")
(("1" (split)
(("1" (lemma "transitive_closure_is_monotone")
(("1" (inst - "R!1" "reflexive_closure(R!1)")
(("1" (split)
(("1" (expand* "subset?" "member")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil)
("2" (hide-all-but 1)
(("2"
(expand* "subset?" "reflexive_closure"
"union" "member")
(("2" (skosimp) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2"
(lemma "transitive_closure_of_reflexive"
("R" "reflexive_closure(R!1)"))
(("2" (expand* "preorder?" "reflexive?")
(("2" (flatten) (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "transitive_closure" "IUnion")
(("2" (skolem!)
(("2" (generalize-skolem-constants)
(("2" (induct "i_1")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (skosimp*)
(("3" (expand "iterate" -3)
(("3" (expand "o")
(("3" (skosimp)
(("3"
(case "preorder_closure(R!2)(x!4, y!1)")
(("1" (hide -2 -3 -4)
(("1"
(expand*
"reflexive_closure"
"union"
"member"
"preorder_closure"
"IUnion")
(("1"
(skolem!)
(("1"
(split)
(("1"
(inst + "i!2 + 1")
(("1"
(expand "iterate" +)
(("1"
(expand "o")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(splash -1)
(("1"
(inst?)
(("1" (assert) nil nil))
nil)
("2"
(assert)
(("2"
(expand "iterate")
(("2"
(expand*
"preorder_closure"
"IUnion")
(("2"
(inst + 0)
(("2"
(expand "iterate")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive_closure_of_reflexive application-judgement
"(preorder?)" closure_ops nil)
(preorder? const-decl "bool" orders nil)
(preorder_closure const-decl "(preorder?)" closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(transitive_closure const-decl "(transitive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops 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 closure_ops nil)
(subset? const-decl "bool" sets nil)
(transitive_closure_is_monotone formula-decl nil closure_ops nil)
(transitive_closure_of_reflexive judgement-tcc nil closure_ops nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" closure_ops nil)
(preorder_closure_reflexive_transitive formula-decl nil closure_ops
nil)
(nat_induction formula-decl nil naturalnumbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(O const-decl "bool" relation_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IUnion const-decl "set[T]" indexed_sets nil))
shostak))
(reflexive_closure_identity 0
(reflexive_closure_identity-1 nil 3315152617
("" (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 closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(member const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil))
shostak))
(irreflexive_kernel_identity 0
(irreflexive_kernel_identity-1 nil 3315152638
("" (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 closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(irreflexive? const-decl "bool" relations nil)
(member const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil))
shostak))
(symmetric_closure_identity 0
(symmetric_closure_identity-1 nil 3315152643
("" (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 closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(symmetric_converse application-judgement "(symmetric?[T])"
relation_converse_props nil)
(member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(pred type-eq-decl nil defined_types nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(symmetric_closure const-decl "(symmetric?)" closure_ops nil))
shostak))
(symmetric_kernel_identity 0
(symmetric_kernel_identity-1 nil 3315152648
("" (grind-with-ext :if-match all) 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 closure_ops nil)
(PRED type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(symmetric_converse application-judgement "(symmetric?[T])"
relation_converse_props nil)
(member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(pred type-eq-decl nil defined_types nil)
(intersection const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(symmetric_kernel const-decl "(symmetric?)" closure_ops nil))
shostak))
(asymmetric_kernel_identity 0
(asymmetric_kernel_identity-1 nil 3315152663
("" (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 closure_ops nil)
(pred type-eq-decl nil defined_types nil)
(asymmetric? const-decl "bool" relations_extra nil)
(irreflexive_converse application-judgement "(irreflexive?[T])"
relation_converse_props nil)
(antisymmetric_converse application-judgement "(antisymmetric?[T])"
relation_converse_props nil)
(member const-decl "bool" sets nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(asymmetric_kernel const-decl "(asymmetric?)" closure_ops nil))
shostak))
(transitive_closure_identity 0
(transitive_closure_identity-1 nil 3315152670
("" (skolem-typepred)
(("" (expand* "transitive_closure" "IUnion")
(("" (decompose-equality)
(("" (iff)
(("" (prop)
(("1"
(case "FORALL (i: posnat), (a, b: T): iterate(lessp!1, i)(a, b) IMPLIES lessp!1(a, b)")
(("1" (skolem!)
(("1" (inst - "i!1" "x!1" "x!2")
(("1" (assert) nil nil)) nil))
nil)
("2" (hide -1 2)
(("2" (induct "i")
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (skosimp*)
(("3" (expand "iterate" -3)
(("3" (expand "o")
(("3" (skosimp)
(("3" (splash -1)
(("1" (inst - "a!1" "y!1")
(("1"
(assert)
(("1"
(expand "transitive?")
(("1"
(inst - "a!1" "y!1" "b!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "iterate")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + 1) (("2" (rewrite "iterate_1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IUnion const-decl "set[T]" indexed_sets nil)
(transitive_closure const-decl "(transitive?)" closure_ops nil)
(iterate_1 formula-decl nil relation_iterate nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nat_induction formula-decl nil naturalnumbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(O const-decl "bool" relation_props nil)
(iterate def-decl "pred[[T, T]]" relation_iterate nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals 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)
(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)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(preorder_closure_identity 0
(preorder_closure_identity-1 nil 3315153008
("" (skolem!)
(("" (rewrite "preorder_closure_reflexive_transitive")
(("" (use "transitive_closure_identity")
(("" (use "reflexive_closure_identity") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((preorder_closure_reflexive_transitive formula-decl nil closure_ops
nil)
(T formal-type-decl nil closure_ops nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(preorder? const-decl "bool" orders nil)
(transitive_closure_of_reflexive application-judgement
"(preorder?)" closure_ops nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" closure_ops nil)
(reflexive_closure_identity formula-decl nil closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(transitive_closure const-decl "(transitive?)" closure_ops nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(transitive_closure_identity formula-decl nil closure_ops nil))
shostak))
(preorder_closure_reflexive 0
(preorder_closure_reflexive-1 nil 3318256600
("" (skolem-typepred)
(("" (expand "order?")
(("" (flatten)
(("" (rewrite "preorder_closure_reflexive_transitive")
(("" (rewrite "transitive_closure_identity") nil nil)) nil))
nil))
nil))
nil)
((preorder_closure_reflexive_transitive formula-decl nil closure_ops
nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" closure_ops nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(transitive_closure_identity formula-decl nil closure_ops nil)
(order? const-decl "bool" relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(equivalence_closure_identity 0
(equivalence_closure_identity-1 nil 3315153106
("" (skolem-typepred)
(("" (expand* "equivalence?" "equivalence_closure")
(("" (flatten)
(("" (use "symmetric_closure_identity")
(("" (replace -1)
(("" (use "preorder_closure_identity") nil nil)) nil))
nil))
nil))
nil))
nil)
((equivalence_closure const-decl "(equivalence?)" closure_ops nil)
(symmetric_closure_identity formula-decl nil closure_ops nil)
(symmetric? const-decl "bool" relations nil)
(preorder_closure_preserves_symmetry application-judgement
"(equivalence?)" closure_ops nil)
(pred type-eq-decl nil defined_types nil)
(preorder? const-decl "bool" orders nil)
(preorder_closure_identity formula-decl nil closure_ops nil)
(equivalence? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil closure_ops nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak)))
¤ Dauer der Verarbeitung: 0.55 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.
|
