|
(well_ordered_props
(induced_prefixes 0
(induced_prefixes-1 nil 3316201040
("" (typepred "<")
(("" (skosimp* t)
(("" (expand* "well_ordered?" "well_founded?")
(("" (flatten)
(("" (inst - "complement(seg!1)")
(("" (split)
(("1" (skolem-typepred)
(("1" (inst + "y!1")
(("1" (apply-extensionality 2 :hide? t)
(("1"
(expand* "prefix?" "below" "complement"
"irreflexive_kernel" "difference" "member"
"strict_total_order?" "trichotomous?")
(("1" (flatten)
(("1" (inst -4 "x!1" "y!1")
(("1" (smash)
(("1" (inst - "y!1" "x!1")
(("1" (assert) nil nil)) nil)
("2" (inst - "x!1")
(("2"
(assert)
(("2"
(expand* "complement" "member")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "complement" "member")
(("2" (inst + "t!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((initial_segment type-eq-decl nil well_ordered_props nil)
(member const-decl "bool" sets nil)
(prefix? const-decl "bool" ordered_subset nil)
(set type-eq-decl nil sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(trichotomous? const-decl "bool" orders nil)
(strict_total_order? const-decl "bool" orders nil)
(difference const-decl "set" sets nil)
(seg!1 skolem-const-decl "initial_segment" well_ordered_props nil)
(x!1 skolem-const-decl "T" well_ordered_props nil)
(order? const-decl "bool" relations_extra nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(complement const-decl "set" sets nil)
(well_founded? 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 well_ordered_props nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders nil)
(< formal-const-decl "(well_ordered?[T])" well_ordered_props nil))
shostak))
(increasing_well_ordered 0
(increasing_well_ordered-1 nil 3316201444
("" (typepred "<")
(("" (skolem-typepred)
(("" (expand* "well_ordered?" "well_founded?")
(("" (flatten)
(("" (inst - "{r | f!1(r) < r AND f!1(r) /= r}")
(("" (split)
(("1" (skosimp :preds? t)
(("1"
(expand* "increasing?" "preserves"
"irreflexive_kernel" "difference" "member")
(("1" (inst - "f!1(y!1)" "y!1")
(("1" (ground) (("1" (inst - "f!1(y!1)") nil nil))
nil))
nil))
nil))
nil)
("2" (expand* "strict_total_order?" "trichotomous?")
(("2" (flatten)
(("2" (inst - "t!1" "f!1(t!1)")
(("2" (inst + "t!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((increasing? const-decl "bool" monotone_functions nil)
(preserves const-decl "bool" functions nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(strict_total_order? const-decl "bool" orders nil)
(trichotomous? const-decl "bool" orders nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(well_founded? 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 well_ordered_props nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders nil)
(< formal-const-decl "(well_ordered?[T])" well_ordered_props nil))
shostak))
(initial_segment_isomorphism 0
(initial_segment_isomorphism-1 nil 3316201608
("" (skosimp* t)
(("" (expand* "isomorphic?" "isomorphism?" "restrict" "member")
(("" (skolem!)
(("" (use "induced_prefixes")
(("" (skolem!)
(("" (typepred "f!1(t!1)")
(("" (replace -2 -1)
(("" (expand "below" -1)
((""
(expand* "irreflexive_kernel" "difference"
"member")
(("" (flatten)
(("" (use "increasing_well_ordered")
(("1" (assert)
(("1" (typepred "<")
(("1"
(expand* "well_ordered?"
"strict_total_order?" "strict_order?"
"irreflexive?" "transitive?")
(("1"
(flatten)
(("1"
(inst - "t!1")
(("1"
(inst - "t!1" "f!1(t!1)")
(("1"
(assert)
(("1"
(replace -6 +)
(("1"
(expand "below" +)
(("1"
(expand*
"irreflexive_kernel"
"difference"
"member")
(("1"
(inst
-
"t!1"
"f!1(t!1)"
"t!2")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind)
(("1" (typepred "f!1")
(("1" (expand "bijective?")
(("1"
(flatten)
(("1"
(expand "injective?")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "f!1")
(("2" (expand "bijective?")
(("2"
(flatten)
(("2"
(expand "injective?")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (typepred "f!1")
(("3" (expand "bijective?")
(("3"
(flatten)
(("3"
(expand "injective?")
(("3"
(inst?)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("4" (typepred "f!1")
(("4" (expand "bijective?")
(("4"
(flatten)
(("4"
(expand "injective?")
(("4"
(inst?)
(("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((isomorphism? const-decl "bool" isomorphism nil)
(restrict const-decl "R" restrict nil)
(isomorphic? const-decl "bool" isomorphism nil)
(induced_prefixes formula-decl nil well_ordered_props nil)
(bijective? const-decl "bool" functions nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(preserves const-decl "bool" functions nil)
(irreflexive_kernel_of_antisymmetric application-judgement
"(asymmetric?)" well_ordered_props nil)
(order_to_strict_order application-judgement "(strict_order?)"
well_ordered_props nil)
(t!2 skolem-const-decl "T" well_ordered_props nil)
(injective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(strict_total_order? const-decl "bool" orders nil)
(irreflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(increasing? const-decl "bool" monotone_functions nil)
(seg!1 skolem-const-decl "initial_segment" well_ordered_props nil)
(f!1 skolem-const-decl "(bijective?[T, (seg!1)])"
well_ordered_props nil)
(increasing_well_ordered formula-decl nil well_ordered_props nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(difference 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 well_ordered_props nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(prefix? const-decl "bool" ordered_subset nil)
(well_ordered? const-decl "bool" orders nil)
(< formal-const-decl "(well_ordered?[T])" well_ordered_props nil)
(member const-decl "bool" sets nil)
(initial_segment type-eq-decl nil well_ordered_props nil))
shostak)))
¤ Dauer der Verarbeitung: 0.18 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.
|
