let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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 & DataPart s1 = DataPart s2 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 & DataPart s1 = DataPart s2 holds
DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
set D = Data-Locations SCM+FSA;
let I be Program of SCM+FSA; :: thesis: ( s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 implies DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
set s11 = s1 +* (Initialized I);
set P11 = P1 +* I;
set s21 = s2 +* (Initialized I);
set P21 = P2 +* I;
A1: I c= P1 +* I by FUNCT_4:26;
A2: I c= P2 +* I by FUNCT_4:26;
assume that
A3: s1 . (intloc 0) = 1 and
A4: I is_closed_on s1,P1 and
A5: I is_halting_on s1,P1 and
A6: DataPart s1 = DataPart s2 ; :: thesis: DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
A7: s1 +* (Initialized I) = s1 +* (Initialize I) by A3, Th18;
then A8: DataPart (s1 +* (Initialized I)) = DataPart s1 by SCMFSA8A:11;
then A9: I is_closed_on s1 +* (Initialized I),P1 +* I by A4, A5, SCMFSA8B:8;
s2 . (intloc 0) = 1 by A3, A6, SCMFSA6A:38;
then s2 +* (Initialized I) = s2 +* (Initialize I) by Th18;
then A10: DataPart (s1 +* (Initialized I)) = DataPart (s2 +* (Initialized I)) by A6, A8, SCMFSA8A:11;
A11: Initialize I c= Initialized I by Th19;
Initialized I c= s1 +* (Initialized I) by FUNCT_4:26;
then A12: Initialize I c= s1 +* (Initialized I) by A11, XBOOLE_1:1;
Initialized I c= s2 +* (Initialized I) by FUNCT_4:26;
then A13: Initialize I c= s2 +* (Initialized I) by A11, XBOOLE_1:1;
ProgramPart I = I by RELAT_1:209;
then A14: P1 +* I halts_on s1 +* (Initialized I) by A5, A7, SCMFSA7B:def 8;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialized I)),(LifeSpan ((P1 +* I),(s1 +* (Initialized I))))))) = halt SCM+FSA by EXTPRO_1:def 14;
then CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialized I)),(LifeSpan ((P1 +* I),(s1 +* (Initialized I))))))) = halt SCM+FSA by A9, A10, A12, A13, Th43, A1, A2;
then A15: P2 +* I halts_on s2 +* (Initialized I) by EXTPRO_1:30;
I is_halting_on s1 +* (Initialized I),P1 +* I by A4, A5, A8, SCMFSA8B:8;
then A16: LifeSpan ((P1 +* I),(s1 +* (Initialized I))) = LifeSpan ((P2 +* I),(s2 +* (Initialized I))) by A9, A10, A12, A13, Th44, A1, A2;
thus DataPart (IExec (I,P1,s1)) = DataPart (Result ((P1 +* I),(s1 +* (Initialized I)))) by SCMFSA8B:35
.= DataPart (Comput ((P1 +* I),(s1 +* (Initialized I)),(LifeSpan ((P1 +* I),(s1 +* (Initialized I)))))) by A14, EXTPRO_1:23
.= DataPart (Comput ((P2 +* I),(s2 +* (Initialized I)),(LifeSpan ((P1 +* I),(s1 +* (Initialized I)))))) by A9, A10, A12, A13, Th43, A1, A2
.= DataPart (Result ((P2 +* I),(s2 +* (Initialized I)))) by A16, A15, EXTPRO_1:23
.= DataPart (IExec (I,P2,s2)) by SCMFSA8B:35 ; :: thesis: verum