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

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">monoid</csymbol><ci>S</ci><ci>star</ci></apply>
  <csymbol cd="generic_alg_cats">monoid</csymbol>
 </apply>
</math>

Prefix

in (monoid ( S, star) , monoid)

Popcorn

set1.in(algebraic_cats.monoid($S, $star), generic_alg_cats.monoid)

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">monoid</csymbol></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <bvar><ci>c</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="algebraic_cats">monoid_set</csymbol><ci>S</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>b</ci>
      <apply><csymbol cd="algebraic_cats">monoid_set</csymbol><ci>S</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>c</ci>
      <apply><csymbol cd="algebraic_cats">monoid_set</csymbol><ci>S</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply>
      <apply><csymbol cd="algebraic_cats">monoid_operation</csymbol><ci>S</ci></apply>
      <ci>a</ci>
      <apply>
       <apply><csymbol cd="algebraic_cats">monoid_operation</csymbol><ci>S</ci></apply>
       <ci>b</ci>
       <ci>c</ci>
      </apply>
     </apply>
     <apply>
      <apply><csymbol cd="algebraic_cats">monoid_operation</csymbol><ci>S</ci></apply>
      <apply>
       <apply><csymbol cd="algebraic_cats">monoid_operation</csymbol><ci>S</ci></apply>
       <ci>a</ci>
       <ci>b</ci>
      </apply>
      <ci>c</ci>
     </apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

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

Popcorn

set1.in($S, generic_alg_cats.monoid) ==> quant1.forall[$a, $b, $c -> set1.in($a, algebraic_cats.monoid_set($S)) and set1.in($b, algebraic_cats.monoid_set($S)) and set1.in($c, algebraic_cats.monoid_set($S)) ==> algebraic_cats.monoid_operation($S)($a, algebraic_cats.monoid_operation($S)($b, $c)) = algebraic_cats.monoid_operation($S)(algebraic_cats.monoid_operation($S)($a, $b), $c)]

Rendered Presentation MathML

$$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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">monoid</csymbol></apply>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="algebraic_cats">monoid_set</csymbol><ci>S</ci></apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>b</ci>
     <apply><csymbol cd="algebraic_cats">monoid_set</csymbol><ci>S</ci></apply>
    </apply>
   </apply>
   <apply><csymbol cd="set1">in</csymbol>
    <apply>
     <apply><csymbol cd="algebraic_cats">monoid_operation</csymbol><ci>S</ci></apply>
     <ci>a</ci>
     <ci>b</ci>
    </apply>
    <apply><csymbol cd="algebraic_cats">monoid_set</csymbol><ci>S</ci></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

set1.in($S, generic_alg_cats.monoid) ==> set1.in($a, algebraic_cats.monoid_set($S)) and set1.in($b, algebraic_cats.monoid_set($S)) ==> set1.in(algebraic_cats.monoid_operation($S)($a, $b), algebraic_cats.monoid_set($S))

Rendered Presentation MathML

$$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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">monoid</csymbol></apply>
  <bind><csymbol cd="quant1">exists</csymbol>
   <bvar><ci>id</ci></bvar>
   <apply><csymbol cd="logic1">and</csymbol>
    <bind><csymbol cd="quant1">forall</csymbol>
     <bvar><ci>x</ci></bvar>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply>
       <apply><csymbol cd="algebraic_cats">monoid_operation</csymbol><ci>S</ci></apply>
       <ci>x</ci>
       <ci>id</ci>
      </apply>
      <ci>x</ci>
     </apply>
    </bind>
    <apply><csymbol cd="relation1">eq</csymbol>
     <ci>id</ci>
     <apply><csymbol cd="algebraic_cats">monoid_identity</csymbol><ci>S</ci></apply>
    </apply>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply>
       <apply><csymbol cd="algebraic_cats">monoid_operation</csymbol><ci>S</ci></apply>
       <ci>x</ci>
       <ci>id2</ci>
      </apply>
      <ci>x</ci>
     </apply>
     <apply><csymbol cd="relation1">eq</csymbol><ci>id</ci><ci>id2</ci></apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

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

Popcorn

set1.in($S, generic_alg_cats.monoid) ==> quant1.exists[$id -> quant1.forall[$x -> algebraic_cats.monoid_operation($S)($x, $id) = $x] and $id = algebraic_cats.monoid_identity($S) and (algebraic_cats.monoid_operation($S)($x, $id2) = $x ==> $id = $id2)]

Rendered Presentation MathML

$$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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">monoid</csymbol></apply>
  <bind><csymbol cd="quant1">exists</csymbol>
   <bvar><ci>x</ci></bvar>
   <apply><csymbol cd="set1">in</csymbol>
    <ci>x</ci>
    <apply><csymbol cd="algebraic_cats">monoid_set</csymbol><ci>S</ci></apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

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

Popcorn

set1.in($S, generic_alg_cats.monoid) ==> quant1.exists[$x -> set1.in($x, algebraic_cats.monoid_set($S))]

Rendered Presentation MathML

$$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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">monoid_set</csymbol>
   <apply><csymbol cd="algebraic_cats">monoid</csymbol><ci>S</ci><ci>star</ci><ci>id</ci></apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.monoid_set(algebraic_cats.monoid($S, $star, $id)) = $S

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">monoid_operation</csymbol>
   <apply><csymbol cd="algebraic_cats">monoid</csymbol><ci>S</ci><ci>star</ci><ci>id</ci></apply>
  </apply>
  <ci>star</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.monoid_operation(algebraic_cats.monoid($S, $star, $id)) = $star

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">monoid_identity</csymbol>
   <apply><csymbol cd="algebraic_cats">monoid</csymbol><ci>S</ci><ci>star</ci><ci>id</ci></apply>
  </apply>
  <ci>id</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.monoid_identity(algebraic_cats.monoid($S, $star, $id)) = $id

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">Abelian_monoid</csymbol><ci>S</ci><ci>star</ci><ci>Id</ci></apply>
  <csymbol cd="generic_alg_cats">Abelian_monoid</csymbol>
 </apply>
</math>

Prefix

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

Popcorn

