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 A4: Initialized s1 = Initialize s1 by Th18;
then A5: DataPart (Initialized s1) = DataPart s1 by MEMSTR_0:79;
assume that
A6: I is_closed_on s1,P1 and
A7: 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)) )
A8: I is_closed_on Initialized s1,P1 +* I by A6, A7, A5, SCMFSA8B:5;
assume A9: 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)) )

A10: now

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

end;

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

A13: now

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 A14: not f in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:42, TARSKI:def 2;
hence (Initialized s1) . f = s1 . f by FUNCT_4:11
.= s2 . f by A12
.= (Initialized s2) . f by A14, FUNCT_4:11 ;
:: thesis: verum

end;

A15: intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:41;
then (Initialized s1) . (intloc 0) = (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:13
.= (Initialized s2) . (intloc 0) by A15, FUNCT_4:13 ;
then A16: DataPart (Initialized s1) = DataPart (Initialized s2) by A10, A13, Th33;
A18: I c= P2 +* I by FUNCT_4:25;
A19: I c= P1 +* I by FUNCT_4:25;
A20: P1 +* I halts_on Initialized s1 by A7, A4, 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 A8, A16, Th43, A19, A18;
then A21: P2 +* I halts_on Initialized s2 by EXTPRO_1:29;
I is_halting_on Initialized s1,P1 +* I by A6, A7, A5, SCMFSA8B:5;
then A22: LifeSpan ((P1 +* I),(Initialized s1)) = LifeSpan ((P2 +* I),(Initialized s2)) by A8, A16, Th44, A19, A18;
thus DataPart (IExec (I,P1,s1)) = DataPart (Result ((P1 +* I),(Initialized s1)))
.= DataPart (Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1))))) by A20, EXTPRO_1:23
.= DataPart (Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1))))) by A8, A16, Th43, A19, A18
.= DataPart (Result ((P2 +* I),(Initialized s2))) by A22, A21, EXTPRO_1:23
.= DataPart (IExec (I,P2,s2)) ; :: thesis: verum