let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for g being FinPartState of S st S is realistic holds
dom (ProgramPart (Relocated g,k)) = { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) }
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for g being FinPartState of S st S is realistic holds
dom (ProgramPart (Relocated g,k)) = { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) }
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N; :: thesis: for g being FinPartState of S st S is realistic holds
dom (ProgramPart (Relocated g,k)) = { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) }
let g be FinPartState of S; :: thesis: ( S is realistic implies dom (ProgramPart (Relocated g,k)) = { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) } )
assume S is realistic ; :: thesis: dom (ProgramPart (Relocated g,k)) = { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) }
hence dom (ProgramPart (Relocated g,k)) = dom (IncAddr (Shift (ProgramPart g),k),k) by Th69
.= dom (Shift (ProgramPart g),k) by Def15
.= { (il. S,(j + k)) where j is Element of NAT : il. S,j in dom (ProgramPart g) } by Def16 ;
:: thesis: verum