math/algebra/algebra1.omdoc

<?xml version="1.0" encoding="UTF-8"?>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" >
<!-- generated from Twelf sources by Florian Rabe -->
<theory name="Magma">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <constant name="*">
      <type>
         <om:OMOBJ>
            <om:OMA>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
               <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
               <om:OMA>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
               <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
               <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
            </om:OMA>
            </om:OMA>
         </om:OMOBJ>
      </type>
   </constant>
   <notation for="??*" role="application" fixity="in" associativity="none" precedence="100" implicit="0"/>

</theory>

<view name="OppositeMagma" from="?Magma" to="?Magma">

   <conass name="*">
      <om:OMOBJ>
         <om:OMBIND>
            <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
            <om:OMBVAR>
            <om:OMATTR><om:OMATP>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
               <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
               </om:OMATP><om:OMV name="x"/>
            </om:OMATTR>
         </om:OMBVAR>
            <om:OMBIND>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
               <om:OMBVAR>
               <om:OMATTR><om:OMATP>
                  <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                  <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                  </om:OMATP><om:OMV name="y"/>
               </om:OMATTR>
            </om:OMBVAR>
               <om:OMA>
                  <om:OMS name="*"/>
                  <om:OMV name="y"/>
                  <om:OMV name="x"/>
               </om:OMA>
            </om:OMBIND>
         </om:OMBIND>
      </om:OMOBJ>
   </conass>

</view>

<theory name="MagmaCommut">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <structure name="mag" from="?Magma"></structure><alias name="*" for="??mag/*"/>
   <constant name="commut">
      <type>
         <om:OMOBJ>
            <om:OMA>
               <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
               <om:OMA>
                  <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                        <om:OMBIND>
                           <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                           <om:OMBVAR>
                           <om:OMATTR><om:OMATP>
                              <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                              <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                              </om:OMATP><om:OMV name="y"/>
                           </om:OMATTR>
                        </om:OMBVAR>
                           <om:OMA>
                              <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMV name="x"/>
                                 <om:OMV name="y"/>
                              </om:OMA>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMV name="y"/>
                                 <om:OMV name="x"/>
                              </om:OMA>
                           </om:OMA>
                        </om:OMBIND>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMA>
         </om:OMOBJ>
      </type>
   </constant>


</theory>

<view name="OppositeMagmaCommut" from="?MagmaCommut" to="?MagmaCommut">

   <strass name="mag">
      <OMMOR ><om:OMA>
         <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
         <om:OMS module="OppositeMagma"/>
         <om:OMS name="mag"/>
      </om:OMA></OMMOR>
   </strass>
   <conass name="commut">
      <om:OMOBJ>
         <om:OMA>
            <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
            <om:OMBIND>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
               <om:OMBVAR>
               <om:OMATTR><om:OMATP>
                  <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                  <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                  </om:OMATP><om:OMV name="x"/>
               </om:OMATTR>
            </om:OMBVAR>
               <om:OMA>
                  <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x1"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                        <om:OMA>
                           <om:OMS name="mag/*"/>
                           <om:OMV name="x1"/>
                           <om:OMV name="x"/>
                        </om:OMA>
                        <om:OMA>
                           <om:OMS name="mag/*"/>
                           <om:OMV name="x"/>
                           <om:OMV name="x1"/>
                        </om:OMA>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMBIND>
            <om:OMBIND>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
               <om:OMBVAR>
               <om:OMATTR><om:OMATP>
                  <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                  <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                  </om:OMATP><om:OMV name="x"/>
               </om:OMATTR>
            </om:OMBVAR>
               <om:OMA>
                  <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x1"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                        <om:OMA>
                           <om:OMS name="mag/*"/>
                           <om:OMV name="x1"/>
                           <om:OMV name="x"/>
                        </om:OMA>
                        <om:OMA>
                           <om:OMS name="mag/*"/>
                           <om:OMV name="x"/>
                           <om:OMV name="x1"/>
                        </om:OMA>
                     </om:OMA>
                  </om:OMBIND>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="y"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/proof_theory/derived.omdoc" module="ForallPFExt" name="forall2E"/>
                        <om:OMBIND>
                           <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                           <om:OMBVAR>
                           <om:OMATTR><om:OMATP>
                              <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                              <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                              </om:OMATP><om:OMV name="x1"/>
                           </om:OMATTR>
                        </om:OMBVAR>
                           <om:OMBIND>
                              <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                              <om:OMBVAR>
                              <om:OMATTR><om:OMATP>
                                 <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                                 <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                                 </om:OMATP><om:OMV name="x2"/>
                              </om:OMATTR>
                           </om:OMBVAR>
                              <om:OMA>
                                 <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="x1"/>
                                    <om:OMV name="x2"/>
                                 </om:OMA>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="x2"/>
                                    <om:OMV name="x1"/>
                                 </om:OMA>
                              </om:OMA>
                           </om:OMBIND>
                        </om:OMBIND>
                        <om:OMS name="commut"/>
                        <om:OMV name="y"/>
                        <om:OMV name="x"/>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMBIND>
         </om:OMA>
      </om:OMOBJ>
   </conass>

