let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
set D = Data-Locations ;
let I be Program of SCM+FSA; :: thesis: ( s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
set s11 = Initialized s1;
set P11 = P1 +* I;
set s21 = Initialized s2;
set P21 = P2 +* I;
assume s1 . (intloc 0) = 1 ; :: thesis: ( not I is_closed_on s1,P1 or not I is_halting_on s1,P1 or ex a being read-write Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
then A1: Initialized s1 = Initialize s1 by SCMFSA_M:18;
then A2: DataPart (Initialized s1) = DataPart s1 by MEMSTR_0:79;
assume that
A3: I is_closed_on s1,P1 and
A4: I is_halting_on s1,P1 ; :: thesis: ( ex a being read-write Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
A5: I is_closed_on Initialized s1,P1 +* I by A3, A4, A2, SCMFSA8B:5;
assume A6: for a being read-write Int-Location holds s1 . a = s2 . a ; :: thesis: ( ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )

A7: now :: thesis: for a being read-write Int-Location holds (Initialized s1) . a = (Initialized s2) . a

let a be read-write Int-Location; :: thesis: (Initialized s1) . a = (Initialized s2) . a
( a <> intloc 0 & a <> IC ) by SCMFSA_2:56;
then A8: not a in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
hence (Initialized s1) . a = s1 . a by FUNCT_4:11
.= s2 . a by A6
.= (Initialized s2) . a by A8, FUNCT_4:11 ;
:: thesis: verum

end;

assume A9: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))

A10: now :: thesis: for f being FinSeq-Location holds (Initialized s1) . f = (Initialized s2) . f

let f be FinSeq-Location ; :: thesis: (Initialized s1) . f = (Initialized s2) . f
( f <> intloc 0 & f <> IC ) by SCMFSA_2:57, SCMFSA_2:58;
then A11: not f in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def 2;
hence (Initialized s1) . f = s1 . f by FUNCT_4:11
.= s2 . f by A9
.= (Initialized s2) . f by A11, FUNCT_4:11 ;
:: thesis: verum

end;

A12: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:10;
then (Initialized s1) . (intloc 0) = (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:13
.= (Initialized s2) . (intloc 0) by A12, FUNCT_4:13 ;
then A13: DataPart (Initialized s1) = DataPart (Initialized s2) by A7, A10, SCMFSA_M:20;
A14: I c= P2 +* I by FUNCT_4:25;
A15: I c= P1 +* I by FUNCT_4:25;
A16: P1 +* I halts_on Initialized s1 by A4, A1, SCMFSA7B:def 7;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1)))))) = halt SCM+FSA by EXTPRO_1:def 15;
then CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1)))))) = halt SCM+FSA by A5, A13, Th17, A15, A14;
then A17: P2 +* I halts_on Initialized s2 by EXTPRO_1:29;
I is_halting_on Initialized s1,P1 +* I by A3, A4, A2, SCMFSA8B:5;
then A18: LifeSpan ((P1 +* I),(Initialized s1)) = LifeSpan ((P2 +* I),(Initialized s2)) by A5, A13, Th18, A15, A14;
thus DataPart (IExec (I,P1,s1)) = DataPart (Result ((P1 +* I),(Initialized s1)))
.= DataPart (Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1))))) by A16, EXTPRO_1:23
.= DataPart (Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1))))) by A5, A13, Th17, A15, A14
.= DataPart (Result ((P2 +* I),(Initialized s2))) by A18, A17, EXTPRO_1:23
.= DataPart (IExec (I,P2,s2)) ; :: thesis: verum