set D = Int-Locations \/ FinSeq-Locations ;
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)
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);
assume A1: 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) )
assume A2: ( I is_closed_on s1 & 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) )
assume A3: 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) )
assume A4: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: DataPart (IExec I,s1) = DataPart (IExec I,s2)
A5: ( Initialized I c= s1 +* (Initialized I) & Initialized I c= s2 +* (Initialized I) ) by FUNCT_4:26;
A6: s1 +* (Initialized I) = s1 +* (I +* (Start-At (insloc 0 ))) by A1, Th18;
then DataPart (s1 +* (Initialized I)) = DataPart s1 by SCMFSA8A:11;
then A7: ( I is_closed_on s1 +* (Initialized I) & I is_halting_on s1 +* (Initialized I) ) by A2, SCMFSA8B:8;

A8: now

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

end;

A10: now

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

end;

A12: 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 A12, FUNCT_4:14 ;
then A13: DataPart (s1 +* (Initialized I)) = DataPart (s2 +* (Initialized I)) by A8, A10, Th33;
I +* (Start-At (insloc 0 )) c= Initialized I by Th19;
then A14: ( I +* (Start-At (insloc 0 )) c= s1 +* (Initialized I) & I +* (Start-At (insloc 0 )) c= s2 +* (Initialized I) ) by A5, XBOOLE_1:1;
then A15: LifeSpan (s1 +* (Initialized I)) = LifeSpan (s2 +* (Initialized I)) by A7, A13, Th44;
A16: s1 +* (Initialized I) is halting by A2, A6, SCMFSA7B:def 8;
then ( CurInstr (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) = halt SCM+FSA & ( for k being Element of NAT st CurInstr (Computation (s1 +* (Initialized I)),k) = halt SCM+FSA holds
LifeSpan (s1 +* (Initialized I)) <= k ) ) by AMI_1:def 46;
then CurInstr (Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) = halt SCM+FSA by A7, A13, A14, Th43;
then A17: s2 +* (Initialized I) is halting by AMI_1:def 20;
thus DataPart (IExec I,s1) = DataPart (Result (s1 +* (Initialized I))) by SCMFSA8B:35
.= DataPart (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) by A16, AMI_1:122
.= DataPart (Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) by A7, A13, A14, Th43
.= DataPart (Result (s2 +* (Initialized I))) by A15, A17, AMI_1:122
.= DataPart (IExec I,s2) by SCMFSA8B:35 ; :: thesis: verum