pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #13 from ichung/typo

Browse source 
fix typo
This commit is contained in:
Adam Chlipala 2016-06-30 14:13:41 -04:00 committed by GitHub
commit 2354de6eca
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -3254,7 +3254,7 @@ We start by matching $\ptsto{p}{q}$ with $\ptsto{p}{?a}$, learning that $?a = q$
This crucial step relies on the three key properties of $*$, given in the second row of rules above: commutativity, associativity, and cancellativity\index{cancellativity}.
$$\ptsto{q}{r} * \ptsto{r}{0} \Rightarrow \; \ptsto{?b}{?c} \; * \; \ptsto{q}{?b}$$
We run another cancellation step of $\ptsto{q}{r}$ against $\ptsto{q}{?b}$, learning $?q = r$.
We run another cancellation step of $\ptsto{q}{r}$ against $\ptsto{q}{?b}$, learning $?b = r$.
$$\ptsto{r}{0} \Rightarrow \; \ptsto{r}{?c}$$
Now we can finish the proof by reflexivity of $\Rightarrow$, learning $?c = 0$.