let p be FinPartState of SCM; :: thesis: for k, loc being Element of NAT
for I being Instruction of SCM st loc in dom (ProgramPart p) & I = p . loc holds
IncAddr (I,k) = (Relocated (p,k)) . (loc + k)
let k, loc be Element of NAT ; :: thesis: for I being Instruction of SCM st loc in dom (ProgramPart p) & I = p . loc holds
IncAddr (I,k) = (Relocated (p,k)) . (loc + k)
let I be Instruction of SCM; :: thesis: ( loc in dom (ProgramPart p) & I = p . loc implies IncAddr (I,k) = (Relocated (p,k)) . (loc + k) )
assume that
A1: loc in dom (ProgramPart p) and
A2: I = p . loc ; :: thesis: IncAddr (I,k) = (Relocated (p,k)) . (loc + k)
A3: loc in dom (IncAddr ((ProgramPart p),k)) by A1, COMPOS_1:def 40;
reconsider i = loc as Element of NAT ;
i + k in { (j + k) where j is Element of NAT : j in dom (ProgramPart p) } by A1;
then loc + k in dom (Reloc ((ProgramPart p),k)) by COMPOS_1:117;
then A4: loc + k in dom (ProgramPart (Relocated (p,k))) by COMPOS_1:116;
ProgramPart p c= p by RELAT_1:88;
then A5: I = (ProgramPart p) . loc by A1, A2, GRFUNC_1:8;
ProgramPart (Relocated (p,k)) c= Relocated (p,k) by RELAT_1:88;
then (Relocated (p,k)) . (loc + k) = (ProgramPart (Relocated (p,k))) . (loc + k) by A4, GRFUNC_1:8
.= (Reloc ((ProgramPart p),k)) . (loc + k) by COMPOS_1:116
.= (Shift ((IncAddr ((ProgramPart p),k)),k)) . (loc + k) by Th19
.= (IncAddr ((ProgramPart p),k)) . loc by A3, VALUED_1:def 12
.= IncAddr (((ProgramPart p) /. loc),k) by A1, COMPOS_1:def 40
.= IncAddr (I,k) by A1, A5, PARTFUN1:def 8 ;
hence IncAddr (I,k) = (Relocated (p,k)) . (loc + k) ; :: thesis: verum