|
(well_ordered_traversal
(well_ordering_has_first 0
(well_ordering_has_first-1 nil 3318619967
("" (grind :if-match nil)
(("" (inst -4 "fullset[T]")
(("" (split)
(("1" (skolem!)
(("1" (inst + "y!1")
(("1" (skosimp)
(("1" (inst - "r!1")
(("1" (inst - "r!1" "y!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset") (("2" (inst + "t!1") nil nil)) nil))
nil))
nil))
nil)
((set type-eq-decl nil sets nil)
(irreflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(trichotomous? const-decl "bool" orders nil)
(strict_total_order? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(has_least? const-decl "bool" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(T formal-type-decl nil well_ordered_traversal nil)
(has_first? const-decl "bool" well_ordered_traversal nil))
shostak))
(first_TCC1 0
(first_TCC1-1 nil 3318619947
("" (skolem-typepred)
(("" (forward-chain "well_ordering_has_first") nil nil)) nil)
((well_ordering_has_first formula-decl nil well_ordered_traversal
nil)
(has_first? const-decl "bool" well_ordered_traversal nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil well_ordered_traversal nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(last_TCC1 0
(last_TCC1-1 nil 3318619947 ("" (subtype-tcc) nil nil)
((has_last? const-decl "bool" well_ordered_traversal nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(irreflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(trichotomous? const-decl "bool" orders nil)
(strict_total_order? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil)
(linear_order_to_total_order application-judgement "(total_order?)"
well_ordered_traversal nil)
(T formal-type-decl nil well_ordered_traversal nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(greatest? const-decl "bool" minmax_orders nil)
(has_greatest? const-decl "bool" minmax_orders nil))
nil))
(well_ordering_has_next 0
(well_ordering_has_next-1 nil 3318620127
("" (grind :if-match nil)
(("" (inst -4 "above(t!1, lessp!1)")
(("" (split)
(("1" (skolem-typepred)
(("1" (assert)
(("1" (flatten)
(("1" (inst + "y!1")
(("1" (assert)
(("1" (skosimp :preds? t)
(("1" (inst - "r!1")
(("1" (inst - "y!1" "r!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst 3 "x!1")
(("2" (assert)
(("2" (skosimp :preds? t)
(("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((suffix? const-decl "bool" ordered_subset nil)
(set type-eq-decl nil sets nil)
(order? const-decl "bool" relations_extra nil)
(irreflexive_kernel_of_antisymmetric application-judgement
"(asymmetric?)" well_ordered_traversal nil)
(order_to_strict_order application-judgement "(strict_order?)"
well_ordered_traversal nil)
(irreflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(trichotomous? const-decl "bool" orders nil)
(strict_total_order? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(has_least? const-decl "bool" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(union const-decl "set" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(has_next? const-decl "bool" well_ordered_traversal nil)
(nonempty? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" 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 well_ordered_traversal nil))
shostak))
(next_TCC1 0
(next_TCC1-1 nil 3318619947
("" (skolem-typepred)
(("" (forward-chain "well_ordering_has_next") nil nil)) nil)
((well_ordering_has_next formula-decl nil well_ordered_traversal
nil)
(has_next? const-decl "bool" well_ordered_traversal nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil well_ordered_traversal nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(last_no_next 0
(last_no_next-1 nil 3318620416
(""
(expand* "has_last?" "has_next?" "has_greatest?" "greatest?"
"fullset" "upper_bound?" "nonempty?" "empty?" "above"
"reflexive_closure" "union" "irreflexive_kernel" "difference"
"member")
(("" (skosimp* t)
(("" (inst - "last(lessp!1)")
(("" (typepred "last(lessp!1)")
((""
(expand* "greatest?" "fullset" "upper_bound?"
"reflexive_closure" "union" "member")
(("" (inst - "x!1")
(("" (assert)
((""
(expand* "well_ordered?" "strict_total_order?"
"strict_order?" "irreflexive?" "transitive?")
(("" (flatten)
(("" (inst - "x!1")
(("" (inst - "x!1" "last(lessp!1)" "x!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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 well_ordered_traversal nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders 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)
(TRUE const-decl "bool" booleans nil)
(set type-eq-decl nil sets nil)
(PRED type-eq-decl nil defined_types nil)
(reflexive? const-decl "bool" relations nil)
(last const-decl
"(LAMBDA (t: T): greatest?(t, fullset[T], reflexive_closure(<)))"
well_ordered_traversal nil)
(has_last? const-decl "bool" well_ordered_traversal nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(fullset const-decl "set" sets nil)
(nonempty? const-decl "bool" sets nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(union const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(empty? const-decl "bool" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(greatest? const-decl "bool" minmax_orders nil)
(has_next? const-decl "bool" well_ordered_traversal nil))
shostak))
(last_is_last 0
(last_is_last-1 nil 3318620611
("" (skosimp :preds? t)
(("" (typepred "last(lessp!1)")
(("" (grind :if-match nil)
(("" (inst - "x!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((last const-decl
"(LAMBDA (t: T): greatest?(t, fullset[T], reflexive_closure(<)))"
well_ordered_traversal nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(fullset const-decl "set" sets nil)
(has_last? const-decl "bool" well_ordered_traversal nil)
(greatest? const-decl "bool" minmax_orders nil)
(set type-eq-decl nil sets nil)
(linear_order_to_total_order application-judgement "(total_order?)"
well_ordered_traversal nil)
(full? const-decl "bool" sets nil)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(well_founded? const-decl "bool" orders nil)
(strict_total_order? const-decl "bool" orders nil)
(trichotomous? const-decl "bool" orders nil)
(strict_order? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(irreflexive? const-decl "bool" relations nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(union const-decl "set" sets nil)
(member 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 well_ordered_traversal nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders nil))
shostak))
(well_ordering_has_prev 0
(well_ordering_has_prev-1 nil 3318620643
("" (skosimp :preds? t)
(("" (expand "has_prev?")
(("" (skolem-typepred)
(("" (typepred "next(lessp!1)(r!1)")
(("" (replace -4)
(("" (grind :if-match nil)
(("" (inst + "r!1")
(("" (assert)
(("" (skosimp :preds? t)
(("" (assert)
(("" (flatten)
(("" (inst - "r!2" "r!1")
(("" (assert)
(("" (inst - "r!2")
((""
(inst - "r!2")
((""
(inst - "r!2" "t!1" "r!2")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((has_prev? const-decl "bool" well_ordered_traversal nil)
(next const-decl
"(LAMBDA (t_1: T): least?(t_1, above(t, <), reflexive_closure(<)))"
well_ordered_traversal nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(reflexive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(suffix? const-decl "bool" ordered_subset nil)
(order? const-decl "bool" relations_extra nil)
(least? const-decl "bool" minmax_orders nil)
(set type-eq-decl nil sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(union const-decl "set" sets nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(irreflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(strict_order? const-decl "bool" orders nil)
(trichotomous? const-decl "bool" orders nil)
(strict_total_order? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(greatest? const-decl "bool" minmax_orders nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(linear_order_to_total_order application-judgement "(total_order?)"
well_ordered_traversal nil)
(irreflexive_kernel_of_antisymmetric application-judgement
"(asymmetric?)" well_ordered_traversal nil)
(order_to_strict_order application-judgement "(strict_order?)"
well_ordered_traversal nil)
(prefix? const-decl "bool" ordered_subset nil)
(has_next? const-decl "bool" well_ordered_traversal 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_traversal nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders nil))
shostak))
(prev_TCC1 0
(prev_TCC1-1 nil 3318619947
("" (skolem-typepred)
(("" (forward-chain "well_ordering_has_prev") nil nil)) nil)
((well_ordering_has_prev formula-decl nil well_ordered_traversal
nil)
(has_prev? const-decl "bool" well_ordered_traversal nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil well_ordered_traversal nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil)))
¤ Dauer der Verarbeitung: 0.40 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.
|
