|
(card_function
(infinite_bijection 0
(infinite_bijection-1 nil 3313930340
("" (skosimp*)
(("" (expand "is_finite")
(("" (skosimp*)
(("" (inst + "N!1" "f!2 o f!1")
(("1" (expand "bijective?")
(("1" (flatten)
(("1" (expand "o")
(("1" (expand "restrict")
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (inst -4 "f!1(x1!1)" "f!1(x2!1)")
(("1" (assert)
(("1" (inst - "x1!1" "x2!1")
(("1" (assert) nil nil)) nil))
nil)
("2" (expand "fullset")
(("2" (propax) nil nil)) nil)
("3" (expand "fullset")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "fullset") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((is_finite const-decl "bool" finite_sets nil)
(f!1 skolem-const-decl "[D -> R]" card_function nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(R formal-type-decl nil card_function nil)
(D formal-type-decl nil card_function nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(restrict const-decl "R" restrict nil)
(O const-decl "T3" function_props nil)
(injective? const-decl "bool" functions nil)
(bijective? const-decl "bool" functions nil))
shostak))
(finite_bijection 0
(finite_bijection-1 nil 3313930567
("" (expand "fullset")
(("" (expand "is_finite")
(("" (skosimp*)
(("" (lemma "bijective_inverse_exists" ("f" "f!1"))
(("1" (expand "exists1")
(("1" (flatten)
(("1" (skolem -1 ("g"))
(("1" (lemma "bij_inv_is_bij_alt" ("f" "f!1" "g" "g"))
(("1" (inst + "N!1" "f!2 o g")
(("1" (expand "bijective?")
(("1" (flatten)
(("1" (hide-all-but (-1 -7 1))
(("1" (expand "restrict")
(("1" (expand "injective?")
(("1"
(expand "o")
(("1"
(skosimp*)
(("1"
(inst -2 "g(x1!1)" "g(x2!1)")
(("1"
(assert)
(("1"
(inst - "x1!1" "x2!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
((is_finite const-decl "bool" finite_sets nil)
(R formal-type-decl nil card_function nil)
(D formal-type-decl nil card_function nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bijective_inverse_exists formula-decl nil function_inverse_def
nil)
(bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
(inverse? const-decl "bool" function_inverse_def nil)
(injective? const-decl "bool" functions nil)
(O const-decl "T3" function_props nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(TRUE const-decl "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)
(exists1 const-decl "bool" exists1 nil)
(fullset const-decl "set" sets nil))
shostak))
(infinite_injection 0
(infinite_injection-1 nil 3313931578
("" (expand "fullset")
(("" (expand "is_finite")
(("" (skosimp*)
(("" (inst + "N!1" "f!2 o f!1")
(("" (expand "restrict")
(("" (expand "injective?")
(("" (skosimp*)
(("" (expand "o")
(("" (inst -3 "f!1(x1!1)" "f!1(x2!1)")
(("" (assert)
(("" (inst - "x1!1" "x2!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((is_finite const-decl "bool" finite_sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(D formal-type-decl nil card_function nil)
(TRUE const-decl "bool" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(R formal-type-decl nil card_function nil)
(O const-decl "T3" function_props nil)
(injective? const-decl "bool" functions nil)
(fullset const-decl "set" sets nil))
shostak))
(finite_injection 0
(finite_injection-1 nil 3313931479
("" (skosimp)
(("" (lemma "infinite_injection" ("f" "f!1"))
(("" (assert) nil nil)) nil))
nil)
((R formal-type-decl nil card_function nil)
(D formal-type-decl nil card_function nil)
(infinite_injection formula-decl nil card_function nil))
shostak))
(infinite_surjection 0
(infinite_surjection-1 nil 3313931185
("" (expand "fullset")
(("" (expand "is_finite")
(("" (skosimp*)
(("" (lemma "surjective_inverse_exists" ("f" "f!1"))
(("1" (skosimp)
(("1" (lemma "inj_inv_alt" ("f" "f!1" "g" "g!1"))
(("1" (inst + "N!1" "f!2 o g!1")
(("1" (expand "restrict")
(("1" (expand "o ")
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (inst -5 "g!1(x1!1)" "g!1(x2!1)")
(("1" (assert)
(("1" (inst - "x1!1" "x2!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
((is_finite const-decl "bool" finite_sets nil)
(R formal-type-decl nil card_function nil)
(D formal-type-decl nil card_function nil)
(surjective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(surjective_inverse_exists formula-decl nil function_inverse_def
nil)
(inj_inv_alt formula-decl nil function_inverse_def nil)
(inverse? const-decl "bool" function_inverse_def nil)
(injective? const-decl "bool" functions nil)
(O const-decl "T3" function_props nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(TRUE const-decl "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)
(fullset const-decl "set" sets nil))
shostak))
(finite_surjection 0
(finite_surjection-1 nil 3313931452
("" (skosimp*)
(("" (lemma "infinite_surjection" ("f" "f!1"))
(("" (assert) nil nil)) nil))
nil)
((R formal-type-decl nil card_function nil)
(D formal-type-decl nil card_function nil)
(infinite_surjection formula-decl nil card_function nil))
shostak)))
¤ Dauer der Verarbeitung: 0.2 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.
|
