OpenMath Content Dictionary: algebraic_cats

Canonical URL:

http://www.openmath.org/cd/algebraic_cats.ocd

CD File:

algebraic_cats.ocd

CD as XML Encoded OpenMath:

algebraic_cats.omcd

Defines:

Abelian_group, Abelian_group_identity, Abelian_group_inverse, Abelian_group_operation, Abelian_group_set, Abelian_monoid, Abelian_monoid_identity, Abelian_monoid_operation, Abelian_monoid_set, Abelian_semigroup, Abelian_semigroup_operation, Abelian_semigroup_set, Euclidean_domain, Euclidean_domain_abs, Euclidean_domain_negative, Euclidean_domain_plus, Euclidean_domain_set, Euclidean_domain_times, Euclidean_domain_zero, field, field_negative, field_one, field_plus, field_reciprocal, field_set, field_times, field_zero, group, group_identity, group_inverse, group_operation, group_set, groupoid, groupoid_operation, groupoid_set, integral_domain, integral_domain_negative, integral_domain_one, integral_domain_plus, integral_domain_set, integral_domain_times, integral_domain_zero, monoid, monoid_identity, monoid_operation, monoid_set, non_commutative_ring, non_commutative_ring_negative, non_commutative_ring_plus, non_commutative_ring_set, non_commutative_ring_times, non_commutative_ring_zero, ordered_Abelian_group, ordered_Abelian_group_identity, ordered_Abelian_group_inverse, ordered_Abelian_group_operation, ordered_Abelian_group_order, ordered_Abelian_group_set, ordered_Abelian_monoid, ordered_Abelian_monoid_identity, ordered_Abelian_monoid_operation, ordered_Abelian_monoid_order, ordered_Abelian_monoid_set, ordered_group, ordered_group_identity, ordered_group_inverse, ordered_group_operation, ordered_group_order, ordered_group_set, ordered_monoid, ordered_monoid_identity, ordered_monoid_operation, ordered_monoid_order, ordered_monoid_set, ordered_ring, ordered_ring_negative, ordered_ring_order, ordered_ring_plus, ordered_ring_set, ordered_ring_times, ordered_ring_zero, ring, ring_negative, ring_plus, ring_set, ring_times, ring_zero, ringoid, ringoid_plus, ringoid_set, ringoid_times, semigroup, semigroup_operation, semigroup_set

Date:

2002-06-17

Version:

0

Review Date:

2005-04-01

Status:

experimental

Uses CD:

generic_alg_cats, logic1, meta_cats, quant1, relation1, set1

A CD of basic algebraic category constructors. This CD holds constructors of individual instances of the categories, with defining properties of the categories and accessor symbols to allow access to attributes of the categories.

monoid

Description:

This is the constructor for monoids. A monoid comprises a set and an operation over elements of the set. The set must contain a unique identity element (relative to the operation). That is an element, I, such that I*a=a*I=a where a represents an arbitrary element of S and * represents the operation. The operation * must be associative over S. The monoid constructor takes three arguments, the set of the monoid, a binary function taking two elements of the set into itself to represent the operation of the monoid and an element of the set to represent the identity of the monoid.

Commented Mathematical property (CMP):

This constructor may be used to build monoids

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMA>
        <OMS cd="algebraic_cats" name="monoid"/>
        <OMV name="S"/>
        <OMV name="star"/>
      </OMA>
      <OMS cd="generic_alg_cats" name="monoid"/>
    </OMA>
  </OMOBJ>

in (monoid ( S, star) , monoid)

$$\mathrm{monoid}(S,\mathrm{star})\in \mathrm{monoid}$$

Commented Mathematical property (CMP):

