paquete semántico: premisas flotantes con \inferencia anidada

Question

Estoy escribiendo configurando una semántica de grandes pasos usando el paquete semanticy su comando \inference.

Yo uso el compilador LuaLaTeX.

Sin embargo, cuando compongo más inferencecomandos y uno de ellos representa un axioma, es decir, una regla sin premisas, la otra premisa comienza a flotar. Parece que está intentando realizar una alineación vertical.

Aquí hay un ejemplo:

\inference[\(\mathcal{E'}=\) \textsc{EC-IfF}]
{ 
    % ------- THIS PREMISE FLOATS
    \overset{\mathcal{E'_0}}
    {
             \langle b, σ \rangle \downarrow \texttt{false}
    }
    &
    {
        \inference
        [\textsc{EC-Skip}]
        {}
        {
        \langle \texttt{skip}, σ \rangle \downarrow σ
    }
    }
}
{
            \langle
            \texttt{if } b \texttt{ then } 
            (c_0 ; \texttt{ while } b \texttt{ do } c_0)
            \texttt{ else skip}, σ
            \rangle
    \downarrow
    σ''
}

Answer 1

En el ejemplo del OP, la línea de base se conserva en todo el "numerador" grande. Si bien se puede argumentar que esa es la forma correcta de hacerlo, se puede anular ese valor predeterminado aplicándolo \abovebaseline[-\dp\strutbox]{...}a la inferencia ED-Skip.

\documentclass{article}
\usepackage{semantic,amsmath,stackengine}
\begin{document}
\inference[\(\mathcal{E'}=\) \textsc{EC-IfF}]
{ 
    % ------- THIS PREMISE FLOATS
    \overset{\mathcal{E'_0}}
    {
             \langle b, σ \rangle \downarrow \texttt{false}
    }
    &
    {
        \abovebaseline[-\dp\strutbox]{\inference
        [\textsc{EC-Skip}]
        {}
        {
        \langle \texttt{skip}, σ \rangle \downarrow σ
    }}
    }
}
{
            \langle
            \texttt{if } b \texttt{ then } 
            (c_0 ; \texttt{ while } b \texttt{ do } c_0)
            \texttt{ else skip}, σ
            \rangle
    \downarrow
    σ''
}
\end{document}