set1.in(algebraic_cats.Abelian_monoid($S, $star, $Id), generic_alg_cats.Abelian_monoid)

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">Abelian_monoid</csymbol></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>a</ci>
     <apply><apply/><ci>S</ci></apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>b</ci>
     <apply><apply/><ci>S</ci></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply>
      <apply><csymbol cd="algebraic_cats">Abelian_monoid_operation</csymbol><ci>S</ci></apply>
      <ci>a</ci>
      <ci>b</ci>
     </apply>
     <apply>
      <apply><csymbol cd="algebraic_cats">Abelian_monoid_operation</csymbol><ci>S</ci></apply>
      <ci>b</ci>
      <ci>a</ci>
     </apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

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

Popcorn

set1.in($S, generic_alg_cats.Abelian_monoid) ==> quant1.forall[$a, $b -> set1.in($a, ()($S)) and set1.in($b, ()($S)) and algebraic_cats.Abelian_monoid_operation($S)($a, $b) = algebraic_cats.Abelian_monoid_operation($S)($b, $a)]

Rendered Presentation MathML

$$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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">Abelian_monoid_set</csymbol>
   <apply><csymbol cd="algebraic_cats">Abelian_monoid</csymbol><ci>S</ci><ci>star</ci><ci>id</ci></apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.Abelian_monoid_set(algebraic_cats.Abelian_monoid($S, $star, $id)) = $S

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">Abelian_monoid_set</csymbol>
   <apply><csymbol cd="algebraic_cats">Abelian_monoid</csymbol><ci>S</ci><ci>star</ci><ci>id</ci></apply>
  </apply>
  <ci>star</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.Abelian_monoid_set(algebraic_cats.Abelian_monoid($S, $star, $id)) = $star

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">Abelian_monoid_set</csymbol>
   <apply><csymbol cd="algebraic_cats">Abelian_monoid</csymbol><ci>S</ci><ci>star</ci><ci>id</ci></apply>
  </apply>
  <ci>id</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.Abelian_monoid_set(algebraic_cats.Abelian_monoid($S, $star, $id)) = $id

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_monoid</csymbol>
   <ci>S</ci>
   <ci>star</ci>
   <ci>Id</ci>
   <ci>lt</ci>
  </apply>
  <csymbol cd="generic_alg_cats">ordered_monoid</csymbol>
 </apply>
</math>

Prefix

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

Popcorn

set1.in(algebraic_cats.ordered_monoid($S, $star, $Id, $lt), generic_alg_cats.ordered_monoid)

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">ordered_monoid</csymbol></apply>
  <apply><csymbol cd="logic1">and</csymbol>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">or</csymbol>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
       <ci>a</ci>
       <ci>b</ci>
      </apply>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
       <ci>b</ci>
       <ci>a</ci>
      </apply>
     </apply>
    </apply>
   </bind>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <bvar><ci>c</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>c</ci>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
        <ci>a</ci>
        <ci>b</ci>
       </apply>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
        <ci>b</ci>
        <ci>c</ci>
       </apply>
      </apply>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
       <ci>a</ci>
       <ci>c</ci>
      </apply>
     </apply>
    </apply>
   </bind>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
        <ci>a</ci>
        <ci>b</ci>
       </apply>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
        <ci>b</ci>
        <ci>a</ci>
       </apply>
      </apply>
      <apply><csymbol cd="relation1">eq</csymbol><ci>a</ci><ci>b</ci></apply>
     </apply>
    </apply>
   </bind>
  </apply>
 </apply>
</math>

Prefix

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

Popcorn

set1.in($S, generic_alg_cats.ordered_monoid) ==> quant1.forall[$a, $b -> set1.in($a, algebraic_cats.ordered_monoid_set($S)) and set1.in($b, algebraic_cats.ordered_monoid_set($S)) ==> algebraic_cats.ordered_monoid_order($S)($a, $b) > algebraic_cats.ordered_monoid_order($S)($b, $a)] and quant1.forall[$a, $b, $c -> set1.in($a, algebraic_cats.ordered_monoid_set($S)) and set1.in($b, algebraic_cats.ordered_monoid_set($S)) and set1.in($c, algebraic_cats.ordered_monoid_set($S)) ==> algebraic_cats.ordered_monoid_order($S)($a, $b) and algebraic_cats.ordered_monoid_order($S)($b, $c) ==> algebraic_cats.ordered_monoid_order($S)($a, $c)] and quant1.forall[$a, $b -> set1.in($a, algebraic_cats.ordered_monoid_set($S)) and set1.in($b, algebraic_cats.ordered_monoid_set($S)) ==> algebraic_cats.ordered_monoid_order($S)($a, $b) and algebraic_cats.ordered_monoid_order($S)($b, $a) ==> $a = $b]

Rendered Presentation MathML

$$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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_monoid_set</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_monoid</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.ordered_monoid_set(algebraic_cats.ordered_monoid($S, $star, $id, $leq)) = $S

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_monoid_operation</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_monoid</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>star</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.ordered_monoid_operation(algebraic_cats.ordered_monoid($S, $star, $id, $leq)) = $star

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_monoid_identity</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_monoid</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>id</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.ordered_monoid_identity(algebraic_cats.ordered_monoid($S, $star, $id, $leq)) = $id

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_monoid</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>leq</ci>
 </apply>
</math>

Prefix

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

Popcorn

algebraic_cats.ordered_monoid_order(algebraic_cats.ordered_monoid($S, $star, $id, $leq)) = $leq

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid</csymbol>
   <ci>S</ci>
   <ci>star</ci>
   <ci>Id</ci>
   <ci>lt</ci>
  </apply>
  <csymbol cd="generic_alg_cats">ordered_Abelian_monoid</csymbol>
 </apply>
</math>

Prefix

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

Popcorn

set1.in(algebraic_cats.ordered_Abelian_monoid($S, $star, $Id, $lt), generic_alg_cats.ordered_Abelian_monoid)

Rendered Presentation MathML

$$\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):

