Missed loop invariant in big-step semantics

This commit is contained in:
Adam Chlipala 2020-04-05 09:30:01 -04:00
parent 7bc0425ccf
commit 477788abaa

View file

@ -3251,7 +3251,7 @@ $$\infer{\bigstep{(h, v, \{I\} \while{b}{c})}{(h', v')}}{
\denote{b}(h, v)
& \bigstep{(h, v, c; \{I\} \while{b}{c})}{(h', v')}
}
\quad \infer{\bigstep{(h, v, \while{b}{c})}{(h, v)}}{
\quad \infer{\bigstep{(h, v, \{I\} \while{b}{c})}{(h, v)}}{
\neg \denote{b}(h, v)
}$$