# structural operational semantic equivalence

We add the following derivation rule to the structural operational semantic:

< repeat S until b, s >$$\Rightarrow$$ < S; if b then skip else (repeat S until b) >

Prove that "repeat S until b" is equivalent to "S; if b then skip else (repeat S until b)" in the structural operational semantic.

I've tried the following:

In one direction:

Asumming < S; if b then skip else (repeat S until b), s > $$\Rightarrow^*$$ s'

We can prove < repeat S until b, s > $$\Rightarrow$$ s'

by using the specified derivation rule and the assumption:

< repeat S until b, s >$$\Rightarrow$$ < S; if b then skip else (repeat S until b) > $$\Rightarrow$$ s'

How can we prove the other direction?