Commit 7e477f28 authored by Aleš Bizjak's avatar Aleš Bizjak

Removed obsolete axiom from the defn of Ex(M).

parent 93f602ed
Pipeline #2459 passed with stage
......@@ -163,8 +163,6 @@ The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
\infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
\axiom{\munit \nequiv{n} \munit}
\axiom{\bot \nequiv{n} \bot}
\end{mathpar}
$\exm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment