|
(chain_chain
(chain_incl_partial_order 0
(chain_incl_partial_order-1 nil 3314727370
("" (lemma "subset_partial_order[T]") (("" (grind) nil nil)) nil)
((subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(chain_incl const-decl "bool" chain_chain 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)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(y!1 skolem-const-decl "chain[T, <=]" chain_chain nil)
(x!2 skolem-const-decl "T" chain_chain nil)
(chain nonempty-type-eq-decl nil chain nil)
(chain? const-decl "bool" chain nil)
(<= formal-const-decl "(partial_order?[T])" chain_chain nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans 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)
(restrict const-decl "R" restrict nil)
(dichotomous? const-decl "bool" orders nil)
(total_order? const-decl "bool" orders nil)
(subset_partial_order formula-decl nil sets_lemmas nil)
(T formal-type-decl nil chain_chain nil))
nil))
(chain_union_TCC1 0
(chain_union_TCC1-1 nil 3314727370
("" (typepred "<=")
(("" (grind :if-match nil)
(("" (inst -7 "a!1" "a!2")
(("" (split)
(("1" (inst - "x!1")
(("1" (assert)
(("1" (inst - "x!1" "y!1") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (inst - "y!1")
(("2" (assert)
(("2" (inst -4 "x!1" "y!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(restrict const-decl "R" restrict nil)
(dichotomous? const-decl "bool" orders nil)
(total_order? const-decl "bool" orders nil)
(chain? const-decl "bool" chain nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
restrict_order_props nil)
(preorder_restrict application-judgement "(preorder?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
restrict_order_props nil)
(set type-eq-decl nil sets nil)
(subchain nonempty-type-eq-decl nil chain_chain nil)
(chain_incl const-decl "bool" chain_chain nil)
(chain_chain nonempty-type-eq-decl nil chain_chain nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(Union const-decl "set" sets nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(chain_incl_partial_order name-judgement
"(partial_order?[subchain])" chain_chain 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 chain_chain nil)
(pred type-eq-decl nil defined_types nil)
(partial_order? const-decl "bool" orders nil)
(<= formal-const-decl "(partial_order?[T])" chain_chain nil))
nil))
(chain_union_upper_bound 0
(chain_union_upper_bound-1 nil 3314727563 ("" (grind) nil nil)
((chain_chain nonempty-type-eq-decl nil chain_chain nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(chain_incl_partial_order name-judgement
"(partial_order?[subchain])" chain_chain 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)
(restrict const-decl "R" restrict nil)
(dichotomous? const-decl "bool" orders nil)
(total_order? const-decl "bool" orders nil)
(FALSE const-decl "bool" booleans nil)
(chain_union const-decl "subchain" chain_chain nil)
(member const-decl "bool" sets nil)
(Union const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(chain_incl const-decl "bool" chain_chain nil)
(subchain nonempty-type-eq-decl nil chain_chain nil)
(chain? const-decl "bool" chain nil)
(<= formal-const-decl "(partial_order?[T])" chain_chain nil)
(partial_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types 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 chain_chain nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(extend const-decl "R" extend nil))
shostak)))
¤ Dauer der Verarbeitung: 0.28 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.
|
