|
(directed_orders
(directed_def 0
(directed_def-1 nil 3348332767
("" (skosimp)
((""
(case "FORALL (X:set[T],n:nat):
is_finite(X) AND card(X) = n AND subset?(X, D!1) IMPLIES
(EXISTS (x: (D!1)):
bounded_orders.upper_bound?(x, X, lesseqp!1))")
(("1" (skosimp)
(("1" (inst - "X!1" "card(X!1)") (("1" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (skosimp)
(("1" (typepred "D!1")
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (skosimp)
(("1" (expand "member")
(("1" (inst + "x!1")
(("1" (expand "upper_bound?")
(("1" (skosimp)
(("1" (typepred "r!1")
(("1"
(rewrite "card_is_0")
(("1"
(replace -5)
(("1"
(expand "emptyset")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lemma "nonempty_card" ("S" "X!1"))
(("2" (assert)
(("2" (inst - "rest(X!1)")
(("2" (lemma "rest_subset" ("a" "X!1"))
(("2" (lemma "card_rest" ("S" "X!1"))
(("2" (split -1)
(("1" (replace -6)
(("1" (replace -1)
(("1" (hide -1 -6)
(("1"
(lemma "finite_rest" ("A" "X!1"))
(("1"
(lemma
"subset_transitive"
("a"
"rest(X!1)"
"b"
"X!1"
"c"
"D!1"))
(("1"
(assert)
(("1"
(skosimp)
(("1"
(typepred "x!1")
(("1"
(hide -2 -3 -4 -7)
(("1"
(lemma
"choose_rest"
("a" "X!1"))
(("1"
(split -1)
(("1"
(expand "upper_bound?")
(("1"
(typepred "D!1")
(("1"
(expand
"directed?")
(("1"
(inst
-
"x!1"
"_")
(("1"
(assert)
(("1"
(inst
-
"choose(X!1)")
(("1"
(split -2)
(("1"
(skosimp)
(("1"
(inst
+
"z!1")
(("1"
(skosimp)
(("1"
(typepred
"r!1")
(("1"
(replace
-5
-1
rl)
(("1"
(expand
"add")
(("1"
(split
-1)
(("1"
(replace
-1)
(("1"
(propax)
nil
nil))
nil)
("2"
(expand
"member")
(("2"
(inst
-8
"r!1")
(("2"
(typepred
"lesseqp!1")
(("2"
(expand
"partial_order?")
(("2"
(expand
"preorder?")
(("2"
(flatten)
(("2"
(expand
"transitive?")
(("2"
(inst
-
"r!1"
"x!1"
"z!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"subset?")
(("2"
(expand
"member")
(("2"
(inst
-6
"choose(X!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((upper_bound? const-decl "bool" bounded_orders nil)
(directed? const-decl "bool" directed_orders nil)
(partial_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(is_finite const-decl "bool" finite_sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers 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 directed_orders nil)
(X!1 skolem-const-decl "set[T]" directed_orders nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(nat_induction formula-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" directed_orders
nil)
(card_is_0 formula-decl nil finite_sets nil)
(x!1 skolem-const-decl "T" directed_orders nil)
(D!1 skolem-const-decl "(directed?(lesseqp!1))" directed_orders
nil)
(lesseqp!1 skolem-const-decl "(partial_order?[T])" directed_orders
nil)
(nonempty_card formula-decl nil finite_sets nil)
(rest const-decl "set" sets nil)
(card_rest formula-decl nil finite_sets nil)
(subset_transitive formula-decl nil sets_lemmas nil)
(choose const-decl "(p)" sets nil)
(X!1 skolem-const-decl "set[T]" directed_orders nil)
(r!1 skolem-const-decl "(X!1)" directed_orders nil)
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(add const-decl "(nonempty?)" sets nil)
(choose_rest formula-decl nil sets_lemmas nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(finite_rest judgement-tcc nil finite_sets nil)
(rest_subset formula-decl nil sets_lemmas nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(directed_least_bounded_above 0
(directed_least_bounded_above-1 nil 3347297982
("" (skosimp)
(("" (typepred "lesseqp!1")
(("" (expand "directed_complete_partial_order?")
(("" (flatten)
(("" (expand "directed_complete?")
(("" (inst - "D!1") 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 directed_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(partial_order? const-decl "bool" orders nil)
(directed? const-decl "bool" directed_orders nil)
(directed_complete? const-decl "bool" directed_orders nil))
shostak))
(dcpo_is_po 0
(dcpo_is_po-1 nil 3347297970 ("" (judgement-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 directed_orders nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
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)
(directed_complete? const-decl "bool" directed_orders nil)
(reflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil))
nil))
(complete_upper_semilattice_is_dcpo 0
(complete_upper_semilattice_is_dcpo-1 nil 3347299395
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "complete_upper_semilattice?")
(("" (expand "directed_complete_partial_order?")
(("" (flatten)
(("" (assert)
(("" (expand "directed_complete?")
(("" (skosimp) (("" (inst - "D!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((complete_upper_semilattice? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil directed_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(directed? const-decl "bool" directed_orders nil)
(partial_order? const-decl "bool" orders nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(directed_complete? const-decl "bool" directed_orders nil))
nil))
(pdcpo_is_dcpo 0
(pdcpo_is_dcpo-1 nil 3347297970 ("" (judgement-tcc) nil nil)
((pointed_directed_complete_partial_order? const-decl "bool"
directed_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)
(fullset const-decl "set" sets nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(reflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(T formal-type-decl nil directed_orders 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)
(directed_complete? const-decl "bool" directed_orders nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil))
nil))
(pdcpo_is_ccpo 0
(pdcpo_is_ccpo-1 nil 3347773705
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "pointed_directed_complete_partial_order?")
(("" (expand "directed_complete_partial_order?")
(("" (flatten)
(("" (expand "chain_complete_partial_order?")
(("" (assert)
(("" (expand "chain_complete?")
(("" (skosimp)
(("" (expand "directed_complete?")
(("" (case "empty?(C!1)")
(("1" (rewrite "emptyset_is_empty?")
(("1" (replace -1)
(("1" (expand "least_bounded_above?")
(("1"
(expand "has_least?")
(("1"
(skosimp)
(("1"
(expand "least?")
(("1"
(flatten)
(("1"
(expand "lower_bound?")
(("1"
(inst + "t!1")
(("1"
(expand
"least_upper_bound?")
(("1"
(split 1)
(("1"
(expand "upper_bound?")
(("1"
(skosimp)
(("1"
(typepred "r!1")
(("1"
(expand
"emptyset")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(inst -6 "r!1")
(("2"
(expand "fullset")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst - "C!1")
(("2" (split 1)
(("1" (expand "nonempty?")
(("1" (propax) nil nil)) nil)
("2" (typepred "C!1")
(("2"
(expand "directed?")
(("2"
(expand "chain?")
(("2"
(expand "total_order?")
(("2"
(expand "dichotomous?")
(("2"
(expand "restrict")
(("2"
(skosimp)
(("2"
(inst - "x!2" "y!1")
(("2"
(split -1)
(("1"
(inst + "y!1")
(("1"
(expand
"partial_order?")
(("1"
(expand
"preorder?")
(("1"
(flatten)
(("1"
(expand
"reflexive?")
(("1"
(inst
-
"y!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "x!2")
(("2"
(expand
"partial_order?")
(("2"
(expand
"preorder?")
(("2"
(flatten)
(("2"
(expand
"reflexive?")
(("2"
(inst
-
"x!2")
(("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))
nil))
nil))
nil))
nil))
nil))
nil)
((pointed_directed_complete_partial_order? const-decl "bool"
directed_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil directed_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(chain_complete_partial_order? const-decl "bool" directed_orders
nil)
(chain_complete? const-decl "bool" directed_orders nil)
(directed_complete? const-decl "bool" directed_orders nil)
(directed? const-decl "bool" directed_orders nil)
(partial_order? const-decl "bool" orders nil)
(nonempty? const-decl "bool" sets nil)
(C!1 skolem-const-decl "(chain?[T, x!1])" directed_orders nil)
(x!1 skolem-const-decl "(pointed_directed_complete_partial_order?)"
directed_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(dichotomous? const-decl "bool" orders nil)
(reflexive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(y!1 skolem-const-decl "T" directed_orders nil)
(x!2 skolem-const-decl "T" directed_orders nil)
(restrict const-decl "R" restrict nil)
(total_order? const-decl "bool" orders nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(preorder_restrict application-judgement "(preorder?[S])"
restrict_order_props nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
restrict_order_props nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(finite_emptyset name-judgement "finite_set[T]" directed_orders
nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(emptyset const-decl "set" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(fullset const-decl "set" sets nil)
(r!1 skolem-const-decl "T" directed_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(chain? const-decl "bool" chain nil)
(empty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil))
nil)))
¤ Dauer der Verarbeitung: 0.41 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.
|
