algebraic_cats.omcd

<OMOBJ xmlns:om="http://www.openmath.org/OpenMath"
       xmlns="http://www.openmath.org/OpenMath">
   <OMA>
      <OMS cd="meta" name="CD"/>
      <OMA>
         <OMS cd="meta" name="CDComment"/>
         <OMSTR>This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDName"/>
         <OMSTR>algebraic_cats</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDURL"/>
         <OMSTR>http://www.openmath.org/cd/algebraic_cats.ocd</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDReviewDate"/>
         <OMSTR>2017-12-31</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDStatus"/>
         <OMSTR>experimental</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDate"/>
         <OMSTR>2002-06-17</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDVersion"/>
         <OMSTR>0</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDRevision"/>
         <OMSTR>3</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDComment"/>
         <OMSTR>Author: J B Collins</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDComment"/>
         <OMSTR>Author: Bill Naylor</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="Description"/>
         <OMSTR>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.</OMSTR>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>monoid</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor may be used to build monoids</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,1) comprises a monoid then for all a,b,c in S | a*(b*c)=(a*b)*c</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>the operation of the monoid is closed over the set of the monoid</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,1) is a monoid then there exists a unique identity element in S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>the set of a monoid must contain at least one element</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>monoid_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a monoid, it returns the set of the monoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the monoid (S,*,1) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>monoid_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a monoid, it returns the operation of the monoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the monoid (S,*,1) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>monoid_identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a monoid, it returns the identity of the monoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The identity of the monoid (S,*,1) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_monoid</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor may be used to build Abelian_monoids</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,1) comprises an Abelian monoid then for all a,b in S | a*b=b*a</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
                           <OMS cd="generic_alg_cats" name="Abelian_monoid"/>
                           <OMV name="S"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="set1" name="in"/>
                        <OMV name="b"/>
                        <OMA>
                           <OMS 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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_monoid_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an Abelian monoid, it returns the set of the Abelian monoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the Abelian monoid (S,*,1) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_monoid_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an Abelian monoid, it returns the operation of the Abelian monoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the Abelian monoid (S,*,1)= *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_monoid_identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an Abelian monoid, it returns the identity of the Abelian monoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The identity of the Abelian monoid (S,*,1) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_monoid</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor may be used to build ordered monoids</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>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</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_monoid_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered monoid. It returns a set which should be the set of the ordered monoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the ordered monoid (S,*,1,\leq) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_monoid_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the ordered monoid (S,*,1,\leq) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_monoid_identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The identity of the ordered monoid (S,*,1,\leq) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_monoid_order</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The order of the ordered monoid (S,*,1,\leq) = \leq</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_monoid</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor may be used to build ordered Abelian monoids</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>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</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_monoid_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the ordered Abelian monoid (S,*,1,/leq) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_monoid_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the ordered Abelian monoid (S,*,1,/leq) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_monoid_identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The identity of the ordered Abelian monoid (S,*,1,/leq) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_monoid_order</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The ordering of the ordered Abelian monoid (S,*,1,/leq) = /leq</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>groupoid</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor may be used to build groupoids</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*) comprises a groupoid, then for all a,b in S | a*b is a member of S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
                        <OMS 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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>groupoid_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a groupoid. It returns the set of the groupoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the groupoid (S,*) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>groupoid_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a groupoid. It returns a binary function which should represent the operation of the groupoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the groupoid (S,*) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>semigroup</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor may be used to build semigroups</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*) comprises a semigroup then for all a,b,c in S | a*(b*c)=(a*b)*c</OMSTR>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>semigroup_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a semigroup. It returns the set of the semigroup.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the semigroup (S,*) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>semigroup_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a semigroup. It returns a binary function which should represent the operation of the semigroup.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the semigroup (S,*) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_semigroup</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor may be used to build Abelian semigroups</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>If (S,*) comprises an Abelian semigroup, then for all a,b in S|a*b=b*a</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
                           <OMS cd="generic_alg_cats" name="Abelian_semigroup"/>
                           <OMV name="S"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="set1" name="in"/>
                        <OMV name="b"/>
                        <OMA>
                           <OMS 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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_semigroup_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an Abelian semigroup. It returns a set, which should be the set of the Abelian semigroup.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the Abelian semigroup (S,*) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_semigroup_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the Abelian semigroup (S,*) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="CDComment"/>
            <OMSTR>This symbol is an alternative model for the symbol declare_group in the CD group1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>group</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This symbol may be used to build groups</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,1,inv:S-&gt;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</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>group_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a group. It returns a set, which should be the set of the group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the group (S,*,1,inv) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>group_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a group. It returns a binary function, which represents the operation of the group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the group (S,*,1,inv) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>group_identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a group. It returns the identity of the group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The identity of the group (S,*,1,inv) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>group_inverse</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a group. It returns a unary function, which is the inverse mapping for the group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The inverse of the group (S,*,1,inv) = inv</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_group</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>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.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor may be used to build ordered groups</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,1,inv:S-&gt;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</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_group_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered group. It returns the set of the ordered group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the ordered group (S,*,1,inv,leq) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_group_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered group. It returns a binary function, which represents the operation of the ordered group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the ordered group (S,*,1,inv,leq) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <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="missing"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_group_identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered group. It returns the identity of the ordered group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The identity of the ordered group (S,*,1,inv,leq) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_identity"/>
                  <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="id"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_group_inverse</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered group. It returns a unary function, which is the inverse function of the ordered group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The inverse of the ordered group (S,*,1,inv,leq) = inv</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_inverse"/>
                  <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="inv"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_group_order</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered group. It returns a binary function, which represents the ordering of the ordered group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The order of the ordered group (S,*,1,inv,leq) = leq</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_group_order"/>
                  <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="leq"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_group</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for Abelian groups, that is a group such that the operation is commutative between members of the group. The Abelian_group constructor takes four arguments, the set of the Abelian group, a binary function taking two elements of the set into itself to represent the operation of the Abelian group, an element of the set to represent the identity of the Abelian group and a unary function taking the set into itself to specify inverse elements.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor builds Abelian groups</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Abelian_group"/>
                  <OMV name="S"/>
                  <OMV name="star"/>
                  <OMV name="id"/>
                  <OMV name="inv"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="Abelian_group"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,1,inv) comprises an Abelian group then for all a,b in S | a*b = b*a</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="Abelian_group"/>
               </OMA>
               <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="Abelian_group_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="set1" name="in"/>
                           <OMV name="b"/>
                           <OMA>
                              <OMS cd="algebraic_cats" name="Abelian_group_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="relation1" name="eq"/>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="Abelian_group_operation"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMV name="a"/>
                           <OMV name="b"/>
                        </OMA>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="Abelian_group_operation"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMV name="b"/>
                           <OMV name="a"/>
                        </OMA>
                     </OMA>
                  </OMA>
               </OMBIND>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_group_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an Abelian group. It returns the set of the Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the Abelian group (S,*,1,inv) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Abelian_group_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_group_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an Abelian group. It returns a binary function, which represents the operation of the Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the Abelian group (S,*,1,inv) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Abelian_group_operation"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                  </OMA>
               </OMA>
               <OMV name="star"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_group_identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an Abelian group. It returns the identity of the Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The identity of the Abelian group (S,*,1,inv) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Abelian_group_identity"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                  </OMA>
               </OMA>
               <OMV name="id"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Abelian_group_inverse</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an Abelian group. It reurns a unary function, which should be the inverse function for the Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The inverse of the Abelian group (S,*,1,inv) = inv</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Abelian_group_inverse"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                  </OMA>
               </OMA>
               <OMV name="inv"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_group</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for ordered Abelian groups, that is an Abelian group on which there is an ordering relation. The ordered_Abelian_group constructor takes five arguments, the set of the ordered Abelian group, a binary function taking two elements of the set into itself to represent the operation of the ordered Abelian group, an element of the set to represent the identity of the ordered Abelian group, a unary function taking the set into itself to specify inverse elements and a binary function taking two elements of the set into the booleans to specify the ordering of the ordered Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor builds ordered Abelian groups</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_group"/>
                  <OMV name="S"/>
                  <OMV name="star"/>
                  <OMV name="id"/>
                  <OMV name="inv"/>
                  <OMV name="leq"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="ordered_Abelian_group"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,1,inv:S-&gt;S,\leq) represents an ordered Abelian 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</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS name="ordered_Abelian_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_Abelian_group_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_Abelian_group_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="logic1" name="or"/>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_Abelian_group_order"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="a"/>
                              <OMV name="b"/>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_Abelian_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_Abelian_group_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_Abelian_group_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="c"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_Abelian_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_Abelian_group_order"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="a"/>
                                 <OMV name="b"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ordered_Abelian_group_order"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="b"/>
                                 <OMV name="c"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_Abelian_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_Abelian_group_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_Abelian_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_Abelian_group_order"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="a"/>
                                 <OMV name="b"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ordered_Abelian_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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_group_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered Abelian group. It returns the set of the ordered Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the ordered Abelian group (S,*,1,inv,leq) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_group_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_group_operation</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered Abelian group. It returns a binary function, which represents the operation of the ordered Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The operation of the ordered Abelian group (S,*,1,inv,leq) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_group_operation"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="star"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_group_identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered Abelian group. It returns the identity of the ordered Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The identity of the ordered Abelian group (S,*,1,inv,leq) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_group_identity"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="id"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_group_inverse</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered Abelian group. It returns a unary function, which is the inverse function of the ordered Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The inverse of the ordered Abelian group (S,*,1,inv,leq) = inv</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_group_inverse"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="inv"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_Abelian_group_order</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered Abelian group. It returns a binary function, which should represent the ordering of the ordered Abelian group.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The order of the ordered Abelian group (S,*,1,inv,leq) = leq</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_Abelian_group_order"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_Abelian_group"/>
                     <OMV name="S"/>
                     <OMV name="star"/>
                     <OMV name="id"/>
                     <OMV name="inv"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="leq"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ringoid</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for ringoids. A ringoid is a set together with two operations + and *. * is left and right distributive over +. The ringoid constructor takes three arguments, the set of the ringoid, a binary function from the set into itself to represent the * operation and a binary function from the set into itself to represent the + operation.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The ringoid constructor builds ringoids</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ringoid"/>
                  <OMV name="S"/>
                  <OMV name="times"/>
                  <OMV name="plus"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="ringoid"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (a,*,+) comprises a ringoid then for all a,b,c in S | a*(b+c) = a*b+a*c</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="ringoid"/>
               </OMA>
               <OMBIND>
                  <OMS cd="quant1" name="forall"/>
                  <OMBVAR>
                     <OMV name="a"/>
                     <OMV name="b"/>
                     <OMV name="c"/>
                  </OMBVAR>
                  <OMA>
                     <OMS cd="logic1" name="and"/>
                     <OMA>
                        <OMS cd="set1" name="in"/>
                        <OMV name="a"/>
                        <OMA>
                           <OMS cd="algebraic_cats" name="ringoid_set"/>
                           <OMV name="S"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="set1" name="in"/>
                        <OMV name="b"/>
                        <OMA>
                           <OMS cd="algebraic_cats" name="ringoid_set"/>
                           <OMV name="S"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="set1" name="in"/>
                        <OMV name="c"/>
                        <OMA>
                           <OMS cd="algebraic_cats" name="ringoid_set"/>
                           <OMV name="S"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="relation1" name="eq"/>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="ringoid_times"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMV name="a"/>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ringoid_plus"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="b"/>
                              <OMV name="c"/>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="ringoid_plus"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ringoid_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="a"/>
                              <OMV name="b"/>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ringoid_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="a"/>
                              <OMV name="c"/>
                           </OMA>
                        </OMA>
                     </OMA>
                  </OMA>
               </OMBIND>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>(b+c)*a = b*a+c*a</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="ringoid"/>
               </OMA>
               <OMBIND>
                  <OMS cd="quant1" name="forall"/>
                  <OMBVAR>
                     <OMV name="a"/>
                     <OMV name="b"/>
                     <OMV name="c"/>
                  </OMBVAR>
                  <OMA>
                     <OMS cd="logic1" name="and"/>
                     <OMA>
                        <OMS cd="set1" name="in"/>
                        <OMV name="a"/>
                        <OMA>
                           <OMS cd="algebraic_cats" name="ringoid_set"/>
                           <OMV name="S"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="set1" name="in"/>
                        <OMV name="b"/>
                        <OMA>
                           <OMS cd="algebraic_cats" name="ringoid_set"/>
                           <OMV name="S"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="set1" name="in"/>
                        <OMV name="c"/>
                        <OMA>
                           <OMS cd="algebraic_cats" name="ringoid_set"/>
                           <OMV name="S"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="relation1" name="eq"/>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="ringoid_times"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ringoid_plus"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="b"/>
                              <OMV name="c"/>
                           </OMA>
                           <OMV name="a"/>
                        </OMA>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="ringoid_plus"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ringoid_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="b"/>
                              <OMV name="a"/>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ringoid_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="c"/>
                              <OMV name="a"/>
                           </OMA>
                        </OMA>
                     </OMA>
                  </OMA>
               </OMBIND>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ringoid_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a ringoid. It returns a set which represents the set of the ringoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the ringoid (S,*,+) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ringoid_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ringoid"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ringoid_times</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a ringoid. It returns a binary function which represents the multiplicative operation (*) of the ringoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The mulitplication operation of the ringoid (S,*,+) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ringoid_times"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ringoid"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                  </OMA>
               </OMA>
               <OMV name="times"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ringoid_plus</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a ringoid. It returns a binary function which represents the additive operation (+) of the ringoid.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The addition operation of the ringoid (S,*,+) = +</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ringoid_plus"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ringoid"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                  </OMA>
               </OMA>
               <OMV name="plus"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ring</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for rings. A ring is a set together with two operations + and *. A ring is an Abelian group under + and a semigroup under *. A ring has a further rule which associates the two operation, that is left and right distributivity. The ring constructor takes five arguments, the set of the ring, a binary function from the set into itself to represent the * operation, a binary function from the set into itself to represent the + operation, an element of the set of the ring to represent the additive identity 0 and a unary function from the set into itself to represent additive inverses (i.e. inverses under +, or negatives).</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor builds rings</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ring"/>
                  <OMV name="S"/>
                  <OMV name="times"/>
                  <OMV name="plus"/>
                  <OMV name="zero"/>
                  <OMV name="neg"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="ring"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>A ring is a ringoid</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,+,0,neg:S-&gt;S) comprises a ring then * is both left and right distributive over +. That is: For all a,b,c in S, a*(b+c)=(a*b)+(a*c) and (b+c)*a=(b*a)+(c*a)</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="ring"/>
               </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 cd="algebraic_cats" name="ring_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="set1" name="in"/>
                           <OMV name="b"/>
                           <OMA>
                              <OMS cd="algebraic_cats" name="ring_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="set1" name="in"/>
                           <OMV name="c"/>
                           <OMA>
                              <OMS cd="algebraic_cats" name="ring_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="logic1" name="and"/>
                        <OMA>
                           <OMS cd="relation1" name="eq"/>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ring_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="a"/>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ring_plus"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="b"/>
                                 <OMV name="c"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ring_plus"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ring_times"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="a"/>
                                 <OMV name="b"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ring_times"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="a"/>
                                 <OMV name="c"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ring_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ring_plus"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="b"/>
                                 <OMV name="c"/>
                              </OMA>
                              <OMV name="a"/>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ring_plus"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ring_times"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="b"/>
                                 <OMV name="a"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ring_times"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="c"/>
                                 <OMV name="a"/>
                              </OMA>
                           </OMA>
                        </OMA>
                     </OMA>
                  </OMA>
               </OMBIND>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ring_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a ring. It returns the set of the ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the ring (S,*,+,0,neg) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ring_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ring_times</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a ring. It returns a binary function which represents the multiplicative operation of the ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The times of the ring (S,*,+,0,neg) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ring_times"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="times"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ring_plus</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a ring. It returns a binary function which represents the additive operation of the ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The plus of the ring (S,*,+,0,neg) = +</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ring_plus"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="plus"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ring_zero</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a ring. It returns the additive identity of the ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The zero of the ring (S,*,+,0,neg) = 0</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ring_zero"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="zero"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ring_negative</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a ring. It returns a unary function which should be the negative function of the ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The negative function of the ring (S,*,+,0,neg) = neg</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ring_negative"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="neg"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_ring</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for ordered rings, that is a ring on which there is an ordering relation. The ordered_ring constructor takes six arguments, the set of the ordered ring, a binary function from the set into itself to represent the multiplicative operation (*), a binary function from the set into itself to represent the additive operation (+), an element of the set of the ordered ring to represent the additive identity 0, a unary function from the set into itself to represent additive inverses (i.e. inverses under +, or negatives) and a binary function from the set into the booleans to represent the ordering relation.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor builds ordered rings</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_ring"/>
                  <OMV name="S"/>
                  <OMV name="times"/>
                  <OMV name="plus"/>
                  <OMV name="zero"/>
                  <OMV name="neg"/>
                  <OMV name="leq"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="ordered_ring"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,+,0,neg:S-&gt;S,\leq) constitutes an ordered ring, 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</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS name="ordered_ring" 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_ring_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_ring_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="logic1" name="or"/>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_ring_order"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="a"/>
                              <OMV name="b"/>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_ring_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_ring_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_ring_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="c"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_ring_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_ring_order"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="a"/>
                                 <OMV name="b"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ordered_ring_order"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="b"/>
                                 <OMV name="c"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_ring_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_ring_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="ordered_ring_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_ring_order"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="a"/>
                                 <OMV name="b"/>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="ordered_ring_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>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_ring_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered ring. It returns the set of the ordered ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the ordered ring (S,*,+,0,-,leq) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_ring_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_ring_times</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the multiplicative operation of the ordered ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The times of the ordered ring (S,*,+,0,-,leq) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_ring_times"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="times"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_ring_plus</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the additive operation of the ordered ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The + of the ordered ring (S,*,+,0,-,leq) = +</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_ring_plus"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="plus"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_ring_zero</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered ring. It returns the zero of the ordered ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The zero of the ordered ring (S,*,+,0,-,leq) = 0</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_ring_zero"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="zero"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_ring_negative</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered ring. It returns a unary function to represent the additive inverse function of the ordered ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The negative of the ordered ring (S,*,+,0,-,leq) = -</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_ring_negative"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="neg"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>ordered_ring_order</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the order function on the ordered ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The order of the ordered ring (S,*,+,0,-,leq) = leq</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="ordered_ring_order"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="ordered_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="leq"/>
                  </OMA>
               </OMA>
               <OMV name="leq"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>non_commutative_ring</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for non commutative rings, these are rings over which the * operator is not commutative. the non_commutative_ring constructor takes five arguments: The set of the non-commutative ring. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the non-commutative ring to specify the additive identity, 0. And a unary function taking the set of the non-commutative ring into itself to represent the additive inverses of the non-commutative ring (i.e. inverses under +, or negatives).</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor builds non-commutative rings</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="non_commutative_ring"/>
                  <OMV name="S"/>
                  <OMV name="times"/>
                  <OMV name="plus"/>
                  <OMV name="zero"/>
                  <OMV name="neg"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="non_commutative_ring"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,+,0,neg:S-&gt;S) constitutes a non-commutative ring, then there exist a,b in S such that a*b~=b*a</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="non_commutative_ring"/>
               </OMA>
               <OMBIND>
                  <OMS cd="quant1" name="exists"/>
                  <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="non_commutative_ring_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="set1" name="in"/>
                           <OMV name="b"/>
                           <OMA>
                              <OMS cd="algebraic_cats" name="non_commutative_ring_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="relation1" name="neq"/>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="non_commutative_ring_times"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMV name="a"/>
                           <OMV name="b"/>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="non_commutative_ring_times"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMV name="b"/>
                           <OMV name="a"/>
                        </OMA>
                     </OMA>
                  </OMA>
               </OMBIND>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>non_commutative_ring_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a non-commutative ring. It returns the set of the non-commutative ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the non-commutative ring (S,*,+,0,-) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="non_commutative_ring_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="non_commutative_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>non_commutative_ring_times</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a non-commutative ring. It returns a binary function, which represents the multiplicative function of the non-commutative ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The times of the non-commutative ring (S,*,+,0,-) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="non_commutative_ring_times"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="non_commutative"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="times"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>non_commutative_ring_plus</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a non-commutative ring. It returns a binary function, which represents the additive function of the non-commutative ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The plus of the non-commutative ring (S,*,+,0,-) = +</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="non_commutative_ring_plus"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="non_commutative_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="plus"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>non_commutative_ring_zero</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a non-commutative ring. It returns the zero of the non-commutative ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The zero of the non-commutative ring (S,*,+,0,-) = 0</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="non_commutative_ring_zero"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="non_commutative_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="zero"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>non_commutative_ring_negative</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a non-commutative ring. It returns a unary function, which represents the multiplicative inverse of the non-commutative ring.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The negative of the non-commutative ring (S,*,+,0,-) = -</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="non_commutative_ring_negative"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="non_commutative_ring"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="neg"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Euclidean_domain</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for Euclidean domains. A Euclidean domain is a ring on which there is no zero divisors together with an integer norm function. The Euclidean_domain constructor takes six arguments: The set of the Euclidean domain. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the Euclidean domain to specify the additive identity, 0. A unary function taking the set of the Euclidean domain into itself to represent the additive inverses (i.e. inverses under +, or negatives). And a unary function taking elements of the set into the positive integers, to represent the integer norm function.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor builds Euclidean domains</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Euclidean_domain"/>
                  <OMV name="S"/>
                  <OMV name="times"/>
                  <OMV name="plus"/>
                  <OMV name="zero"/>
                  <OMV name="neg"/>
                  <OMV name="abs"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="Euclidean_domain"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>if (S,*,+,0,neg:S-&gt;S,abs:S-&gt;Z^+) constitutes a Euclidean domain then for every a,b ~= 0 in S then abs(a*b) &gt;= abs(a) and abs(a*b) &gt;= abs(b) and for every a,b ~= 0 in S then there exists q and r in S such that a=q*b + r and abs(r) &lt; abs(B) or r=0</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="Euclidean_domain"/>
               </OMA>
               <OMA>
                  <OMS cd="logic1" name="and"/>
                  <OMBIND>
                     <OMS cd="quant1" name="exists"/>
                     <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="Euclidean_domain_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="Euclidean_domain_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="relation1" name="neq"/>
                              <OMV name="a"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="Euclidean_domain_zero"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="relation1" name="neq"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="Euclidean_domain_zero"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="logic1" name="and"/>
                           <OMA>
                              <OMS cd="relation1" name="geq"/>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="Euclidean_domain_abs"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMA>
                                    <OMA>
                                       <OMS cd="algebraic_cats" name="Euclidean_domain_times"/>
                                       <OMV name="S"/>
                                    </OMA>
                                    <OMV name="a"/>
                                    <OMV name="b"/>
                                 </OMA>
                              </OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="Euclidean_domain_abs"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="a"/>
                           </OMA>
                           <OMA>
                              <OMS cd="relation1" name="geq"/>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="Euclidean_domain_abs"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMA>
                                    <OMA>
                                       <OMS cd="algebraic_cats" name="Euclidean_domain_times"/>
                                       <OMV name="S"/>
                                    </OMA>
                                    <OMV name="a"/>
                                    <OMV name="b"/>
                                 </OMA>
                              </OMA>
                              <OMA>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="Euclidean_domain_abs"/>
                                    <OMV name="S"/>
                                 </OMA>
                                 <OMV name="b"/>
                              </OMA>
                           </OMA>
                        </OMA>
                     </OMA>
                  </OMBIND>
                  <OMBIND>
                     <OMS cd="quant1" name="exists"/>
                     <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="Euclidean_domain_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="set1" name="in"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="Euclidean_domain_set"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="relation1" name="neq"/>
                              <OMV name="a"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="Euclidean_domain_zero"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMS cd="relation1" name="neq"/>
                              <OMV name="b"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="Euclidean_domain_zero"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                        </OMA>
                        <!--exists q and r in S such that a=q*b + r and abs(r) &lt; abs(b) or r=0--><OMBIND>
                           <OMS cd="quant1" name="exists"/>
                           <OMBVAR>
                              <OMV name="q"/>
                              <OMV name="r"/>
                           </OMBVAR>
                           <OMA>
                              <OMS cd="logic1" name="or"/>
                              <OMA>
                                 <OMS cd="relation1" name="eq"/>
                                 <OMV name="r"/>
                                 <OMA>
                                    <OMS cd="algebraic_cats" name="Euclidean_domain_zero"/>
                                    <OMV name="S"/>
                                 </OMA>
                              </OMA>
                              <OMA>
                                 <OMS cd="logic1" name="and"/>
                                 <OMA>
                                    <OMS cd="set1" name="in"/>
                                    <OMV name="q"/>
                                    <OMA>
                                       <OMS cd="algebraic_cats" name="Euclidean_domain_set"/>
                                       <OMV name="S"/>
                                    </OMA>
                                 </OMA>
                                 <OMA>
                                    <OMS cd="set1" name="in"/>
                                    <OMV name="r"/>
                                    <OMA>
                                       <OMS cd="algebraic_cats" name="Euclidean_domain_set"/>
                                       <OMV name="S"/>
                                    </OMA>
                                 </OMA>
                                 <OMA>
                                    <OMS cd="relation1" name="eq"/>
                                    <OMV name="a"/>
                                    <OMA>
                                       <OMA>
                                          <OMS cd="algebraic_cats" name="Euclidean_domain_plus"/>
                                          <OMV name="S"/>
                                       </OMA>
                                       <OMA>
                                          <OMA>
                                             <OMS cd="algebraic_cats" name="Euclidean_domain_times"/>
                                             <OMV name="S"/>
                                          </OMA>
                                          <OMV name="q"/>
                                          <OMV name="b"/>
                                       </OMA>
                                       <OMV name="r"/>
                                    </OMA>
                                 </OMA>
                                 <OMA>
                                    <OMS cd="relation1" name="lt"/>
                                    <OMA>
                                       <OMA>
                                          <OMS cd="algebraic_cats" name="Euclidean_domain_abs"/>
                                          <OMV name="S"/>
                                       </OMA>
                                       <OMV name="r"/>
                                    </OMA>
                                    <OMA>
                                       <OMA>
                                          <OMS cd="algebraic_cats" name="Euclidean_domain_abs"/>
                                          <OMV name="S"/>
                                       </OMA>
                                       <OMV name="b"/>
                                    </OMA>
                                 </OMA>
                              </OMA>
                           </OMA>
                        </OMBIND>
                     </OMA>
                  </OMBIND>
               </OMA>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Euclidean_domain_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a Euclidean domain. It returns the set of the Euclidean domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the Euclidean domain (S,*,+,0,-,abs) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Euclidean_domain_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Euclidean_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="abs"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Euclidean_domain_times</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a Euclidean domain. It returns a binary function, which represents the multiplicative operation of the Euclidean domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The times of the Euclidean domain (S,*,+,0,-,abs) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Euclidean_domain_times"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Euclidean_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="abs"/>
                  </OMA>
               </OMA>
               <OMV name="times"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Euclidean_domain_plus</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a Euclidean domain. It returns a binary function, which represents the additive operation of the Euclidean domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The plus of the Euclidean domain (S,*,+,0,-,abs) = +</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Euclidean_domain_plus"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Euclidean_domain_plus"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="abs"/>
                  </OMA>
               </OMA>
               <OMV name="plus"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Euclidean_domain_zero</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a Euclidean domain. It returns the additive identity of the Euclidean domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The zero of the Euclidean domain (S,*,+,0,-,abs) = 0</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Euclidean_domain_zero"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Euclidean_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="abs"/>
                  </OMA>
               </OMA>
               <OMV name="zero"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Euclidean_domain_negative</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a Euclidean domain. It returns a unary function, which represents additive inverses of the Euclidean domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The negative of the Euclidean domain (S,*,+,0,-,abs) = -</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Euclidean_domain_negative"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Euclidean_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="abs"/>
                  </OMA>
               </OMA>
               <OMV name="neg"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>Euclidean_domain_abs</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a Euclidean domain. It returns a unary function, which is the absolute value function of the Euclidean domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The absolute value function of the Euclidean domain (S,*,+,0,-,abs) = abs</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="Euclidean_domain_abs"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="Euclidean_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                     <OMV name="abs"/>
                  </OMA>
               </OMA>
               <OMV name="abs"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>field</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for fields. A field is an Abelian group under +, the set of the field complement {0} with * is an Abelian group, a field has a further rule which associates the two operations, that is left and right distributivity. The field constructor takes seven arguments: The set of the field. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the field to specify the multiplicative identity, 1. A member of the set of the field to specify the additive identity, 0. A unary function taking the set of the field into itself to represent the multiplicative inverses (i.e. inverses under *). A unary function taking the set of the field into itself to represent the additive inverses (i.e. inverses under +, or negatives).</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor builds fields</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="fields"/>
                  <OMV name="S"/>
                  <OMV name="times"/>
                  <OMV name="plus"/>
                  <OMV name="one"/>
                  <OMV name="zero"/>
                  <OMV name="inv"/>
                  <OMV name="neg"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="fields"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the field complement {0} with * is an Abelian group</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="field"/>
               </OMA>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMA>
                     <OMS cd="set1" name="setdiff"/>
                     <OMA>
                        <OMS cd="algebraic_cats" name="field_set"/>
                        <OMV name="S"/>
                     </OMA>
                     <OMA>
                        <OMS cd="set1" name="set"/>
                        <OMA>
                           <OMS cd="algebraic_cats" name="field_zero"/>
                        </OMA>
                     </OMA>
                  </OMA>
                  <OMS cd="generic_alg_cats" name="Abelian_group"/>
               </OMA>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>field_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a field. It returns the set of the field.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the field (S,*,+,1,0,inv,-) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="field_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="field"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="inv"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>field_times</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a field. It returns a binary function, to represent the multiplicative operation of the field.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The times of the field (S,*,+,1,0,inv,-) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="field_times"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="field"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="inv"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="times"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>field_plus</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a field. It returns a binary function, to represent the additive operation of the field.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The plus of the field (S,*,+,1,0,inv,-) = +</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="field_plus"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="field"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="inv"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="plus"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>field_one</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a field. It returns the multiplicative identity of the field.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The one of the field (S,*,+,1,0,inv,-) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="field_one"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="field"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="inv"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="one"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>field_zero</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a field. It returns the additive identity of the field.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The zero of the field (S,*,+,1,0,inv,-) = 0</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="field_zero"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="field"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="inv"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="zero"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>field_reciprocal</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a field. It returns a unary function, which is the multiplicative inverse function of the field.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The reciprocal of the field (S,*,+,1,0,inv,-) = inv</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="field_reciprocal"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="field"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="inv"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="inv"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>field_negative</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be a field. It returns a unary function, which is the additive inverse function of the field.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The negative of the field (S,*,+,1,0,inv,-) = -</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="field_negative"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="field"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="inv"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="neg"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>integral_domain</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol is the constructor for integral domains. An integral domain is a ring which is commutative under *, it has a multiplicative identity (under *), and has no zero divisors. The integral_domain constructor takes six arguments. The set of the integral domain, a binary function from the set into itself to represent the * operation, a binary function from the set into itself to represent the + operation, an element of the set of the ring to represent the multiplicative identity 1, an element of the set of the ring to represent the additive identity 0, and a unary function from the set into itself to represent additive inverses (i.e. inverses under +, or negatives).</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>This constructor builds integral domains</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="set1" name="in"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="integral_domain"/>
                  <OMV name="S"/>
                  <OMV name="times"/>
                  <OMV name="one"/>
                  <OMV name="plus"/>
                  <OMV name="zero"/>
                  <OMV name="neg"/>
               </OMA>
               <OMS cd="generic_alg_cats" name="integral_domain"/>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>An integral domain is commutative under *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="integral_domain"/>
               </OMA>
               <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="integral_domain_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="set1" name="in"/>
                           <OMV name="b"/>
                           <OMA>
                              <OMS cd="algebraic_cats" name="integral_domain_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                     </OMA>
                     <OMA>
                        <OMS cd="relation1" name="eq"/>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="integral_domain_times"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMV name="a"/>
                           <OMV name="b"/>
                        </OMA>
                        <OMA>
                           <OMA>
                              <OMS cd="algebraic_cats" name="integral_domain_times"/>
                              <OMV name="S"/>
                           </OMA>
                           <OMV name="b"/>
                           <OMV name="a"/>
                        </OMA>
                     </OMA>
                  </OMA>
               </OMBIND>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>An integral domain has a multiplicative identity</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="integral_domain"/>
               </OMA>
               <OMBIND>
                  <OMS cd="quant1" name="exists"/>
                  <OMBVAR>
                     <OMV name="id"/>
                  </OMBVAR>
                  <OMBIND>
                     <OMS cd="quant1" name="forall"/>
                     <OMBVAR>
                        <OMV name="x"/>
                     </OMBVAR>
                     <OMA>
                        <OMS cd="logic1" name="and"/>
                        <OMA>
                           <OMS cd="relation1" name="eq"/>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="integral_domain_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="id"/>
                              <OMV name="x"/>
                           </OMA>
                           <OMV name="x"/>
                        </OMA>
                        <OMA>
                           <OMS cd="relation1" name="eq"/>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="integral_domain_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="x"/>
                              <OMV name="id"/>
                           </OMA>
                           <OMV name="x"/>
                        </OMA>
                     </OMA>
                  </OMBIND>
               </OMBIND>
            </OMA>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>An integral domain has no zero divisors</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="logic1" name="implies"/>
               <OMA>
                  <OMS cd="set1" name="in"/>
                  <OMV name="S"/>
                  <OMS cd="generic_alg_cats" name="integral_domain"/>
               </OMA>
               <OMA>
                  <OMS cd="logic1" name="not"/>
                  <OMBIND>
                     <OMS cd="quant1" name="exists"/>
                     <OMBVAR>
                        <OMV name="zerodiv"/>
                     </OMBVAR>
                     <OMA>
                        <OMS cd="logic1" name="implies"/>
                        <OMA>
                           <OMS cd="set1" name="in"/>
                           <OMV name="x"/>
                           <OMA>
                              <OMS cd="algebraic_cats" name="integral_domain_set"/>
                              <OMV name="S"/>
                           </OMA>
                        </OMA>
                        <OMA>
                           <OMS cd="logic1" name="and"/>
                           <OMA>
                              <OMS cd="relation1" name="neq"/>
                              <OMV name="x"/>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="integral_domain_zero"/>
                                 <OMV name="S"/>
                              </OMA>
                           </OMA>
                           <OMA>
                              <OMA>
                                 <OMS cd="algebraic_cats" name="integral_domain_times"/>
                                 <OMV name="S"/>
                              </OMA>
                              <OMV name="zerodiv"/>
                              <OMV name="x"/>
                           </OMA>
                        </OMA>
                     </OMA>
                  </OMBIND>
               </OMA>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>integral_domain_set</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an integral domain. It returns the set of the integral domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The set of the integral domain (S,*,+,1,0,-) = S</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="integral_domain_set"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="integral_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="S"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>integral_domain_times</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an integral domain. It returns a binary function which represents the multiplicative operation of the integral domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The times of the integral domain (S,*,+,1,0,-) = *</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="integral_domain_times"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="integral_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="times"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>integral_domain_plus</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an integral domain. It returns a binary function which represents the additive operation of the integral domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The plus of the integral domain (S,*,+,1,0,-) = +</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="integral_domain_plus"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="integral_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="plus"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>integral_domain_one</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an integral domain. It returns the multiplicative identity of the integral domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The one of the integral domain (S,*,+,1,0,-) = 1</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="integral_domain_one"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="integral_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="one"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>integral_domain_zero</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an integral domain. It returns the additive identity of the integral domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The zero of the integral domain (S,*,+,1,0,-) = 0</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="integral_domain_zero"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="integral_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="zero"/>
            </OMA>
         </OMA>
      </OMA>
      <OMA>
         <OMS cd="meta" name="CDDefinition"/>
         <OMA>
            <OMS cd="meta" name="Name"/>
            <OMSTR>integral_domain_negative</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="Description"/>
            <OMSTR>This symbol takes one argument which should be an integral domain. It returns a unary function which represents the additive inverse function of the integral domain.</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="CMP"/>
            <OMSTR>The negative of the integral domain (S,*,+,1,0,-) = -</OMSTR>
         </OMA>
         <OMA>
            <OMS cd="meta" name="FMP"/>
            <OMA>
               <OMS cd="relation1" name="eq"/>
               <OMA>
                  <OMS cd="algebraic_cats" name="integral_domain_negative"/>
                  <OMA>
                     <OMS cd="algebraic_cats" name="integral_domain"/>
                     <OMV name="S"/>
                     <OMV name="times"/>
                     <OMV name="plus"/>
                     <OMV name="one"/>
                     <OMV name="zero"/>
                     <OMV name="neg"/>
                  </OMA>
               </OMA>
               <OMV name="neg"/>
            </OMA>
         </OMA>
      </OMA>
   </OMA>
</OMOBJ>