let s be State of SCM ; :: thesis: for d being Data-Location
for l being Instruction-Location of SCM holds
( d in dom s & l in dom s )
let d be Data-Location ; :: thesis: for l being Instruction-Location of SCM holds
( d in dom s & l in dom s )
let l be Instruction-Location of SCM ; :: thesis: ( d in dom s & l in dom s )
d in SCM-Data-Loc by AMI_3:def 2;
then d in {(IC SCM )} \/ SCM-Data-Loc by XBOOLE_0:def 3;
then d in ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by XBOOLE_0:def 3;
hence d in dom s by AMI_1:79, AMI_3:4; :: thesis: l in dom s
l in NAT by AMI_1:def 4;
then l in ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by XBOOLE_0:def 3;
hence l in dom s by AMI_1:79, AMI_3:4; :: thesis: verum