</view>

<theory name="Semigroup">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <structure name="mag" from="?Magma"></structure><alias name="*" for="??mag/*"/>
   <constant name="assoc">
      <type>
         <om:OMOBJ>
            <om:OMA>
               <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
               <om:OMA>
                  <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                        <om:OMBIND>
                           <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                           <om:OMBVAR>
                           <om:OMATTR><om:OMATP>
                              <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                              <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                              </om:OMATP><om:OMV name="y"/>
                           </om:OMATTR>
                        </om:OMBVAR>
                           <om:OMA>
                              <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                              <om:OMBIND>
                                 <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                                 <om:OMBVAR>
                                 <om:OMATTR><om:OMATP>
                                    <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                                    <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                                    </om:OMATP><om:OMV name="z"/>
                                 </om:OMATTR>
                              </om:OMBVAR>
                                 <om:OMA>
                                    <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                                    <om:OMA>
                                       <om:OMS name="mag/*"/>
                                       <om:OMA>
                                          <om:OMS name="mag/*"/>
                                          <om:OMV name="x"/>
                                          <om:OMV name="y"/>
                                       </om:OMA>
                                       <om:OMV name="z"/>
                                    </om:OMA>
                                    <om:OMA>
                                       <om:OMS name="mag/*"/>
                                       <om:OMV name="x"/>
                                       <om:OMA>
                                          <om:OMS name="mag/*"/>
                                          <om:OMV name="y"/>
                                          <om:OMV name="z"/>
                                       </om:OMA>
                                    </om:OMA>
                                 </om:OMA>
                              </om:OMBIND>
                           </om:OMA>
                        </om:OMBIND>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMA>
         </om:OMOBJ>
      </type>
   </constant>


</theory>

