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!
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.