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 (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 SCM+FSA ; :: 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 A1: ( J is_closed_on s1 & J +* (Start-At (insloc 0 )) c= s1 & J +* (Start-At (insloc 0 )) c= s2 & 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) )
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) )
A2: (IC (Computation s1,i)) + 0 = IC (Computation s1,i) ;
A3: s2 = s2 +* (J +* (Start-At (insloc 0 ))) by A1, FUNCT_4:79
.= (s2 +* J) +* (Start-At (insloc 0 )) by FUNCT_4:15
.= (s2 +* (Start-At (insloc 0 ))) +* J by SCMFSA6B:14 ;
ProgramPart (Relocated J,0 ) = J by Th9;
then A4: ProgramPart (Relocated J,0 ) c= s2 by A3, FUNCT_4:26;
A5: IncAddr (CurInstr (Computation s1,i)),0 = CurInstr (Computation s1,i) by Th8;
IC s2 = IC (s2 +* (J +* (Start-At (insloc 0 )))) by A1, FUNCT_4:79
.= IC ((s2 +* J) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= insloc 0 by AMI_1:111 ;
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, A5, Th42; :: thesis: verum