<xsl:transform version="1.0"
    xmlns:xsl  ="http://www.w3.org/1999/XSL/Transform"
    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#"
    xmlns:m="http://www.w3.org/1998/Math/MathML"
    >

<xsl:output method="xml" indent="yes"/>

<xsl:template match='/'>
  <xsl:processing-instruction name="xml-stylesheet"> type="text/xsl" href="http://www.w3.org/Math/XSL/mathml.xsl"</xsl:processing-instruction>
  <xsl:text>&#x0A;</xsl:text>
  <m:math>
    <xsl:apply-templates />
  </m:math>
</xsl:template>

<xsl:template match='*[@class="Rule"]'>
  <m:apply>
    <m:forall />

    <xsl:for-each select=".//h:var">
      <!-- @@TODO: sort/uniq -->
      <m:bvar><m:ci><xsl:value-of select="." /></m:ci></m:bvar>
    </xsl:for-each>

    <m:apply>
      <m:implies />
      <m:apply>
	<m:and />
	<xsl:for-each select=".//h:ul/h:li">
	  <xsl:call-template name="extract-prop"/>
	</xsl:for-each>
      </m:apply>
      
      <!-- support both the dl style and the table style -->
      <xsl:for-each select="h:dt">
	<xsl:call-template name="extract-prop"/>
      </xsl:for-each>
      <xsl:for-each select="h:tr[last()]/h:td">
	<xsl:call-template name="extract-prop"/>
      </xsl:for-each>
    </m:apply>
  </m:apply>
</xsl:template>

<xsl:template name="extract-prop">
  <xsl:choose>
    <!-- E in F(X, Y, Z, ...) -->
    <xsl:when test='h:tt[text()="in"]'>
      <m:apply>
	<m:csymbol encoding="RDF" definitionURL="http://www.w3.org/2000/10/swap/list#in">in</m:csymbol>
	<xsl:apply-templates select="*[1]" mode="term"/>

	<m:apply>
	  <xsl:apply-templates select="*[3]" mode="term"/>

	  <xsl:choose>
	    <!-- n-ary -->
	    <xsl:when test="count(*) > 4">
	      <m:list>
		<xsl:for-each select="*[position() > 3]">
		  <xsl:apply-templates select="." mode="term"/>
		</xsl:for-each>
	      </m:list>
	    </xsl:when>
	    
	    <xsl:otherwise>
	      <xsl:apply-templates select="*[4]" mode="term"/>
	    </xsl:otherwise>
	  </xsl:choose>
	</m:apply>
      </m:apply>
    </xsl:when>

    <!-- V = F(X, Y, Z, ...) -->
    <xsl:when test='contains(., "=")'>
      <m:apply>
	<xsl:apply-templates select="*[2]" mode="term"/>

	<xsl:choose>
	  <!-- n-ary -->
	  <xsl:when test="count(*) > 3">
	    <m:list>
	      <xsl:for-each select="*[position() > 2]">
		<xsl:apply-templates select="." mode="term"/>
	      </xsl:for-each>
	    </m:list>
	  </xsl:when>

	  <xsl:otherwise>
	    <xsl:apply-templates select="*[3]" mode="term"/>
	  </xsl:otherwise>
	</xsl:choose>

	<xsl:apply-templates select="*[1]" mode="term"/>
      </m:apply>
    </xsl:when>

    <!-- P(S, O) -->
    <xsl:otherwise>
      <m:apply>
	<xsl:apply-templates select="*[1]" mode="term"/>
	<xsl:apply-templates select="*[2]" mode="term"/>
	<xsl:apply-templates select="*[3]" mode="term"/>
      </m:apply>
    </xsl:otherwise>
  </xsl:choose>
</xsl:template>

<xsl:template match="h:var" mode="term">
  <m:ci><xsl:value-of select="." /></m:ci>
</xsl:template>

<xsl:template match="h:a" mode="term">
  <m:csymbol encoding="RDF" definitionURL="{@href}">@@</m:csymbol>
</xsl:template>

<xsl:template match="h:q" mode="term">
  <m:ms><xsl:value-of select="." /></m:ms>
</xsl:template>

<!-- don't pass text thru -->
<xsl:template match="text()|@*">
</xsl:template>

</xsl:transform>