|
(relations_extra
(strict_order_is_asymmetric 0
(strict_order_is_asymmetric-1 nil 3308139199
("" (skosimp* t)
(("" (expand "strict_order?")
(("" (flatten)
(("" (expand "asymmetric?")
(("" (skosimp*)
(("" (expand "transitive?")
(("" (inst - "x!2" "y!1" "x!2")
(("" (assert)
(("" (expand "irreflexive?") (("" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((asymmetric? const-decl "bool" relations_extra nil)
(transitive? const-decl "bool" relations nil)
(irreflexive? const-decl "bool" relations 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 relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(strict_order? const-decl "bool" orders nil))
shostak))
(asymmetric_is_antisymmetric 0
(asymmetric_is_antisymmetric-1 nil 3308139286
("" (skosimp* t)
(("" (expand "asymmetric?")
(("" (expand "antisymmetric?")
(("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((antisymmetric? const-decl "bool" relations 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 relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(asymmetric? const-decl "bool" relations_extra nil))
shostak))
(asymmetric_is_irreflexive 0
(asymmetric_is_irreflexive-1 nil 3308139358
("" (skosimp* t)
(("" (expand "irreflexive?")
(("" (expand "asymmetric?")
(("" (skosimp*) (("" (inst?) (("" (prop) nil nil)) nil)) nil))
nil))
nil))
nil)
((irreflexive? const-decl "bool" relations 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 relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(asymmetric? const-decl "bool" relations_extra nil))
shostak))
(reflexive 0
(reflexive-3 nil 3308138472
("" (skolem-typepred)
(("" (expand "reflexive?") (("" (propax) nil nil)) nil)) nil)
((reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra 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-2 nil 3308137563
("" (skosimp* t)
(("" (auto-rewrite-defs) (("" (assert) (("" (inst?) nil nil)) nil))
nil))
nil)
nil nil)
(reflexive-1 nil 3308137369 ("" (grind) nil nil) nil shostak))
(irreflexive 0
(irreflexive-3 nil 3308138470
("" (skolem-typepred)
(("" (expand "irreflexive?") (("" (propax) nil nil)) nil)) nil)
((irreflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra 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-2 nil 3308137556
("" (skosimp* t)
(("" (auto-rewrite-defs) (("" (assert) (("" (inst?) nil nil)) nil))
nil))
nil)
nil nil)
(irreflexive-1 nil 3308137450 ("" (grind) nil nil) nil nil))
(symmetric 0
(symmetric-2 nil 3308138467
("" (skolem-typepred)
(("" (expand "symmetric?") (("" (propax) nil nil)) nil)) nil)
((symmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil)
(symmetric-1 nil 3308137453
("" (skosimp* t)
(("" (auto-rewrite-defs)
(("" (assert)
(("" (inst - "x!1" "y!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
nil nil))
(antisymmetric 0
(antisymmetric-2 nil 3308138464
("" (skolem-typepred)
(("" (expand "antisymmetric?") (("" (propax) nil nil)) nil)) nil)
((antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil)
(antisymmetric-1 nil 3308137572
("" (skosimp* t)
(("" (auto-rewrite-defs)
(("" (assert) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
nil nil))
(asymmetric 0
(asymmetric-1 nil 3308139089
("" (skolem-typepred)
(("" (expand "asymmetric?") (("" (propax) nil nil)) nil)) nil)
((asymmetric? const-decl "bool" relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(transitive 0
(transitive-2 nil 3308138460
("" (skolem-typepred)
(("" (expand "transitive?") (("" (propax) nil nil)) nil)) nil)
((transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra 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-1 nil 3308137577
("" (skosimp* t)
(("" (auto-rewrite-defs)
(("" (assert)
(("" (inst - "x!1" "y!1" "z!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
nil nil))
(dichotomous 0
(dichotomous-2 nil 3308138452
("" (skolem-typepred)
(("" (expand "dichotomous?") (("" (propax) nil nil)) nil)) nil)
((dichotomous? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil)
(dichotomous-1 nil 3308137580
("" (skosimp* t)
(("" (auto-rewrite-defs)
(("" (assert) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
nil nil))
(trichotomous 0
(trichotomous-2 nil 3308138441
("" (skolem-typepred)
(("" (expand "trichotomous?") (("" (propax) nil nil)) nil)) nil)
((trichotomous? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil)
(trichotomous-1 nil 3308137584
("" (skosimp* t)
(("" (auto-rewrite-defs)
(("" (assert) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
nil nil))
(dichotomous_is_trichotomous 0
(dichotomous_is_trichotomous-1 nil 3308166081
("" (skosimp* t)
(("" (expand* "trichotomous?" "dichotomous?")
(("" (skosimp*) (("" (inst?) (("" (prop) nil nil)) nil)) nil))
nil))
nil)
((trichotomous? const-decl "bool" orders 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 relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(dichotomous? const-decl "bool" orders nil))
shostak))
(well_founded 0
(well_founded-1 nil 3308138322
("" (skolem-typepred)
(("" (expand "well_founded?") (("" (propax) nil nil)) nil)) nil)
((well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil relations_extra nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(reflexive_closure_TCC1 0
(reflexive_closure_TCC1-1 nil 3308173829 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(reflexive? const-decl "bool" relations nil))
shostak))
(irreflexive_kernel_TCC1 0
(irreflexive_kernel_TCC1-1 nil 3308173829 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(irreflexive? const-decl "bool" relations nil))
shostak))
(symmetric_closure_TCC1 0
(symmetric_closure_TCC1-1 nil 3308173829 ("" (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))
shostak))
(symmetric_kernel_TCC1 0
(symmetric_kernel_TCC1-1 nil 3308173829 ("" (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))
shostak))
(reflexive_closure_preserves_transitive 0
(reflexive_closure_preserves_transitive-1 nil 3308174613
("" (skosimp* t)
((""
(expand* "preorder?" "transitive?" "reflexive_closure" "union"
"member")
(("" (skosimp*)
(("" (inst - "x!1" "y!1" "z!1")
(("" (assert) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" relations_extra nil)
(preorder? const-decl "bool" orders 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 relations_extra nil)
(PRED type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil))
shostak))
(strict_order_to_partial_order 0
(strict_order_to_partial_order-1 nil 3308174139
("" (skosimp* t)
(("" (expand* "partial_order?" "preorder?")
((""
(expand* "antisymmetric?" "reflexive_closure" "union" "member")
(("" (skosimp*)
(("" (assert)
(("" (use "asymmetric") (("" (prop) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((reflexive_closure_preserves_transitive application-judgement
"(preorder?)" relations_extra nil)
(partial_order? const-decl "bool" orders nil)
(asymmetric formula-decl nil relations_extra nil)
(asymmetric? const-decl "bool" relations_extra nil)
(antisymmetric? const-decl "bool" relations nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" relations_extra 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 relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(strict_order? const-decl "bool" orders nil))
shostak))
(reflexive_closure_dichotomous 0
(reflexive_closure_dichotomous-1 nil 3308223765
("" (skosimp*)
(("" (expand* "dichotomous?" "reflexive_closure" "union" "member")
(("" (skosimp*)
(("" (use "trichotomous") (("" (prop) nil nil)) nil)) nil))
nil))
nil)
((reflexive_closure const-decl "(reflexive?)" relations_extra nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(dichotomous? const-decl "bool" orders nil)
(trichotomous formula-decl nil relations_extra nil)
(trichotomous? 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)
(T formal-type-decl nil relations_extra nil))
nil))
(strict_total_order_to_total_order 0
(strict_total_order_to_total_order-1 nil 3308223200
("" (skosimp*)
(("" (expand "total_order?") (("" (propax) nil nil)) nil)) nil)
((reflexive_closure_dichotomous application-judgement
"(dichotomous?)" relations_extra nil)
(strict_order_to_partial_order application-judgement
"(partial_order?)" relations_extra nil)
(total_order? const-decl "bool" orders nil))
shostak))
(partial_order_to_strict_order 0
(partial_order_to_strict_order-1 nil 3308174139
("" (skosimp* t)
((""
(expand* "strict_order?" "transitive?" "irreflexive_kernel"
"difference" "member")
(("" (skosimp*)
(("" (lemma "transitive")
(("" (assert)
(("" (inst - "R!1" "x!1" "y!1" "z!1")
(("" (assert)
(("" (replace -5 :hide? t)
(("" (lemma "antisymmetric")
(("" (inst - "R!1" "z!1" "y!1")
(("" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive? const-decl "bool" relations nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" relations_extra
nil)
(strict_order? const-decl "bool" orders nil)
(transitive formula-decl nil relations_extra nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(antisymmetric formula-decl nil relations_extra 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 relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(partial_order? const-decl "bool" orders nil))
shostak))
(irreflexive_kernel_trichotomous 0
(irreflexive_kernel_trichotomous-1 nil 3308223871
("" (skosimp*)
((""
(expand* "trichotomous?" "irreflexive_kernel" "difference"
"member")
(("" (skosimp*)
(("" (assert)
(("" (use "dichotomous") (("" (prop) nil nil)) nil)) nil))
nil))
nil))
nil)
((irreflexive_kernel const-decl "(irreflexive?)" relations_extra
nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(trichotomous? const-decl "bool" orders nil)
(T formal-type-decl nil relations_extra nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(dichotomous? const-decl "bool" orders nil)
(dichotomous formula-decl nil relations_extra nil))
nil))
(total_order_to_strict_total_order 0
(total_order_to_strict_total_order-1 nil 3308223398
("" (skosimp*)
(("" (expand "strict_total_order?") (("" (propax) nil nil)) nil))
nil)
((irreflexive_kernel_trichotomous application-judgement
"(trichotomous?)" relations_extra nil)
(partial_order_to_strict_order application-judgement
"(strict_order?)" relations_extra nil)
(strict_total_order? const-decl "bool" orders nil))
shostak))
(symmetric_kernel_of_preorder 0
(symmetric_kernel_of_preorder-1 nil 3308174139
("" (skosimp* t)
(("" (expand "equivalence?")
(("" (prop)
(("1"
(expand* "reflexive?" "symmetric_kernel" "intersection"
"converse" "member")
(("1" (skosimp*)
(("1" (use "reflexive") (("1" (prop) nil nil)) nil)) nil))
nil)
("2"
(expand* "transitive?" "symmetric_kernel" "intersection"
"converse" "member")
(("2" (skosimp*)
(("2" (lemma "transitive")
(("2" (inst-cp - "R!1" "x!1" "y!1" "z!1")
(("2" (inst - "R!1" "z!1" "y!1" "x!1")
(("2" (prop) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((equivalence? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(transitive formula-decl nil relations_extra nil)
(symmetric_kernel const-decl "(symmetric?)" relations_extra nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(reflexive? const-decl "bool" relations nil)
(reflexive formula-decl nil relations_extra nil)
(PRED type-eq-decl nil defined_types 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 relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(preorder? const-decl "bool" orders 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.
|
