(commutative_semigroup
(IMP_commutative_groupoid_TCC1 0
(IMP_commutative_groupoid_TCC1-1 nil 3294074461
("" (lemma "fullset_is_commutative_semigroup")
(("" (expand "commutative_semigroup?")
(("" (expand "commutative_groupoid?")
(("" (expand "semigroup?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((commutative_semigroup? const-decl "bool" semigroup_def nil)
(commutative_groupoid? const-decl "bool" groupoid_def nil)
(fullset_is_commutative_semigroup formula-decl nil
commutative_semigroup nil))
shostak))
(IMP_semigroup_TCC1 0
(IMP_semigroup_TCC1-1 nil 3294074461
("" (lemma "fullset_is_commutative_semigroup")
(("" (expand "commutative_semigroup?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil)
((commutative_semigroup? const-decl "bool" semigroup_def nil)
(fullset_is_commutative_semigroup formula-decl nil
commutative_semigroup nil))
shostak))
(commutative_semigroup_TCC1 0
(commutative_semigroup_TCC1-1 nil 3294074461
("" (lemma "fullset_is_commutative_semigroup")
(("" (propax) nil nil)) nil)
((fullset_is_commutative_semigroup formula-decl nil
commutative_semigroup nil))
shostak))
(commutative_semigroup_is_semigroup 0
(commutative_semigroup_is_semigroup-1 nil 3294074461
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "commutative_semigroup?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((commutative_semigroup nonempty-type-eq-decl nil
commutative_semigroup nil)
(commutative_semigroup? const-decl "bool" semigroup_def nil)
(* formal-const-decl "[T, T -> T]" commutative_semigroup nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil commutative_semigroup nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(commutative_semigroup_is_commutative_groupoid 0
(commutative_semigroup_is_commutative_groupoid-1 nil 3294079423
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "commutative_semigroup?")
(("" (expand "semigroup?")
(("" (expand "commutative_groupoid?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((commutative_semigroup nonempty-type-eq-decl nil
commutative_semigroup nil)
(commutative_semigroup? const-decl "bool" semigroup_def nil)
(* formal-const-decl "[T, T -> T]" commutative_semigroup nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil commutative_semigroup nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(commutative_groupoid? const-decl "bool" groupoid_def nil))
shostak)))
¤ Dauer der Verarbeitung: 0.0 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.
|