SSL countability_aux.prf
Interaktion und
(countability_auxnil 3406351233"" (expand "is_countable" )"" (inst + "lambda (x:(emptyset[T])): 0" )"" (expand "injective?" )"" (skosimp)"" (typepred "x1!1" )"" (expand "emptyset" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil countability_aux nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" countability nil ))nil 3406351272"" (skosimp)"" (expand "is_countable" )"" (inst + "lambda (x:(singleton(t!1))):0" )"" (expand "injective?" )"" (skosimp)"" (typepred "x1!1" )"" (typepred "x2!1" )"" (expand "singleton" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countability nil )NOT const-decl "[bool -> bool]" booleans nil )"T" countability_aux nil )"bool" functions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"(singleton?)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countability_aux nil ))nil 3406352219"" (skosimp)"" (typepred "X!1" )"" (expand "is_countable" )"" (skosimp)"" (typepred "f!1" )"" (case "X!1(t!1)" )"1" (inst + "f!1" )"1" (split)"1" (skosimp)"1" (expand "add" )"1" (expand "member" )"1" (assert )"1" (hide -2) (("1" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "injective?" )"2" (skosimp)"2" (typepred "x1!1" )"2" (typepred "x2!1" )"2" (expand "add" )"2" (expand "member" )"2" "x1!1" "x2!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "lambda (x:(add(t!1, X!1))): if x = t!1 then 0 else f!1(x)+1 endif" )"1" (expand "injective?" )"1" (skosimp)"1" (case-replace "x1!1 = t!1" )"1" (lift-if) (("1" (assert ) nil nil )) nil )"2" (case-replace "x2!1 = t!1" )"1" (lift-if) (("1" (assert ) nil nil )) nil )"2" (assert )"2" (inst - "x1!1" "x2!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "x!1" )"2" (expand "add" )"2" (expand "member" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countability_aux nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(is_countable)" countability_aux nil )"T" countability_aux nil )"(injective?[(X!1), nat])" countability_auxnil )"(nonempty?)" sets nil )"bool" sets nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"posint" nil )"posint" nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil ))nil 3406352813"" (skosimp)"" (typepred "X!1" )"" (expand "is_countable" )"" (skosimp)"" (typepred "f!1" )"" (case "X!1(t!1)" )"1" (inst + "lambda (x:(remove(t!1, X!1))): f!1(x)" )"1" (expand "injective?" )"1" (skosimp)"1" (typepred "x1!1" )"1" (typepred "x2!1" )"1" (expand "remove" )"1" (expand "member" )"1" (flatten)"1" "x1!1" "x2!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "x!1" )"2" (expand "remove" )"2" (expand "member" ) (("2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "lambda (x:(remove(t!1, X!1))): f!1(x)" )"1" (expand "injective?" )"1" (skosimp)"1" (typepred "x1!1" )"1" (typepred "x2!1" )"1" (expand "remove" )"1" (expand "member" )"1" (flatten)"1" "x1!1" "x2!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "x!1" )"2" (expand "remove" )"2" (expand "member" ) (("2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" countability nil )set type-eq-decl nil sets nil )nil countability_aux nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"(injective?[(X!1), nat])" countability_auxnil )"(is_countable)" countability_aux nil )"T" countability_aux nil )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil ))nil 3406352737"" (skosimp)"" "countable_subset" "S" "intersection(X!1, S!1)" "Count" "X!1" ))"" (rewrite "intersection_subset1" ) nil nil )) nil ))nil )nil countability_aux nil )nil countability nil )"bool" countability nil )"set" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countability nil )nil sets_lemmas nil ))nil 3406352606"" (skosimp)"" (lemma "countable_intersection1" ("S" "S!1" "X" "X!1" ))"" (rewrite "intersection_commutative" ) nil nil )) nil ))nil )"bool" countability nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil countability_aux nil )nil countability_aux nil )nil sets_lemmas nil )"countable_set[T]" nil ))nil 3406352658"" (skosimp)"" (lemma "difference_subset" ("a" "X!1" "b" "S!1" ))"" "countable_subset" "S" "difference(X!1, S!1)" "A" "X!1" ))"" (assert ) nil nil )) nil ))nil ))nil )nil countability_aux nil )"bool" countability nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil sets_lemmas nil )"(partial_order?[set[T]])" nil )"countable_set[T]" 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
