test/phase5/exact-contextual-abbreviation-consumer.tex


1
2
3
4
5
6
7
8
9
10
11

\import{test/phase5/exact-contextual-abbreviation.tex}

\begin{abbreviation}\label{phase5_context_quantified}
    $a$ is phase five universally absorbing iff
    for all $b$ we have $a\phasefivedot b = a$.
\end{abbreviation}

\begin{abbreviation}\label{phase5_context_quantified_explicit}
    $A$ is a phase five explicit universal absorber of $a$ iff
    for all $b$ we have $\phasefivecombine[A](a,b) = a$.
\end{abbreviation}