# SS Exercise Session Lecture 9


$s := [x \mapsto 3, y \mapsto 5]$

$\langle x:= 2; (skip; y := 3), s \rangle \to s[x \mapsto 2, y \mapsto 3] = [x \mapsto 2, y \mapsto 3]$

$\langle x:= 2, s\rangle \to s[x \mapsto 2]$
$\langle(skip; y := 3), s \rangle \to s[x \mapsto 2][y \mapsto 3]$

$\langle x:= 2, s\rangle \to s[x \mapsto 2]$
$\langle skip, s[x \mapsto 2] \rangle \to s[x \mapsto 2]$
$\langle y := 3, s[x \mapsto 2] \rangle \to s[x \mapsto 2][y \mapsto 3]$


$\langle S, s \rangle \Rightarrow \langle \textbf{if } x \geq y \textbf{ then } (x := x-1; y := y+1; \textbf{ while } x \geq y \textbf { do } x := x-1; y := y+1;) \textbf{ else skip}, s \rangle$
$\langle \textbf{if } b \textbf{ then } (S_1; \textbf{ while b do } S_1) \textbf{ else skip}, s \rangle \Rightarrow $

$\
a_0+\cfrac{1}{a_1+\cfrac{1}{a_2+\cfrac{1}{a_3+\cdots}}}
]$

$\[
\cfrac[l]{1}{\sqrt{2}+
\cfrac[r]{1}{\sqrt{2}+
\cfrac{1}{\sqrt{2}+\dotsb}}}
\]$