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 & DataPart s1 = DataPart s2 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 & DataPart s1 = DataPart s2 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 & I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 ) ; :: thesis: DataPart (IExec I,s1) = DataPart (IExec I,s2)
A2: ( Initialized I c= s1 +* (Initialized I) & Initialized I c= s2 +* (Initialized I) ) by FUNCT_4:26;
s2 . (intloc 0 ) = 1 by A1, SCMFSA6A:38;
then A3: ( s1 +* (Initialized I) = s1 +* (I +* (Start-At (insloc 0 ))) & s2 +* (Initialized I) = s2 +* (I +* (Start-At (insloc 0 ))) ) by A1, Th18;
then A4: DataPart (s1 +* (Initialized I)) = DataPart s1 by SCMFSA8A:11;
then A5: ( I is_closed_on s1 +* (Initialized I) & I is_halting_on s1 +* (Initialized I) ) by A1, SCMFSA8B:8;
A6: DataPart (s1 +* (Initialized I)) = DataPart (s2 +* (Initialized I)) by A1, A3, A4, SCMFSA8A:11;
I +* (Start-At (insloc 0 )) c= Initialized I by Th19;
then A7: ( I +* (Start-At (insloc 0 )) c= s1 +* (Initialized I) & I +* (Start-At (insloc 0 )) c= s2 +* (Initialized I) ) by A2, XBOOLE_1:1;
then A8: LifeSpan (s1 +* (Initialized I)) = LifeSpan (s2 +* (Initialized I)) by A5, A6, Th44;
A9: s1 +* (Initialized I) is halting by A1, A3, 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 A5, A6, A7, Th43;
then A10: 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 A9, AMI_1:122
.= DataPart (Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) by A5, A6, A7, Th43
.= DataPart (Result (s2 +* (Initialized I))) by A8, A10, AMI_1:122
.= DataPart (IExec I,s2) by SCMFSA8B:35 ; :: thesis: verum