mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
Merge pull request #38 from mdempsky/parity-subtract
Add missing "O - O = E" abstraction case
This commit is contained in:
commit
72c0bc3a04
1 changed files with 1 additions and 0 deletions
|
@ -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 \\
|
||||
|
|
Loading…
Reference in a new issue