Exercise 1

Visual

Exercise 2

y := n;
result := 1;
while !y > 0 do
	(result := !result * !x;
	 y := !y - 1)

while True do skip

Configurations are $C_{1}; (C_{2}; C_{3})$ and $(C_{1}, C_{2}), C_{3}$ . Transitions for the first one are:

Transitions for the second one are:

Based on the properties:

If $⟨ C \cdot ni l, ni l, m ⟩ \Rightarrow ⟨ ni l, r, m^{'} ⟩$ , then $⟨ C \cdot c \cdot ni l, ni l, m ⟩ \Rightarrow ⟨ c, r, m^{'} ⟩$ .
If $⟨ c \cdot ni l, ni l, m ⟩$ does not terminate then $⟨ C \cdot c, ni l, m ⟩$ does not terminate.

We can prove that they have the same semantics as they:

In PLD work repository.