\def\I{{\cal I}}
\def\Z{{\bf Z}}
\def\Q{{\bf Q}}
\def\C{{\bf C}}
\def\R{{\bf R}}
\def\CL{\mathop{\rm CL}}
\def\IDA{{}_{\rm DA}\int}
\def\DDA{D_{\rm DA}}
\def\cDA{constant${}_{\rm DA}$}
\def\fracDDA#1#2{\frac{{\rm d}#1}{{\rm d}_{\rm DA}#2}}
\def\Ied{{}_{\epsilon\delta}\int}
\def\Ded{D_{\epsilon\delta}}
\def\fracDed#1#2{\frac{{\rm d}#1}{{\rm d}_{\epsilon\delta}#2}}
\documentclass{article}   % Without notes
\usepackage{verbatim}
\usepackage{url}

\title{Conditions in MathML}
\author{James Davenport\\\url{J.H.Davenport@bath.ac.uk}}

\begin{document}
\maketitle
\begin{abstract}\noindent
JHD's attempt (currently very incomplete) to look at the uses of 
\verb+condition+ in the MathML2 specification. Appendix C is now complete.
\end{abstract}
\section{Introduction}
This note follows from the OpenMath tele-conference at 15:00
GMT\footnote{16:00 BST, 17:00 CET.} on 10/10/2008. See
Michael Kohlhase (\url{m.kohlhase@jacobs-university.de})'s mail
\url{48F05077.7010004@jacobs-university.de}.
%Date: Sat, 11 Oct 2008 09:06:31 +0200
\par
The summary reads as follows.
\begin{quotation}\noindent
James was tasked to make sense of the integration/differentiation
examples from the MathML2 spec and make concrete suggestions for the
expression-based calculus CD.
\end{quotation}
The detailed record shows that it should be a wider look at {\it all\/} uses
of condition, and this version is an attempt to look at all occurrences of
\verb+condition+ in the MathML2 specification.
\par
From table \ref{Ctable} (page \pageref{Ctable}) we see that the only dubious
case in Appendix C is in section \ref{C2272}, wher ethe aletrnative in MK's
note \cite{MK} seems not to conform to OpenMath in practice.
\begin{table}[h]
\caption{{\tt condition} in Appendix C\label{Ctable}}
\begin{tabular}{llll}
MathML 2&heading&This&resolution\\
Appendix C&&document&\\
C.2.2.4&{\tt interval}&section \ref{C224}&{\tt suchthat}; ??\\
C.2.2.5&{\tt inverse}&section \ref{C225}&{\tt forallrestricted}\\
C.2.2.7&{\tt condition}&section \ref{C2271}&{\tt suchthat}\\
C.2.2.7&{\tt condition}&section \ref{C2272}&Needs work\\
C.2.2.14&{\tt image}&section \ref{C2214}&{\tt forallrestricted}${}^1$\\
C.2.2.15&{\tt domainofapplication}&section \ref{C2215}&none needed\\
C.2.3.1&{\tt quotient}&section \ref{C231}&{\tt forallrestricted}${}^1$\\
C.2.3.2&{\tt factorial}&section \ref{C232}&{\tt forallrestricted}${}^1$\\
C.2.3.3&{\tt divide}&section \ref{C233}&{\tt forallrestricted}${}^1$\\
C.2.3.4&{\tt max}&section \ref{C234}&{\tt map}\\
C.2.3.5&{\tt min}&section \ref{C235}&{\tt map}\\
C.2.3.7&{\tt plus}&section \ref{C237}&{\tt forallrestricted}${}^1$\\
C.2.3.8&{\tt power}&section \ref{C238}&{\tt forallrestricted}${}^1$\\
C.2.3.9&{\tt quotient}&section \ref{C239}&As section \ref{C231}\\
C.2.3.10&{\tt times}&section \ref{C2310}&No formal MathML;\\
&&&As section \ref{C237}\\
C.2.3.18&{\tt times}&section \ref{C2318}&Apparently meaningless\\
C.2.3.23&{\tt real}&section \ref{C2323}&{\tt forallrestricted}${}^1$\\
C.2.5.1&{\tt int}&section \ref{C251}&As section \ref{C2272}\\
C.2.5.6&{\tt bvar}&section \ref{C256}&{\tt forallrestricted}${}^1$\\
C.2.5.8&{\tt divergence}&section \ref{C258}&Use {\tt limit1} CD\\
C.2.6.1&{\tt set}&section \ref{C261}&{\tt suchthat}\\
C.2.6.2&{\tt list}&section \ref{C262}&{\tt suchthat/list1}\\
C.2.6.7&{\tt subset}&section \ref{C267}&Apparently meaningless\\
C.2.7.1&{\tt sum}&section \ref{C271}&{\tt sum}\\
C.2.7.2&{\tt product}&section \ref{C272}&{\tt product}\\
C.2.7.3&{\tt limit}&section \ref{C273}&{\tt limit}\\
C.2.10.2&{\tt matrix}&section \ref{C2102}&No equivalent\\
C.2.11.3&{\tt rational}&section \ref{C2113}&{\tt forallrestricted}\\
C.2.11.6&{\tt primes}&section \ref{C2116}&{\tt forallrestricted}${}^1$\\
C.2.11.15&{\tt infinity}&section \ref{C211151}&{\tt forallrestricted}${}^1$\\
C.2.11.15&{\tt infinity}&section \ref{C211152}&Use {\tt limit1} CD\\
\end{tabular}
\begin{center}
${}^1$ or nothing special
\end{center}
\end{table}
\section{Appendix C}
\subsection{C.2.2.4 MMLdefinition: {\tt interval}}\label{C224}
This contains the following example.
\begin{verbatim}
<interval>
  <bvar><ci>x</ci></bvar>
  <condition>
    <apply><lt/><cn>0</cn><ci>x</ci></apply>
    </condition>
