(cyclic_monoidnil 3294400674"" (lemma "fullset_is_cyclic_monoid" )"" (expand "cyclic_monoid?" ) (("" (flatten) nil nil )) nil )) nil )"bool" cyclic_monoid_def nil )nil cyclic_monoid nil ))nil 3294400675"" (lemma "fullset_is_cyclic_monoid" ) (("" (propax) nil nil )) nil )nil cyclic_monoid nil ))nil 3294401795"" (skosimp) (("" (typepred "M!1" ) (("" (propax) nil nil )) nil ))nil )nil cyclic_monoid nil )"bool" cyclic_monoid_def nil )"T" cyclic_monoid nil )"[T, T -> T]" cyclic_monoid nil )set type-eq-decl nil sets nil )nil cyclic_monoid nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3294400677"" (skosimp)"" (typepred "x!1" )"" (expand "cyclic_monoid?" ) (("" (flatten) nil nil )) nil ))nil ))nil )nil cyclic_monoid nil )"bool" cyclic_monoid_def nil )"T" cyclic_monoid nil )"[T, T -> T]" cyclic_monoid nil )set type-eq-decl nil sets nil )nil cyclic_monoid nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3294400677"" (skosimp)"" (typepred "x!1" )"" (expand "cyclic_monoid?" )"" (expand "commutative_monoid?" )"" (flatten)"" (assert )"" (skosimp)"" (lemma "fullset_is_cyclic_monoid" )"" (expand "cyclic_monoid?" )"" (flatten)"" (skosimp)"" (hide -3 -4 -1)"" (expand "commutative?" )"" (skosimp)"" case "generated_set(a!2)(x!2)" )"1" case "generated_set(a!2)(y!1)" )"1" expand "generated_set" )"1" "1" replace -1)"1" replace -2)"1" expand "restrict" )"1" rewrite "power_mult" )"1" rewrite "power_mult" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -2 * rl)"2" expand "fullset" )"2" (propax) nil nil ))nil ))nil ))nil )"2" replace -1 * rl)"2" expand "fullset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cyclic_monoid nil )"bool" cyclic_monoid_def nil )"T" cyclic_monoid nil )"[T, T -> T]" cyclic_monoid nil )set type-eq-decl nil sets nil )nil cyclic_monoid nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" monoid_def nil )nil cyclic_monoid nil )nil monoid 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 )"nonneg_int" nil )"R" restrict nil )"set" sets nil )"set[T]" monoid_def nil )"bool" operator_defs nil ))quality 93%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
