let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st s1 . (intloc 0) = 1 & 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 really-closed Program of SCM+FSA st s1 . (intloc 0) = 1 & 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 ;
let I be really-closed Program of SCM+FSA; :: thesis: ( s1 . (intloc 0) = 1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 implies DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2)) )
set s11 = Initialized s1;
set P11 = P1 +* I;
set s21 = Initialized s2;
set P21 = P2 +* I;
A1: I c= P1 +* I by FUNCT_4:25;
A2: I c= P2 +* I by FUNCT_4:25;
assume that
A3: s1 . (intloc 0) = 1 and
A4: I is_halting_on s1,P1 and
A5: DataPart s1 = DataPart s2 ; :: thesis: DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))
A6: Initialized s1 = Initialize s1 by A3, SCMFSA_M:18;
then A7: DataPart (Initialized s1) = DataPart s1 by MEMSTR_0:79;
s2 . (intloc 0) = 1 by A3, A5, SCMFSA_M:2;
then Initialized s2 = Initialize s2 by SCMFSA_M:18;
then A8: DataPart (Initialized s1) = DataPart (Initialized s2) by A5, A7, MEMSTR_0:79;
A9: P1 +* I halts_on Initialized s1 by A4, A6;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1)))))) = halt SCM+FSA by EXTPRO_1:def 15;
then CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1)))))) = halt SCM+FSA by A8, Th9, A1, A2;
then A10: P2 +* I halts_on Initialized s2 by EXTPRO_1:29;
I is_halting_on Initialized s1,P1 +* I by A4, A7, SCMFSA8B:5;
then A11: LifeSpan ((P1 +* I),(Initialized s1)) = LifeSpan ((P2 +* I),(Initialized s2)) by A8, Th10, A1, A2;
thus DataPart (IExec (I,P1,s1)) = DataPart (Result ((P1 +* I),(Initialized s1)))
.= DataPart (Comput ((P1 +* I),(Initialized s1),(LifeSpan ((P1 +* I),(Initialized s1))))) by A9, EXTPRO_1:23
.= DataPart (Comput ((P2 +* I),(Initialized s2),(LifeSpan ((P1 +* I),(Initialized s1))))) by A8, Th9, A1, A2
.= DataPart (Result ((P2 +* I),(Initialized s2))) by A11, A10, EXTPRO_1:23
.= DataPart (IExec (I,P2,s2)) ; :: thesis: verum