</interval>
\end{verbatim}
Presumably this represents $(0,\infty)$. Equally, this is presumably intended
to close over \verb+<interval>+, i.e. $x$ is bound in this expression, and
freely $\alpha$-convertible. However, it seems to JHD to be purely ``luck''
that this defines an interval. What about the following?
\begin{verbatim}
<interval>
  <bvar><ci>x</ci></bvar>
  <condition>
    <apply><lt/><cn>1</cn>
       <apply> <power/>
         <ci>x</ci>
         <cn>2</cn>
         </apply>
      </apply>
    </condition>
</interval>
\end{verbatim}
By the same logic, this is $(-\infty,-1)\cup(1,\infty)$.  As far as JHD can
see, this use of \verb+interval+ is basically a declaration of a set, coupled
with an assertion that that set is in fact an interval, which assertion is, in
fact, true in the first case, but not the second.
\par
The declaration of the set can be done with \verb+suchthat+, the assertion is
a problem OpenMath has not really addressed.
\subsection{C.2.2.5 MMLdefinition: {\tt inverse}}\label{C225}
This contains the following example (our formatting).
\begin{verbatim}
<apply><forall/>
  <bvar><ci>y</ci></bvar>
  <bvar><ci type="function">f</ci></bvar>
  <condition>
    <apply><in/>
      <ci>y</ci>
      <apply>
        <csymbol definitionURL="domain">
          <mtext>Domain</mtext></csymbol>
        <apply><inverse/><ci type="function">f</ci></apply>
      </apply>
    </apply>
  </condition>
  <apply><eq/>
    <apply><ci type="function">f</ci>
      <apply><apply><inverse/><ci type="function">f</ci></apply>
        <ci>y</ci>
      </apply>
    </apply>
    <ci>y</ci>
  </apply>