if (S,*,1) comprises a monoid then for all a,b,c in S | a*(b*c)=(a*b)*c

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMV name="S"/>
      <OMS cd="generic_alg_cats" name="monoid"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="a"/>
        <OMV name="b"/>
        <OMV name="c"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="a"/>
            <OMA>
              <OMS name="monoid_set" cd="algebraic_cats"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMS name="monoid_set" cd="algebraic_cats"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="c"/>
            <OMA>
              <OMS name="monoid_set" cd="algebraic_cats"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMA>
              <OMS name="monoid_operation" cd="algebraic_cats"/>
              <OMV name="S"/>
            </OMA>
            <OMV name="a"/>
            <OMA>
              <OMA>
                <OMS name="monoid_operation" cd="algebraic_cats"/>
                <OMV name="S"/>
              </OMA>
              <OMV name="b"/>
              <OMV name="c"/>
            </OMA>
          </OMA>
          <OMA>
            <OMA>
              <OMS name="monoid_operation" cd="algebraic_cats"/>
              <OMV name="S"/>
            </OMA>
            <OMA>
              <OMA>
                <OMS name="monoid_operation" cd="algebraic_cats"/>
                <OMV name="S"/>
              </OMA>
              <OMV name="a"/>
              <OMV name="b"/>
            </OMA>
            <OMV name="c"/>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

implies (in ( S, monoid) , forall [ a b c ] . (implies (and (in ( a, monoid_set ( S) ) , in ( b, monoid_set ( S) ) , in ( c, monoid_set ( S) ) ) , eq (monoid_operation ( S) ( a, monoid_operation ( S) ( b, c) ) , monoid_operation ( S) (monoid_operation ( S) ( a, b) , c) ) ) ) )

$$S\in \mathrm{monoid}\Rightarrow \forall \hspace{0.17em}a,b,c.a\in \mathrm{monoid\_set}\left(S\right)\wedge b\in \mathrm{monoid\_set}\left(S\right)\wedge c\in \mathrm{monoid\_set}\left(S\right)\Rightarrow \left(\mathrm{monoid\_operation}\left(S\right)\right)(a,\left(\mathrm{monoid\_operation}\left(S\right)\right)(b,c))=\left(\mathrm{monoid\_operation}\left(S\right)\right)(\left(\mathrm{monoid\_operation}\left(S\right)\right)(a,b),c)$$

Commented Mathematical property (CMP):

the operation of the monoid is closed over the set of the monoid

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA><OMS cd="logic1" name="implies"/>
    <OMA><OMS cd="set1" name="in"/>
      <OMV name="S"/>
      <OMS cd="generic_alg_cats" name="monoid"/>
    </OMA>
    <OMA><OMS cd="logic1" name="implies"/>
       <OMA><OMS cd="logic1" name="and"/>
         <OMA><OMS cd="set1" name="in"/>
           <OMV name="a"/>           
           <OMA>
             <OMS name="monoid_set" cd="algebraic_cats"/>
             <OMV name="S"/>
           </OMA>
         </OMA>
         <OMA><OMS cd="set1" name="in"/>
           <OMV name="b"/>
           <OMA>
             <OMS name="monoid_set" cd="algebraic_cats"/>
             <OMV name="S"/>
           </OMA>
         </OMA>
       </OMA>
       <OMA><OMS cd="set1" name="in"/>
         <OMA>
           <OMA>
             <OMS name="monoid_operation" cd="algebraic_cats"/>
             <OMV name="S"/>
           </OMA>
           <OMV name="a"/>
           <OMV name="b"/>
         </OMA>
         <OMA>
           <OMS name="monoid_set" cd="algebraic_cats"/>
           <OMV name="S"/>
         </OMA>
       </OMA>
    </OMA>
  </OMA>
</OMOBJ>

implies (in ( S, monoid) , implies (and (in ( a, monoid_set ( S) ) , in ( b, monoid_set ( S) ) ) , in (monoid_operation ( S) ( a, b) , monoid_set ( S) ) ) )

$$S\in \mathrm{monoid}\Rightarrow a\in \mathrm{monoid\_set}\left(S\right)\wedge b\in \mathrm{monoid\_set}\left(S\right)\Rightarrow \left(\mathrm{monoid\_operation}\left(S\right)\right)(a,b)\in \mathrm{monoid\_set}\left(S\right)$$

Commented Mathematical property (CMP):

