let l be Element of NAT ; :: thesis: for I being Program of SCM+FSA holds ProgramPart (Relocated I,l) = IncAddr (Shift I,l),l
let I be Program of SCM+FSA ; :: thesis: ProgramPart (Relocated I,l) = IncAddr (Shift I,l),l
ProgramPart I = I by AMI_1:105;
hence ProgramPart (Relocated I,l) = (ProgramPart ((Start-At ((IC I) + l)) +* (IncAddr (Shift I,l),l))) +* (ProgramPart (DataPart I)) by FUNCT_4:75
.= (ProgramPart ((Start-At ((IC I) + l)) +* (IncAddr (Shift I,l),l))) +* {} by AMI_1:136
.= ProgramPart ((Start-At ((IC I) + l)) +* (IncAddr (Shift I,l),l)) by FUNCT_4:22
.= (ProgramPart (Start-At ((IC I) + l))) +* (ProgramPart (IncAddr (Shift I,l),l)) by FUNCT_4:75
.= {} +* (ProgramPart (IncAddr (Shift I,l),l)) by AMI_1:135
.= ProgramPart (IncAddr (Shift I,l),l) by FUNCT_4:21
.= IncAddr (Shift I,l),l by AMI_1:105 ;
:: thesis: verum