eth-janishutz/eth-summaries
1
0
Fork 0
mirror of https://github.com/janishutz/eth-summaries.git synced 2026-05-30 16:21:19 +02:00
Code Issues Packages Projects Releases Wiki Activity

[FMFP] Fix small error

Browse Source
This commit is contained in:
Janis Hutz
2026-05-04 09:18:14 +02:00
parent 3d6d85f4df
commit 1d38412334
2 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
semester4/fmfp/formal-methods-functional-programming-summary.pdf
BIN
View File
Binary file not shown.
semester4/fmfp/parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex
+1 -1
View File
@@ -36,7 +36,7 @@ In IMP however, this kind of action leads to equivalence:
\] \]
So what we have to prove is this: So what we have to prove is this:
\[ \[
\forall b, s, \sigma, \sigma'.(\vdash \langle \texttt{while b do s end}, \sigma \rangle \; \simeq \; \forall b, s, \sigma, \sigma'.(\vdash \langle \texttt{while b do s end}, \sigma \rangle \; \Leftrightarrow \;
\vdash \langle \texttt{if b then s; while b do s end end}, \sigma \rangle \rightarrow \sigma') \vdash \langle \texttt{if b then s; while b do s end end}, \sigma \rangle \rightarrow \sigma')
\] \]