<view name="OppositeSemigroup" from="?Semigroup" to="?Semigroup">

   <strass name="mag">
      <OMMOR ><om:OMA>
         <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
         <om:OMS module="OppositeMagma"/>
         <om:OMS name="mag"/>
      </om:OMA></OMMOR>
   </strass>
   <conass name="assoc">
      <om:OMOBJ>
         <om:OMA>
            <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
            <om:OMBIND>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
               <om:OMBVAR>
               <om:OMATTR><om:OMATP>
                  <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                  <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                  </om:OMATP><om:OMV name="x"/>
               </om:OMATTR>
            </om:OMBVAR>
               <om:OMA>
                  <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x1"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                        <om:OMBIND>
                           <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                           <om:OMBVAR>
                           <om:OMATTR><om:OMATP>
                              <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                              <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                              </om:OMATP><om:OMV name="x2"/>
                           </om:OMATTR>
                        </om:OMBVAR>
                           <om:OMA>
                              <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Equal" name="eq"/>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMV name="x2"/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="x1"/>
                                    <om:OMV name="x"/>
                                 </om:OMA>
                              </om:OMA>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="x2"/>
                                    <om:OMV name="x1"/>
                                 </om:OMA>
                                 <om:OMV name="x"/>
                              </om:OMA>
                           </om:OMA>
                        </om:OMBIND>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMBIND>
            <om:OMBIND>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
               <om:OMBVAR>
               <om:OMATTR><om:OMATP>
                  <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                  <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                  </om:OMATP><om:OMV name="z"/>
               </om:OMATTR>
            </om:OMBVAR>
               <om:OMA>
                  <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                        <om:OMBIND>
                           <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                           <om:OMBVAR>
                           <om:OMATTR><om:OMATP>
                              <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                              <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                              </om:OMATP><om:OMV name="x3"/>
                           </om:OMATTR>
                        </om:OMBVAR>
                           <om:OMA>
                              <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Equal" name="eq"/>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMV name="x3"/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="x"/>
                                    <om:OMV name="z"/>
                                 </om:OMA>
                              </om:OMA>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="x3"/>
                                    <om:OMV name="x"/>
                                 </om:OMA>
                                 <om:OMV name="z"/>
                              </om:OMA>
                           </om:OMA>
                        </om:OMBIND>
                     </om:OMA>
                  </om:OMBIND>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="y"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
                        <om:OMBIND>
                           <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                           <om:OMBVAR>
                           <om:OMATTR><om:OMATP>
                              <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                              <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                              </om:OMATP><om:OMV name="x"/>
                           </om:OMATTR>
                        </om:OMBVAR>
                           <om:OMA>
                              <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Equal" name="eq"/>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMV name="x"/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="y"/>
                                    <om:OMV name="z"/>
                                 </om:OMA>
                              </om:OMA>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="x"/>
                                    <om:OMV name="y"/>
                                 </om:OMA>
                                 <om:OMV name="z"/>
                              </om:OMA>
                           </om:OMA>
                        </om:OMBIND>
                        <om:OMBIND>
                           <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                           <om:OMBVAR>
                           <om:OMATTR><om:OMATP>
                              <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                              <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                              </om:OMATP><om:OMV name="x"/>
                           </om:OMATTR>
                        </om:OMBVAR>
                           <om:OMA>
                              <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="EqualPF" name="sym"/>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="x"/>
                                    <om:OMV name="y"/>
                                 </om:OMA>
                                 <om:OMV name="z"/>
                              </om:OMA>
                              <om:OMA>
                                 <om:OMS name="mag/*"/>
                                 <om:OMV name="x"/>
                                 <om:OMA>
                                    <om:OMS name="mag/*"/>
                                    <om:OMV name="y"/>
                                    <om:OMV name="z"/>
                                 </om:OMA>
                              </om:OMA>
                              <om:OMA>
                                 <om:OMS base="/logics/first-order/proof_theory/derived.omdoc" module="ForallPFExt" name="forall3E"/>
                                 <om:OMBIND>
                                    <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                                    <om:OMBVAR>
                                    <om:OMATTR><om:OMATP>
                                       <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                                       <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                                       </om:OMATP><om:OMV name="x1"/>
                                    </om:OMATTR>
                                 </om:OMBVAR>
                                    <om:OMBIND>
                                       <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                                       <om:OMBVAR>
                                       <om:OMATTR><om:OMATP>
                                          <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                                          <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                                          </om:OMATP><om:OMV name="x2"/>
                                       </om:OMATTR>
                                    </om:OMBVAR>
                                       <om:OMBIND>
                                          <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                                          <om:OMBVAR>
                                          <om:OMATTR><om:OMATP>
                                             <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                                             <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                                             </om:OMATP><om:OMV name="x3"/>
                                          </om:OMATTR>
                                       </om:OMBVAR>
                                          <om:OMA>
                                             <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                                             <om:OMA>
                                                <om:OMS name="mag/*"/>
                                                <om:OMA>
                                                   <om:OMS name="mag/*"/>
                                                   <om:OMV name="x1"/>
                                                   <om:OMV name="x2"/>
                                                </om:OMA>
                                                <om:OMV name="x3"/>
                                             </om:OMA>
                                             <om:OMA>
                                                <om:OMS name="mag/*"/>
                                                <om:OMV name="x1"/>
                                                <om:OMA>
                                                   <om:OMS name="mag/*"/>
                                                   <om:OMV name="x2"/>
                                                   <om:OMV name="x3"/>
                                                </om:OMA>
                                             </om:OMA>
                                          </om:OMA>
                                       </om:OMBIND>
                                    </om:OMBIND>
                                 </om:OMBIND>
                                 <om:OMS name="assoc"/>
                                 <om:OMV name="x"/>
                                 <om:OMV name="y"/>
                                 <om:OMV name="z"/>
                              </om:OMA>
                           </om:OMA>
                        </om:OMBIND>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMBIND>
         </om:OMA>
      </om:OMOBJ>
   </conass>

