[Om] Mathematical Vernacular in formulae

[Peter Horn]

Hey!

> $\{\langle a,b\rangle\bigl|\text{$a\in T$ and $P$ terminates for $a$ with $b$}\}$

Whenever I advertise OM (and I did that quite some times in the last
couple of years), I tell people that OM is focusing on semantics and
that (normally) all semantics is encoded in OMSs, whereas everything
else is just 'stupid' building blocks.

This is an example where the actual semantics is encoded in
whatever-but-not-an-OMS, so from a formal point of view I'm quite
unhappy. I think introducing a terminates_for symbol is the right way
to go.

It is probably impossible to use one language for both, semantics and markup...

Just my 5 shekel,
    Peter