(A_groupnil 3397569694 ("" (subtype-tcc) nil nil )"(bijective?[T1, T3])" nil )"(surjective?[T1, T3])" function_props nil )"(injective?[T1, T3])" nil ))nil ))nil 3397569250"" (skosimp*) (("" (inst + "id(S!1)" ) nil nil )) nil )nil A_group nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" functions nil )nil A_group nil )"maps(S)" A_group nil ))nil ))nil 3397569259"" (skosimp*)"" (expand "group?" )"" (prop)"1" (expand "monoid?" )"1" (prop)"1" (expand "monad?" )"1" (prop)"1" (expand "groupoid?" )"1" (expand "star_closed?" )"1" (assert )"1" (skosimp*) (("1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (grind) nil nil )"3" (grind)"1" (expand "identity" )"1" (apply-extensionality 1 :hide? t) nil nil ))nil )"2" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil ))nil )"2" (grind)"2" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil ))nil )"2" (expand "inv_exists?" )"2" (skosimp*)"2" (typepred "x!1" )"2" (inst + "(inverse(x!1))" )"1" (grind)"1" (apply-extensionality 1 :hide? t)"1" (inst?)"1" (assert )"1" (lemma "epsilon_ax[(S!1)]" )"1" (inst?)"1" (assert )"1" (inst + "x!2" ) nil nil )) nil ))nil )"2" (typepred "S!1" )"2" (expand "nonempty?" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil )"2" (typepred "S!1" )"2" (expand "nonempty?" )"2" (typepred "S!1" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil )"2" (typepred "S!1" )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (skosimp*)"2" (expand "member" )"2" (inst + "x!2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality 1 :hide? t)"1" (inst?)"1" (assert )"1" (lemma "epsilon_ax[(S!1)]" )"1" (inst?)"1" (assert )"1" (inst - "x!2" ) nil nil )) nil ))nil )"2" (typepred "S!1" )"2" (expand "nonempty?" )"2" expand "empty?" )"2" "2" assert )"2" (inst + "x!3" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "S!1" )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (skosimp*)"2" assert )"2" (inst + "x!3" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "S!1" )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (skosimp*)"2" (assert )"2" (inst + "x!2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil )"3" (typepred "S!1" )"3" (expand "nonempty?" )"3" (expand "empty?" )"3" (assert )"3" (skosimp*) (("3" (inst + "x!2" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" group_def nil )"bool" group_def nil )"T" A_group nil )"bool" sets nil )"T" A_group nil )"[T, T -> boolean]" equalities nil )"T" epsilons nil )nil defined_types nil )nil epsilons nil )"{x: D | f(x) = y}" nil )"(fullset[maps(S!1)])" A_group nil )"D" function_inverse nil )"bool" booleans nil )"(nonempty?[T])" A_group nil )"(bijective?[R, D])" function_inverse nil )"bool" monoid_def nil )"bool" operator_defs nil )"bool" monad_def nil )identity ? const-decl "bool" operator_defs nil )nil A_group nil )"bool" functions nil )"bool" sets nil )set type-eq-decl nil sets nil )nil A_group nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" functions nil )"bool" functions nil )"T3" function_props nil )identity const-decl "(bijective?[T, T])" identity nil )"maps(S)" A_group nil )"bool" groupoid_def nil )"(bijective?[T1, T3])" nil )"(surjective?[T1, T3])" function_props nil )"(injective?[T1, T3])" nil )"set" sets nil )"R" restrict nil )"[maps(S), maps(S) -> maps(S)]" A_group nil )"bool" sets nil ))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.15Bemerkung:
(vorverarbeitet)
¤ *Bot Zugriff
