[Om] Multistep "equation" symbol?

[Lars Hellström]

Is there an established OM symbol for "multistep equations" (see 
example below)? If not, would it make sense as part of some official 
content dictionary?

The situation I'm thinking about is that of expressing something like 
the following LaTeX fragment:

   \sqrt{n^2+1} - n
   =
   n \left( \frac{1}{n}\sqrt{n^2+1} - 1 \right)
   =
   n \left( \sqrt{ 1 + \frac{1}{n^2} } - 1 \right)
   \stackrel{
     \text{(since \(\sqrt{1+x} \leq 1 + x/2\))}
   }{\leq}
   n \left( 1 + \frac{1}{2n^2}  - 1 \right)
   =
   \frac{1}{2n}
   \to
   0

(This is not my motivating example -- that would instead be the 
derivation of a rewrite rule from given axioms -- but this has the 
advantage of being immediately familiar.) Points to note are:

  * There are several steps in this thing, yet it constitutes
    a natural unit (in whatever document it is part of).

  * Not all steps employ the same relation.

  * Some instances of a relation carry remarks explaining why
    that step holds.

Partially transformed into OM, this might become

<OMA><OMS name="multistep">
   <OMFOREIGN encoding="LaTeX">
     \sqrt{n^2+1} - n
   </OMFOREIGN>
   <OMS cd="relation1" name="eq"/>
   <OMFOREIGN encoding="LaTeX">
     n \left( \frac{1}{n}\sqrt{n^2+1} - 1 \right)
   </OMFOREIGN>
   <OMS cd="relation1" name="eq"/>
   <OMFOREIGN encoding="LaTeX">
     n \left( \sqrt{ 1 + \frac{1}{n^2} } - 1 \right)
   </OMFOREIGN>
   <OMATTR>
     <OMATP>
       <OMS name="because">
       <OMFOREIGN encoding="LaTeX">
         \sqrt{1+x} \leq 1 + x/2 </OMFOREIGN>
     </OMATP>
     <OMS cd="relation1" name="leq"/>
   </OMATTR>
   <OMFOREIGN encoding="LaTeX">
     n \left( 1 + \frac{1}{2n^2}  - 1 \right)
   </OMFOREIGN>
   <OMS cd="relation1" name="eq"/>
   <OMFOREIGN encoding="LaTeX">
     \frac{1}{2n}
   </OMFOREIGN>
   <OMS cd="limit1" name="tendsto"/> <!-- Not quite right? -->
   <OMS cd="alg1" name="zero"/>
</OMA>

where an expression

<OMA><OMS name="multistep">
   x0 R1 x1 R2 x2 ... Rn xn
</OMA>

is equivalent to

<OMA><OMS cd="logic1" name="and"/>
   <OMA> R1 x0 x1 </OMA>
   <OMA> R2 x1 x2 </OMA>
   ...
   <OMA> Rn xn-1 xn </OMA>
</OMA>


Now, I suppose it could be argued that such a "multistep" symbol is 
unnecessary because of this equivalence -- I think there has been a 
similar argument that the elementary relation symbols should not be 
n-ary as the binary forms together with logic1#and suffice for 
expressing the same thing -- but my gut feeling is that this 
"multistep" is more than a mere conjunction of statements, even if that 
is exactly what it amounts to as far as logic is concerned. It might be 
that I'm letting concerns for presentation affect me -- my primary 
use-case is indeed to export derivations from the program that 
discovered them to another that will generate a presentation -- but it 
seems rather onerous to request from a presentation generator that it 
will reconstruct the underlying "multistep equation" from a logic1#and 
expression such as the above. Deciding what to combine and what not to 
combine is a delicate problem, which I'd rather not delegate to 
unqualified software or personnel.

Lars Hellström


PS: While typing up the example, I noticed that it probably wouldn't be 
correct since limit1#tendsto (MathML3-ish?) is defined to be ternary, 
requesting a type-of-limit as first argument. While I suppose one could 
use a lambda to work around that, I can't help wondering why the limit 
type is an argument in the first place; wouldn't an attribution be more 
appropriate?