let s, s1 be State of SCMPDS; :: thesis:
let n0, n1, n2 be Nat; :: thesis:
let c1, c2 be Integer; :: thesis:
assume A1: for i being Nat st i >= n0 & i <> n1 & i <> n2 holds
s1 . (intpos i) = s . (intpos i) ; :: thesis:
assume A2: n1 <= n2 ; :: thesis:
assume A3: ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( c1 <= n1 & n2 <= c2 & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) ; :: thesis:

per cases by A3;

suppose A4: ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) ; :: thesis:

hereby :: thesis:

let i be Nat; :: thesis:
assume that
A5: i >= n0 and
( i < c1 or i > c2 ) ; :: thesis:

suppose ( i <> n1 & i <> n2 ) ; :: thesis:

hence s1 . (intpos i) = s . (intpos i) by A1, A5; :: thesis:

end;

suppose A6: ( not i <> n1 or not i <> n2 ) ; :: thesis:

hereby :: thesis:

per cases by A6;

suppose i = n1 ; :: thesis:

hence s1 . (intpos i) = s . (intpos i) by A4; :: thesis:

end;

suppose i = n2 ; :: thesis:

hence s1 . (intpos i) = s . (intpos i) by A4; :: thesis:

end;

end;

end;

end;

end;

end;

end;

suppose A7: ( c1 <= n1 & n2 <= c2 & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ; :: thesis:

hereby :: thesis:

let i be Nat; :: thesis:
assume that
A8: i >= n0 and
A9: ( i < c1 or i > c2 ) ; :: thesis:

per cases by A9;

suppose i < c1 ; :: thesis:

then i < n1 by A7, XXREAL_0:2;
hence s1 . (intpos i) = s . (intpos i) by A1, A2, A8; :: thesis:

end;

suppose i > c2 ; :: thesis:

then i > n2 by A7, XXREAL_0:2;
hence s1 . (intpos i) = s . (intpos i) by A1, A2, A8; :: thesis:

end;

end;

end;

end;

end;