...show

Note that I use functional notation for the state transition relations and ; more importantly, because they are both functions, it's sound to use equational reasoning in the proof.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.