OpenMath XML (source)

  <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>
              </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_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>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="c"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_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_Abelian_monoid_order"/>
                    <OMV name="S"/>
                  </OMA>
                  <OMV name="a"/>
                  <OMV name="b"/>
                </OMA>
                <OMA>
                  <OMA>
                    <OMS cd="algebraic_cats" name="ordered_Abelian_monoid_order"/>
                    <OMV name="S"/>
                  </OMA>
                  <OMV name="b"/>
                  <OMV name="c"/>
                </OMA>
              </OMA>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_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_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>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="implies"/>
              <OMA>
                <OMS cd="logic1" name="and"/>
                <OMA>
                  <OMA>
                    <OMS cd="algebraic_cats" name="ordered_Abelian_monoid_order"/>
                    <OMV name="S"/>
                  </OMA>
                  <OMV name="a"/>
                  <OMV name="b"/>
                </OMA>
                <OMA>
                  <OMA>
                    <OMS cd="algebraic_cats" name="ordered_Abelian_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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">ordered_Abelian_monoid</csymbol></apply>
  <apply><csymbol cd="logic1">and</csymbol>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">or</csymbol>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
       <ci>a</ci>
       <ci>b</ci>
      </apply>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_monoid_order</csymbol><ci>S</ci></apply>
       <ci>b</ci>
       <ci>a</ci>
      </apply>
     </apply>
    </apply>
   </bind>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <bvar><ci>c</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>c</ci>
       <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_order</csymbol><ci>S</ci></apply>
        <ci>a</ci>
        <ci>b</ci>
       </apply>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_order</csymbol><ci>S</ci></apply>
        <ci>b</ci>
        <ci>c</ci>
       </apply>
      </apply>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_order</csymbol><ci>S</ci></apply>
       <ci>a</ci>
       <ci>c</ci>
      </apply>
     </apply>
    </apply>
   </bind>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_order</csymbol><ci>S</ci></apply>
        <ci>a</ci>
        <ci>b</ci>
       </apply>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_order</csymbol><ci>S</ci></apply>
        <ci>b</ci>
        <ci>a</ci>
       </apply>
      </apply>
      <apply><csymbol cd="relation1">eq</csymbol><ci>a</ci><ci>b</ci></apply>
     </apply>
    </apply>
   </bind>
  </apply>
 </apply>
</math>

Prefix

implies (in ( S, ordered_Abelian_monoid) , and (forall [ a b ] . (implies (and (in ( a, ordered_Abelian_monoid_set ( S) ) , in ( b, ordered_Abelian_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_Abelian_monoid_set ( S) ) , in ( b, ordered_Abelian_monoid_set ( S) ) , in ( c, ordered_Abelian_monoid_set ( S) ) ) , implies (and (ordered_Abelian_monoid_order ( S) ( a, b) , ordered_Abelian_monoid_order ( S) ( b, c) ) , ordered_Abelian_monoid_order ( S) ( a, c) ) ) ) , forall [ a b ] . (implies (and (in ( a, ordered_Abelian_monoid_set ( S) ) , in ( b, ordered_Abelian_monoid_set ( S) ) ) , implies (and (ordered_Abelian_monoid_order ( S) ( a, b) , ordered_Abelian_monoid_order ( S) ( b, a) ) , eq ( a, b) ) ) ) ) )

Popcorn

set1.in($S, generic_alg_cats.ordered_Abelian_monoid) ==> quant1.forall[$a, $b -> set1.in($a, algebraic_cats.ordered_Abelian_monoid_set($S)) and set1.in($b, algebraic_cats.ordered_Abelian_monoid_set($S)) ==> algebraic_cats.ordered_monoid_order($S)($a, $b) > algebraic_cats.ordered_monoid_order($S)($b, $a)] and quant1.forall[$a, $b, $c -> set1.in($a, algebraic_cats.ordered_Abelian_monoid_set($S)) and set1.in($b, algebraic_cats.ordered_Abelian_monoid_set($S)) and set1.in($c, algebraic_cats.ordered_Abelian_monoid_set($S)) ==> algebraic_cats.ordered_Abelian_monoid_order($S)($a, $b) and algebraic_cats.ordered_Abelian_monoid_order($S)($b, $c) ==> algebraic_cats.ordered_Abelian_monoid_order($S)($a, $c)] and quant1.forall[$a, $b -> set1.in($a, algebraic_cats.ordered_Abelian_monoid_set($S)) and set1.in($b, algebraic_cats.ordered_Abelian_monoid_set($S)) ==> algebraic_cats.ordered_Abelian_monoid_order($S)($a, $b) and algebraic_cats.ordered_Abelian_monoid_order($S)($b, $a) ==> $a = $b]

Rendered Presentation MathML

$$S\in \mathrm{ordered\_Abelian\_monoid}\Rightarrow \forall \hspace{0.17em}a,b.a\in \mathrm{ordered\_Abelian\_monoid\_set}\left(S\right)\wedge b\in \mathrm{ordered\_Abelian\_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\_Abelian\_monoid\_set}\left(S\right)\wedge b\in \mathrm{ordered\_Abelian\_monoid\_set}\left(S\right)\wedge c\in \mathrm{ordered\_Abelian\_monoid\_set}\left(S\right)\Rightarrow \left(\mathrm{ordered\_Abelian\_monoid\_order}\left(S\right)\right)(a,b)\wedge \left(\mathrm{ordered\_Abelian\_monoid\_order}\left(S\right)\right)(b,c)\Rightarrow \left(\mathrm{ordered\_Abelian\_monoid\_order}\left(S\right)\right)(a,c)\wedge \forall \hspace{0.17em}a,b.a\in \mathrm{ordered\_Abelian\_monoid\_set}\left(S\right)\wedge b\in \mathrm{ordered\_Abelian\_monoid\_set}\left(S\right)\Rightarrow \left(\mathrm{ordered\_Abelian\_monoid\_order}\left(S\right)\right)(a,b)\wedge \left(\mathrm{ordered\_Abelian\_monoid\_order}\left(S\right)\right)(b,a)\Rightarrow a=b$$

Signatures:

sts

ordered_Abelian_monoid_set

Description:

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

Commented Mathematical property (CMP):

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

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_set</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

eq (ordered_Abelian_monoid_set (ordered_Abelian_monoid ( S, star, id, leq) ) , S)

Popcorn

algebraic_cats.ordered_Abelian_monoid_set(algebraic_cats.ordered_Abelian_monoid($S, $star, $id, $leq)) = $S

Rendered Presentation MathML

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

Signatures:

sts

ordered_Abelian_monoid_operation

Description:

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

Commented Mathematical property (CMP):

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

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_operation</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>star</ci>
 </apply>
</math>

Prefix

eq (ordered_Abelian_monoid_operation (ordered_Abelian_monoid ( S, star, id, leq) ) , star)