if (S,*,1) is a monoid then there exists a unique identity element in S

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA><OMS cd="logic1" name="implies"/>
      <OMA><OMS cd="set1" name="in"/>
        <OMV name="S"/>
        <OMS cd="generic_alg_cats" name="monoid"/>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="exists"/>
        <OMBVAR><OMV name="id"/></OMBVAR>
        <OMA><OMS cd="logic1" name="and"/>
          <OMBIND>
            <OMS cd="quant1" name="forall"/>
            <OMBVAR><OMV name="x"/></OMBVAR>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMA>
                <OMA>
                  <OMS name="monoid_operation" cd="algebraic_cats"/>
                  <OMV name="S"/>
                </OMA>
                <OMV name="x"/>
                <OMV name="id"/>
              </OMA>
              <OMV name="x"/>
            </OMA>
          </OMBIND>
          <OMA>
            <OMS cd="relation1" name="eq"/>
            <OMV name="id"/>
            <OMA>
              <OMS cd="algebraic_cats" name="monoid_identity"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMA>
                <OMA>
                  <OMS name="monoid_operation" cd="algebraic_cats"/>
                  <OMV name="S"/>
                </OMA>
                <OMV name="x"/>
                <OMV name="id2"/>
              </OMA>
              <OMV name="x"/>
            </OMA>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMV name="id"/>
              <OMV name="id2"/>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
    </OMA>
  </OMOBJ>

implies (in ( S, monoid) , exists [ id] . (and (forall [ x] . (eq (monoid_operation ( S) ( x, id) , x) ) , eq ( id, monoid_identity ( S) ) , implies (eq (monoid_operation ( S) ( x, id2) , x) , eq ( id, id2) ) ) ) )

$$S\in \mathrm{monoid}\Rightarrow \exists \hspace{0.17em}\mathrm{id}.\forall \hspace{0.17em}x.\left(\mathrm{monoid\_operation}\left(S\right)\right)(x,\mathrm{id})=x\wedge \mathrm{id}=\mathrm{monoid\_identity}\left(S\right)\wedge (\left(\mathrm{monoid\_operation}\left(S\right)\right)(x,{\mathrm{id}}_2)=x\Rightarrow \mathrm{id}={\mathrm{id}}_2)$$

Commented Mathematical property (CMP):

the set of a monoid must contain at least one element

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="logic1" name="implies"/>
  <OMA>
    <OMS cd="set1" name="in"/>
    <OMV name="S"/>
    <OMS cd="generic_alg_cats" name="monoid"/>
  </OMA>
  <OMBIND>
    <OMS cd="quant1" name="exists"/>
    <OMBVAR><OMV name="x"/></OMBVAR>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMV name="x"/>
      <OMA>
        <OMS cd="algebraic_cats" name="monoid_set"/>
        <OMV name="S"/>
      </OMA>
    </OMA>
  </OMBIND>
</OMA>
</OMOBJ>

implies (in ( S, monoid) , exists [ x] . (in ( x, monoid_set ( S) ) ) )

$$S\in \mathrm{monoid}\Rightarrow \exists \hspace{0.17em}x.x\in \mathrm{monoid\_set}\left(S\right)$$

Signatures:

sts

monoid_set

Description:

This symbol takes one argument which should be a monoid, it returns the set of the monoid.

Commented Mathematical property (CMP):

The set of the monoid (S,*,1) = S

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="monoid_set"/>
        <OMA>
          <OMS cd="algebraic_cats" name="monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
        </OMA>
      </OMA>
      <OMV name="S"/>
    </OMA>
  </OMOBJ>

eq (monoid_set (monoid ( S, star, id) ) , S)

$$\mathrm{monoid\_set}\left(\mathrm{monoid}(S,\mathrm{star},\mathrm{id})\right)=S$$

Signatures:

sts

monoid_operation

Description:

This symbol takes one argument which should be a monoid, it returns the operation of the monoid.

Commented Mathematical property (CMP):

The operation of the monoid (S,*,1) = *

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="monoid_operation"/>
        <OMA>
          <OMS cd="algebraic_cats" name="monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
        </OMA>
      </OMA>
      <OMV name="star"/>
    </OMA>
  </OMOBJ>

eq (monoid_operation (monoid ( S, star, id) ) , star)

$$\mathrm{monoid\_operation}\left(\mathrm{monoid}(S,\mathrm{star},\mathrm{id})\right)=\mathrm{star}$$

Signatures:

sts

monoid_identity

Description:

This symbol takes one argument which should be a monoid, it returns the identity of the monoid.

Commented Mathematical property (CMP):

