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