Popcorn

algebraic_cats.ordered_Abelian_monoid_operation(algebraic_cats.ordered_Abelian_monoid($S, $star, $id, $leq)) = $star

Rendered Presentation MathML

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

Signatures:

sts

ordered_Abelian_monoid_identity

Description:

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

Commented Mathematical property (CMP):

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

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_identity</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>id</ci>
 </apply>
</math>

Prefix

eq (ordered_Abelian_monoid_identity (ordered_Abelian_monoid ( S, star, id, leq) ) , id)

Popcorn

algebraic_cats.ordered_Abelian_monoid_identity(algebraic_cats.ordered_Abelian_monoid($S, $star, $id, $leq)) = $id

Rendered Presentation MathML

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

Signatures:

sts

ordered_Abelian_monoid_order

Description:

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

Commented Mathematical property (CMP):

The ordering of the ordered Abelian monoid (S,*,1,/leq) = /leq

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid_order</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_Abelian_monoid</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>leq</ci>
 </apply>
</math>

Prefix

eq (ordered_Abelian_monoid_order (ordered_Abelian_monoid ( S, star, id, leq) ) , leq)

Popcorn

algebraic_cats.ordered_Abelian_monoid_order(algebraic_cats.ordered_Abelian_monoid($S, $star, $id, $leq)) = $leq

Rendered Presentation MathML

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

Signatures:

sts

groupoid

Description:

This symbol is the constructor for groupoids, that is an algebraic structure on a set, with a binary operation. The operator of the groupoid must be closed over the set of the groupoid. The groupoid constructor takes two arguments, the set of the groupoid and a binary function which represents the operation of the groupoid.

Commented Mathematical property (CMP):

This constructor may be used to build groupoids

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">groupoid</csymbol><ci>S</ci><ci>star</ci></apply>
  <csymbol cd="generic_alg_cats">groupoid</csymbol>
 </apply>
</math>

Prefix

in (groupoid ( S, star) , groupoid)

Popcorn

set1.in(algebraic_cats.groupoid($S, $star), generic_alg_cats.groupoid)

Rendered Presentation MathML

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

Commented Mathematical property (CMP):

if (S,*) comprises a groupoid, then for all a,b in S | a*b is a member of S

Formal Mathematical property (FMP):

OpenMath XML (source)

<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="groupoid"/>
  </OMA>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="a"/>
      <OMV name="b"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMA cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="a"/>
          <OMA>
            <OMS cd="algebraic_cats" name="groupoid_set"/>
            <OMV name="S"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="b"/>
          <OMA>
            <OMS cd="algebraic_cats" name="groupoid_set"/>
            <OMV name="S"/>
          </OMA>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMA>
          <OMA>
            <OMS cd="algebraic_cats" name="groupoid_operation"/>
            <OMV name="S"/>
          </OMA>
          <OMV name="a"/>
          <OMV name="b"/>
        </OMA>
        <OMA>
          <OMS cd="algebraic_cats" name="groupoid_set"/>
          <OMV name="S"/>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">groupoid</csymbol></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply>
     <apply/>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="algebraic_cats">groupoid_set</csymbol><ci>S</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>b</ci>
      <apply><csymbol cd="algebraic_cats">groupoid_set</csymbol><ci>S</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <apply>
      <apply><csymbol cd="algebraic_cats">groupoid_operation</csymbol><ci>S</ci></apply>
      <ci>a</ci>
      <ci>b</ci>
     </apply>
     <apply><csymbol cd="algebraic_cats">groupoid_set</csymbol><ci>S</ci></apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (in ( S, groupoid) , forall [ a b ] . (implies ( () (in ( a, groupoid_set ( S) ) , in ( b, groupoid_set ( S) ) ) , in (groupoid_operation ( S) ( a, b) , groupoid_set ( S) ) ) ) )

Popcorn

set1.in($S, generic_alg_cats.groupoid) ==> quant1.forall[$a, $b -> ()(set1.in($a, algebraic_cats.groupoid_set($S)), set1.in($b, algebraic_cats.groupoid_set($S))) ==> set1.in(algebraic_cats.groupoid_operation($S)($a, $b), algebraic_cats.groupoid_set($S))]

Rendered Presentation MathML

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

Signatures:

sts

groupoid_set

Description:

This symbol takes one argument which should be a groupoid. It returns the set of the groupoid.

Commented Mathematical property (CMP):

The set of the groupoid (S,*) = S

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">groupoid_set</csymbol>
   <apply><csymbol cd="algebraic_cats">groupoid</csymbol><ci>S</ci><ci>star</ci></apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

eq (groupoid_set (groupoid ( S, star) ) , S)

Popcorn

algebraic_cats.groupoid_set(algebraic_cats.groupoid($S, $star)) = $S

Rendered Presentation MathML

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

Signatures:

sts

groupoid_operation

Description:

This symbol takes one argument which should be a groupoid. It returns a binary function which should represent the operation of the groupoid.

Commented Mathematical property (CMP):

The operation of the groupoid (S,*) = *

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">groupoid_operation</csymbol>
   <apply><csymbol cd="algebraic_cats">groupoid</csymbol><ci>S</ci><ci>star</ci></apply>
  </apply>
  <ci>star</ci>
 </apply>
</math>

Prefix

eq (groupoid_operation (groupoid ( S, star) ) , star)

Popcorn

algebraic_cats.groupoid_operation(algebraic_cats.groupoid($S, $star)) = $star

Rendered Presentation MathML

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

Signatures:

sts

semigroup

Description:

This symbol is the constructor for semigroups, that is groupoids for which the operator of the semigroup is associative over the set of the semigroup. The semigroup constructor takes two arguments, the set of the semigroup and a binary function which represents the operation of the semigroup.

Commented Mathematical property (CMP):

This constructor may be used to build semigroups

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">semigroup</csymbol><ci>S</ci><ci>star</ci></apply>
  <csymbol cd="generic_alg_cats">semigroup</csymbol>
 </apply>
</math>

Prefix

in (semigroup ( S, star) , semigroup)

Popcorn

set1.in(algebraic_cats.semigroup($S, $star), generic_alg_cats.semigroup)

Rendered Presentation MathML

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

Commented Mathematical property (CMP):

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

Formal Mathematical property (FMP):

OpenMath XML (source)

