Quellcode-Bibliothek set_dichotomous.prf
Sprache: Lisp
(set_dichotomousnil 3315051270 ("" (subtype-tcc) nil nil )nil set_dichotomous nil )"bool" functions nil )nil set_dichotomous nil )set type-eq-decl nil sets nil )nil set_dichotomous nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" sets nil ))nil ))nil 3315051270"" (grind-with-ext) nil nil )nil set_dichotomous nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil set_dichotomous nil )"bool" functions nil )nil set_dichotomous nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"bool" sets nil )"bool" set_dichotomous nil )"bool" relations nil )"bool" relations nil )"bool" orders nil )"bool" relations nil )"bool" orders nil ))nil ))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" "extend[D, (t!1`1), R, epsilon(fullset[R])](t!1`2)" )"1" (expand * "surjective?" "full?" "member" )"1" (skosimp*)"1" "(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" "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" "3" "3" "3" "1" "x2!1" )"1" (assert ) nil nil ))nil )"2" "x1!1" )"2" (assert ) nil nil ))nil )"3" "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" "({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" "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" "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" "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" "choose[(ch!1)]({sub_inj: (ch!1) | sub_inj`1(x2!1)})`2" )"1" expand * "injective?" "subset?" "member" )"1" "x1!1" )"1" "1" "1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" expand * "nonempty?" "empty?" "member" )"2" (inst?) nil nil )) nil ))nil )"2" "choose[(ch!1)]({sub_inj: (ch!1) | sub_inj`1(x1!1)})`2" )"1" expand * "injective?" "subset?" "member" )"1" "x2!1" )"1" "1" "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 )"bool" set_dichotomous nil )nil set_dichotomous nil )"bool" functions nil )nil set_dichotomous nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil set_dichotomous nil )nil zorn nil )"bool" chain nil )nil chain nil )"chain[subset_injection, injection_order]" nil )"(p)" sets nil )"bool" sets nil )"bool" orders nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"R" restrict nil )"bool" orders nil )"bool" sets nil )"(partial_order?[set[T]])" nil )"(partial_order?[set[T]])" nil )"(r!1`1)" set_dichotomous nil )"(ch!1)" set_dichotomous nil )"({d | EXISTS (sub_inj: (ch!1)): sub_inj`1(d)})" set_dichotomousnil )"({d | EXISTS (sub_inj: (ch!1)): sub_inj`1(d)})" set_dichotomousnil )"bool" bounded_orders nil )"bool" bounded_orders nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"subset_injection" set_dichotomous nil )"bool" functions nil )"bool" sets nil )"(nonempty?)" sets nil )"D" set_dichotomous nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"R" set_dichotomous nil )nil sets_lemmas nil )nil defined_types nil )"T" epsilons nil )"R" extend nil )"bool" booleans nil )"bool" minmax_orders nil )"set" sets nil ))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 )nil function_inverse_defnil )nil set_dichotomous nil )nil set_dichotomous nil )nil booleans nil )nil booleans nil )"bool" functions nil )"[D -> R]" set_dichotomous nil )nil function_inverse_def nil )"[R -> D]" set_dichotomous nil )"bool" function_inverse_def nil )"bool" functions nil )"set" sets nil ) (set type-eq-decl nil sets nil )"T" epsilons nil )nil defined_types nil )"bool" booleans nil )nil set_dichotomous nil ))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 )nil set_dichotomous nil )nil set_dichotomous nil )"bool" functions nil )nil function_inverse nil )"bool" booleans nil )nil booleans nil )nil booleans nil )"D" function_inverse nil )"bool" functions nil )"[D -> R]" set_dichotomous nil )nil set_dichotomous nil ))quality 100%
¤ 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.0.17Bemerkung:
(vorverarbeitet)
¤ *Bot Zugriff
2026-03-28
