let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1 & I +* (Start-At (0,SCM+FSA)) c= s1 & I +* (Start-At (0,SCM+FSA)) c= s2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let J be Program of SCM+FSA; :: thesis: ( J is_closed_on s1 & J +* (Start-At (0,SCM+FSA)) c= s1 & J +* (Start-At (0,SCM+FSA)) c= s2 & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
assume that
A1: J is_closed_on s1 and
A2: J +* (Start-At (0,SCM+FSA)) c= s1 and
A3: J +* (Start-At (0,SCM+FSA)) c= s2 and
A4: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT holds
( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
A5: ProgramPart (Relocated (J,0)) = J by Th9;
s2 = s2 +* (J +* (Start-At (0,SCM+FSA))) by A3, FUNCT_4:79
.= Initialize (s2 +* J) by FUNCT_4:15
.= (Initialize s2) +* J by COMPOS_1:83 ;
then A6: ProgramPart (Relocated (J,0)) c= s2 by A5, FUNCT_4:26;
let i be Element of NAT ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
A7: (IC (Comput ((ProgramPart s1),s1,i))) + 0 = IC (Comput ((ProgramPart s1),s1,i)) ;
A8: IC s2 = IC (s2 +* (J +* (Start-At (0,SCM+FSA)))) by A3, FUNCT_4:79
.= IC ((s2 +* J) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= 0 by FUNCT_4:121 ;
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),0) = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) by COMPOS_1:91;
hence ( IC (Comput ((ProgramPart s1),s1,i)) = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) by A1, A2, A4, A7, A6, A8, Th42; :: thesis: verum