fmfp.tex

$$
\begin{aligned}
s_{body} &\equiv x:=x+1\\
s_{loop} &\equiv \text{while } x-y < 0 \text{ do } s_{body} \text{ end}\\
s &\equiv (x:=3;y:=4);s_{loop}
\end{aligned}
$$

$$
\begin{aligned}
\langle s, \sigma\rangle &\rightarrow^1_1 \langle y:=4; s_{loop},\sigma[x \mapsto3] \rangle\\
&\rightarrow^1_1 \langle s_{loop},\sigma[x, y \mapsto3, 4] \rangle\\
&\rightarrow^1_1 \langle \text{if }x -y < 0 \text{ then } s_{body}; s_{loop} \text{ else skip end},\sigma[x, y \mapsto 3, 4] \rangle\\
&\rightarrow^1_1 \langle s_{body}; s_{loop} ,\sigma[x, y \mapsto3, 4] \rangle\\
&\rightarrow^1_1 \langle s_{loop} ,\sigma[x, y \mapsto 4, 4] \rangle\\
&\rightarrow^1_1 \langle \text{if }x -y < 0 \text{ then } s_{body}; s_{loop} \text{ else skip end},\sigma[x, y \mapsto 4, 4] \rangle\\
&\rightarrow^1_1 \langle \text{skip},\sigma[x, y \mapsto 4, 4] \rangle\\
&\rightarrow^1_1 \sigma[x, y \mapsto 4, 4] = \sigma'\\
\end{aligned}
$$

$$
\cfrac
{\cfrac{\cfrac{}{\langle x:=3,\sigma\rangle \rightarrow_1\sigma[x\mapsto3]}ASS_{SOS}}{\langle x:=3;y:=4, \sigma\rangle \rightarrow_1 \langle y:=4,\sigma[x \mapsto3] \rangle}SEQ1_{SOS}}
{\langle (x:=3;y:=4);s_{loop}, \sigma\rangle \rightarrow_1 \langle y:=4; s_{loop},\sigma[x \mapsto3] \rangle} SEQ2_{SOS}
$$