<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="semigroup"/>
  </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>
        <OMA cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="a"/>
          <OMA>
            <OMS cd="algebraic_cats" name="semigroup_set"/>
            <OMV name="S"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="b"/>
          <OMA>
            <OMS cd="algebraic_cats" name="semigroup_set"/>
            <OMV name="S"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="c"/>
          <OMA>
            <OMS cd="algebraic_cats" name="semigroup_set"/>
            <OMV name="S"/>
          </OMA>
        </OMA>
      </OMA>
    </OMA>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMA>
          <OMS cd="algebraic_cats" name="semigroup_operation"/>
          <OMV name="S"/>
        </OMA>
        <OMV name="a"/>
        <OMA>
          <OMA>
            <OMS cd="algebraic_cats" name="semigroup_operation"/>
            <OMV name="S"/>
          </OMA>
          <OMV name="b"/>
          <OMV name="c"/>
        </OMA>
      </OMA>
      <OMA>
        <OMA>
          <OMS cd="algebraic_cats" name="semigroup_operation"/>
          <OMV name="S"/>
        </OMA>
        <OMA>
          <OMA>
            <OMS cd="algebraic_cats" name="semigroup_operation"/>
            <OMV name="S"/>
          </OMA>
          <OMV name="a"/>
          <OMV name="b"/>
        </OMA>
        <OMV name="c"/>
      </OMA>
    </OMA>
  </OMBIND>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">semigroup</csymbol></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <bvar><ci>c</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply>
     <apply/>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="algebraic_cats">semigroup_set</csymbol><ci>S</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>b</ci>
      <apply><csymbol cd="algebraic_cats">semigroup_set</csymbol><ci>S</ci></apply>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <ci>c</ci>
      <apply><csymbol cd="algebraic_cats">semigroup_set</csymbol><ci>S</ci></apply>
     </apply>
    </apply>
   </apply>
   <apply><csymbol cd="relation1">eq</csymbol>
    <apply>
     <apply><csymbol cd="algebraic_cats">semigroup_operation</csymbol><ci>S</ci></apply>
     <ci>a</ci>
     <apply>
      <apply><csymbol cd="algebraic_cats">semigroup_operation</csymbol><ci>S</ci></apply>
      <ci>b</ci>
      <ci>c</ci>
     </apply>
    </apply>
    <apply>
     <apply><csymbol cd="algebraic_cats">semigroup_operation</csymbol><ci>S</ci></apply>
     <apply>
      <apply><csymbol cd="algebraic_cats">semigroup_operation</csymbol><ci>S</ci></apply>
      <ci>a</ci>
      <ci>b</ci>
     </apply>
     <ci>c</ci>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (in ( S, semigroup) , forall [ a b c ] . (implies ( () (in ( a, semigroup_set ( S) ) , in ( b, semigroup_set ( S) ) , in ( c, semigroup_set ( S) ) ) ) eq (semigroup_operation ( S) ( a, semigroup_operation ( S) ( b, c) ) , semigroup_operation ( S) (semigroup_operation ( S) ( a, b) , c) ) ) )

Popcorn

set1.in($S, generic_alg_cats.semigroup) ==> quant1.forall[$a, $b, $c -> algebraic_cats.semigroup_operation($S)($a, algebraic_cats.semigroup_operation($S)($b, $c)) = algebraic_cats.semigroup_operation($S)(algebraic_cats.semigroup_operation($S)($a, $b), $c)]

Rendered Presentation MathML

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

Signatures:

sts

semigroup_set

Description:

This symbol takes one argument which should be a semigroup. It returns the set of the semigroup.

Commented Mathematical property (CMP):

The set of the semigroup (S,*) = S

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">semigroup_set</csymbol>
   <apply><csymbol cd="algebraic_cats">semigroup</csymbol><ci>S</ci><ci>star</ci></apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

eq (semigroup_set (semigroup ( S, star) ) , S)

Popcorn

algebraic_cats.semigroup_set(algebraic_cats.semigroup($S, $star)) = $S

Rendered Presentation MathML

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

Signatures:

sts

semigroup_operation

Description:

This symbol takes one argument which should be a semigroup. It returns a binary function which should represent the operation of the semigroup.

Commented Mathematical property (CMP):

The operation of the semigroup (S,*) = *

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">semigroup_operation</csymbol>
   <apply><csymbol cd="algebraic_cats">semigroup</csymbol><ci>S</ci><ci>star</ci></apply>
  </apply>
  <ci>star</ci>
 </apply>
</math>

Prefix

eq (semigroup_operation (semigroup ( S, star) ) , star)

Popcorn

algebraic_cats.semigroup_operation(algebraic_cats.semigroup($S, $star)) = $star

Rendered Presentation MathML

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

Signatures:

sts

Abelian_semigroup

Description:

This symbol is the constructor for an Abelian semigroup, that is a semigroup which has an operator which is commutative over the set of the semigroup. The Abelian semigroup constructor takes two arguments, the set of the Abelian semigroup and a binary function which represents the operation of the Abelian semigroup.

Commented Mathematical property (CMP):

This constructor may be used to build Abelian semigroups

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">Abelian_semigroup</csymbol><ci>S</ci><ci>star</ci></apply>
  <csymbol cd="generic_alg_cats">Abelian_semigroup</csymbol>
 </apply>
</math>

Prefix

in (Abelian_semigroup ( S, star) , Abelian_semigroup)

Popcorn

set1.in(algebraic_cats.Abelian_semigroup($S, $star), generic_alg_cats.Abelian_semigroup)

Rendered Presentation MathML

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

Commented Mathematical property (CMP):

If (S,*) comprises an Abelian semigroup, then for all a,b in S|a*b=b*a

Formal Mathematical property (FMP):

