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