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 AMISTD_2:69
.= Reloc (ProgramPart (Relocated I,m)),n by RELAT_1:209
.= Reloc (Reloc (ProgramPart I),m),n by AMISTD_2:69
.= IncAddr (IncAddr (Shift (Shift (ProgramPart I),m),n),m),n by AMISTD_2:75
.= 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 AMISTD_2:69 ; :: thesis: verum