pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-03 17:36:19 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Update frap_book.tex

Browse source 
Typo? Otherwise for \infer{ s \to^* s } that would assume an identity closure which afaik is not necessary.
This commit is contained in:
Lef Ioannidis 2018-03-10 16:23:58 -05:00 committed by GitHub
parent 078e29f8a9
commit 47d82f10b8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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

@ -1017,7 +1017,7 @@ Actually, the words ``state machine'' suggest to many people that the state set
\end{definition} \end{definition}
For an arbitrary transition relation $\to$, not just the one defined above for factorial, we define its \emph{transitive-reflexive closure}\index{transitive-reflexive closure} $\to^*$ with two inference rules: For an arbitrary transition relation $\to$, not just the one defined above for factorial, we define its \emph{transitive-reflexive closure}\index{transitive-reflexive closure} $\to^*$ with two inference rules:
$$\infer{s \to^* s}{} $$\infer{s \to^* s'}{}
\quad \infer{s \to^* s''}{ \quad \infer{s \to^* s''}{
s \to s' s \to s'
& s' \to^* s'' & s' \to^* s''