let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis:
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
A2: for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d and
A3: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis:

A4: now

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

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

hence (Initialized s1) . d = 1 by SCMFSA6A:38
.= (Initialized s2) . d by A6, SCMFSA6A:38 ;
:: thesis:

end;

suppose d <> intloc 0 ; :: thesis:

then A7: not d is read-only by SF_MASTR:def 5;
hence (Initialized s1) . d = s1 . d by SCMFSA6C:3
.= s2 . d by A2, A5, A7
.= (Initialized s2) . d by A7, SCMFSA6C:3 ;
:: thesis:

end;

end;

end;

set S1 = Initialized s1;
set Q1 = P1 +* I;
set S2 = Initialized s2;
set Q2 = P2 +* I;
assume A8: not I refers a ; :: thesis:
A9: Initialized s2 = Initialize (Initialized s2) by MEMSTR_0:44;
assume that
A10: I is_closed_on Initialized s1,P1 and
A11: I is_halting_on Initialized s1,P1 ; :: thesis:

A12: now

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

end;

then I is_halting_on Initialized s2,P2 by A8, A10, A11, A4, Th40;
then A13: P2 +* I halts_on Initialized s2 by A9, SCMFSA7B:def 7;
A14: Initialized s1 = Initialize (Initialized s1) by MEMSTR_0:44;
then A15: P1 +* I halts_on Initialized s1 by A11, SCMFSA7B:def 7;

let l be Element of NAT ; :: thesis:
assume l < LifeSpan ((P1 +* I),(Initialized s1)) ; :: thesis:
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialized s1),l))) <> halt SCM+FSA by A15, EXTPRO_1:def 15;
hence CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),l))) <> halt SCM+FSA by A8, A10, A4, A12, A14, A9, Th38; :: thesis:

end;

then A16: for l being Element of NAT st CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),l))) = halt SCM+FSA holds
LifeSpan ((P1 +* I),(Initialized s1)) <= l ;
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1)))))) = CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1)))))) by A8, A10, A4, A12, A14, A9, Th38
.= halt SCM+FSA by A15, EXTPRO_1:def 15 ;
then A17: LifeSpan ((P1 +* I),(Initialized s1)) = LifeSpan ((P2 +* I),(Initialized s2)) by A13, A16, EXTPRO_1:def 15;
then A18: Result ((P2 +* I),(Initialized s2)) = Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1)))) by A13, EXTPRO_1:23;
A19: Result ((P1 +* I),(Initialized s1)) = Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1)))) by A15, EXTPRO_1:23;
X1: Result ((P1 +* I),(Initialized s1)) = IExec (I,P1,s1) by Th36;
X2: Result ((P2 +* I),(Initialized s2)) = IExec (I,P2,s2) by Th36;
thus for d being Int-Location st a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d by X2, X1, A8, A10, A4, A12, A14, A9, A18, A19, Th38; :: thesis:
thus for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f by X2, X1, A8, A10, A4, A12, A14, A9, A18, A19, Th38; :: thesis:
thus IC (IExec (I,P1,s1)) = IC (Result ((P1 +* I),(Initialized s1))) by SCMFSA6B:def 1
.= IC (Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1))))) by A15, EXTPRO_1:23
.= IC (Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P2 +* I),(Initialized s2))))) by A8, A10, A4, A12, A14, A9, A17, Th38
.= IC (Result ((P2 +* I),(Initialized s2))) by A13, EXTPRO_1:23
.= IC (IExec (I,P2,s2)) by SCMFSA6B:def 1 ; :: thesis: