From ebcd23ee6c2e60ac3a2f592d3e021753fbf6e054 Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Mon, 16 Mar 2020 12:58:20 -0700
Subject: [PATCH] Add missing "O - O = E" abstraction case

This case is implemented by parity_subtract in
AbstractInterpretation.v and is necessary to calculate the "most
precise abstraction."

See also #28, #37.
---
 frap_book.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/frap_book.tex b/frap_book.tex
index fe226d6..53ec2c6 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -1984,6 +1984,7 @@ As an example, consider this formalization of even-odd analysis, whose proof of
   \O \; \hat{+} \; \O &=& \E \\
   \_ \; \hat{+} \; \_ &=& \top \\
   \E \; \hat{-} \; \E &=& \E \\
+  \O \; \hat{-} \; \O &=& \E \\
   \_ \; \hat{-} \; \_ &=& \top \\
   \E \; \hat{\times} \; \_ &=& \E \\
   \_ \; \hat{\times} \; \E &=& \E \\