diff --git a/docs/model.tex b/docs/model.tex index 2b8984db03c4fabac97153c623870bd1452f0657..772089a25b3604bd7bd32df939faeb651a3993db 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}