(monoid_def
 (power_TCC1 0
  (power_TCC1-1 nil 3296995136 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (power_TCC2 0
  (power_TCC2-1 nil 3296995136 ("" (grind) nil nil) nil shostak))
 (generated_set_lem 0
  (generated_set_lem-1 nil 3396972577
   ("" (skosimp*)
    (("" (expand "generated_set") (("" (inst?) nil nil)) nil)) nil)
   ((generated_set const-decl "set[T]" monoid_def nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak))
 (monoid?_TCC1 0
  (monoid?_TCC1-1 nil 3301141924
   ("" (expand "monad?")
    (("" (expand "groupoid?")
      (("" (expand "star_closed?")
        (("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil))
      nil))
    nil)
   ((star_closed? const-decl "bool" groupoid_def nil)
    (member const-decl "bool" sets nil)
    (monad? const-decl "bool" monad_def nil))
   shostak))
 (commutative_monoid?_TCC1 0
  (commutative_monoid?_TCC1-1 nil 3301141924
   ("" (expand "monoid?")
    (("" (expand "monad?")
      (("" (expand "groupoid?")
        (("" (expand "star_closed?")
          (("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((monad? const-decl "bool" monad_def nil)
    (member const-decl "bool" sets nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (monoid? const-decl "bool" monoid_def nil))
   shostak))
 (finite_commutative_monoid?_TCC1 0
  (finite_commutative_monoid?_TCC1-1 nil 3301141924
   ("" (expand "finite_monoid?")
    (("" (expand "monoid?")
      (("" (expand "monad?")
        (("" (expand "groupoid?")
          (("" (expand "star_closed?")
            (("" (expand "member") (("" (skosimp*) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((monoid? const-decl "bool" monoid_def nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (member const-decl "bool" sets nil)
    (monad? const-decl "bool" monad_def nil)
    (finite_monoid? const-decl "bool" monoid_def nil))
   shostak)))