</apply>
\end{verbatim}
The associated textual description is 
\begin{verbatim}
ForAll( y, such y in domain( f^(-1) ), f( f^(-1)(y) ) = y
\end{verbatim}
which does not include the fact that $f$ is in the scope of $\forall$.
\par
This usage seems to be basically a ``typed quantifier'', and as such could
look like the following.
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS name="forallrestricted" cd="quant2"/>
    <OMA>
      <OMS name="domain" cd="fns1"/>
      <OMA>
        <OMS name="inverse" cd="fns1"/>
        <OMV name="f"/>
      </OMA>
    </OMA>
  </OMA>
  <OMBVAR> <OMV name="y"/> </OMBVAR>
  <OMA>
    <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMV name= "f"/>
      <OMA>
        <OMA>
          <OMS name="inverse" cd="fns1"/>
          <OMV name= "f"/>
        </OMA>
        <OMV name= "y"/>
      </OMA>
    </OMA>
    <OMV name= "y"/>
  </OMA>
</OMBIND>
\end{verbatim}
This resembles the ``vernacular'', and does not bind $f$. If we wanted to do
so, along the lines of the MathML, we would have to wrap the whole thing in
another \verb+forall+. The two cannot be combined, as we want to be able to
$\alpha$-convert $f$ in the argument of \verb+forallrestricted+, and, as MK's
note of the tele-conference reads:
\begin{quotation}\noindent
In particular, we do not
      want to accept the occurrence of the bound variable in the
      (complex) binding operator. In particular, the OpenMath2 standard
      restricts alpha-conversion to the second and third children of the
      OMBIND, which is consistent with this view.
\end{quotation} 
See section \ref{sec:defintcond} below for an example of where this rule
bites.
\subsection{C.2.2.7 MMLdefinition: {\tt condition}}
This section contains two examples.
\subsubsection{C.2.2.7(1) MMLdefinition: {\tt condition}}\label{C2271}
\begin{verbatim}
<condition>
  <apply><lt/>
    <apply><power/><ci>x</ci><cn>5</cn></apply>
    <cn>3</cn>
  </apply>
</condition>
\end{verbatim}
It is hard to understand the meaning of this fragment in isolation (and
presumably the reader was not intended to do so). If it was intended to be
part of an encoding of a set (mathematically, representing the interval
$(-\infty,3^{1/5})$, or possibly $[0,3^{1/5})$), then \verb+suchthat+ from
\verb+set1+ is appropriate. Here is the example from \verb+set1+ reworked to
match the MathML example (as $(-\infty,3^{1/5})$: if one wanted $[0,3^{1/5})$
one would have to add $x\ge0$, or change from $\bf R$ as the base set).
\begin{verbatim}
<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0"
       cdbase="http://www.openmath.org/cd">
  <OMA>
    <OMS cd="set1" name="suchthat"/>
    <OMS cd="setname1" name="R"/>
    <OMBIND>
      <OMS cd="fns1" name="lambda"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="relation1" name="lt"/>
        <OMA>
          <OMS cd="arith1" name="power"/>
          <OMV name="x"/>
          <OMI> 5 </OMI>
        </OMA>
        <OMI> 3 </OMI>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
\end{verbatim}
We should note that the OpenMath makes it clear that $x$ is bound by the
(\verb+OMBIND+ whose first child is the)
\verb+lambda+, whereas the MathML, being only a fragment, does not state the
scope.
\subsubsection{C.2.2.7(2) MMLdefinition: {\tt
condition}}\label{sec:defintcond}\label{C2272}
(Ouf formatting.)
\begin{verbatim}
<apply><int/>
  <bvar><ci>x</ci></bvar>
  <condition>
    <apply><in/><ci>x</ci><ci type="set">C</ci></apply>
  </condition>
  <apply><ci type="function">f</ci><ci>x</ci></apply>
</apply>
\end{verbatim}
This seems, to JHD, to be typical of the confusion that can arise over
\verb+condition+s. Let us look at this expression in the vernacular: 
\begin{equation}\label{defintcond}
\int_{x\in C}f(x){\rm d} x,
\end{equation}
and observe that this is probably equivalent to $\int_{C}f(x){\rm d} x$.
\par
In terms of \verb+calculus1+ (calculus with functions \cite{JHD})
this can be expressed as 
\begin{verbatim}
<OMA>
  <OMS cd="calculus1" name="defint"/>
  <OMV name="C"/>
  <OMV name="f"/>
</OMA>
\end{verbatim}
and $x$ doesn't appear at all. If one wants it to, then one writes
\begin{verbatim}
<OMA>
  <OMS cd="calculus1" name="defint"/>
  <OMV name="C"/>
  <OMBIND>
    <OMS cd="fns1" name="lambda"/>
    <OMBVAR>
      <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMV name="f"/>
      <OMV name="x"/>
    </OMA>
  </OMBIND>
</OMA>
\end{verbatim}
as in the example in \verb+calculus1+.
\par
MK's note \cite{MK} on \verb+calculus3+ (calculus with expressions \cite{JHD}), suggests (in MathML syntax)
\begin{verbatim}
<bind>
  <apply>
    <csymbol cd="calculus3">defintset</csymbol>
    <ci>C</ci>
  </apply>
  <bvar><ci>x</ci></bvar>
  <apply><ci>f</ci><ci>x</ci></apply>
</bind>
\end{verbatim}
which is a precise translation of the previous one from the language of
functions to expressions.
In OpenMath syntax it would be the following.
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS cd="calculus3" name="defintset"/>
    <OMV name="C"/>
  </OMA>
  <OMBVAR>
    <OMV name="x"/>
  </OMBVAR>
  <OMA>
    <OMV name="f"/>
    <OMV name="x"/>
  </OMA>
</bind>
\end{verbatim}
MK's note also suggests an alternative way of expressing (\ref{defintcond}),
which in MathML syntax would be the following.
\begin{verbatim}
<bind>
  <apply>
    <csymbol cd="calciulus3">defintcond</csymbol>
    <apply><in/>
      <ci>x</ci>
      <ci>C</ci>
    </apply>
  </apply>
  <bvar><ci>x</ci></bvar>
  <apply><ci>f</ci><ci>x</ci></apply>
</bind> 
\end{verbatim}
In OpenMath syntax it would be the following.
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS cd="calculus3" name="defintcond"/>
    <OMA>
      <OMS name="in" cd="set1"/>
      <OMV name="x"/>
      <OMV name="C"/>
    </OMA>
  </OMA>
  <OMBVAR>
    <OMV name="x"/>
  </OMBVAR>
  <OMA>
    <OMV name="f"/>
    <OMV name="x"/>
  </OMA>
</bind>
\end{verbatim}
This, however, falls foul of %OpenMath's rule that 
\begin{quotation}\noindent
the OpenMath2 standard restricts alpha-conversion to the second and third
children of the OMBIND
\end{quotation}
and hence JHD does not see how \verb+defintcond+ as postulated can make its
way into OpenMath.
\subsection{C.2.2.14 MMLdefinition: {\tt image}\label{C2214}}
This section contains the following example.
\begin{verbatim}
<apply><forall/>
  <bvar><ci>x</ci></bvar>
  <condition>
    <apply><in/>
      <ci>x</ci>
      <apply><image/><ci>f</ci></apply>
    </apply>
  </condition>
  <apply><in/>
    <ci>x</ci>
    <apply><codomain/><ci>f</ci></apply>
  </apply>
</apply>
\end{verbatim}
The following remarks could be made.
\begin{enumerate}
\item This cries out for \verb"forallrestricted".
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS name="forallrestricted" cd="quant2"/>
    <OMA>
      <OMS name="image" cd="fns1"/>
      <OMV name="f"/>
    </OMA>
  </OMA>
  <OMBVAR> <OMV name="x"/> </OMBVAR>
  <OMA>
    <OMS name="in" cd="set1"/>
    <OMV name="x"/> 
    <OMA>
      <OMS name="codomain" cd="fns1"/>
      <OMV name= "f"/>
    </OMA>
  </OMA>
</OMBIND>
\end{verbatim}
\item It is a pretty good case for the ``forall with implies'' trick.
\begin{verbatim}
<OMBIND>
  <OMS name="forall" cd="quant1"/>
  <OMBVAR> <OMV name="x"/> </OMBVAR>
  <OMA>
    <OMS name="implies" cd="logic1"/>
    <OMA>
      <OMS name="in" cd="set1"/>
      <OMV name="x"/> 
      <OMA>
        <OMS name="image" cd="fns1"/>
        <OMV name= "f"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS name="in" cd="set1"/>
      <OMV name="x"/> 
      <OMA>
        <OMS name="codomain" cd="fns1"/>
        <OMV name= "f"/>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
\end{verbatim}
\item Why use quantifiers at all?
\begin{verbatim}
<OMA>
  <OMS name="subset" cd="set1"/>
  <OMA>
    <OMS name="image" cd="fns1"/>
    <OMV name= "f"/>
  </OMA>
  <OMA>
    <OMS name="codomain" cd="fns1"/>
    <OMV name= "f"/>
  </OMA>
</OMBIND>
\end{verbatim}
Indeed there could be (possibly even ought to be, since in ZF it is the
{\it definition\/} of $\subset$) a FMP of \verb+subset+ that made this
equivalent to expression 2.
\end{enumerate}
\subsection{C.2.2.15 MMLdefinition: {\tt domainofapplication}}\label{C2215}
This contains the interesting statement
\begin{quotation}\noindent
Special cases of this qualifier can be abbreviated using one of interval
{\tt condition} or an ({\tt lowlimit},{\tt uplimit}) pair.
\end{quotation}
The examples given are
\begin{verbatim}
<apply><int/>
  <domainofapplication><ci>C</ci></domainofapplication>
  <ci>f </ci>
</apply>
\end{verbatim}
(which is a fairly straight-forward definite integral) and
\begin{verbatim}
<apply><int/>
      <domainofapplication>
        <set>
          <bvar><ci>t</ci></bvar>
          <condition>
            <apply><in/>
              <ci>t</ci>
              <ci type="set">C</ci>
            </apply>
          </condition>
        </set>
      </domainofapplication>
      <ci>f</ci>
</apply>
\end{verbatim}
which seems to this author to be a redundant variant. 
\subsection{C.2.3.1 MMLdefinition: {\tt quotient}}\label{C231}
This has the following property (presumably meant to be the equivalent of
OpenMath's FMP\footnote{OpenMath's FMP for {\tt quotient} in {\tt integer1} is
currently missing the proviso $b\ne0$.}).
\begin{verbatim} 
ForAll( [a,b], b != 0, a = b*quotient(a,b) + rem(a,b) )