The identity of the monoid (S,*,1) = 1

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="monoid_identity"/>
        <OMA>
          <OMS cd="algebraic_cats" name="monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
        </OMA>
      </OMA>
      <OMV name="id"/>
    </OMA>
  </OMOBJ>

eq (monoid_identity (monoid ( S, star, id) ) , id)

$$\mathrm{monoid\_identity}\left(\mathrm{monoid}(S,\mathrm{star},\mathrm{id})\right)=\mathrm{id}$$

Signatures:

sts

Abelian_monoid

Description:

This is the constructor for Abelian monoids. An Abelian monoid is a monoid, such that the operation is commutative between members of the Abelian monoid. The Abelian_monoid constructor takes three arguments, the set of the Abelian monoid, a binary function taking two elements of the set into itself to represent the operation of the Abelian monoid and an element of the set to represent the identity of the Abelian monoid.

Commented Mathematical property (CMP):

This constructor may be used to build Abelian_monoids

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMA>
        <OMS cd="algebraic_cats" name="Abelian_monoid"/>
        <OMV name="S"/>
        <OMV name="star"/>
        <OMV name="Id"/>
      </OMA>
      <OMS cd="generic_alg_cats" name="Abelian_monoid"/>
    </OMA>
  </OMOBJ>

in (Abelian_monoid ( S, star, Id) , Abelian_monoid)

$$\mathrm{Abelian\_monoid}(S,\mathrm{star},\mathrm{Id})\in \mathrm{Abelian\_monoid}$$

Commented Mathematical property (CMP):

if (S,*,1) comprises an Abelian monoid then for all a,b in S | a*b=b*a

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMV name="S"/>
        <OMS cd="generic_alg_cats" name="Abelian_monoid"/>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="forall"/>
        <OMBVAR>
          <OMV name="a"/>
          <OMV name="b"/>
        </OMBVAR>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="a"/>
            <OMA>
              <OMA cd="generic_alg_cats" name="Abelian_monoid"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMA cd="generic_alg_cats" name="Abelian_monoid"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="relation1" name="eq"/>
            <OMA>
              <OMA>
                <OMS cd="algebraic_cats" name="Abelian_monoid_operation"/>
                <OMV name="S"/>
              </OMA>
              <OMV name="a"/>
              <OMV name="b"/>
            </OMA>
            <OMA>
              <OMA>
                <OMS cd="algebraic_cats" name="Abelian_monoid_operation"/>
                <OMV name="S"/>
              </OMA>
              <OMV name="b"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
    </OMA>
  </OMOBJ>

implies (in ( S, Abelian_monoid) , forall [ a b ] . (and (in ( a, () ( S) ) , in ( b, () ( S) ) , eq (Abelian_monoid_operation ( S) ( a, b) , Abelian_monoid_operation ( S) ( b, a) ) ) ) )

$$S\in \mathrm{Abelian\_monoid}\Rightarrow \forall \hspace{0.17em}a,b.a\in \left(\right)\left(S\right)\wedge b\in \left(\right)\left(S\right)\wedge \left(\mathrm{Abelian\_monoid\_operation}\left(S\right)\right)(a,b)=\left(\mathrm{Abelian\_monoid\_operation}\left(S\right)\right)(b,a)$$

Signatures:

sts

Abelian_monoid_set

Description:

This symbol takes one argument which should be an Abelian monoid, it returns the set of the Abelian monoid.

Commented Mathematical property (CMP):

The set of the Abelian monoid (S,*,1) = S

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="Abelian_monoid_set"/>
        <OMA>
          <OMS cd="algebraic_cats" name="Abelian_monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
        </OMA>
      </OMA>
      <OMV name="S"/>
    </OMA>
  </OMOBJ>

eq (Abelian_monoid_set (Abelian_monoid ( S, star, id) ) , S)

$$\mathrm{Abelian\_monoid\_set}\left(\mathrm{Abelian\_monoid}(S,\mathrm{star},\mathrm{id})\right)=S$$

Signatures:

sts

Abelian_monoid_operation

Description:

This symbol takes one argument which should be an Abelian monoid, it returns the operation of the Abelian monoid.

Commented Mathematical property (CMP):

