|
(bounded_order_props
(singleton_is_lub_set 0
(singleton_is_lub_set-1 nil 3330924431
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "lub_set?")
(("" (expand "singleton?")
(("" (expand "least_bounded_above?")
(("" (skosimp)
(("" (typepred "x!2")
(("" (inst + "x!2")
(("" (expand "least_upper_bound?")
(("" (split)
(("1" (expand "upper_bound?")
(("1" (skosimp)
(("1" (inst - "r!1")
(("1" (assert)
(("1"
(typepred "<=")
(("1"
(expand "partial_order?")
(("1"
(expand "preorder?")
(("1"
(flatten)
(("1"
(expand "reflexive?")
(("1"
(inst - "r!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (expand "upper_bound?")
(("2" (inst - "x!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((singleton? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(reflexive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(lub_set? const-decl "bool" bounded_order_props nil))
shostak))
(lub_TCC1 0
(lub_TCC1-1 nil 3330403776
(""
(inst +
"LAMBDA (S:(lub_set?)):epsilon!(x:T):bounded_orders[T].least_upper_bound?(x,S,<=)")
(("1" (skosimp)
(("1" (typepred "S!1")
(("1" (expand "lub_set?")
(("1" (use "epsilon_ax[T]")
(("1" (split -1)
(("1" (propax) nil nil)
("2" (expand "least_bounded_above?")
(("2" (propax) nil nil)) nil))
nil)
("2" (expand "least_bounded_above?")
(("2" (skosimp) (("2" (inst + "t!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "S!1")
(("2" (expand "lub_set?")
(("2" (expand "least_bounded_above?")
(("2" (skosimp) (("2" (inst + "t!1") nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((least_bounded_above? const-decl "bool" bounded_orders nil)
(epsilon_ax formula-decl nil epsilons nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(epsilon const-decl "T" epsilons nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(lub_set? const-decl "bool" bounded_order_props nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil bounded_order_props nil))
shostak))
(lub_rew_TCC1 0
(lub_rew_TCC1-1 nil 3353512817 ("" (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)
(set type-eq-decl nil sets nil)
(lub_set? const-decl "bool" bounded_order_props nil)
(T formal-type-decl nil bounded_order_props nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil))
nil))
(lub_rew 0
(lub_rew-1 nil 3353512818
("" (skosimp)
(("" (typepred "SA!1")
(("" (typepred "lub(SA!1)")
(("" (typepred "lub(<=)(SA!1)")
(("" (expand "least_upper_bound?")
(("" (flatten)
(("" (typepred "<=")
(("" (expand "partial_order?")
(("" (flatten)
(("" (inst - "lub(SA!1)")
(("" (inst - "lub(<=)(SA!1)")
(("" (split -4)
(("1" (split -6)
(("1" (expand "antisymmetric?")
(("1"
(inst - "lub(SA!1)" "lub(<=)(SA!1)")
(("1" (assert) nil nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lub_set? const-decl "bool" bounded_order_props nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(antisymmetric? const-decl "bool" relations nil)
(pred type-eq-decl nil defined_types nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(partial_order? const-decl "bool" orders nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(lub const-decl
"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
bounded_order_props nil))
shostak))
(lub_singleton 0
(lub_singleton-1 nil 3330924634
("" (skosimp)
(("" (typepred "lub(singleton(x!1))")
(("" (expand "least_upper_bound?")
(("" (flatten)
(("" (inst - "x!1")
(("" (expand "upper_bound?")
(("" (inst - "x!1")
(("1" (split -2)
(("1" (typepred "<=")
(("1" (expand "partial_order?")
(("1" (flatten)
(("1" (expand "antisymmetric?")
(("1" (inst - "lub(singleton(x!1))" "x!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "r!1")
(("2" (expand "singleton")
(("2" (typepred "<=")
(("2" (expand "partial_order?")
(("2" (expand "preorder?")
(("2"
(flatten)
(("2"
(expand "reflexive?")
(("2"
(inst - "r!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "singleton") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(lub const-decl
"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
bounded_order_props nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(lub_set? const-decl "bool" bounded_order_props nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(antisymmetric? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(reflexive? const-decl "bool" relations nil)
(x!1 skolem-const-decl "T" bounded_order_props nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" bounded_order_props nil))
shostak))
(lub_lem 0
(lub_lem-1 nil 3330483947
("" (skosimp)
(("" (typepred "lub(SA!1)")
(("" (case-replace "lub(SA!1)=x!1")
(("1" (assert) nil nil)
("2" (assert)
(("2" (name-replace "LUB" "lub(SA!1)")
(("2" (lemma "unique_least_upper_bound[T]")
(("2" (inst - "SA!1" "<=" "_" "_")
(("2" (inst - "LUB" "x!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lub const-decl
"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
bounded_order_props nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(lub_set? const-decl "bool" bounded_order_props nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(unique_least_upper_bound formula-decl nil bounded_orders nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(above_lub 0
(above_lub-1 nil 3330751210
("" (skosimp)
(("" (typepred "lub(YA!1)")
(("" (typepred "lub(XA!1)")
(("" (expand "least_upper_bound?")
(("" (flatten)
(("" (inst -4 "lub(XA!1)")
(("" (split -4)
(("1" (propax) nil nil)
("2" (expand "upper_bound?")
(("2" (skosimp)
(("2" (typepred "r!1")
(("2" (expand "above?")
(("2" (inst -5 "r!1")
(("2" (skosimp)
(("2" (typepred "y!1")
(("2"
(inst -3 "y!1")
(("2"
(assert)
(("2"
(typepred "<=")
(("2"
(expand "partial_order?")
(("2"
(expand "preorder?")
(("2"
(flatten)
(("2"
(expand "transitive?")
(("2"
(inst
-
"r!1"
"y!1"
"lub(XA!1)")
(("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)
((lub const-decl
"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
bounded_order_props nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(lub_set? const-decl "bool" bounded_order_props nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(above? const-decl "bool" bounded_order_props nil))
shostak))
(singleton_is_glb_set 0
(singleton_is_glb_set-1 nil 3330924431
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "singleton?")
(("" (skosimp)
(("" (expand "glb_set?")
(("" (expand "greatest_bounded_below?")
(("" (inst + "x!2")
(("" (expand "greatest_lower_bound?")
(("" (split)
(("1" (expand "lower_bound?")
(("1" (skosimp)
(("1" (typepred "<=")
(("1" (expand "partial_order?")
(("1" (expand "preorder?")
(("1"
(flatten)
(("1"
(expand "reflexive?")
(("1"
(inst - "x!2")
(("1"
(typepred "r!1")
(("1"
(inst - "r!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (expand "lower_bound?")
(("2" (inst - "x!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((singleton? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(partial_order? const-decl "bool" orders nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(preorder? const-decl "bool" orders nil)
(reflexive? const-decl "bool" relations nil)
(glb_set? const-decl "bool" bounded_order_props nil))
shostak))
(glb_TCC1 0
(glb_TCC1-1 nil 3330403776
(""
(inst +
"LAMBDA (S:(glb_set?)):epsilon!(x:T):bounded_orders[T].greatest_lower_bound?(x,S,<=)")
(("1" (skosimp)
(("1" (typepred "S!1")
(("1" (use "epsilon_ax[T]")
(("1" (split -1)
(("1" (propax) nil nil)
("2" (expand "glb_set?")
(("2" (expand "greatest_bounded_below?")
(("2" (propax) nil nil)) nil))
nil))
nil)
("2" (expand "glb_set?")
(("2" (expand "greatest_bounded_below?")
(("2" (skosimp) (("2" (inst + "t!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "S!1")
(("2" (expand "glb_set?")
(("2" (expand "greatest_bounded_below?")
(("2" (skosimp) (("2" (inst + "t!1") nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((epsilon_ax formula-decl nil epsilons nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(epsilon const-decl "T" epsilons nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(glb_set? const-decl "bool" bounded_order_props nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil bounded_order_props nil))
shostak))
(glb_rew_TCC1 0
(glb_rew_TCC1-1 nil 3353512817 ("" (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)
(set type-eq-decl nil sets nil)
(glb_set? const-decl "bool" bounded_order_props nil)
(T formal-type-decl nil bounded_order_props nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil))
nil))
(glb_rew 0
(glb_rew-1 nil 3353512945
("" (skosimp)
(("" (typepred "SB!1")
(("" (typepred "glb(<=)(SB!1)")
(("" (typepred "glb(SB!1)")
(("" (typepred "<=")
(("" (expand "partial_order?")
(("" (expand "greatest_lower_bound?")
(("" (flatten)
(("" (inst - "glb(<=)(SB!1)")
(("" (inst - "glb(SB!1)")
(("" (split -4)
(("1" (split -6)
(("1" (expand "antisymmetric?")
(("1" (inst - "glb(SB!1)" "glb(<=)(SB!1)")
(("1" (assert) nil nil)) nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((glb_set? const-decl "bool" bounded_order_props nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(glb const-decl
"{x | bounded_orders[T].greatest_lower_bound?(x, SB, <=)}"
bounded_order_props nil)
(antisymmetric? const-decl "bool" relations nil)
(pred type-eq-decl nil defined_types nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(partial_order? const-decl "bool" orders nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil))
shostak))
(glb_singleton 0
(glb_singleton-1 nil 3330924838
("" (skosimp)
(("" (typepred "glb(singleton(x!1))")
(("" (expand "greatest_lower_bound?")
(("" (flatten)
(("" (expand "lower_bound?")
(("" (case "singleton(x!1)(x!1)")
(("1" (inst - "x!1")
(("1" (inst - "x!1")
(("1" (split -3)
(("1" (typepred "<=")
(("1" (expand "partial_order?")
(("1" (flatten)
(("1" (expand "antisymmetric?")
(("1" (inst - "glb(singleton(x!1))" "x!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "r!1")
(("2" (expand "singleton")
(("2" (typepred "<=")
(("2" (expand "partial_order?")
(("2"
(expand "preorder?")
(("2"
(flatten)
(("2"
(expand "reflexive?")
(("2"
(inst - "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "singleton") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(glb const-decl
"{x | bounded_orders[T].greatest_lower_bound?(x, SB, <=)}"
bounded_order_props nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(glb_set? const-decl "bool" bounded_order_props nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(reflexive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(x!1 skolem-const-decl "T" bounded_order_props nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" bounded_order_props nil)
(lower_bound? const-decl "bool" bounded_orders nil))
shostak))
(glb_lem 0
(glb_lem-1 nil 3330484050
("" (skosimp)
(("" (typepred "glb(SB!1)")
(("" (case-replace "glb(SB!1) = x!1")
(("1" (assert) nil nil)
("2" (assert)
(("2"
(lemma "unique_greatest_lower_bound"
("<=" "<=" "S" "SB!1" "t" "glb(SB!1)" "r" "x!1"))
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((glb const-decl
"{x | bounded_orders[T].greatest_lower_bound?(x, SB, <=)}"
bounded_order_props nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(glb_set? const-decl "bool" bounded_order_props nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(unique_greatest_lower_bound formula-decl nil bounded_orders nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(below_glb 0
(below_glb-1 nil 3330750355
("" (skosimp)
(("" (typepred "glb(XB!1)")
(("" (typepred "glb(YB!1)")
(("" (expand "greatest_lower_bound?")
(("" (flatten)
(("" (inst - "glb(XB!1)")
(("" (split -2)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (expand "lower_bound?")
(("2" (skosimp)
(("2" (typepred "r!1")
(("2" (expand "below?")
(("2" (inst -5 "r!1")
(("2" (skosimp)
(("2"
(inst -3 "y!1")
(("2"
(typepred "<=")
(("2"
(expand "partial_order?")
(("2"
(expand "preorder?")
(("2"
(flatten)
(("2"
(expand "transitive?")
(("2"
(inst
-
"glb(XB!1)"
"y!1"
"r!1")
(("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)
((glb const-decl
"{x | bounded_orders[T].greatest_lower_bound?(x, SB, <=)}"
bounded_order_props nil)
(<= formal-const-decl "(partial_order?[T])" bounded_order_props
nil)
(partial_order? const-decl "bool" orders nil)
(glb_set? const-decl "bool" bounded_order_props nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil bounded_order_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(below? const-decl "bool" bounded_order_props nil)
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(lower_bound? const-decl "bool" bounded_orders nil))
shostak)))
¤ Dauer der Verarbeitung: 0.31 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.
|
