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
.= (s2 +* J) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:15
.= (s2 +* (Start-At 0 ,SCM+FSA )) +* 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 (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 Th8;
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