</view>

<theory name="SemigroupCommut">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <structure name="sg" from="?Semigroup"></structure>
   <structure name="mc" from="?MagmaCommut">
      <strass name="mag">
         <OMMOR ><om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMS module="Semigroup" name="mag"/>
            <om:OMS name="sg"/>
         </om:OMA></OMMOR>
      </strass>
   </structure>

</theory>

<view name="OppositeSemigroupCommut" from="?SemigroupCommut" to="?SemigroupCommut">

   <strass name="sg">
      <OMMOR ><om:OMA>
         <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
         <om:OMS module="OppositeSemigroup"/>
         <om:OMS name="sg"/>
      </om:OMA></OMMOR>
   </strass>
   <strass name="mc">
      <OMMOR ><om:OMA>
         <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
         <om:OMS module="OppositeMagmaCommut"/>
         <om:OMS name="mc"/>
      </om:OMA></OMMOR>
   </strass>

</view>

<theory name="MagmaIdempotent">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/><alias name="|-" for="/logics/first-order/proof_theory/fol.omdoc?FOLEQPF?|-"/><alias name="forall" for="/logics/first-order/syntax/modules.omdoc?Forall?forall"/><alias name="==" for="/logics/first-order/proof_theory/fol.omdoc?FOLEQPF?=="/>

   <structure name="mag" from="?Magma"></structure><alias name="*" for="??mag/*"/>
   <constant name="idem">
      <type>
         <om:OMOBJ>
            <om:OMA>
               <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
               <om:OMA>
                  <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                        <om:OMA>
                           <om:OMS name="mag/*"/>
                           <om:OMV name="x"/>
                           <om:OMV name="x"/>
                        </om:OMA>
                        <om:OMV name="x"/>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMA>
         </om:OMOBJ>
      </type>
   </constant>


</theory>

<theory name="Band">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <structure name="sg" from="?Semigroup"></structure>
   <structure name="midem" from="?MagmaIdempotent">
      <strass name="mag">
         <OMMOR ><om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMS module="Semigroup" name="mag"/>
            <om:OMS name="sg"/>
         </om:OMA></OMMOR>
      </strass>
   </structure>

</theory>

<theory name="MagmaRightIden">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/><alias name="i" for="/logics/first-order/syntax/base.omdoc?BaseFOL?i"/><alias name="|-" for="/logics/first-order/proof_theory/fol.omdoc?FOLEQPF?|-"/><alias name="forall" for="/logics/first-order/syntax/modules.omdoc?Forall?forall"/><alias name="==" for="/logics/first-order/proof_theory/fol.omdoc?FOLEQPF?=="/>

   <structure name="mag" from="?Magma"></structure><alias name="*" for="??mag/*"/>
   <constant name="e">
      <type>
         <om:OMOBJ>
            <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
         </om:OMOBJ>
      </type>
   </constant>

   <constant name="iden">
      <type>
         <om:OMOBJ>
            <om:OMA>
               <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
               <om:OMA>
                  <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                        <om:OMA>
                           <om:OMS name="mag/*"/>
                           <om:OMV name="x"/>
                           <om:OMS name="e"/>
                        </om:OMA>
                        <om:OMV name="x"/>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMA>
         </om:OMOBJ>
      </type>
   </constant>


</theory>

<theory name="MagmaIdentity">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <structure name="rid" from="?MagmaRightIden"></structure><alias name="*" for="??rid/mag/*"/><alias name="e" for="??rid/e"/>
   <structure name="lid" from="?MagmaRightIden">
      <strass name="mag">
         <OMMOR ><om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMS module="OppositeMagma"/>
            <om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMS module="MagmaRightIden" name="mag"/>
            <om:OMS name="rid"/>
         </om:OMA>
         </om:OMA></OMMOR>
      </strass>
      <conass name="e">
         <om:OMOBJ>
            <om:OMS name="rid/e"/>
         </om:OMOBJ>
      </conass>
   </structure>

