base.omdoc revision 239352d9aec4bc3823511873533fa812cbe259c7
<?xml version="1.0" encoding="UTF-8"?>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" >
<!-- generated from Twelf sources by Florian Rabe -->
<theory name="Level'" meta="http://cds.omdoc.org/foundations/lf/lf.omdoc?lf">
<constant name="cl">
<type>
<om:OMOBJ>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="type"/>
</om:OMOBJ>
</type>
</constant>
<constant name="exp">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMS name="cl"/>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="type"/>
</om:OMA>
</om:OMOBJ>
</type>
</constant>
<notation for="??exp" role="application" fixity="pre" precedence="0" implicit="0"/>
</theory>
<theory name="Level" meta="http://cds.omdoc.org/foundations/lf/lf.omdoc?lf">
<constant name="cl">
<type>
<om:OMOBJ>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="type"/>
</om:OMOBJ>
</type>
</constant>
<constant name="exp">
<type>
<om:OMOBJ>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMS name="cl"/>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="type"/>
</om:OMA>
</om:OMOBJ>
</type>
</constant>
<notation for="??exp" role="application" fixity="pre" precedence="0" implicit="0"/>
<constant name="==">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMS name="cl"/>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="type"/>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??==" role="application" fixity="in" associativity="none" precedence="50" implicit="1"/>
<constant name="refl">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMS name="cl"/>
</om:OMATP><om:OMV name="X1"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="X1"/>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMS name="=="/>
<om:OMV name="X1"/>
<om:OMV name="A"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??refl" role="application" implicit="2"/>
<constant name="sym">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMS name="cl"/>
</om:OMATP><om:OMV name="X1"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="X1"/>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="X1"/>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMA>
<om:OMS name="=="/>
<om:OMV name="X1"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMA>
<om:OMS name="=="/>
<om:OMV name="X1"/>
<om:OMV name="B"/>
<om:OMV name="A"/>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??sym" role="application" implicit="3"/>
<constant name="trans">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMS name="cl"/>
</om:OMATP><om:OMV name="X1"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="X1"/>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="X1"/>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="X1"/>
</om:OMA>
</om:OMATP><om:OMV name="C"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMA>
<om:OMS name="=="/>
<om:OMV name="X1"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMA>
<om:OMS name="=="/>
<om:OMV name="X1"/>
<om:OMV name="B"/>
<om:OMV name="C"/>
</om:OMA>
<om:OMA>
<om:OMS name="=="/>
<om:OMV name="X1"/>
<om:OMV name="A"/>
<om:OMV name="C"/>
</om:OMA>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??trans" role="application" implicit="4"/>
<constant name="cong">
<type>
<om:OMOBJ>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMS name="cl"/>
</om:OMATP><om:OMV name="C"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="C"/>
</om:OMA>
</om:OMATP><om:OMV name="A"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="C"/>
</om:OMA>
</om:OMATP><om:OMV name="B"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="implicit_Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMS name="cl"/>
</om:OMATP><om:OMV name="D"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMA>
<om:OMS name="=="/>
<om:OMV name="C"/>
<om:OMV name="A"/>
<om:OMV name="B"/>
</om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="Pi"/>
<om:OMBVAR>
<om:OMATTR><om:OMATP>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="oftype"/>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/foundations/lf/lf.omdoc" module="lf" name="arrow"/>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="C"/>
</om:OMA>
<om:OMA>
<om:OMS name="exp"/>
<om:OMV name="D"/>
</om:OMA>
</om:OMA>
</om:OMATP><om:OMV name="F"/>
</om:OMATTR>
</om:OMBVAR>
<om:OMA>
<om:OMS name="=="/>
<om:OMV name="D"/>
<om:OMA>
<om:OMV name="F"/>
<om:OMV name="A"/>
</om:OMA>
<om:OMA>
<om:OMV name="F"/>
<om:OMV name="B"/>
</om:OMA>
</om:OMA>
</om:OMBIND>
</om:OMA>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMBIND>
</om:OMOBJ>
</type>
</constant>
<notation for="??cong" role="application" implicit="4"/>
</theory>
<theory name="TypesTerms" meta="http://cds.omdoc.org/foundations/lf/lf.omdoc?lf">
<structure name="types" from="?Level"></structure><alias name="tp" for="??types/cl"/><alias name="tm" for="??types/exp"/><alias name="==" for="??types/=="/>
</theory>
<theory name="KindsTypesTerms" meta="http://cds.omdoc.org/foundations/lf/lf.omdoc?lf">
<structure name="kinds" from="?Level"></structure><alias name="kd" for="??kinds/cl"/><alias name="tf" for="??kinds/exp"/><alias name="===" for="??kinds/=="/>
<constant name="tp'">
<type>
<om:OMOBJ>
<om:OMS name="kinds/cl"/>
</om:OMOBJ>
</type>
</constant>
<structure name="types" from="?Level">
<conass name="cl">
<om:OMOBJ>
<om:OMA>
<om:OMS name="kinds/exp"/>
<om:OMS name="tp'"/>
</om:OMA>
</om:OMOBJ>
</conass>
</structure><alias name="tp" for="??types/cl"/><alias name="tm" for="??types/exp"/><alias name="==" for="??types/=="/>
</theory>
<view name="TypesToTypes" from="?TypesTerms" to="?KindsTypesTerms">
<strass name="types">
<OMMOR ><om:OMS name="types"/></OMMOR>
</strass>
</view>
</omdoc>