OpenMath XML (source)

  <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_semigroup"/>
      </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_semigroup"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMA cd="generic_alg_cats" name="Abelian_semigroup"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="relation1" name="eq"/>
            <OMA>
              <OMA>
                <OMS cd="algebraic_cats" name="Abelian_semigroup_operation"/>
                <OMV name="S"/>
              </OMA>
              <OMV name="a"/>
              <OMV name="b"/>
            </OMA>
            <OMA>
              <OMA>
                <OMS cd="algebraic_cats" name="Abelian_semigroup_operation"/>
                <OMV name="S"/>
              </OMA>
              <OMV name="b"/>
              <OMV name="a"/>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
    </OMA>
  </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">Abelian_semigroup</csymbol></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>a</ci>
     <apply><apply/><ci>S</ci></apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>b</ci>
     <apply><apply/><ci>S</ci></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply>
      <apply><csymbol cd="algebraic_cats">Abelian_semigroup_operation</csymbol><ci>S</ci></apply>
      <ci>a</ci>
      <ci>b</ci>
     </apply>
     <apply>
      <apply><csymbol cd="algebraic_cats">Abelian_semigroup_operation</csymbol><ci>S</ci></apply>
      <ci>b</ci>
      <ci>a</ci>
     </apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (in ( S, Abelian_semigroup) , forall [ a b ] . (and (in ( a, () ( S) ) , in ( b, () ( S) ) , eq (Abelian_semigroup_operation ( S) ( a, b) , Abelian_semigroup_operation ( S) ( b, a) ) ) ) )

Popcorn

set1.in($S, generic_alg_cats.Abelian_semigroup) ==> quant1.forall[$a, $b -> set1.in($a, ()($S)) and set1.in($b, ()($S)) and algebraic_cats.Abelian_semigroup_operation($S)($a, $b) = algebraic_cats.Abelian_semigroup_operation($S)($b, $a)]

Rendered Presentation MathML

$$S\in \mathrm{Abelian\_semigroup}\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\_semigroup\_operation}\left(S\right)\right)(a,b)=\left(\mathrm{Abelian\_semigroup\_operation}\left(S\right)\right)(b,a)$$

Signatures:

sts

Abelian_semigroup_set

Description:

This symbol takes one argument which should be an Abelian semigroup. It returns a set, which should be the set of the Abelian semigroup.

Commented Mathematical property (CMP):

The set of the Abelian semigroup (S,*) = S

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">Abelian_semigroup_set</csymbol>
   <apply><csymbol cd="algebraic_cats">Abelian_semigroup</csymbol><ci>S</ci><ci>star</ci></apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

eq (Abelian_semigroup_set (Abelian_semigroup ( S, star) ) , S)

Popcorn

algebraic_cats.Abelian_semigroup_set(algebraic_cats.Abelian_semigroup($S, $star)) = $S

Rendered Presentation MathML

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

Signatures:

sts

Abelian_semigroup_operation

Description:

This symbol takes one argument which should be an Abelian semigroup. It returns a binary function, which should represent the operation of the Abelian semigroup.

Commented Mathematical property (CMP):

The operation of the Abelian semigroup (S,*) = *

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">Abelian_semigroup_operation</csymbol>
   <apply><csymbol cd="algebraic_cats">Abelian_semigroup</csymbol><ci>S</ci><ci>star</ci></apply>
  </apply>
  <ci>star</ci>
 </apply>
</math>

Prefix

eq (Abelian_semigroup_operation (Abelian_semigroup ( S, star) ) , star)

Popcorn

algebraic_cats.Abelian_semigroup_operation(algebraic_cats.Abelian_semigroup($S, $star)) = $star

Rendered Presentation MathML

$$\mathrm{Abelian\_semigroup\_operation}\left(\mathrm{Abelian\_semigroup}(S,\mathrm{star})\right)=\mathrm{star}$$

Signatures:

sts

This symbol is an alternative model for the symbol declare_group in
the CD group1

group

Description:

This symbol is the constructor for groups, that is a monoid for which every element is invertible. The group constructor takes four arguments, the set of the group, a binary function taking two elements of the set into itself to represent the operation of the group, an element of the set to represent the identity of the group and a unary function taking the set into itself to specify inverse elements of the group.

Commented Mathematical property (CMP):

This symbol may be used to build groups

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">group</csymbol><ci>S</ci><ci>star</ci></apply>
  <csymbol cd="generic_alg_cats">group</csymbol>
 </apply>
</math>

Prefix

in (group ( S, star) , group)

Popcorn

set1.in(algebraic_cats.group($S, $star), generic_alg_cats.group)

Rendered Presentation MathML

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

Commented Mathematical property (CMP):

if (S,*,1,inv:S->S) comprises a group then for all a in S | inv(a) is a member of S and inv(a)*a=a*inv(a)=1

Formal Mathematical property (FMP):

OpenMath XML (source)

  <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="group"/>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="forall"/>
        <OMBVAR>
          <OMV name="a"/>
        </OMBVAR>
        <OMA>
          <OMS cd="logic1" name="implies"/>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="algebraic_cats" name="group_set"/>
              <OMV name="S"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="logic1" name="and"/>
            <OMA>
              <OMS cd="logic1" name="in"/>
              <OMV name="a"/>
              <OMA>
                <OMS cd="algebraic_cats" name="group_set"/>
                <OMV name="S"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="group_operation"/>
                  <OMV name="S"/>
                </OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="group_inverse"/>
                  <OMV name="a"/>
                </OMA>
                <OMV name="a"/>
              </OMA>
              <OMA>
                <OMS cd="algebraic_cats" name="group_identity"/>
                <OMV name="S"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="group_operation"/>
                  <OMV name="S"/>
                </OMA>
                <OMV name="a"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="group_inverse"/>
                  <OMV name="a"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="algebraic_cats" name="group_identity"/>
                <OMV name="S"/>
              </OMA>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
    </OMA>
  </OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">group</csymbol></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="algebraic_cats">group_set</csymbol><ci>S</ci></apply>
    </apply>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="logic1">in</csymbol>
      <ci>a</ci>
      <apply><csymbol cd="algebraic_cats">group_set</csymbol><ci>S</ci></apply>
     </apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply>
       <apply><csymbol cd="algebraic_cats">group_operation</csymbol><ci>S</ci></apply>
       <apply><csymbol cd="algebraic_cats">group_inverse</csymbol><ci>a</ci></apply>
       <ci>a</ci>
      </apply>
      <apply><csymbol cd="algebraic_cats">group_identity</csymbol><ci>S</ci></apply>
     </apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply>
       <apply><csymbol cd="algebraic_cats">group_operation</csymbol><ci>S</ci></apply>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">group_inverse</csymbol><ci>a</ci></apply>
      </apply>
      <apply><csymbol cd="algebraic_cats">group_identity</csymbol><ci>S</ci></apply>
     </apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (in ( S, group) , forall [ a ] . (implies (in ( a, group_set ( S) ) , and (in ( a, group_set ( S) ) , eq (group_operation ( S) (group_inverse ( a) , a) , group_identity ( S) ) , eq (group_operation ( S) ( a, group_inverse ( a) ) , group_identity ( S) ) ) ) ) )

