<?xml version="1.0" encoding="UTF-8"?>
<!-- generated from Twelf sources by Florian Rabe -->
<theory name="TruthMOD">
<include from="/meta/sttifol.omdoc?STTIFOLEQ"/>
<include from="base.omdoc?BaseMOD"/>
<constant name="true'">
<type>
<om:OMOBJ>
</om:OMOBJ>
</type>
</constant>
<constant name="true1">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
<om:OMS name="true'"/>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
</constant>
</theory>
<include >
</include>
<conass name="true">
<om:OMOBJ>
<om:OMS name="true'"/>
</om:OMOBJ>
</conass>
</view>
<theory name="FalsityMOD">
<include from="/meta/sttifol.omdoc?STTIFOLEQ"/>
<include from="base.omdoc?BaseMOD"/>
<constant name="false'">
<type>
<om:OMOBJ>
</om:OMOBJ>
</type>
</constant>
<constant name="false0">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
<om:OMS name="false'"/>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
</constant>
</theory>
<include >
</include>
<conass name="false">
<om:OMOBJ>
<om:OMS name="false'"/>
</om:OMOBJ>
</conass>
</view>
<theory name="NEGMOD">
<include from="/meta/sttifol.omdoc?STTIFOLEQ"/>
<include from="base.omdoc?BaseMOD"/>
<constant name="not'">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
</constant>
<constant name="not1">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="not'"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??not1" role="application" implicit="1"/>
<constant name="not0">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="not'"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??not0" role="application" implicit="1"/>
<constant name="not''">
<type>
<om:OMOBJ>
<om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMS name="not'"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<constant name="not1'">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="not''"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="p"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="not'"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="not1"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??not1'" role="application" implicit="1"/>
<constant name="not0'">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="not''"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="p"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="not'"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="not0"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??not0'" role="application" implicit="1"/>
</theory>
<include >
</include>
<conass name="not">
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMS name="not'"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMBIND>
</om:OMOBJ>
</conass>
</view>
<theory name="DISJMOD">
<include from="/meta/sttifol.omdoc?STTIFOLEQ"/>
<include from="base.omdoc?BaseMOD"/>
<constant name="or'">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
</constant>
<constant name="or1">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="or'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??or1" role="application" implicit="2"/>
<constant name="or0">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="or'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??or0" role="application" implicit="2"/>
<constant name="or''">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="or'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??or''" role="application" fixity="in" associativity="left" precedence="10" implicit="0"/>
<constant name="or1'">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="or''"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="p"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="or'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMV name="p"/>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="q"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="or'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="or1"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="r"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="or'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="or1"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??or1'" role="application" implicit="2"/>
<constant name="or0'">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="or''"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="p"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="or'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="or0"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??or0'" role="application" implicit="2"/>
</theory>
<include >
</include>
<conass name="or">
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="or'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</conass>
</view>
<theory name="CONJMOD">
<include from="/meta/sttifol.omdoc?STTIFOLEQ"/>
<include from="base.omdoc?BaseMOD"/>
<constant name="and'">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
</constant>
<constant name="and1">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="and'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??and1" role="application" implicit="2"/>
<constant name="and0">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="and'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??and0" role="application" implicit="2"/>
<constant name="and''">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="and'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??and''" role="application" fixity="in" associativity="left" precedence="10" implicit="0"/>
<constant name="and1'">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="and''"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="p"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="and'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="and1"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??and1'" role="application" implicit="2"/>
<constant name="and0'">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="and''"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="p"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="and'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="and0"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??and0'" role="application" implicit="2"/>
</theory>
<include >
</include>
<conass name="and">
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="and'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</conass>
</view>
<theory name="IMPMOD">
<include from="/meta/sttifol.omdoc?STTIFOLEQ"/>
<include from="base.omdoc?BaseMOD"/>
<constant name="imp'">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
</constant>
<constant name="imp1">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="imp'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??imp1" role="application" implicit="2"/>
<constant name="imp0">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="imp'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??imp0" role="application" implicit="2"/>
<constant name="imp''">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMA>
</om:OMA>
</om:OMA>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="imp'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??imp''" role="application" fixity="in" associativity="right" precedence="15" implicit="0"/>
<constant name="imp1'">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="imp''"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="p"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="imp'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="imp1"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??imp1'" role="application" implicit="2"/>
<constant name="imp0'">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMS name="imp''"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
<definition>
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="p"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="imp'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
<om:OMA>
<om:OMS name="imp0"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMV name="p"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</definition>
</constant>
<notation for="??imp0'" role="application" implicit="2"/>
</theory>
<include >
</include>
<conass name="imp">
<om:OMOBJ>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMA>
<om:OMA>
</om:OMA>
<om:OMS name="imp'"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMV name="B"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</conass>
</view>
</omdoc>