</theory>

<theory name="Monoid">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <structure name="sg" from="?Semigroup"></structure><alias name="*" for="??sg/mag/*"/>
   <structure name="miden" from="?MagmaIdentity">
      <strass name="rid/mag">
         <OMMOR ><om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMS module="Semigroup" name="mag"/>
            <om:OMS name="sg"/>
         </om:OMA></OMMOR>
      </strass>
   </structure><alias name="e" for="??miden/rid/e"/>

</theory>

<theory name="MonoidCommut">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/><alias name="|-" for="/logics/first-order/proof_theory/fol.omdoc?FOLEQPF?|-"/><alias name="forall" for="/logics/first-order/syntax/modules.omdoc?Forall?forall"/><alias name="==" for="/logics/first-order/proof_theory/fol.omdoc?FOLEQPF?=="/>

   <structure name="mon" from="?Monoid"></structure>
   <structure name="mc" from="?MagmaCommut">
      <strass name="mag">
         <OMMOR ><om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMS module="Semigroup" name="mag"/>
            <om:OMS module="Monoid" name="sg"/>
         </om:OMA>
            <om:OMS name="mon"/>
         </om:OMA></OMMOR>
      </strass>
   </structure>

</theory>

<theory name="MagmaRightInv">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/><alias name="i" for="/logics/first-order/syntax/base.omdoc?BaseFOL?i"/><alias name="|-" for="/logics/first-order/proof_theory/fol.omdoc?FOLEQPF?|-"/><alias name="forall" for="/logics/first-order/syntax/modules.omdoc?Forall?forall"/><alias name="==" for="/logics/first-order/proof_theory/fol.omdoc?FOLEQPF?=="/>

   <structure name="id" from="?MagmaIdentity"></structure><alias name="*" for="??id/rid/mag/*"/><alias name="e" for="??id/rid/e"/>
   <constant name="inv">
      <type>
         <om:OMOBJ>
            <om:OMA>
               <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
               <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
               <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
            </om:OMA>
         </om:OMOBJ>
      </type>
   </constant>

   <constant name="inverse">
      <type>
         <om:OMOBJ>
            <om:OMA>
               <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
               <om:OMA>
                  <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
                  <om:OMBIND>
                     <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
                     <om:OMBVAR>
                     <om:OMATTR><om:OMATP>
                        <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
                        <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
                        </om:OMATP><om:OMV name="x"/>
                     </om:OMATTR>
                  </om:OMBVAR>
                     <om:OMA>
                        <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
                        <om:OMA>
                           <om:OMS name="id/rid/mag/*"/>
                           <om:OMV name="x"/>
                           <om:OMA>
                              <om:OMS name="inv"/>
                              <om:OMV name="x"/>
                           </om:OMA>
                        </om:OMA>
                        <om:OMS name="id/rid/e"/>
                     </om:OMA>
                  </om:OMBIND>
               </om:OMA>
            </om:OMA>
         </om:OMOBJ>
      </type>
   </constant>


</theory>

<theory name="Group">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <structure name="mon" from="?Monoid"></structure><alias name="*" for="??mon/sg/mag/*"/><alias name="e" for="??mon/miden/rid/e"/>
   <structure name="minv" from="?MagmaRightInv">
      <strass name="id">
         <OMMOR ><om:OMS name="mon/miden"/></OMMOR>
      </strass>
   </structure><alias name="inv" for="??minv/inv"/>

</theory>

<theory name="GroupAbelian">
   <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>

   <structure name="g" from="?Group"></structure><alias name="+" for="??g/mon/sg/mag/*"/><alias name="0" for="??g/mon/miden/rid/e"/><alias name="-" for="??g/minv/inv"/>
   <structure name="mc" from="?MagmaCommut">
      <strass name="mag">
         <OMMOR ><om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMA>
            <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
            <om:OMS module="Semigroup" name="mag"/>
            <om:OMS module="Monoid" name="sg"/>
         </om:OMA>
            <om:OMS module="Group" name="mon"/>
         </om:OMA>
            <om:OMS name="g"/>
         </om:OMA></OMMOR>
      </strass>
   </structure>

</theory>

</omdoc>