The operation of the Abelian monoid (S,*,1)= *

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="Abelian_monoid_set"/>
        <OMA>
          <OMS cd="algebraic_cats" name="Abelian_monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
        </OMA>
      </OMA>
      <OMV name="star"/>
    </OMA>
  </OMOBJ>

eq (Abelian_monoid_set (Abelian_monoid ( S, star, id) ) , star)

$$\mathrm{Abelian\_monoid\_set}\left(\mathrm{Abelian\_monoid}(S,\mathrm{star},\mathrm{id})\right)=\mathrm{star}$$

Signatures:

sts

Abelian_monoid_identity

Description:

This symbol takes one argument which should be an Abelian monoid, it returns the identity of the Abelian monoid.

Commented Mathematical property (CMP):

The identity of the Abelian monoid (S,*,1) = 1

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="Abelian_monoid_set"/>
        <OMA>
          <OMS cd="algebraic_cats" name="Abelian_monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
        </OMA>
      </OMA>
      <OMV name="id"/>
    </OMA>
  </OMOBJ>

eq (Abelian_monoid_set (Abelian_monoid ( S, star, id) ) , id)

$$\mathrm{Abelian\_monoid\_set}\left(\mathrm{Abelian\_monoid}(S,\mathrm{star},\mathrm{id})\right)=\mathrm{id}$$

Signatures:

sts

ordered_monoid

Description:

This is the constructor for ordered monoids, that is monoids on which there is an ordering relation. The ordered_monoid constructor takes four arguments, the set of the ordered monoid, a binary function taking two elements of the set into itself to represent the operation of the ordered monoid, an element of the set to represent the identity of the ordered monoid and a binary function taking two elements of the set into the booleans to represent the ordering on the ordered monoid.

Commented Mathematical property (CMP):

This constructor may be used to build ordered monoids

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMA>
        <OMS cd="algebraic_cats" name="ordered_monoid"/>
        <OMV name="S"/>
        <OMV name="star"/>
        <OMV name="Id"/>
        <OMV name="lt"/>
      </OMA>
      <OMS cd="generic_alg_cats" name="ordered_monoid"/>
    </OMA>
  </OMOBJ>

in (ordered_monoid ( S, star, Id, lt) , ordered_monoid)

$$\mathrm{ordered\_monoid}(S,\mathrm{star},\mathrm{Id},\mathrm{lt})\in \mathrm{ordered\_monoid}$$

Commented Mathematical property (CMP):

if (S,*,1,\leq) represents an ordered monoid, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMV name="S"/>
        <OMS name="ordered_monoid" cd="generic_alg_cats"/>
      </OMA>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMBIND>
          <OMS cd="quant1" name="forall"/>
          <OMBVAR>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMBVAR>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="and"/>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="a"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="b"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="or"/>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_order"/>
                  <OMV name="S"/>
                </OMA>
                <OMV name="a"/>
                <OMV name="b"/>
              </OMA>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_order"/>
                  <OMV name="S"/>
                </OMA>
                <OMV name="b"/>
                <OMV name="a"/>
              </OMA>
            </OMA>
          </OMA>
        </OMBIND>
        <OMBIND>
          <OMS cd="quant1" name="forall"/>
          <OMBVAR>
            <OMV name="a"/>
            <OMV name="b"/>
            <OMV name="c"/>
          </OMBVAR>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="and"/>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="a"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="b"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="c"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="and"/>
                <OMA>
                  <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_order"/>
                  <OMV name="S"/>
                </OMA>
                  <OMV name="a"/>
                  <OMV name="b"/>
                </OMA>
                <OMA>
                  <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_order"/>
                  <OMV name="S"/>
                </OMA>
                  <OMV name="b"/>
                  <OMV name="c"/>
                </OMA>
              </OMA>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_order"/>
                  <OMV name="S"/>
                </OMA>
                  <OMV name="a"/>
                  <OMV name="c"/>
              </OMA>
            </OMA>
          </OMA>
        </OMBIND>
        <OMBIND>
          <OMS cd="quant1" name="forall"/>
          <OMBVAR>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMBVAR>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="and"/>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="a"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="b"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="and"/>
                <OMA>
                  <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_order"/>
                  <OMV name="S"/>
                </OMA>
                  <OMV name="a"/>
                  <OMV name="b"/>
                </OMA>
                <OMA>
                  <OMA>
                  <OMS cd="algebraic_cats" name="ordered_monoid_order"/>
                  <OMV name="S"/>
                </OMA>
                  <OMV name="b"/>
                  <OMV name="a"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="relation1" name="eq"/>
                <OMV name="a"/>
                <OMV name="b"/>
              </OMA>
            </OMA>
          </OMA>
        </OMBIND>
      </OMA>
    </OMA>
  </OMOBJ>