<apply><forall/>
  <bvar><ci>a</ci></bvar>
  <bvar><ci>b</ci></bvar>
  <condition><apply><neq/><ci>b</ci><cn>0</cn></apply></condition>
  <apply><eq/>
    <ci>a</ci>
    <apply><plus/>
      <apply><times/>
          <ci>b</ci>
          <apply><quotient/><ci>a</ci><ci>b</ci></apply>
      </apply>
  <apply><rem/><ci>a</ci><ci>b</ci></apply>
    </apply>
  </apply>
</apply>
\end{verbatim}
Again, this seems to be a pretty good case for the ``forall with implies''
trick, though \verb+forallrestricted+ could be used.
\begin{verbatim}
<OMBIND>
  <OMS name="forall" cd="quant1"/>
  <OMBVAR> <OMV name="a"/> <OMV name="b"/> </OMBVAR>
  <OMA>
    <OMS name="implies" cd="logic1"/>
    <OMA>
      <OMS name="neq" cd="relation1"/>
      <OMV name="b"/> 
      <OMS name="zero" cd="arith1"/>
    </OMA>
    <OMA>
      <OMS name="eq" cd="relation1"/>
      <OMV name="a"/> 
      <OMA>
        <OMS name="plus" cd="arith1"/>
        <OMA>
          <OMS name="times" cd="arith1"/>
          <OMV name="b"/> 
          <OMA>
            <OMS name="quotient" cd="integer1"/>
            <OMV name="a"/> 
            <OMV name="b"/> 
          </OMA>
        </OMA>
        <OMA>
          <OMS name="remainder" cd="integer1"/>
          <OMV name="a"/> 
          <OMV name="b"/> 
        </OMA>
      </OMA>
    </OMA>
  </OMA>
