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 A1: ( loc in dom (ProgramPart p) & I = p . loc ) ; :: thesis: IncAddr I,k = (Relocated p,k) . (loc + k)
A2: ProgramPart p c= p by RELAT_1:88;
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 A4: loc + k in dom (ProgramPart (Relocated p,k)) by Th23;
A5: loc in dom (IncAddr (ProgramPart p),k) by A1, Def5;
A6: 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
.= (IncAddr (Shift (ProgramPart p),k),k) . (loc + k) by Th22
.= (Shift (IncAddr (ProgramPart p),k),k) . (loc + k) by Th19
.= (IncAddr (ProgramPart p),k) . loc by A5, VALUED_1:def 12
.= IncAddr ((ProgramPart p) /. loc),k by A1, Def5
.= IncAddr I,k by A1, A6, PARTFUN1:def 8 ;
hence IncAddr I,k = (Relocated p,k) . (loc + k) ; :: thesis: verum