Popcorn

set1.in($S, generic_alg_cats.group) ==> quant1.forall[$a -> set1.in($a, algebraic_cats.group_set($S)) ==> logic1.in($a, algebraic_cats.group_set($S)) and algebraic_cats.group_operation($S)(algebraic_cats.group_inverse($a), $a) = algebraic_cats.group_identity($S) and algebraic_cats.group_operation($S)($a, algebraic_cats.group_inverse($a)) = algebraic_cats.group_identity($S)]

Rendered Presentation MathML

$$S\in \mathrm{group}\Rightarrow \forall \hspace{0.17em}a.a\in \mathrm{group\_set}\left(S\right)\Rightarrow \mathrm{in}(a,\mathrm{group\_set}\left(S\right))\wedge \left(\mathrm{group\_operation}\left(S\right)\right)(\mathrm{group\_inverse}\left(a\right),a)=\mathrm{group\_identity}\left(S\right)\wedge \left(\mathrm{group\_operation}\left(S\right)\right)(a,\mathrm{group\_inverse}\left(a\right))=\mathrm{group\_identity}\left(S\right)$$

Signatures:

sts

group_set

Description:

This symbol takes one argument which should be a group. It returns a set, which should be the set of the group.

Commented Mathematical property (CMP):

The set of the group (S,*,1,inv) = S

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">group_set</csymbol>
   <apply><csymbol cd="algebraic_cats">group</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>inv</ci>
   </apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

eq (group_set (group ( S, star, id, inv) ) , S)

Popcorn

algebraic_cats.group_set(algebraic_cats.group($S, $star, $id, $inv)) = $S

Rendered Presentation MathML

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

Signatures:

sts

group_operation

Description:

This symbol takes one argument which should be a group. It returns a binary function, which represents the operation of the group.

Commented Mathematical property (CMP):

The operation of the group (S,*,1,inv) = *

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">group_operation</csymbol>
   <apply><csymbol cd="algebraic_cats">group</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>inv</ci>
   </apply>
  </apply>
  <ci>star</ci>
 </apply>
</math>

Prefix

eq (group_operation (group ( S, star, id, inv) ) , star)

Popcorn

algebraic_cats.group_operation(algebraic_cats.group($S, $star, $id, $inv)) = $star

Rendered Presentation MathML

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

Signatures:

sts

group_identity

Description:

This symbol takes one argument which should be a group. It returns the identity of the group.

Commented Mathematical property (CMP):

The identity of the group (S,*,1,inv) = 1

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">group_identity</csymbol>
   <apply><csymbol cd="algebraic_cats">group</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>inv</ci>
   </apply>
  </apply>
  <ci>id</ci>
 </apply>
</math>

Prefix

eq (group_identity (group ( S, star, id, inv) ) , id)

Popcorn

algebraic_cats.group_identity(algebraic_cats.group($S, $star, $id, $inv)) = $id

Rendered Presentation MathML

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

Signatures:

sts

group_inverse

Description:

This symbol takes one argument which should be a group. It returns a unary function, which is the inverse mapping for the group.

Commented Mathematical property (CMP):

The inverse of the group (S,*,1,inv) = inv

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">group_inverse</csymbol>
   <apply><csymbol cd="algebraic_cats">group</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>inv</ci>
   </apply>
  </apply>
  <ci>inv</ci>
 </apply>
</math>

Prefix

eq (group_inverse (group ( S, star, id, inv) ) , inv)

Popcorn

algebraic_cats.group_inverse(algebraic_cats.group($S, $star, $id, $inv)) = $inv

Rendered Presentation MathML

$$\mathrm{group\_inverse}\left(\mathrm{group}(S,\mathrm{star},\mathrm{id},\mathrm{inv})\right)=\mathrm{inv}$$

Signatures:

sts

ordered_group

Description:

This symbol is the constructor for ordered groups, that is a group on which there is an ordering relation. The ordered_group constructor takes five arguments, the set of the ordered group, a binary function taking two elements of the set into itself to represent the operation of the ordered group, an element of the set to represent the identity of the ordered group, a unary function taking the set into itself to specify inverse elements of the ordered group and a binary function taking two elements of the set into the booleans to specify the ordering of the ordered group.

Commented Mathematical property (CMP):

This constructor may be used to build ordered groups

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">in</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_group</csymbol>
   <ci>S</ci>
   <ci>star</ci>
   <ci>id</ci>
   <ci>inv</ci>
   <ci>leq</ci>
  </apply>
  <csymbol cd="generic_alg_cats">ordered_group</csymbol>
 </apply>
</math>

Prefix

in (ordered_group ( S, star, id, inv, leq) , ordered_group)

Popcorn

set1.in(algebraic_cats.ordered_group($S, $star, $id, $inv, $leq), generic_alg_cats.ordered_group)

Rendered Presentation MathML

$$\mathrm{ordered\_group}(S,\mathrm{star},\mathrm{id},\mathrm{inv},\mathrm{leq})\in \mathrm{ordered\_group}$$

Commented Mathematical property (CMP):

if (S,*,1,inv:S->S,\leq) represents an ordered group, 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):

