<?xml version="1.0"?>
<?xml-stylesheet  type="text/xsl" href="http://www.w3.org/Math/XSL/mathml.xsl"?>
<m:math xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:h="http://www.w3.org/1999/xhtml" xmlns:s="http://www.w3.org/2000/01/rdf-schema#" xmlns:r="http://www.w3.org/1999/02/22-rdf-syntax-ns#">
  <m:apply>
    <m:forall/>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>U</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>T</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TP</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>T</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>G</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TP</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>N</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>U</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>N</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>G</m:ci>
    </m:bvar>
    <m:apply>
      <m:implies/>
      <m:apply>
        <m:and/>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/log#uri">@@</m:csymbol>
          <m:ci>IR</m:ci>
          <m:ci>U</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#transformation">@@</m:csymbol>
          <m:ci>IR</m:ci>
          <m:ci>T</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#txprop">@@</m:csymbol>
          <m:ci>T</m:ci>
          <m:ci>TP</m:ci>
        </m:apply>
        <m:apply>
          <m:ci>TP</m:ci>
          <m:ci>N</m:ci>
          <m:ci>G</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#doc">@@</m:csymbol>
          <m:ci>U</m:ci>
          <m:ci>N</m:ci>
        </m:apply>
      </m:apply>
      <m:apply>
        <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#result">@@</m:csymbol>
        <m:ci>IR</m:ci>
        <m:ci>G</m:ci>
      </m:apply>
    </m:apply>
  </m:apply>
  <m:apply>
    <m:forall/>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>F</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>G</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>H</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>F</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>G</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>H</m:ci>
    </m:bvar>
    <m:apply>
      <m:implies/>
      <m:apply>
        <m:and/>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#result">@@</m:csymbol>
          <m:ci>IR</m:ci>
          <m:ci>F</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#result">@@</m:csymbol>
          <m:ci>IR</m:ci>
          <m:ci>G</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/log#conjuction">@@</m:csymbol>
          <m:list>
            <m:ci>F</m:ci>
            <m:ci>G</m:ci>
          </m:list>
          <m:ci>H</m:ci>
        </m:apply>
      </m:apply>
      <m:apply>
        <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#result">@@</m:csymbol>
        <m:ci>IR</m:ci>
        <m:ci>H</m:ci>
      </m:apply>
    </m:apply>
  </m:apply>
  <m:apply>
    <m:forall/>
    <m:bvar>
      <m:ci>E</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>N</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>A</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>E</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>A</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>A</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>V</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>A</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>REF</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>V</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>BASE</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>E</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TXURI</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>REF</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>BASE</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TX</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TXURI</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>N</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TX</m:ci>
    </m:bvar>
    <m:apply>
      <m:implies/>
      <m:apply>
        <m:and/>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/list#in">in</m:csymbol>
          <m:ci>E</m:ci>
          <m:apply>
            <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/infoset/infoset-daml#children">@@</m:csymbol>
            <m:ci>N</m:ci>
          </m:apply>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/list#in">in</m:csymbol>
          <m:ci>A</m:ci>
          <m:apply>
            <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/infoset/infoset-daml#attributes">@@</m:csymbol>
            <m:ci>E</m:ci>
          </m:apply>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#namespace-uri">@@</m:csymbol>
          <m:ci>A</m:ci>
          <m:ms>http://www.w3.org/2003/g/data-view#</m:ms>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#local-name">@@</m:csymbol>
          <m:ci>A</m:ci>
          <m:ms>transformation</m:ms>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#string">@@</m:csymbol>
          <m:ci>A</m:ci>
          <m:ci>V</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/list#in">in</m:csymbol>
          <m:ci>REF</m:ci>
          <m:apply>
            <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#tokenize">@@</m:csymbol>
            <m:list>
              <m:ci>V</m:ci>
              <m:ms>[ \t\r\n]</m:ms>
            </m:list>
          </m:apply>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#base-uri">@@</m:csymbol>
          <m:ci>E</m:ci>
          <m:ci>BASE</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#resolve-uri">@@</m:csymbol>
          <m:list>
            <m:ci>REF</m:ci>
            <m:ci>BASE</m:ci>
          </m:list>
          <m:ci>TXURI</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/log#uri">@@</m:csymbol>
          <m:ci>TX</m:ci>
          <m:ci>TXURI</m:ci>
        </m:apply>
      </m:apply>
      <m:apply>
        <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#txlink">@@</m:csymbol>
        <m:ci>N</m:ci>
        <m:ci>TX</m:ci>
      </m:apply>
    </m:apply>
  </m:apply>
  <m:apply>
    <m:forall/>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>U</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>N</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>U</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>N</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TX</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TX</m:ci>
    </m:bvar>
    <m:apply>
      <m:implies/>
      <m:apply>
        <m:and/>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/log#uri">@@</m:csymbol>
          <m:ci>IR</m:ci>
          <m:ci>U</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#doc">@@</m:csymbol>
          <m:ci>U</m:ci>
          <m:ci>N</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#txlink">@@</m:csymbol>
          <m:ci>N</m:ci>
          <m:ci>TX</m:ci>
        </m:apply>
      </m:apply>
      <m:apply>
        <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#transformation">@@</m:csymbol>
        <m:ci>IR</m:ci>
        <m:ci>TX</m:ci>
      </m:apply>
    </m:apply>
  </m:apply>
  <m:apply>
    <m:forall/>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>U</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>U</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>N</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>E</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>N</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>NS</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>E</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>NSDOC</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>NS</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>NSDOC</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>G</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>G</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>SPO</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>SPO</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>NSDOC</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TX</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>IR</m:ci>
    </m:bvar>
    <m:bvar>
      <m:ci>TX</m:ci>
    </m:bvar>
    <m:apply>
      <m:implies/>
      <m:apply>
        <m:and/>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/log#uri">@@</m:csymbol>
          <m:ci>IR</m:ci>
          <m:ci>U</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#doc">@@</m:csymbol>
          <m:ci>U</m:ci>
          <m:ci>N</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/list#in">in</m:csymbol>
          <m:ci>E</m:ci>
          <m:apply>
            <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/infoset/infoset-daml#children">@@</m:csymbol>
            <m:ci>N</m:ci>
          </m:apply>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2006/xpath-functions#namespace-uri">@@</m:csymbol>
          <m:ci>E</m:ci>
          <m:ci>NS</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/log#uri">@@</m:csymbol>
          <m:ci>NSDOC</m:ci>
          <m:ci>NS</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#result">@@</m:csymbol>
          <m:ci>NSDOC</m:ci>
          <m:ci>G</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/log#includes">@@</m:csymbol>
          <m:ci>G</m:ci>
          <m:ci>SPO</m:ci>
        </m:apply>
        <m:apply>
          <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/log#_statement">@@</m:csymbol>
          <m:list>
            <m:ci>NSDOC</m:ci>
            <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#namespaceTransformation">@@</m:csymbol>
            <m:ci>TX</m:ci>
          </m:list>
          <m:ci>SPO</m:ci>
        </m:apply>
      </m:apply>
      <m:apply>
        <m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2003/g/data-view#transformation">@@</m:csymbol>
        <m:ci>IR</m:ci>
        <m:ci>TX</m:ci>
      </m:apply>
    </m:apply>
  </m:apply>
</m:math>
