Quelle  commutative_semigroup.prf

(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)))