|
(relations_closure
(RC_TCC1 0
(RC_TCC1-1 nil 3370210023 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(reflexive? const-decl "bool" relations nil))
nil))
(change_to_RC 0
(change_to_RC-1 nil 3375182313
("" (expand* "reflexive_closure" "RC") nil nil)
((RC const-decl "reflexive" relations_closure nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops
"orders/"))
shostak))
(R_subset_RC 0
(R_subset_RC-1 nil 3371210190
("" (skeep)
(("" (expand* "subset?" "member")
(("" (skeep)
(("" (expand* "RC" "union" "member") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(RC const-decl "reflexive" relations_closure nil))
shostak))
(RC_idempotent 0
(RC_idempotent-1 nil 3370210197
("" (skeep)
(("" (lemma "reflexive_closure_identity")
(("" (inst -1 "RC(R)")
(("" (rewrite-lemma "change_to_RC" ("R" "RC(R)")) nil nil))
nil))
nil))
nil)
((T formal-type-decl nil relations_closure nil)
(reflexive_closure_identity formula-decl nil closure_ops "orders/")
(change_to_RC formula-decl nil relations_closure nil)
(RC const-decl "reflexive" relations_closure nil)
(reflexive type-eq-decl nil relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(RC_characterization 0
(RC_characterization-1 nil 3370210321
("" (skeep)
(("" (prop)
(("1" (lemma "reflexive_closure_identity")
(("1" (inst?)
(("1" (rewrite-lemma "change_to_RC" ("R" "S"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(change_to_RC formula-decl nil relations_closure nil)
(reflexive_closure_identity formula-decl nil closure_ops "orders/")
(T formal-type-decl nil relations_closure nil))
shostak))
(SC_TCC1 0
(SC_TCC1-1 nil 3370210023 ("" (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))
(change_to_SC 0
(change_to_SC-1 nil 3375182425
("" (expand* "symmetric_closure" "SC") nil nil)
((SC const-decl "symmetric" relations_closure nil)
(symmetric_closure const-decl "(symmetric?)" closure_ops
"orders/"))
shostak))
(R_subset_SC 0
(R_subset_SC-1 nil 3371210082
("" (skeep)
(("" (expand* "subset?" "member")
(("" (skeep)
(("" (expand* "SC" "union" "member") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(SC const-decl "symmetric" relations_closure nil))
shostak))
(SC_idempotent 0
(SC_idempotent-1 nil 3370210671
("" (skeep)
(("" (lemma "symmetric_closure_identity")
(("" (inst -1 "SC(R)")
(("" (rewrite-lemma "change_to_SC" ("R" "SC(R)")) nil nil))
nil))
nil))
nil)
((T formal-type-decl nil relations_closure nil)
(symmetric_closure_identity formula-decl nil closure_ops "orders/")
(change_to_SC formula-decl nil relations_closure nil)
(SC const-decl "symmetric" relations_closure nil)
(symmetric type-eq-decl nil relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(SC_characterization 0
(SC_characterization-1 nil 3370210710
("" (skeep)
(("" (prop)
(("1" (lemma "symmetric_closure_identity")
(("1" (inst?)
(("1" (rewrite-lemma "change_to_SC" ("R" "S"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(change_to_SC formula-decl nil relations_closure nil)
(symmetric_closure_identity formula-decl nil closure_ops "orders/")
(T formal-type-decl nil relations_closure nil))
shostak))
(TC_TCC1 0
(TC_TCC1-1 nil 3370210023
("" (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 relations_closure 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 "orders/")
(transitive? const-decl "bool" relations nil)
(IUnion const-decl "set[T]" indexed_sets nil))
nil))
(change_to_TC 0
(change_to_TC-1 nil 3375182475
("" (expand* "transitive_closure" "TC") nil nil)
((TC const-decl "transitive" relations_closure nil)
(transitive_closure const-decl "(transitive?)" closure_ops
"orders/"))
shostak))
(R_subset_TC 0
(R_subset_TC-1 nil 3371210276
("" (skeep)
(("" (expand* "subset?" "member")
(("" (skeep)
(("" (expand* "TC" "IUnion")
(("" (inst 1 "1") (("" (rewrite "iterate_1") nil nil)) nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(TC const-decl "transitive" relations_closure nil)
(T formal-type-decl nil relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(iterate_1 formula-decl nil relation_iterate "orders/")
(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))
shostak))
(TC_converse 0
(TC_converse-1 nil 3372708950
("" (skeep)
(("" (decompose-equality)
(("" (expand* "TC" "IUnion")
(("" (iff)
(("" (prop)
(("1" (skolem * "i")
(("1" (rewrite "iterate_converse")
(("1" (expand "converse") (("1" (inst?) nil nil)) nil))
nil))
nil)
("2" (expand "converse" -1)
(("2" (skolem * "i")
(("2" (inst?)
(("2" (rewrite "iterate_converse")
(("2" (expand "converse") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive_converse application-judgement "(transitive?[T])"
relation_converse_props nil)
(pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(transitive type-eq-decl nil relations_closure nil)
(TC const-decl "transitive" relations_closure nil)
(converse const-decl "pred[[T2, T1]]" relation_defs 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 relations_closure 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)
(iterate_converse formula-decl nil relation_iterate "orders/")
(IUnion const-decl "set[T]" indexed_sets nil))
shostak))
(TC_idempotent 0
(TC_idempotent-1 nil 3370214273
("" (skeep)
(("" (lemma "transitive_closure_identity")
(("" (inst -1 "TC(R)")
(("" (rewrite-lemma "change_to_TC" ("R" "TC(R)")) nil nil))
nil))
nil))
nil)
((T formal-type-decl nil relations_closure nil)
(transitive_closure_identity formula-decl nil closure_ops
"orders/")
(change_to_TC formula-decl nil relations_closure nil)
(TC const-decl "transitive" relations_closure nil)
(transitive type-eq-decl nil relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(TC_characterization 0
(TC_characterization-1 nil 3370211587
("" (skeep)
(("" (prop)
(("1" (lemma "transitive_closure_identity")
(("1" (inst?)
(("1" (rewrite-lemma "change_to_TC" ("R" "S"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(change_to_TC formula-decl nil relations_closure nil)
(transitive_closure_identity formula-decl nil closure_ops
"orders/")
(T formal-type-decl nil relations_closure nil))
shostak))
(RTC_TCC1 0
(RTC_TCC1-1 nil 3370210023
("" (expand "reflexive_transitive?")
(("" (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 "orders/")
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_closure 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 "orders/")
(reflexive_transitive? const-decl "bool" relations_closure nil))
nil))
(change_to_RTC 0
(change_to_RTC-1 nil 3375182493
("" (expand* "preorder_closure" "RTC") nil nil)
((RTC const-decl "reflexive_transitive" relations_closure nil)
(preorder_closure const-decl "(preorder?)" closure_ops "orders/"))
shostak))
(R_subset_RTC 0
(R_subset_RTC-1 nil 3371209765
("" (skeep)
(("" (expand* "subset?" "member")
(("" (skeep)
(("" (expand* "RTC" "IUnion")
(("" (inst 1 "1") (("" (rewrite "iterate_1") nil nil)) nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(RTC const-decl "reflexive_transitive" relations_closure nil)
(T formal-type-decl nil relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(iterate_1 formula-decl nil relation_iterate "orders/")
(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))
shostak))
(iterate_RTC 0
(iterate_RTC-1 nil 3372720815
("" (skeep)
(("" (expand* "subset?" "member" "RTC" "IUnion")
(("" (skeep) (("" (inst 1 "n") nil nil)) nil)) nil))
nil)
((member const-decl "bool" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(RTC const-decl "reflexive_transitive" relations_closure nil)
(subset? const-decl "bool" sets 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))
shostak))
(RTC_idempotent 0
(RTC_idempotent-1 nil 3370216879
("" (skeep)
(("" (lemma " preorder_closure_identity")
(("" (inst -1 "RTC(R)")
(("1" (rewrite-lemma "change_to_RTC" ("R" "RTC(R)")) nil nil)
("2" (assert)
(("2" (expand "preorder?")
(("2" (hide 2)
(("2" (typepred "RTC(R)")
(("2" (expand "reflexive_transitive?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil relations_closure nil)
(preorder_closure_identity formula-decl nil closure_ops "orders/")
(NOT const-decl "[bool -> bool]" booleans nil)
(change_to_RTC formula-decl nil relations_closure 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)
(reflexive_transitive? const-decl "bool" relations_closure nil)
(reflexive_transitive type-eq-decl nil relations_closure nil)
(RTC const-decl "reflexive_transitive" relations_closure nil)
(R skolem-const-decl "pred[[T, T]]" relations_closure nil))
shostak))
(RTC_characterization 0
(RTC_characterization-1 nil 3370216958
("" (skeep)
(("" (prop)
(("1" (lemma " preorder_closure_identity")
(("1" (inst?)
(("1" (rewrite-lemma "change_to_RTC" ("R" "S"))
(("1" (assert) nil nil)) nil)
("2" (expand* "reflexive_transitive?" "preorder?") nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
(preorder? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(change_to_RTC formula-decl nil relations_closure nil)
(reflexive_transitive? const-decl "bool" relations_closure nil)
(preorder_closure_identity formula-decl nil closure_ops "orders/")
(T formal-type-decl nil relations_closure nil))
shostak))
(EC_TCC1 0
(EC_TCC1-1 nil 3375182313
("" (skeep)
(("" (lemma "preorder_closure_preserves_symmetry")
(("" (inst -1 "SC(R)")
(("" (rewrite-lemma "change_to_RTC" ("R" "SC(R)")) nil nil))
nil))
nil))
nil)
((T formal-type-decl nil relations_closure nil)
(preorder_closure_preserves_symmetry judgement-tcc nil closure_ops
"orders/")
(change_to_RTC formula-decl nil relations_closure nil)
(SC const-decl "symmetric" relations_closure nil)
(symmetric type-eq-decl nil relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(change_to_EC 0
(change_to_EC-1 nil 3375182512
("" (skeep)
(("" (expand* "equivalence_closure" "EC")
(("" (rewrite-lemma "change_to_SC" ("R" "R"))
(("" (rewrite-lemma "change_to_RTC" ("R" "SC(R)")) nil nil))
nil))
nil))
nil)
((EC const-decl "equivalence" relations_closure nil)
(equivalence_closure const-decl "(equivalence?)" closure_ops
"orders/")
(change_to_RTC formula-decl nil relations_closure nil)
(PRED type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(symmetric type-eq-decl nil relations_closure nil)
(SC const-decl "symmetric" relations_closure 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 relations_closure nil)
(change_to_SC formula-decl nil relations_closure nil))
shostak))
(R_subset_EC 0
(R_subset_EC-1 nil 3371210430
("" (skeep)
(("" (lemma "R_subset_SC")
(("" (inst?)
(("" (expand* "subset?" "member")
(("" (skeep)
(("" (inst?)
(("" (expand "EC")
(("" (expand* "RTC" "IUnion")
(("" (inst 1 "1")
(("" (rewrite "iterate_1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((R_subset_SC formula-decl nil relations_closure nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(RTC const-decl "reflexive_transitive" relations_closure nil)
(SC const-decl "symmetric" relations_closure nil)
(symmetric type-eq-decl nil relations_closure nil)
(symmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(iterate_1 formula-decl nil relation_iterate "orders/")
(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)
(EC const-decl "equivalence" relations_closure 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 relations_closure nil))
shostak))
(RTC_subset_EC 0
(RTC_subset_EC-1 nil 3372883240
("" (skeep)
(("" (expand "EC")
(("" (lemma "R_subset_SC")
(("" (inst?)
(("" (lemma "preorder_closure_is_monotone")
(("" (inst -1 "R" "SC(R)")
(("" (rewrite-lemma "change_to_RTC" ("R" "R"))
(("" (rewrite-lemma "change_to_RTC" ("R" "SC(R)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((EC const-decl "equivalence" relations_closure nil)
(T formal-type-decl nil relations_closure nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(PRED type-eq-decl nil defined_types nil)
(symmetric? const-decl "bool" relations nil)
(symmetric type-eq-decl nil relations_closure nil)
(SC const-decl "symmetric" relations_closure nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(change_to_RTC formula-decl nil relations_closure nil)
(preorder_closure_is_monotone formula-decl nil closure_ops
"orders/")
(R_subset_SC formula-decl nil relations_closure nil))
shostak))
(EC_idempotent 0
(EC_idempotent-1 nil 3370261011
("" (skeep)
(("" (lemma "equivalence_closure_identity")
(("" (inst -1 "EC(R)")
(("" (rewrite-lemma "change_to_EC" ("R" "EC(R)")) nil nil))
nil))
nil))
nil)
((T formal-type-decl nil relations_closure nil)
(equivalence_closure_identity formula-decl nil closure_ops
"orders/")
(change_to_EC formula-decl nil relations_closure nil)
(EC const-decl "equivalence" relations_closure nil)
(equivalence type-eq-decl nil relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(equivalence? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(EC_characterization 0
(EC_characterization-1 nil 3370261180
("" (skeep)
(("" (prop)
(("1" (lemma "equivalence_closure_identity")
(("1" (inst?)
(("1" (rewrite-lemma "change_to_EC" ("R" "S"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((S skolem-const-decl "pred[[T, T]]" relations_closure nil)
(pred type-eq-decl nil defined_types nil)
(equivalence? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(change_to_EC formula-decl nil relations_closure nil)
(equivalence_closure_identity formula-decl nil closure_ops
"orders/")
(T formal-type-decl nil relations_closure nil))
shostak)))
¤ Dauer der Verarbeitung: 0.16 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.
|
