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 & I is_halting_on s1 & ( 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,s1)) = DataPart (IExec (I,s2))
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of SCM+FSA; :: thesis: ( s1 . (intloc 0) = 1 & I is_closed_on s1 & I is_halting_on s1 & ( 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,s1)) = DataPart (IExec (I,s2)) )
set s11 = s1 +* (Initialized I);
set s21 = s2 +* (Initialized I);
A1: I +* (Start-At (0,SCM+FSA)) c= Initialized I by Th19;
Initialized I c= s1 +* (Initialized I) by FUNCT_4:26;
then A2: I +* (Start-At (0,SCM+FSA)) c= s1 +* (Initialized I) by A1, XBOOLE_1:1;
Initialized I c= s2 +* (Initialized I) by FUNCT_4:26;
then A3: I +* (Start-At (0,SCM+FSA)) c= s2 +* (Initialized I) by A1, XBOOLE_1:1;
assume s1 . (intloc 0) = 1 ; :: thesis: ( not I is_closed_on s1 or not I is_halting_on s1 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,s1)) = DataPart (IExec (I,s2)) )
then A4: s1 +* (Initialized I) = s1 +* (Initialize I) by Th18;
then A5: DataPart (s1 +* (Initialized I)) = DataPart s1 by SCMFSA8A:11;
assume that
A6: I is_closed_on s1 and
A7: I is_halting_on s1 ; :: 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,s1)) = DataPart (IExec (I,s2)) )
A8: I is_closed_on s1 +* (Initialized I) by A6, A7, A5, SCMFSA8B:8;
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,s1)) = DataPart (IExec (I,s2)) )

A10: now

let a be read-write Int-Location ; :: thesis: (s1 +* (Initialized I)) . a = (s2 +* (Initialized I)) . a
A11: not a in dom (Initialized I) by SCMFSA6A:48;
hence (s1 +* (Initialized I)) . a = s1 . a by FUNCT_4:12
.= s2 . a by A9
.= (s2 +* (Initialized I)) . a by A11, FUNCT_4:12 ;
:: thesis: verum

end;

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

A13: now

let f be FinSeq-Location ; :: thesis: (s1 +* (Initialized I)) . f = (s2 +* (Initialized I)) . f
A14: not f in dom (Initialized I) by SCMFSA6A:49;
hence (s1 +* (Initialized I)) . f = s1 . f by FUNCT_4:12
.= s2 . f by A12
.= (s2 +* (Initialized I)) . f by A14, FUNCT_4:12 ;
:: thesis: verum

end;

A15: intloc 0 in dom (Initialized I) by SCMFSA6A:45;
then (s1 +* (Initialized I)) . (intloc 0) = (Initialized I) . (intloc 0) by FUNCT_4:14
.= (s2 +* (Initialized I)) . (intloc 0) by A15, FUNCT_4:14 ;
then A16: DataPart (s1 +* (Initialized I)) = DataPart (s2 +* (Initialized I)) by A10, A13, Th33;
TX11: ProgramPart (s1 +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by AMI_1:123;
TX21: ProgramPart (s2 +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by AMI_1:123;
A17: ProgramPart (s1 +* (Initialized I)) halts_on s1 +* (Initialized I) by A7, A4, SCMFSA7B:def 8;
then CurInstr ((ProgramPart (s1 +* (Initialized I))),(Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))))))) = halt SCM+FSA by EXTPRO_1:def 14;
then CurInstr ((ProgramPart (s2 +* (Initialized I))),(Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))))))) = halt SCM+FSA by A8, A16, A2, A3, Th43, TX11, TX21;
then A18: ProgramPart (s2 +* (Initialized I)) halts_on s2 +* (Initialized I) by EXTPRO_1:30;
I is_halting_on s1 +* (Initialized I) by A6, A7, A5, SCMFSA8B:8;
then A19: LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))) = LifeSpan ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I))) by A8, A16, A2, A3, Th44;
thus DataPart (IExec (I,s1)) = DataPart (Result ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))) by SCMFSA8B:35
.= DataPart (Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by A17, EXTPRO_1:23
.= DataPart (Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by A8, A16, A2, A3, Th43
.= DataPart (Result ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)))) by A19, A18, EXTPRO_1:23
.= DataPart (IExec (I,s2)) by SCMFSA8B:35 ; :: thesis: verum