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)) = Reloc ((ProgramPart (ProgramPart (Relocated (I,m)))),n) by COMPOS_1:116
.= Reloc ((ProgramPart (Relocated (I,m))),n) by RELAT_1:209
.= Reloc ((Reloc ((ProgramPart I),m)),n) by COMPOS_1:116
.= IncAddr ((IncAddr ((Shift ((Shift ((ProgramPart I),m)),n)),m)),n) by COMPOS_1:121
.= IncAddr ((IncAddr ((Shift ((ProgramPart I),(m + n))),m)),n) by VALUED_1:22
.= Reloc ((ProgramPart I),(m + n)) by SCMFSA_4:27
.= ProgramPart (Relocated (I,(m + n))) by COMPOS_1:116 ; :: thesis: verum