From 33806ff8c2c3652b77de4722b9cc88ea61087464 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 13 Dec 2017 11:50:38 +0100
Subject: [PATCH] docs: entailment needs validity
---
docs/model.tex | 1 +
1 file changed, 1 insertion(+)
diff --git a/docs/model.tex b/docs/model.tex
index 2b8984db0..772089a25 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -117,6 +117,7 @@ We can now define \emph{semantic} logical entailment.
\forall \rs \in \monoid.\;
\forall \venv \in \Sem{\vctx},\;
\\&
+n \in \mval(\rs) \land
n \in \Sem{\vctx \proves \prop : \Prop}_\venv(\rs)
\Ra n \in \Sem{\vctx \proves \propB : \Prop}_\venv(\rs)
\end{aligned}
--
GitLab