diff --git a/hw2/while-semantics.pdf b/hw2/while-semantics.pdf
index a7d9bf8..311d8b2 100644
Binary files a/hw2/while-semantics.pdf and b/hw2/while-semantics.pdf differ
diff --git a/hw2/while-semantics.tex b/hw2/while-semantics.tex
index 2f35dcc..6f31556 100644
--- a/hw2/while-semantics.tex
+++ b/hw2/while-semantics.tex
@@ -150,9 +150,10 @@ such as sequencing operations ($e_1;e_2$).
 }
 \bsrule{B-WhileTrue}{
   \bstep{e_1}{\sigma}{\true}{\sigma'} \\
-  \bstep{e_2}{\sigma'}{v}{\sigma''}
+  \bstep{e_2}{\sigma'}{v_1}{\sigma''} \\
+  \bstep{\whilee{e_1}{e_2}}{\sigma''}{v}{\sigma'''}
 }{
-  \bstep{\whilee{e_1}{e_2}}{\sigma}{v}{\sigma''}
+  \bstep{\whilee{e_1}{e_2}}{\sigma}{v}{\sigma'''}
 }
 \bsrule{B-WhileFalse}{
   \bstep{e_1}{\sigma}{\false}{\sigma'}