|
(partial_order_lift
(lift_TCC1 0
(lift_TCC1-1 nil 3353068079 ("" (subtype-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 partial_order_lift nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(directed_complete? const-decl "bool" directed_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(partial_order? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(/= const-decl "boolean" notequal nil))
nil))
(lift_TCC2 0
(lift_TCC2-1 nil 3353068079 ("" (subtype-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 partial_order_lift nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(directed_complete? const-decl "bool" directed_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(partial_order? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(/= const-decl "boolean" notequal nil))
nil))
(lift_TCC3 0
(lift_TCC3-1 nil 3353068079
("" (skosimp)
(("" (typepred "lesseqp!1")
(("" (expand "pointed_directed_complete_partial_order?")
(("" (split)
(("1" (expand "directed_complete_partial_order?")
(("1" (expand "partial_order?")
(("1" (expand "preorder?")
(("1" (flatten)
(("1" (split)
(("1" (expand "reflexive?")
(("1" (skosimp)
(("1" (assert)
(("1" (inst - "down[T](x!1)") nil nil)) nil))
nil))
nil)
("2" (expand "transitive?")
(("2" (skosimp*)
(("2" (assert)
(("2" (flatten)
(("2" (assert)
(("2"
(flatten)
(("2"
(inst
-
"down(x!1)"
"down(y!1)"
"down(z!1)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "antisymmetric?")
(("3" (skosimp*)
(("3" (split -1)
(("1" (assert) nil nil)
("2" (flatten)
(("2" (assert)
(("2"
(flatten)
(("2"
(inst - "down(x!1)" "down(y!1)")
(("2"
(assert)
(("2"
(lemma
"down_equal"
("y1" "x!1" "y2" "y!1"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "directed_complete?")
(("4" (skosimp)
(("4" (typepred "D!1")
(("4" (name "DD" "{x:T | D!1(up(x))}")
(("4" (case "nonempty?(DD)")
(("1"
(inst - "DD")
(("1"
(expand "least_bounded_above?")
(("1"
(skosimp)
(("1"
(inst + "up(t!1)")
(("1"
(expand "least_upper_bound?")
(("1"
(flatten)
(("1"
(split)
(("1"
(hide -9)
(("1"
(expand "upper_bound?")
(("1"
(skosimp)
(("1"
(typepred "r!1")
(("1"
(inst
-9
"down(r!1)")
(("1"
(expand "DD")
(("1"
(lemma
"up_down"
("y" "r!1"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand "upper_bound?")
(("2"
(case-replace
"r!1=bottom")
(("1"
(assert)
(("1"
(hide 1)
(("1"
(expand
"nonempty?"
-3)
(("1"
(expand
"empty?")
(("1"
(skosimp)
(("1"
(expand
"member")
(("1"
(expand
"DD")
(("1"
(inst
-
"up(x!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(inst
-10
"down(r!1)")
(("2"
(split -10)
(("1"
(propax)
nil
nil)
("2"
(skosimp)
(("2"
(typepred
"r!2")
(("2"
(expand
"DD")
(("2"
(inst
-
"up(r!2)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide 2)
(("2"
(expand "directed?")
(("2"
(skosimp)
(("2"
(expand "DD")
(("2"
(inst
-
"up(x!1)"
"up(y!1)")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst + "down(z!1)")
(("1"
(assert)
nil
nil)
("2"
(expand "DD")
(("2"
(lemma
"up_down"
("y" "z!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "nonempty?" 1)
(("2"
(expand "least_bounded_above?")
(("2"
(inst + "bottom")
(("2"
(expand "least_upper_bound?")
(("2"
(expand "upper_bound?")
(("2"
(hide -8 -4 -5 -6 -7 -2)
(("2"
(skosimp)
(("2"
(typepred "r!1")
(("2"
(expand "empty?")
(("2"
(expand "DD")
(("2"
(expand "member")
(("2"
(inst
-
"down(r!1)")
(("1"
(lemma
"up_down"
("y" "r!1"))
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "has_least?")
(("2" (expand "fullset")
(("2" (inst + "bottom")
(("2" (expand "least?")
(("2" (expand "lower_bound?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil partial_order_lift nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(partial_order? const-decl "bool" orders nil)
(directed_complete? const-decl "bool" directed_orders nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bottom adt-constructor-decl "(bottom?)" lift_adt nil)
(bottom? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(directed? const-decl "bool" directed_orders nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(z!1 skolem-const-decl "(D!1)" partial_order_lift nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "T" partial_order_lift nil)
(r!2 skolem-const-decl "(DD)" partial_order_lift nil)
(every adt-def-decl "boolean" lift_adt nil)
(PRED type-eq-decl nil defined_types nil)
(D!1 skolem-const-decl "(directed?(LAMBDA (x, y: lift[T]):
x = bottom[T] OR
(y /= bottom[T] AND lesseqp!1(down[T](x), down[T](y)))))"
partial_order_lift nil)
(r!1 skolem-const-decl "(D!1)" partial_order_lift nil)
(up_down formula-decl nil lift_props nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(lesseqp!1 skolem-const-decl
"(directed_complete_partial_order?[T])" partial_order_lift nil)
(DD skolem-const-decl "[T -> bool]" partial_order_lift nil)
(r!1 skolem-const-decl "(D!1)" partial_order_lift nil)
(up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
(antisymmetric? const-decl "bool" relations nil)
(down_equal formula-decl nil lift_props nil)
(transitive? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(lift type-decl nil lift_adt nil)
(up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
(down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
(preorder? const-decl "bool" orders nil)
(fullset const-decl "set" sets nil)
(least? const-decl "bool" minmax_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(pointed_directed_complete_partial_order? const-decl "bool"
directed_orders nil))
nil)))
¤ Dauer der Verarbeitung: 0.32 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.
|