implies (in ( S, ordered_monoid) , and (forall [ a b ] . (implies (and (in ( a, ordered_monoid_set ( S) ) , in ( b, ordered_monoid_set ( S) ) ) , or (ordered_monoid_order ( S) ( a, b) , ordered_monoid_order ( S) ( b, a) ) ) ) , forall [ a b c ] . (implies (and (in ( a, ordered_monoid_set ( S) ) , in ( b, ordered_monoid_set ( S) ) , in ( c, ordered_monoid_set ( S) ) ) , implies (and (ordered_monoid_order ( S) ( a, b) , ordered_monoid_order ( S) ( b, c) ) , ordered_monoid_order ( S) ( a, c) ) ) ) , forall [ a b ] . (implies (and (in ( a, ordered_monoid_set ( S) ) , in ( b, ordered_monoid_set ( S) ) ) , implies (and (ordered_monoid_order ( S) ( a, b) , ordered_monoid_order ( S) ( b, a) ) , eq ( a, b) ) ) ) ) )

$$S\in \mathrm{ordered\_monoid}\Rightarrow \forall \hspace{0.17em}a,b.a\in \mathrm{ordered\_monoid\_set}\left(S\right)\wedge b\in \mathrm{ordered\_monoid\_set}\left(S\right)\Rightarrow \left(\mathrm{ordered\_monoid\_order}\left(S\right)\right)(a,b)\vee \left(\mathrm{ordered\_monoid\_order}\left(S\right)\right)(b,a)\wedge \forall \hspace{0.17em}a,b,c.a\in \mathrm{ordered\_monoid\_set}\left(S\right)\wedge b\in \mathrm{ordered\_monoid\_set}\left(S\right)\wedge c\in \mathrm{ordered\_monoid\_set}\left(S\right)\Rightarrow \left(\mathrm{ordered\_monoid\_order}\left(S\right)\right)(a,b)\wedge \left(\mathrm{ordered\_monoid\_order}\left(S\right)\right)(b,c)\Rightarrow \left(\mathrm{ordered\_monoid\_order}\left(S\right)\right)(a,c)\wedge \forall \hspace{0.17em}a,b.a\in \mathrm{ordered\_monoid\_set}\left(S\right)\wedge b\in \mathrm{ordered\_monoid\_set}\left(S\right)\Rightarrow \left(\mathrm{ordered\_monoid\_order}\left(S\right)\right)(a,b)\wedge \left(\mathrm{ordered\_monoid\_order}\left(S\right)\right)(b,a)\Rightarrow a=b$$

Signatures:

sts

ordered_monoid_set

Description:

This symbol takes one argument which should be an ordered monoid. It returns a set which should be the set of the ordered monoid.

Commented Mathematical property (CMP):

The set of the ordered monoid (S,*,1,\leq) = S

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="ordered_monoid_set"/>
        <OMA>
          <OMS cd="algebraic_cats" name="ordered_monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
          <OMV name="leq"/>
        </OMA>
      </OMA>
      <OMV name="S"/>
    </OMA>
  </OMOBJ>

eq (ordered_monoid_set (ordered_monoid ( S, star, id, leq) ) , S)

$$\mathrm{ordered\_monoid\_set}\left(\mathrm{ordered\_monoid}(S,\mathrm{star},\mathrm{id},\mathrm{leq})\right)=S$$

Signatures:

sts

ordered_monoid_operation

Description:

This symbol takes one argument which should be an ordered monoid. It returns a binary function between elements of the set of the ordered monoid, which should represent the operation of the ordered monoid.

Commented Mathematical property (CMP):

