let m, n be Element of NAT ; :: thesis: for I being Program of SCM+FSA holds ProgramPart (Relocated (ProgramPart (Relocated I,m)),n) = ProgramPart (Relocated I,(m + n))
let I be Program of SCM+FSA ; :: thesis: ProgramPart (Relocated (ProgramPart (Relocated I,m)),n) = ProgramPart (Relocated I,(m + n))
thus ProgramPart (Relocated (ProgramPart (Relocated I,m)),n) = IncAddr (Shift (ProgramPart (ProgramPart (Relocated I,m))),n),n by SCMFSA_5:2
.= IncAddr (Shift (ProgramPart (Relocated I,m)),n),n by AMI_1:105
.= IncAddr (Shift (IncAddr (Shift (ProgramPart I),m),m),n),n by SCMFSA_5:2
.= IncAddr (IncAddr (Shift (Shift (ProgramPart I),m),n),m),n by SCMFSA_4:35
.= IncAddr (IncAddr (Shift (ProgramPart I),(m + n)),m),n by VALUED_1:22
.= IncAddr (Shift (ProgramPart I),(m + n)),(m + n) by SCMFSA_4:27
.= ProgramPart (Relocated I,(m + n)) by SCMFSA_5:2 ; :: thesis: verum