let k be Element of NAT ; :: thesis: for p being FinPartState of SCM+FSA holds dom (ProgramPart (Relocated p,k)) = { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }
let p be FinPartState of SCM+FSA ; :: thesis: dom (ProgramPart (Relocated p,k)) = { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }
thus dom (ProgramPart (Relocated p,k)) = dom (IncAddr [(Shift (ProgramPart p),k)],k) by Th2
.= dom [(Shift (ProgramPart p),k)] by SCMFSA_4:def 6
.= { (j + k) where j is Element of NAT : j in dom (ProgramPart p) } by VALUED_1:def 12 ; :: thesis: verum