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 +* (I +* (Start-At 0 ,SCM+FSA )) 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 0 ,SCM+FSA )) 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 AMI_1:def 46;
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 AMI_1:146;
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, AMI_1:122
.= 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, AMI_1:122
.= DataPart (IExec I,s2) by SCMFSA8B:35 ; :: thesis: verum