The operation of the ordered monoid (S,*,1,\leq) = *

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="ordered_monoid_operation"/>
        <OMA>
          <OMS cd="algebraic_cats" name="ordered_monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
          <OMV name="leq"/>
        </OMA>
      </OMA>
      <OMV name="star"/>
    </OMA>
  </OMOBJ>

eq (ordered_monoid_operation (ordered_monoid ( S, star, id, leq) ) , star)

$$\mathrm{ordered\_monoid\_operation}\left(\mathrm{ordered\_monoid}(S,\mathrm{star},\mathrm{id},\mathrm{leq})\right)=\mathrm{star}$$

Signatures:

sts

ordered_monoid_identity

Description:

This symbol takes one argument which should be an ordered monoid. It returns an element of the set of the ordered monoid, which should be the identity of the ordered monoid.

Commented Mathematical property (CMP):

The identity of the ordered monoid (S,*,1,\leq) = 1

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="ordered_monoid_identity"/>
        <OMA>
          <OMS cd="algebraic_cats" name="ordered_monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
          <OMV name="leq"/>
        </OMA>
      </OMA>
      <OMV name="id"/>
    </OMA>
  </OMOBJ>

eq (ordered_monoid_identity (ordered_monoid ( S, star, id, leq) ) , id)

$$\mathrm{ordered\_monoid\_identity}\left(\mathrm{ordered\_monoid}(S,\mathrm{star},\mathrm{id},\mathrm{leq})\right)=\mathrm{id}$$

Signatures:

sts

ordered_monoid_order

Description:

This symbol takes one argument which should be an ordered monoid. It returns a binary function between elements of the set of the ordered monoid, which should represent the ordering relation on the ordered monoid.

Commented Mathematical property (CMP):

The order of the ordered monoid (S,*,1,\leq) = \leq

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="algebraic_cats" name="ordered_monoid_order"/>
        <OMA>
          <OMS cd="algebraic_cats" name="ordered_monoid"/>
          <OMV name="S"/>
          <OMV name="star"/>
          <OMV name="id"/>
          <OMV name="leq"/>
        </OMA>
      </OMA>
      <OMV name="leq"/>
    </OMA>
  </OMOBJ>

eq (ordered_monoid_order (ordered_monoid ( S, star, id, leq) ) , leq)

$$\mathrm{ordered\_monoid\_order}\left(\mathrm{ordered\_monoid}(S,\mathrm{star},\mathrm{id},\mathrm{leq})\right)=\mathrm{leq}$$

Signatures:

sts

ordered_Abelian_monoid

Description:

This symbol is the constructor for ordered Abelian monoids, that is Abelian monoids on which there is an ordering relation. The ordered_Abelian_monoid constructor takes four arguments, the set of the ordered Abelian monoid, a binary function taking two elements of the set into itself to represent the operation of the ordered Abelian monoid, an element of the set to represent the identity of the ordered Abelian monoid and a binary function taking two elements of the set into the booleans to represent the ordering of the ordered Abelian monoid.

Commented Mathematical property (CMP):

This constructor may be used to build ordered Abelian monoids

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMA>
        <OMS cd="algebraic_cats" name="ordered_Abelian_monoid"/>
        <OMV name="S"/>
        <OMV name="star"/>
        <OMV name="Id"/>
        <OMV name="lt"/>
      </OMA>
      <OMS cd="generic_alg_cats" name="ordered_Abelian_monoid"/>
    </OMA>
  </OMOBJ>

in (ordered_Abelian_monoid ( S, star, Id, lt) , ordered_Abelian_monoid)

$$\mathrm{ordered\_Abelian\_monoid}(S,\mathrm{star},\mathrm{Id},\mathrm{lt})\in \mathrm{ordered\_Abelian\_monoid}$$

Commented Mathematical property (CMP):

if (S,*,1,\leq) represents an ordered Abelian monoid, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMV name="S"/>
        <OMS name="ordered_Abelian_monoid" cd="generic_alg_cats"/>
      </OMA>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMBIND>
          <OMS cd="quant1" name="forall"/>
          <OMBVAR>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMBVAR>
          <OMA>
            <OMS cd="logic1" name="implies"/>
            <OMA>
              <OMS cd="logic1" name="and"/>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="a"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_monoid_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="b"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_monoid_set"/>
                  <OMV name="S"/>
                </OMA>