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))
set D = Int-Locations \/ FinSeq-Locations;
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 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 ; :: thesis: DataPart (IExec (I,s1)) = DataPart (IExec (I,s2))
A5: s1 +* (Initialized I) = s1 +* (Initialize I) 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 +* (Initialize I) by Th18;
then A8: DataPart (s1 +* (Initialized I)) = DataPart (s2 +* (Initialized I)) by A4, A6, SCMFSA8A:11;
A9: I +* (Start-At (0,SCM+FSA)) c= Initialized I by Th19;
Initialized I c= s1 +* (Initialized I) by FUNCT_4:26;
then A10: I +* (Start-At (0,SCM+FSA)) c= s1 +* (Initialized I) by A9, XBOOLE_1:1;
Initialized I c= s2 +* (Initialized I) by FUNCT_4:26;
then A11: I +* (Start-At (0,SCM+FSA)) c= s2 +* (Initialized I) by A9, XBOOLE_1:1;
TX11: ProgramPart (s1 +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by AMI_1:123;
TX21: ProgramPart (s2 +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by AMI_1:123;
A12: ProgramPart (s1 +* (Initialized I)) halts_on s1 +* (Initialized I) by A3, A5, SCMFSA7B:def 8;
then CurInstr ((ProgramPart (s1 +* (Initialized I))),(Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))))))) = halt SCM+FSA by EXTPRO_1:def 14;
then CurInstr ((ProgramPart (s2 +* (Initialized I))),(Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))))))) = halt SCM+FSA by A7, A8, A10, A11, Th43, TX11, TX21;
then A13: ProgramPart (s2 +* (Initialized I)) halts_on s2 +* (Initialized I) by EXTPRO_1:30;
I is_halting_on s1 +* (Initialized I) by A2, A3, A6, SCMFSA8B:8;
then A14: LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I))) = LifeSpan ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I))) by A7, A8, A10, A11, Th44;
thus DataPart (IExec (I,s1)) = DataPart (Result ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))) by SCMFSA8B:35
.= DataPart (Comput ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by A12, EXTPRO_1:23
.= DataPart (Comput ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)),(LifeSpan ((ProgramPart (s1 +* (Initialized I))),(s1 +* (Initialized I)))))) by A7, A8, A10, A11, Th43
.= DataPart (Result ((ProgramPart (s2 +* (Initialized I))),(s2 +* (Initialized I)))) by A14, A13, EXTPRO_1:23
.= DataPart (IExec (I,s2)) by SCMFSA8B:35 ; :: thesis: verum