Isn't this the same as saying: $\langle S, s\rangle \rightarrow s = \langle S, s\rangle \rightarrow s$ implies that $s=s$? Why do they use a different prime symbol here even though they are the same statement $S$ being executed on the same state $s$.
2nd Question: How does this statement by the author above allow us to "uniquely determine a final state s' if (and only if) the execution of S terminates"
I think I'm missing the point here because this definition came after Induction on the Shape of Derivation Trees.
3rd Question: How will this proof help us perform induction on the shape of derivation trees?