239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<?xml version="1.0" encoding="UTF-8"?>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" >
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<!-- generated from Twelf sources by Florian Rabe -->
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="Magma">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <constant name="*">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </constant>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <notation for="??*" role="application" fixity="in" associativity="none" precedence="100" implicit="0"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<view name="OppositeMagma" from="?Magma" to="?Magma">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <conass name="*">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </conass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</view>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="MagmaCommut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mag" from="?Magma"></structure><alias name="*" for="??mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <constant name="commut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </constant>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<view name="OppositeMagmaCommut" from="?MagmaCommut" to="?MagmaCommut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="mag">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="OppositeMagma"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <conass name="commut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/derived.omdoc" module="ForallPFExt" name="forall2E"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="commut"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </conass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</view>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="Semigroup">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mag" from="?Magma"></structure><alias name="*" for="??mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <constant name="assoc">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </constant>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<view name="OppositeSemigroup" from="?Semigroup" to="?Semigroup">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="mag">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="OppositeMagma"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <conass name="assoc">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Equal" name="eq"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x3"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Equal" name="eq"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x3"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x3"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="ForallPF" name="forallI"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Equal" name="eq"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/modules.omdoc" module="EqualPF" name="sym"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/derived.omdoc" module="ForallPFExt" name="forall3E"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x3"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x3"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x1"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x2"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x3"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="assoc"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="y"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="z"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </conass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</view>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="SemigroupCommut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="sg" from="?Semigroup"></structure>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mc" from="?MagmaCommut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="mag">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="Semigroup" name="mag"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="sg"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </structure>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<view name="OppositeSemigroupCommut" from="?SemigroupCommut" to="?SemigroupCommut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="sg">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="OppositeSemigroup"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="sg"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="mc">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="OppositeMagmaCommut"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mc"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</view>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="MagmaIdempotent">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <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?=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mag" from="?Magma"></structure><alias name="*" for="??mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <constant name="idem">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </constant>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="Band">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="sg" from="?Semigroup"></structure>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="midem" from="?MagmaIdempotent">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="mag">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="Semigroup" name="mag"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="sg"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </structure>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="MagmaRightIden">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <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?=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mag" from="?Magma"></structure><alias name="*" for="??mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <constant name="e">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </constant>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <constant name="iden">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="e"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </constant>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="MagmaIdentity">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="rid" from="?MagmaRightIden"></structure><alias name="*" for="??rid/mag/*"/><alias name="e" for="??rid/e"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="lid" from="?MagmaRightIden">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="mag">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="OppositeMagma"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="MagmaRightIden" name="mag"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="rid"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <conass name="e">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="rid/e"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </conass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </structure>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="Monoid">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="sg" from="?Semigroup"></structure><alias name="*" for="??sg/mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="miden" from="?MagmaIdentity">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="rid/mag">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="Semigroup" name="mag"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="sg"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </structure><alias name="e" for="??miden/rid/e"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="MonoidCommut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <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?=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mon" from="?Monoid"></structure>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mc" from="?MagmaCommut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="mag">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="Semigroup" name="mag"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="Monoid" name="sg"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="mon"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </structure>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="MagmaRightInv">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <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?=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="id" from="?MagmaIdentity"></structure><alias name="*" for="??id/rid/mag/*"/><alias name="e" for="??id/rid/e"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <constant name="inv">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </constant>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <constant name="inverse">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="|-"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/modules.omdoc" module="Forall" name="forall"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="lambda"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMATTR><om:OMATP>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/syntax/base.omdoc" module="BaseFOL" name="i"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATP><om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMATTR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBVAR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="/logics/first-order/proof_theory/fol.omdoc" module="FOLEQPF" name="=="/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="id/rid/mag/*"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="inv"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMV name="x"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="id/rid/e"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMBIND>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMOBJ>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </type>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </constant>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="Group">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mon" from="?Monoid"></structure><alias name="*" for="??mon/sg/mag/*"/><alias name="e" for="??mon/miden/rid/e"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="minv" from="?MagmaRightInv">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="id">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMS name="mon/miden"/></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </structure><alias name="inv" for="??minv/inv"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova<theory name="GroupAbelian">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <include from="/logics/first-order/proof_theory/derived.omdoc?FOLEQPFExt"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <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"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <structure name="mc" from="?MagmaCommut">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <strass name="mag">
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <OMMOR ><om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS base="http://cds.omdoc.org/omdoc/mmt.omdoc" module="mmt" name="composition"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="Semigroup" name="mag"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="Monoid" name="sg"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS module="Group" name="mon"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova <om:OMS name="g"/>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </om:OMA></OMMOR>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </strass>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova </structure>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</theory>
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova</omdoc>