let s1, s2 be State of ; for I being Program of 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)
set D = Int-Locations \/ FinSeq-Locations ;
let I be Program of ; ( 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 that
A1:
s1 . (intloc 0 ) = 1
and
A2:
I is_closed_on s1
and
A3:
I is_halting_on s1
and
A4:
DataPart s1 = DataPart s2
; DataPart (IExec I,s1) = DataPart (IExec I,s2)
A5:
s1 +* (Initialized I) = s1 +* (I +* (Start-At (insloc 0 )))
by A1, Th18;
then A6:
DataPart (s1 +* (Initialized I)) = DataPart s1
by SCMFSA8A:11;
then A7:
I is_closed_on s1 +* (Initialized I)
by A2, A3, SCMFSA8B:8;
s2 . (intloc 0 ) = 1
by A1, A4, SCMFSA6A:38;
then
s2 +* (Initialized I) = s2 +* (I +* (Start-At (insloc 0 )))
by Th18;
then A8:
DataPart (s1 +* (Initialized I)) = DataPart (s2 +* (Initialized I))
by A4, A6, SCMFSA8A:11;
A9:
I +* (Start-At (insloc 0 )) c= Initialized I
by Th19;
Initialized I c= s1 +* (Initialized I)
by FUNCT_4:26;
then A10:
I +* (Start-At (insloc 0 )) c= s1 +* (Initialized I)
by A9, XBOOLE_1:1;
Initialized I c= s2 +* (Initialized I)
by FUNCT_4:26;
then A11:
I +* (Start-At (insloc 0 )) c= s2 +* (Initialized I)
by A9, XBOOLE_1:1;
A12:
ProgramPart (s1 +* (Initialized I)) halts_on s1 +* (Initialized I)
by A3, A5, SCMFSA7B:def 8;
then
CurInstr (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) = halt SCM+FSA
by AMI_1:def 46;
then
CurInstr (Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I)))) = halt SCM+FSA
by A7, A8, A10, A11, Th43;
then A13:
ProgramPart (s2 +* (Initialized I)) halts_on s2 +* (Initialized I)
by AMI_1:146;
I is_halting_on s1 +* (Initialized I)
by A2, A3, A6, SCMFSA8B:8;
then A14:
LifeSpan (s1 +* (Initialized I)) = LifeSpan (s2 +* (Initialized I))
by A7, A8, A10, A11, Th44;
thus DataPart (IExec I,s1) =
DataPart (Result (s1 +* (Initialized I)))
by SCMFSA8B:35
.=
DataPart (Computation (s1 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I))))
by A12, AMI_1:122
.=
DataPart (Computation (s2 +* (Initialized I)),(LifeSpan (s1 +* (Initialized I))))
by A7, A8, A10, A11, Th43
.=
DataPart (Result (s2 +* (Initialized I)))
by A14, A13, AMI_1:122
.=
DataPart (IExec I,s2)
by SCMFSA8B:35
; verum