let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of IL,N
for l being Instruction-Location of S holds DataPart (Start-At l) = {}
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of IL,N
for l being Instruction-Location of S holds DataPart (Start-At l) = {}
let S be non empty IC-Ins-separated AMI-Struct of IL,N; :: thesis: for l being Instruction-Location of S holds DataPart (Start-At l) = {}
let l be Instruction-Location of S; :: thesis: DataPart (Start-At l) = {}
Data-Locations S misses {(IC S)} \/ IL by XBOOLE_1:79;
then Data-Locations S misses {(IC S)} by XBOOLE_1:70;
then Data-Locations S misses dom (Start-At l) by FUNCOP_1:19;
hence DataPart (Start-At l) = {} by RELAT_1:95; :: thesis: verum