</OMBIND>
\end{verbatim}
\subsection{C.2.3.2 MMLdefinition: {\tt factorial}}\label{C232}
This has the following property (presumably meant to be the equivalent of
OpenMath's FMP).
\begin{verbatim} 
ForAll( n, n \gt 0, n! = n*(n-1)! )

              
<apply><forall/>
  <bvar><ci>n</ci></bvar>
  <condition><apply><gt/><ci>n</ci><cn>0</cn></apply></condition>
  <apply><eq/>
    <apply><factorial/><ci>n</ci></apply>
    <apply><times/>
      <ci>n</ci>
      <apply><factorial/>
        <apply><minus/><ci>n</ci><cn>1</cn></apply>
      </apply>
    </apply>
  </apply>
</apply>
\end{verbatim}
Again, this seems to be a pretty good case for the ``forall with implies''
trick, though \verb+forallrestricted+ could be used.
\subsection{C.2.3.3 MMLdefinition: {\tt divide}}\label{C233}
This has the following property (presumably meant to be the equivalent of
OpenMath's FMP).
\begin{verbatim} 
ForAll( a, a!= 0, a/a = 1 ) 
          
<apply><forall/>
  <bvar><ci>a</ci></bvar>
  <condition><apply><neq/><ci>a</ci><cn>0</cn></apply></condition>
  <apply><eq/>
    <apply><divide/><ci>a</ci><ci>a</ci></apply>
    <cn>1</cn>
  </apply>
</apply>
\end{verbatim}
Again, this seems to be a pretty good case for the ``forall with implies''
trick, though \verb+forallrestricted+ could be used.
\subsection{C.2.3.4 MMLdefinition: {\tt max}}\label{C234}
This contains the interesting statement
\begin{quotation}\noindent
The elements may be listed explicitly or they may be described by a {\tt
domainofapplication}, for example, the maximum over all $x$ in the set $A$.
The {\tt domainofapplication} is often abbreviated by placing a {\tt
condition} directly on a bound variable. 
\end{quotation}
The example given is the following (our layout).
\begin{verbatim} 
<apply>
  <max/>
  <bvar><ci>y</ci></bvar>
  <condition>
    <apply>
      <in/>
      <ci>y</ci>
      <interval><cn>0</cn><cn>1</cn></interval>
    </apply>
  </condition>
  <apply><power/><ci> y</ci><cn>3</cn></apply>
</apply>
\end{verbatim}
As OpenMath does not have a \verb+max+ operator acting on functions,
the nearest translation would seem to be the following.
\begin{verbatim} 
<OMA>
  <OMS name="max" cd="minmax1"/>
  <OMA>
    <OMS name="map" cd="set1"/>
    <OMBIND>
      <OMS name="lambda" cd="fns1"/>
      <OMBVAR> <OMV name="y"/> </OMBVAR>
      <OMA>
        <OMS name="power" cd="arith1"/>
        <OMV name="y"/>
        <OMI> 3 </OMI>
      </OMA>
    </OMBIND>
    <OMA>
      <OMS name="interval_cc" cd="interval1"/>
      <OMI> 0 </OMI>
      <OMI> 1 </OMI>
    </OMA>
  </OMA>
</OMA>
\end{verbatim}
We note that OpenMath seems to require us to be precise about the species of
interval we want to use.
\subsection{C.2.3.5 MMLdefinition: {\tt min}}\label{C235}
Nothing new need be said here.
\subsection{C.2.3.7 MMLdefinition: {\tt plus}}\label{C237}
The property here is the following.
\begin{verbatim} 
    Commutativity 
    <apply><forall/>
      <bvar><ci>a</ci></bvar>
      <bvar><ci>b</ci></bvar>
      <condition>
        <apply><and/>
          <apply><in/><ci>a</ci><reals/></apply>
          <apply><in/><ci>b</ci><reals/></apply>
        </apply>
      </condition>
      <apply><eq/>
        <apply><plus/><ci>a</ci><ci>b</ci></apply>
        <apply><plus/><ci>b</ci><ci>a</ci></apply>
      </apply>
    </apply>
\end{verbatim}
Again, this seems to be a pretty good case for the ``forall with implies''
trick, though \verb+forallrestricted+ could be used.
\subsection{C.2.3.8 MMLdefinition: {\tt power}}\label{C238}
The property here is the following.
\begin{verbatim} 
ForAll( a, a!=0, a^0=1 ) 
<apply><forall/>
  <bvar><ci>a</ci></bvar>
  <condition><apply><neq/><ci>a</ci><cn>0</cn></apply></condition>
  <apply><eq/>
    <apply><power/><ci>a</ci><cn>0</cn></apply>
    <cn>1</cn>
  </apply>
</apply>
\end{verbatim}
Again, this seems to be a pretty good case for the ``forall with implies''
trick, though \verb+forallrestricted+ could be used.
\subsection{C.2.3.9 MMLdefinition: {\tt rem}}\label{C239}
This has the same property, and solution, as {\tt quotient} (section
\ref{C231}).
\subsection{C.2.3.10 MMLdefinition: {\tt times}}\label{C2310}
The property here is the following.
\begin{verbatim} 
ForAll( [a,b], condition(in({a,b}, Commutative)), a*b=b*a )
\end{verbatim}
However, no formal translation is given, and it is not clear what one would
be.
\par
Later on we see the following property, to which the same remark applies as in
section \ref{C237}.
\begin{verbatim} 
<apply><forall/>
  <bvar><ci>a</ci></bvar>
  <bvar><ci>b</ci></bvar>
  <condition>
    <apply><and/>
      <apply><in/><ci>a</ci><reals/></apply>
      <apply><in/><ci>b</ci><reals/></apply>
    </apply>
  </condition>
  <apply><eq/>
    <apply><times/><ci>a</ci><ci>b</ci></apply>
    <apply><times/><ci>b</ci><ci>a</ci></apply>
  </apply>
</apply> 
\end{verbatim}
\subsection{C.2.3.18 MMLdefinition: {\tt forall}}\label{C2318}
This contains the following example (our formatting).
\begin{verbatim}
<apply>
  <forall/>
  <bvar><ci> x </ci></bvar>
  <condition>
    <apply><lt/><ci> x </ci><cn> 0 </cn></apply>
  </condition>
  <ci> x </ci>
</apply>
\end{verbatim}
This seems to be $\forall x:x<0 x$. Since this last $x$ is not a Boolean, the
author respectfully submits that this example is ill-typed. In any case
\verb+forallrestricted+ would solve the issue. 
\subsection{C.2.3.23 MMLdefinition: {\tt real}}\label{C2323}
This contains the following property,
\begin{verbatim}
<apply><forall/>
  <bvar><ci>x</ci></bvar>
  <bvar><ci>y</ci></bvar>
  <condition>
    <apply><and/>
      <apply><in/><ci>x</ci><reals/></apply>
      <apply><in/><ci>y</ci><reals/></apply>
    </apply>
  </condition>
  <apply><eq/>
    <apply><real/>
      <apply><plus/>
        <ci> x </ci>
        <apply><times/><imaginaryi/><ci>y</ci></apply>
      </apply>
    </apply>
    <ci> x </ci>
  </apply>
</apply>
\end{verbatim}
Again, this seems to be a pretty good case for the ``forall with implies''
trick, though \verb+forallrestricted+ could be used.
\subsection{C.2.5.1 MMLdefinition: {\tt int}}\label{C251}
This contains the following example.
\begin{verbatim}
<apply><int/>
  <bvar><ci> x </ci></bvar>
  <condition>
    <apply><in/><ci> x </ci><ci type="set"> D </ci></apply>
  </condition>
  <apply><ci type="function"> f </ci><ci> x </ci></apply>
</apply>
\end{verbatim}
The discussion in section \ref{C2272} is appropriate here.
\subsection{C.2.5.6 MMLdefinition: {\tt bvar}}\label{C256}
This contains the following example (our formatting).
\begin{verbatim}
<apply><forall/><bvar><ci>x</ci></bvar>
  <condition><apply><in/><ci>x</ci><reals/></apply></condition>
  <apply>
    <eq/>
    <apply><minus/><ci>x</ci><ci>x</ci></apply>
    <cn>0</cn>
  </apply>
</apply>
\end{verbatim}
Again, this seems to be a pretty good case for the ``forall with implies''
trick, though c\verb+forallrestricted+ ould be used.
\subsection{C.2.5.8 MMLdefinition: {\tt divergence}}\label{C258}
This contains the following example.
\begin{verbatim}
<apply>
  <eq/>
  <apply><divergence/><ci type="vectorfield">a</ci></apply>
  <apply>
    <limit/>
    <bvar><ci> V </ci></bvar>
    <condition>
      <apply>
        <tendsto/>
        <ci> V </ci>
        <cn> 0 </cn>
      </apply>
    </condition>
    <apply>
      <divide/>
      <apply>
        <int encoding="text" definitionURL="SurfaceIntegrals.htm"/>
        <bvar><ci> S</ci></bvar>
        <ci> a </ci>
      </apply>
      <ci> V </ci>
    </apply>
  </apply>
</apply>
\end{verbatim}
Here the relevant part is the limit, which could be expressed (as it is in the
\verb+limit1+ CD) as the following.
\begin{verbatim}
<OMA>
  <OMS cd="limit1" name="limit"/>
  <OMI> 0 </OMI>
  <OMS cd="limit1" name="both_sides"/>
  <OMBIND>
    <OMS cd="fns1" name="lambda"/>
      <OMBVAR>
      <OMV name="V"/>
      </OMBVAR>
      ...
  </OMBIND>
</OMA>
\end{verbatim}
\subsection{C.2.6.1 MMLdefinition: {\tt set}}\label{C261}
This contains the following example.
\begin{verbatim}
<set>
  <bvar><ci> x </ci></bvar>
  <condition>
    <apply><lt/>
      <ci> x </ci>
      <cn> 5 </cn>
    </apply>
  </condition>
  <ci>x</ci>
</set>
\end{verbatim}
It is not clear what this means, but a plausible stab would seem to be the
following.
\begin{verbatim}
<OMA>
  <OMS cd="set1" name="suchthat"/>
  <OMS cd="setname1" name="N"/>
  <OMBIND>
    <OMS cd="fns1" name="lambda"/>
    <OMBVAR>
      <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="lt"/>
    <OMV name="x"/>
      <OMI> 5 </OMI>
    </OMA>
  </OMBIND>
</OMA>
\end{verbatim}
\subsection{C.2.6.2 MMLdefinition: {\tt list}}\label{C262}
This contains the following example.
\begin{verbatim}
<list order="numeric">
  <bvar><ci> x </ci></bvar>
  <condition>
    <apply><lt/>
      <ci> x </ci>
      <cn> 5 </cn>
    </apply>
  </condition>
</list>
\end{verbatim}
There is no direct translation into OpenMath for reaons other than
\verb+condition+, but \verb+sucthat+ in \verb+list1+ seems an obvious tool to
use.
\subsection{C.2.6.7 MMLdefinition: {\tt subset}}\label{C267}
This contains the following example.
\begin{verbatim}
<apply>
  <subset/>
  <subset/>
  <bvar><ci type="set">S</ci></bvar>
  <condition>
    <apply><in/>
      <ci>S</ci>
      <ci type="list">T</ci>
    </apply>
  </condition>
  <ci>S</ci>
</apply>
\end{verbatim}
Even assuming the second \verb+<subset/>+ to be a mistake, the present author
can make no sense of this.
\subsection{C.2.7.1 MMLdefinition: {\tt sum}}\label{C271}
This contains the following example (our formatting).
\begin{verbatim}
<apply><sum/>
  <bvar><ci> x </ci></bvar>
  <condition>
    <apply> <in/><ci> x </ci><ci type="set">B</ci></apply>
  </condition>
  <apply><ci type="function"> f </ci><ci> x </ci></apply>
</apply>
\end{verbatim}
This translates straightforwardly.
\begin{verbatim}
<OMA>
  <OMS name="sum" cd="arith1"/>
  <OMV name="S"/>
  <OMV name="f"/>
</OMA>
\end{verbatim}
We note that there is no need to name the dummy variable at all.
\subsection{C.2.7.2 MMLdefinition: {\tt product}}\label{C272}
The example, and its OpenMath translation, are essentially identicalto the
previous section.
\subsection{C.2.7.3 MMLdefinition: {\tt limit}}\label{C273}
This contains the following example (our formatting).
\begin{verbatim}
<apply><limit/>
  <bvar><ci>x</ci></bvar>
  <condition>
    <apply><tendsto/><ci>x</ci><cn>0</cn></apply>
  </condition>
  <apply><sin/><ci>x</ci></apply>
</apply>
\end{verbatim}
The equivalent OpenMath would be the following.
\begin{verbatim}
<OMA>
  <OMS cd="limit1" name="limit"/>
  <OMI> 0 </OMI>
  <OMS cd="limit1" name="both_sides"/>
  <OMS cd="transc1" name="sin"/>
  </OMBIND>
</OMA>
\end{verbatim}
We again note that there is no need to name the dummy variable at all.
\subsection{C.2.10.2 MMLdefinition: {\tt matrix}}\label{C2102}
This contains the following example (our formatting).
\begin{verbatim}
<matrix>
  <bvar><ci type="integer">i</ci></bvar>
  <bvar><ci type="integer">j</ci></bvar>
  <condition>
    <apply><and/>
      <apply><in/>
        <ci>i</ci>
        <interval><ci>1</ci><ci>5</ci></interval>
      </apply>
      <apply><in/>
        <ci>j</ci>
        <interval><ci>5</ci><ci>9</ci></interval>
      </apply>
    </apply>
  </condition>
  <apply><power/>
    <ci>i</ci>
    <ci>j</ci>
  </apply>
</vector>
\end{verbatim}
We can assume that this should end \verb+</matrix>+ instead of
\verb+</vector>+, but this has no equivalent in OpenMath.
\subsection{C.2.11.3 MMLdefinition: {\tt rational}}\label{C2113}
This contains the following property (our formatting).
\begin{verbatim}
    for all z where z is a rational, there exists 
      integers p and q with p/q = z
<apply><forall/>
  <bvar><ci>z</ci></bvar>
  <condition>
    <apply><in/><ci>z</ci><rationals/></apply>
    </condition>
  <apply><exists/>
    <bvar><ci>p</ci></bvar>
    <bvar><ci>q</ci></bvar>
    <apply><and/>
      <apply><in/><ci>p</ci><integers/></apply>
      <apply><in/><ci>q</ci><integers/></apply>
      <apply><eq/>
        <apply><divide/><ci>p</ci><ci>q</ci></apply>
        <ci>z</ci>
      </apply>
    </apply>
  </apply> 
\end{verbatim}
\verb+forallrestricted+ seems the obvious solution, though the implies trick
could also be used.
\subsection{C.2.11.6 MMLdefinition: {\tt primes}}\label{C2116}
This contains the following property (our formatting).
\begin{verbatim} 
ForAll( [d,p], p is prime, Implies( d | p , d=1 or d=p ) ) 
<apply><forall/>
  <bvar><ci>d</ci></bvar>
  <bvar><ci>p</ci></bvar>
  <condition>
    <apply><and/>
    <apply><in/><ci>p</ci><primes/></apply>
    <apply><in/><ci>d</ci><naturalnumbers/></apply>
    </apply>
  </condition>
  <apply><implies/>
    <apply><factorof/><ci>d</ci><ci>p</ci></apply>
    <apply><or/>
      <apply><eq/><ci>d</ci><cn>1</cn></apply>
      <apply><eq/><ci>d</ci><ci>p</ci></apply>
    </apply>
  </apply>
</apply>
\end{verbatim}
This could be encoded with the forall/implies trick, except that the result
would have two implication signs --- perfectly correct, but possibly harder to
read. We would need to nest \verb+forallrestricted+, as in the following.
\begin{verbatim}
<OMBIND>
  <OMA>
    <OMS name="forallrestricted" cd="quant2"/>
    <OMS name="N" cd="setname1"/>
  </OMA>
  <OMBVAR> <OMV name="d"/> </OMBVAR>
  <OMBIND>
    <OMA>
      <OMS name="forallrestricted" cd="quant2"/>
      <OMS name="P" cd="setname1"/>
    </OMA>
    <OMBVAR> <OMV name="p"/> </OMBVAR>
    ...
  </OMBIND>
</OMBIND> 
\end{verbatim}
\subsection{C.2.11.15 MMLdefinition: {\tt infinity}}\label{C21115}
This contains the following property and example (our formatting).
\subsubsection{C.2.11.15(1) MMLdefinition: {\tt infinity}}\label{C211151}
\begin{verbatim} 
    for all reals x, x \lt infinity
<apply><forall/>
  <bvar><ci>n</ci></bvar>
  <condition><apply><in/><ci>n</ci><reals/></apply></condition>
  <apply><lt/><ci>n</ci><infinity/></apply>
</apply>
\end{verbatim}
\verb+forallrestricted+ seems the obvious solution, though the implies trick
could also be used.
\subsubsection{C.2.11.15(2) MMLdefinition: {\tt infinity}}\label{C211152}
\begin{verbatim} 
<apply><eq/>
  <apply><limit/>
    <bvar><ci>x</ci></bvar>
    <condition>
      <apply><tendsto/><ci>x</ci><infinity/></apply>
      </condition>
    <apply><divide/><cn>1</cn><ci>x</ci></apply>
  </apply>
  <cn>0</cn>
</apply>
\end{verbatim}
From OpenMath's point of view, this is a straightforward limit.
\begin{verbatim} 
<OMA>
  <OMA>
    <OMS cd="limit1" name="limit"/>
    <OMS name="infinity" cd="nums1"/>
    <OMS cd="limit1" name="below"/>
    <OMBIND>
      <OMS cd="fns1" name="lambda"/>
      <OMBVAR> <OMV name="x"/> </OMBVAR>
      <OMA>
        <OMS name="divide" cd="arith1"/>
        <OMI> 1 </OMI>
        <OMV name="x"/>
      </OMA>
    </OMBIND>
  </OMA>
  <OMS cd="alg1" name="zero"/>
</OMA>
\end{verbatim}
\begin{thebibliography}{9}
\bibitem{JHD}
Davenport,J.H.,
OpenMath and MathML:
Differentiating between analysis and algebra.
\url{http://staff.bath.ac.uk/masjhd/differentiate.html},
October 4, 2008.
\bibitem{MK}
Michael Kohlhase
OpenMath3 without conditions: A Proposal for a
MathML3/OM3 Calculus Content Dictionary.
\url{http://svn.openmath.org/OpenMath3/doc/blue/noconds/note.tex},
September 6, 2008.
\end{thebibliography}
\end{document}
\pause
\begin{itemize}
\end{itemize}
\begin{verbatim}
\end{verbatim}
<OMA>
</OMA>