Quelle  ring_with_one_def.prf

(ring_with_one_def
 (commutative_ring_with_one?_TCC1 0
  (commutative_ring_with_one?_TCC1-1 nil 3301146176
   ("" (expand "ring_with_one?")
    (("" (expand "ring?")
      (("" (expand "semigroup?")
        (("" (expand "groupoid?")
          (("" (expand "star_closed?")
            (("" (skosimp*)
              (("" (inst - "x1!1`1" "x1!1`2")
                (("" (expand "member") (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((ring? const-decl "bool" ring_def nil)
    (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil ring_with_one_def nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (ring_with_one? const-decl "bool" ring_with_one_def nil))
   shostak))
 (finite_commutative_ring_with_one?_TCC1 0
  (finite_commutative_ring_with_one?_TCC1-1 nil 3301146176
   ("" (expand "finite_ring_with_one?")
    (("" (expand "ring_with_one?")
      (("" (expand "monoid?")
        (("" (expand "monad?")
          (("" (expand "groupoid?")
            (("" (expand "star_closed?")
              (("" (expand "member") (("" (skosimp*) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((ring_with_one? const-decl "bool" ring_with_one_def 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)
    (finite_ring_with_one? const-decl "bool" ring_with_one_def nil))
   shostak)))