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

fix typo

Browse source
This commit is contained in:
Istvan Chung 2016-06-29 13:25:48 -04:00
parent ea371df876
commit 672e072072
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}. 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}$$ $$\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}$$ $$\ptsto{r}{0} \Rightarrow \; \ptsto{r}{?c}$$
Now we can finish the proof by reflexivity of $\Rightarrow$, learning $?c = 0$. Now we can finish the proof by reflexivity of $\Rightarrow$, learning $?c = 0$.