let p be FinPartState of SCM+FSA ; :: thesis: for k, loc being Element of NAT
for I being Instruction of SCM+FSA 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+FSA st loc in dom (ProgramPart p) & I = p . loc holds
IncAddr I,k = (Relocated p,k) . (loc + k)
let I be Instruction of SCM+FSA ; :: 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 Th3;
A5: loc in dom (IncAddr [(ProgramPart p)],k) by A1, SCMFSA_4:def 6;
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 Th2
.= (Shift (IncAddr [(ProgramPart p)],k),k) . (loc + k) by SCMFSA_4:35
.= (IncAddr [(ProgramPart p)],k) . loc by A5, VALUED_1:def 12
.= IncAddr (pi [(ProgramPart p)],loc),k by A1, SCMFSA_4:24
.= IncAddr I,k by A1, A6, AMI_1:def 47 ;
hence IncAddr I,k = (Relocated p,k) . (loc + k) ; :: thesis: verum