let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being FinPartState of S holds not IC S in dom (ProgramPart p)
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being FinPartState of S holds not IC S in dom (ProgramPart p)
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for p being FinPartState of S holds not IC S in dom (ProgramPart p)
let p be FinPartState of S; :: thesis: not IC S in dom (ProgramPart p)
A1: dom (ProgramPart p) c= IL by RELAT_1:87;
assume IC S in dom (ProgramPart p) ; :: thesis: contradiction
then reconsider l = IC S as Instruction-Location of S by A1, Def4;
not l in dom (ProgramPart p) by Th48;
hence contradiction by Th48; :: thesis: verum