# How to prove the following properties of Small-step semantics?

I have to prove the following 2 properties of the Small-step semantics of the WHILE programming language:

• If $\langle C_1; C_2, s\rangle \rightarrow^k s'$ then there is a state $s''$ and natural numbers $k_1$ and $k_2$ such that $\langle C_1;s \rangle \rightarrow^{k_1} s''$ and $\langle C_2; s'' \rangle \rightarrow^{k_2} s'$ where $k_1 + k_2 = k$.
• If $\langle C_1, s \rangle \rightarrow^k s'$ then $\langle C_1; C_2, s \rangle \rightarrow^k \langle C_2, s'\rangle$.

I am not quite sure which kind of induction I should use. I am not asking for a full proof, I would rather appreciate some hints on which kind of induction I should use in this case. Thanks in advance!

## 1 Answer

I suggest to proceed by induction on $k$. For the inductive basis and step you'll have to look at all the possible cases that the relevant reduction step $\langle C, s \rangle$ can be derived.

• thank you for your answer. I think I figured it out already, using the same approach as you suggested. Apr 4, 2014 at 16:47