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