This program proof technique doesn't specifically account for infinite loops.  It's just if your program does infinite loop, you'll never et your proof to work.

We say that <c,SIGMA>-/->

if there is no memory mapping that SIGMA leads to under command c.  In other words, if the program infinite loops (does not terminate).

Infinite loops are part of this derivation technique, but we don't have a specific symbol for the infinite loop, all we have is the -/-> which
just means the program has no answer.

To prove that two programs are identical, you have to prove that always yield the same result in all situations (ie memory mappings); this isn't always hard to do and you certainly don't have to list them all, but you may have to break them up into cases.

To prove that two programs are NOT identical, all you have to find one memory mapping (assignment of variables) in which the answers do not match.