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 (insloc 0 )) c= Initialized I by Th19;
Initialized I c= s1 +* (Initialized I) by FUNCT_4:26;
then A2: I +* (Start-At (insloc 0 )) c= s1 +* (Initialized I) by A1, XBOOLE_1:1;
Initialized I c= s2 +* (Initialized I) by FUNCT_4:26;
then A3: I +* (Start-At (insloc 0 )) 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 +* (I +* (Start-At (insloc 0 ))) 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;
A17: s1 +* (Initialized I) is halting by A7, A4, SCMFSA7B:def 8;
then CurInstr (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) = halt SCM+FSA by AMI_1:def 46;
then CurInstr (Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) = halt SCM+FSA by A8, A16, A2, A3, Th43;
then A18: s2 +* (Initialized I) is halting by AMI_1:def 20;
I is_halting_on s1 +* (Initialized I) by A6, A7, A5, SCMFSA8B:8;
then A19: LifeSpan (s1 +* (Initialized I)) = LifeSpan (s2 +* (Initialized I)) by A8, A16, A2, A3, Th44;
thus DataPart (IExec I,s1) = DataPart (Result (s1 +* (Initialized I))) by SCMFSA8B:35
.= DataPart (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) by A17, AMI_1:122
.= DataPart (Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) by A8, A16, A2, A3, Th43
.= DataPart (Result (s2 +* (Initialized I))) by A19, A18, AMI_1:122
.= DataPart (IExec I,s2) by SCMFSA8B:35 ; :: thesis: verum