Developing invariants for comparing two strings

Question

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string):

X = S1   
Y = S2

E = true   
// (1)
while X != /\ and Y != /\ and E == true          
  if head(X) == head(Y)           
    X = tail(X)
    Y = tail(Y)
  else
    E = false
// (2)
if !(X == /\ and Y == /\)    
  E = false 
  // (3) S1 != S2 \land E = false
// (4) S1 = S2 <=> E = true
return E

I want to develop invariants at points (1) and (2).

The invariant at (1) I choose is $$S_1 = S_2 \iff X = Y \land E = true.$$

From it, I can derive an invariant at (2):

$$(S_1 = S_2 \iff X = Y \land E = true) \land \lnot(X \neq \Lambda \land Y \neq \Lambda \land E = true).$$

Then I tried to simplify the formula:

$$(S_1 = S_2 \iff X = Y \land E = true) \land (X = \Lambda \lor Y = \Lambda \lor E = false)\\ \equiv \big((S_1 = S_2 \iff X = Y \land E = true) \land (X = \Lambda)\big) \lor \\ \big((S_1 = S_2 \iff X = Y \land E = true) \land (Y = \Lambda)\big) \lor \\ \big((S_1 = S_2 \iff X = Y \land E = true) \land (E = false)\big) \\ \equiv (S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true) \lor \\ (S_1 = S_2 \iff X = \Lambda \land Y = \Lambda \land E = true) \lor \\ \big((S_1 = S_2 \iff X = Y \land E = true) \land (E = false)\big)\\ \equiv \big(S_1 = S_2 \iff (X = \Lambda \land Y = \Lambda) \land (E = true)\big) \lor \\ \big((S_1 = S_2 \iff X = Y \land E = true) \land (E = false)\big)$$

My problems are

• Is the derivation above correct? If so, how to further simplify this formula? In particular, how to deal with the second disjunction? Is it simply $S_1 \neq S_2 \land E = false$?
• How does the invariant at (3) and (4) follow from the one at (2)?
• Can we obtain an invariant at (2) in a single conjunct instead of multiple disjuncts?