wip coinductive notation

Author: conrad-watt

document/core/exec/relaxed.rst

@@ -77,11 +77,12 @@ Traces
 A trace is a coinductive set of :ref:`events <syntax-evt>`. A trace is considered to be a *pre-execution* of a given :ref:`global configuration <syntax-config>` if it can be derived from the events emitted by the coinductive closure of the :ref:`global reduction relation <syntax-reduction>` on that configuration, and all the :ref:`time stamps <syntax-time>` of its constituent events are distinct.
 
 .. math::
-   \frac{
-     \config \stepto^{\evt} \config' \qquad \vdash \config' : \trace \qquad \timeevt(\evt) \notin \timeevt^\ast(\trace)
-   }{
-     \vdash \config : \evt~\trace
-   }
+     \begin{array}{c}
+       \config \stepto^{\evt} \config' \qquad \vdash \config' : \trace \qquad \timeevt(\evt) \notin \timeevt^\ast(\trace) \\[0.2\normalbaselineskip]
+       \hline \\[-0.8\normalbaselineskip]
+       \hline \\[-0.8\normalbaselineskip]
+       \vdash \config : \evt~\trace
+     \end{array}
 
 When a WebAssembly program is executed, all behaviours observed during that execution must correspond to a single :ref:`consistent <relaxed-consistent>` pre-execution of that execution's starting :ref:`configuration <syntax-config>`.