OpenMath XML (source)

  <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_group" 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_group_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="b"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="logic1" name="or"/>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_order"/>
                  <OMV name="S"/>
                </OMA>
                <OMV name="a"/>
                <OMV name="b"/>
              </OMA>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_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_group_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="b"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="c"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_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_group_order"/>
                    <OMV name="S"/>
                  </OMA>
                  <OMV name="a"/>
                  <OMV name="b"/>
                </OMA>
                <OMA>
                  <OMA>
                    <OMS cd="algebraic_cats" name="ordered_group_order"/>
                    <OMV name="S"/>
                  </OMA>
                  <OMV name="b"/>
                  <OMV name="c"/>
                </OMA>
              </OMA>
              <OMA>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_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_group_set"/>
                  <OMV name="S"/>
                </OMA>
              </OMA>
              <OMA>
                <OMS cd="set1" name="in"/>
                <OMV name="b"/>
                <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_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_group_order"/>
                    <OMV name="S"/>
                  </OMA>
                  <OMV name="a"/>
                  <OMV name="b"/>
                </OMA>
                <OMA>
                  <OMA>
                    <OMS cd="algebraic_cats" name="ordered_group_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>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="set1">in</csymbol><ci>S</ci><csymbol cd="generic_alg_cats">ordered_group</csymbol></apply>
  <apply><csymbol cd="logic1">and</csymbol>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_group_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_group_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">or</csymbol>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_group_order</csymbol><ci>S</ci></apply>
       <ci>a</ci>
       <ci>b</ci>
      </apply>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_group_order</csymbol><ci>S</ci></apply>
       <ci>b</ci>
       <ci>a</ci>
      </apply>
     </apply>
    </apply>
   </bind>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <bvar><ci>c</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_group_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_group_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>c</ci>
       <apply><csymbol cd="algebraic_cats">ordered_group_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_group_order</csymbol><ci>S</ci></apply>
        <ci>a</ci>
        <ci>b</ci>
       </apply>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_group_order</csymbol><ci>S</ci></apply>
        <ci>b</ci>
        <ci>c</ci>
       </apply>
      </apply>
      <apply>
       <apply><csymbol cd="algebraic_cats">ordered_group_order</csymbol><ci>S</ci></apply>
       <ci>a</ci>
       <ci>c</ci>
      </apply>
     </apply>
    </apply>
   </bind>
   <bind><csymbol cd="quant1">forall</csymbol>
    <bvar><ci>a</ci></bvar>
    <bvar><ci>b</ci></bvar>
    <apply><csymbol cd="logic1">implies</csymbol>
     <apply><csymbol cd="logic1">and</csymbol>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>a</ci>
       <apply><csymbol cd="algebraic_cats">ordered_group_set</csymbol><ci>S</ci></apply>
      </apply>
      <apply><csymbol cd="set1">in</csymbol>
       <ci>b</ci>
       <apply><csymbol cd="algebraic_cats">ordered_group_set</csymbol><ci>S</ci></apply>
      </apply>
     </apply>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="logic1">and</csymbol>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_group_order</csymbol><ci>S</ci></apply>
        <ci>a</ci>
        <ci>b</ci>
       </apply>
       <apply>
        <apply><csymbol cd="algebraic_cats">ordered_group_order</csymbol><ci>S</ci></apply>
        <ci>b</ci>
        <ci>a</ci>
       </apply>
      </apply>
      <apply><csymbol cd="relation1">eq</csymbol><ci>a</ci><ci>b</ci></apply>
     </apply>
    </apply>
   </bind>
  </apply>
 </apply>
</math>

Prefix

implies (in ( S, ordered_group) , and (forall [ a b ] . (implies (and (in ( a, ordered_group_set ( S) ) , in ( b, ordered_group_set ( S) ) ) , or (ordered_group_order ( S) ( a, b) , ordered_group_order ( S) ( b, a) ) ) ) , forall [ a b c ] . (implies (and (in ( a, ordered_group_set ( S) ) , in ( b, ordered_group_set ( S) ) , in ( c, ordered_group_set ( S) ) ) , implies (and (ordered_group_order ( S) ( a, b) , ordered_group_order ( S) ( b, c) ) , ordered_group_order ( S) ( a, c) ) ) ) , forall [ a b ] . (implies (and (in ( a, ordered_group_set ( S) ) , in ( b, ordered_group_set ( S) ) ) , implies (and (ordered_group_order ( S) ( a, b) , ordered_group_order ( S) ( b, a) ) , eq ( a, b) ) ) ) ) )

Popcorn

set1.in($S, generic_alg_cats.ordered_group) ==> quant1.forall[$a, $b -> set1.in($a, algebraic_cats.ordered_group_set($S)) and set1.in($b, algebraic_cats.ordered_group_set($S)) ==> algebraic_cats.ordered_group_order($S)($a, $b) > algebraic_cats.ordered_group_order($S)($b, $a)] and quant1.forall[$a, $b, $c -> set1.in($a, algebraic_cats.ordered_group_set($S)) and set1.in($b, algebraic_cats.ordered_group_set($S)) and set1.in($c, algebraic_cats.ordered_group_set($S)) ==> algebraic_cats.ordered_group_order($S)($a, $b) and algebraic_cats.ordered_group_order($S)($b, $c) ==> algebraic_cats.ordered_group_order($S)($a, $c)] and quant1.forall[$a, $b -> set1.in($a, algebraic_cats.ordered_group_set($S)) and set1.in($b, algebraic_cats.ordered_group_set($S)) ==> algebraic_cats.ordered_group_order($S)($a, $b) and algebraic_cats.ordered_group_order($S)($b, $a) ==> $a = $b]

Rendered Presentation MathML

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

Signatures:

sts

ordered_group_set

Description:

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

Commented Mathematical property (CMP):

The set of the ordered group (S,*,1,inv,leq) = S

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_group_set</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_group</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>inv</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci>S</ci>
 </apply>
</math>

Prefix

eq (ordered_group_set (ordered_group ( S, star, id, inv, leq) ) , S)

Popcorn

algebraic_cats.ordered_group_set(algebraic_cats.ordered_group($S, $star, $id, $inv, $leq)) = $S

Rendered Presentation MathML

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

Signatures:

sts

ordered_group_operation

Description:

This symbol takes one argument which should be an ordered group. It returns a binary function, which represents the operation of the ordered group.

Commented Mathematical property (CMP):

The operation of the ordered group (S,*,1,inv,leq) = *

Formal Mathematical property (FMP):

OpenMath XML (source)

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

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="algebraic_cats">ordered_group_operation</csymbol>
   <apply><csymbol cd="algebraic_cats">ordered_group</csymbol>
    <ci>S</ci>
    <ci>star</ci>
    <ci>id</ci>
    <ci>inv</ci>
    <ci>leq</ci>
   </apply>
  </apply>
  <ci/>
 </apply>
</math>

Prefix

eq (ordered_group_operation (ordered_group ( S, star, id, inv, leq) ) , )

Popcorn

algebraic_cats.ordered_group_operation(algebraic_cats.ordered_group($S, $star, $id, $inv, $leq)) = $

Rendered Presentation MathML

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