From 7e477f28f2f21dfb609bd38723472f0c080a75dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ale=C5=A1=20Bizjak?= <abizjak@cs.au.dk>
Date: Wed, 27 Jul 2016 19:57:46 +0200
Subject: [PATCH] Removed obsolete axiom from the defn of Ex(M).
---
docs/constructions.tex | 2 --
1 file changed, 2 deletions(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 0840acd32..26cb9746e 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -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$.
--
GitLab