|
(set_dichotomous
(injection_order_TCC1 0
(injection_order_TCC1-1 nil 3315051270 ("" (subtype-tcc) nil nil)
((subset_injection type-eq-decl nil set_dichotomous nil)
(injective? const-decl "bool" functions nil)
(R formal-type-decl nil set_dichotomous nil)
(set type-eq-decl nil sets nil)
(D formal-type-decl nil set_dichotomous nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(partial_injection_order 0
(partial_injection_order-1 nil 3315051270
("" (grind-with-ext) nil nil)
((D formal-type-decl nil set_dichotomous nil)
(set type-eq-decl nil sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(R formal-type-decl nil set_dichotomous nil)
(injective? const-decl "bool" functions nil)
(subset_injection type-eq-decl nil set_dichotomous nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(injection_order const-decl "bool" set_dichotomous 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))
(injective_or_surjective 0
(injective_or_surjective-1 nil 3315051333
("" (flatten)
(("" (lemma "zorn")
(("" (split)
(("1" (skolem!)
(("1" (expand* "maximal?" "fullset")
(("1" (case "full?(t!1`1)")
(("1" (inst 2 "t!1`2")
(("1" (typepred "t!1`2")
(("1" (expand* "full?" "member" "injective?")
(("1" (skosimp)
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (expand* "full?" "member") nil nil))
nil)
("2"
(inst 4
"extend[D, (t!1`1), R, epsilon(fullset[R])](t!1`2)")
(("1" (expand* "surjective?" "full?" "member")
(("1" (skosimp*)
(("1"
(inst +
"(add(x!1, t!1`1), LAMBDA (a: (add(x!1, t!1`1))): IF a = x!1 THEN y!1 ELSE t!1`2(a) ENDIF)")
(("1" (split)
(("1" (expand "injection_order")
(("1" (split)
(("1" (use "subset_add[D]") nil nil)
("2" (skolem!)
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2" (beta)
(("2" (expand* "add" "member") nil nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset") (("2" (propax) nil nil))
nil)
("3" (typepred "t!1`2")
(("3" (expand "injective?")
(("3" (skosimp :preds? t)
(("3"
(expand* "add" "member" "extend"
"fullset")
(("3"
(delete 5)
(("3"
(lift-if)
(("3"
(lift-if)
(("3"
(ground)
(("1"
(inst 5 "x2!1")
(("1" (assert) nil nil))
nil)
("2"
(inst 5 "x1!1")
(("2" (assert) nil nil))
nil)
("3"
(inst - "x1!1" "x2!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (skosimp :preds? t)
(("4" (expand* "add" "member")
(("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (split)
(("1" (expand* "full?" "member")
(("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil)
("2" (skolem!) (("2" (inst + "r!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skolem-typepred)
(("2"
(expand* "bounded_above?" "upper_bound?" "injection_order")
(("2"
(inst +
"({d | EXISTS (sub_inj: (ch!1)): sub_inj`1(d)}, LAMBDA (d: ({d | EXISTS (sub_inj: (ch!1)): sub_inj`1(d)})): choose[(ch!1)]({sub_inj: (ch!1) | sub_inj`1(d)})`2(d))")
(("1" (skolem!)
(("1" (split)
(("1" (expand* "subset?" "member")
(("1" (skosimp) (("1" (inst?) nil nil)) nil)) nil)
("2" (skolem!)
(("2"
(expand* "chain?" "total_order?" "dichotomous?"
"restrict")
(("2"
(inst - "r!1"
"choose[(ch!1)]({sub_inj: (ch!1) | sub_inj`1(d!1)})")
(("1" (expand "injection_order")
(("1" (delete 4)
(("1" (prop)
(("1" (inst?) nil nil)
("2"
(inst - "d!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand* "nonempty?" "empty?" "member")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand* "injective?" "chain?" "total_order?"
"dichotomous?" "restrict")
(("2" (skosimp* :preds? t)
(("2"
(inst -
"choose[(ch!1)]({sub_inj: (ch!1) | sub_inj`1(x1!1)})"
"choose[(ch!1)]({sub_inj: (ch!1) | sub_inj`1(x2!1)})")
(("1" (expand "injection_order")
(("1" (delete 4)
(("1" (prop)
(("1"
(typepred
"choose[(ch!1)]({sub_inj: (ch!1) | sub_inj`1(x2!1)})`2")
(("1"
(expand* "injective?" "subset?" "member")
(("1"
(inst -2 "x1!1")
(("1"
(inst?)
(("1"
(inst?)
(("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(expand* "nonempty?" "empty?" "member")
(("2" (inst?) nil nil)) nil))
nil)
("2"
(typepred
"choose[(ch!1)]({sub_inj: (ch!1) | sub_inj`1(x1!1)})`2")
(("1"
(expand* "injective?" "subset?" "member")
(("1"
(inst -2 "x2!1")
(("1"
(inst?)
(("1"
(inst?)
(("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(expand* "nonempty?" "empty?" "member")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand* "nonempty?" "empty?" "member")
(("2" (inst?) nil nil)) nil)
("3" (expand* "nonempty?" "empty?" "member")
(("3" (inst?) nil nil)) nil))
nil))
nil))
nil)
("3" (skosimp* :preds? t)
(("3" (expand* "nonempty?" "empty?" "member")
(("3" (inst?) nil nil)) nil))
nil)
("4" (skosimp* :preds? t) (("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((injection_order const-decl "bool" set_dichotomous nil)
(subset_injection type-eq-decl nil set_dichotomous nil)
(injective? const-decl "bool" functions nil)
(R formal-type-decl nil set_dichotomous nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(D formal-type-decl nil set_dichotomous nil)
(zorn formula-decl nil zorn nil)
(chain? const-decl "bool" chain nil)
(chain nonempty-type-eq-decl nil chain nil)
(ch!1 skolem-const-decl "chain[subset_injection, injection_order]"
set_dichotomous nil)
(choose const-decl "(p)" sets nil)
(subset? const-decl "bool" sets 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)
(restrict const-decl "R" restrict nil)
(dichotomous? const-decl "bool" orders nil)
(empty? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
set_dichotomous nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(d!1 skolem-const-decl "(r!1`1)" set_dichotomous nil)
(r!1 skolem-const-decl "(ch!1)" set_dichotomous nil)
(x2!1 skolem-const-decl
"({d | EXISTS (sub_inj: (ch!1)): sub_inj`1(d)})" set_dichotomous
nil)
(x1!1 skolem-const-decl
"({d | EXISTS (sub_inj: (ch!1)): sub_inj`1(d)})" set_dichotomous
nil)
(bounded_above? const-decl "bool" bounded_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(full? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(t!1 skolem-const-decl "subset_injection" set_dichotomous nil)
(surjective? const-decl "bool" functions nil)
(nonempty? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(x!1 skolem-const-decl "D" set_dichotomous nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(y!1 skolem-const-decl "R" set_dichotomous nil)
(subset_add formula-decl nil sets_lemmas nil)
(pred type-eq-decl nil defined_types nil)
(epsilon const-decl "T" epsilons nil)
(extend const-decl "R" extend nil)
(TRUE const-decl "bool" booleans nil)
(maximal? const-decl "bool" minmax_orders nil)
(fullset const-decl "set" sets nil))
shostak))
(injective_dichotomous 0
(injective_dichotomous-1 nil 3315052175
("" (lemma "injective_or_surjective")
(("" (prop)
(("1" (skolem!)
(("1" (use "surjective_inverse_exists[D, R]")
(("1" (skolem!)
(("1" (use "inj_inv_alt[D, R]") (("1" (inst? 2) nil nil))
nil))
nil))
nil))
nil)
("2" (inst 2 "LAMBDA r: epsilon(fullset[D])")
(("1" (expand "injective?" 2)
(("1" (skosimp*) (("1" (inst?) nil nil)) nil)) nil)
("2" (skolem!) nil nil))
nil))
nil))
nil)
((surjective_inverse_exists formula-decl nil function_inverse_def
nil)
(D formal-type-decl nil set_dichotomous nil)
(R formal-type-decl nil set_dichotomous nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(surjective? const-decl "bool" functions nil)
(f!1 skolem-const-decl "[D -> R]" set_dichotomous nil)
(inj_inv_alt formula-decl nil function_inverse_def nil)
(g!1 skolem-const-decl "[R -> D]" set_dichotomous nil)
(inverse? const-decl "bool" function_inverse_def nil)
(injective? const-decl "bool" functions nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(epsilon const-decl "T" epsilons nil)
(pred type-eq-decl nil defined_types nil)
(TRUE const-decl "bool" booleans nil)
(injective_or_surjective formula-decl nil set_dichotomous nil))
shostak))
(surjective_dichotomous 0
(surjective_dichotomous-1 nil 3315052243
("" (lemma "injective_or_surjective")
(("" (prop)
(("1" (skolem!) (("1" (inst + "d!1") nil nil)) nil)
("2" (skolem!)
(("2" (inst 3 "f!1")
(("2" (expand "surjective?")
(("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil))
nil))
nil)
("3" (skosimp*)
(("3" (lemma "inv_inj_is_surj[D, R]")
(("1" (inst?)
(("1" (inst? 2) (("1" (inst + "d!1") nil nil)) nil)) nil)
("2" (inst + "d!1") nil nil))
nil))
nil)
("4" (skosimp*) (("4" (inst + "r!1") nil nil)) nil))
nil))
nil)
((D formal-type-decl nil set_dichotomous nil)
(R formal-type-decl nil set_dichotomous nil)
(surjective? const-decl "bool" functions nil)
(inv_inj_is_surj judgement-tcc nil function_inverse nil)
(TRUE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(inverse const-decl "D" function_inverse nil)
(injective? const-decl "bool" functions nil)
(f!1 skolem-const-decl "[D -> R]" set_dichotomous nil)
(injective_or_surjective formula-decl nil set_dichotomous nil))
shostak)))
¤ Dauer der Verarbeitung: 0.24 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.
|
