let s1, s2 be State of SCM+FSA ; :: thesis:
let I be Program of SCM+FSA ; :: thesis:
let a be Int-Location ; :: thesis:
assume that
A1: for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d and
A2: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis:

A3: now

let d be Int-Location ; :: thesis:
assume A4: a <> d ; :: thesis:

per cases ;

suppose A5: d = intloc 0 ; :: thesis:

hence (Initialize s1) . d = 1 by SCMFSA6C:3
.= (Initialize s2) . d by A5, SCMFSA6C:3 ;
:: thesis:

end;

suppose d <> intloc 0 ; :: thesis:

then A6: not d is read-only by SF_MASTR:def 5;
hence (Initialize s1) . d = s1 . d by SCMFSA6C:3
.= s2 . d by A1, A4, A6
.= (Initialize s2) . d by A6, SCMFSA6C:3 ;
:: thesis:

end;

set S1 = s1 +* (Initialized I);
set S2 = s2 +* (Initialized I);
assume A7: I does_not_refer a ; :: thesis:
A8: s2 +* (Initialized I) = (Initialize s2) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
assume that
A9: I is_closed_on Initialize s1 and
A10: I is_halting_on Initialize s1 ; :: thesis:

A11: now

let f be FinSeq-Location ; :: thesis:
thus (Initialize s1) . f = s1 . f by SCMFSA6C:3
.= s2 . f by A2
.= (Initialize s2) . f by SCMFSA6C:3 ; :: thesis:

end;

then I is_halting_on Initialize s2 by A7, A9, A10, A3, Th40;
then A12: s2 +* (Initialized I) is halting by A8, SCMFSA7B:def 8;
A13: s1 +* (Initialized I) = (Initialize s1) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
then A14: s1 +* (Initialized I) is halting by A10, SCMFSA7B:def 8;

let l be Element of NAT ; :: thesis:
assume l < LifeSpan (s1 +* (Initialized I)) ; :: thesis:
then CurInstr (Computation (s1 +* (Initialized I)),l) <> halt SCM+FSA by A14, AMI_1:def 46;
hence CurInstr (Computation (s2 +* (Initialized I)),l) <> halt SCM+FSA by A7, A9, A3, A11, A13, A8, Th38; :: thesis:

end;

hereby :: thesis:

let d be Int-Location ; :: thesis:
assume A19: a <> d ; :: thesis:
thus (IExec I,s1) . d = (Result (s1 +* (Initialized I))) . d by Th36, SCMFSA6A:30
.= (Result (s2 +* (Initialized I))) . d by A7, A9, A3, A11, A13, A8, A17, A18, A19, Th38
.= (IExec I,s2) . d by Th36, SCMFSA6A:30 ; :: thesis:

end;

hereby :: thesis:

let f be FinSeq-Location ; :: thesis:
thus (IExec I,s1) . f = (Result (s1 +* (Initialized I))) . f by Th36, SCMFSA6A:31
.= (Result (s2 +* (Initialized I))) . f by A7, A9, A3, A11, A13, A8, A17, A18, Th38
.= (IExec I,s2) . f by Th36, SCMFSA6A:31 ; :: thesis:

end;

thus IC (IExec I,s1) = IC (Result (s1 +* (Initialized I))) by SCMFSA8A:7
.= IC (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) by A14, AMI_1:122
.= IC (Computation (s2 +* (Initialized I)),(LifeSpan (s2 +* (Initialized I)))) by A7, A9, A3, A11, A13, A8, A16, Th38
.= IC (Result (s2 +* (Initialized I))) by A12, AMI_1:122
.= IC (IExec I,s2) by SCMFSA8A:7 ; :: thesis: