set S1 = {(IC SCMPDS )};
set S2 = SCM-Data-Loc ;
set S3 = NAT ;
let s be State of ; :: thesis: for x being set holds
( not x in dom s or x is Int_position or x = IC SCMPDS or x is Instruction-Location of SCMPDS )
let x be set ; :: thesis: ( not x in dom s or x is Int_position or x = IC SCMPDS or x is Instruction-Location of SCMPDS )
assume A1: x in dom s ; :: thesis: ( x is Int_position or x = IC SCMPDS or x is Instruction-Location of SCMPDS )
dom s = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by AMI_1:79, SCMPDS_3:5;
then ( x in {(IC SCMPDS )} \/ SCM-Data-Loc or x in NAT ) by A1, XBOOLE_0:def 3;
then ( x in {(IC SCMPDS )} or x in SCM-Data-Loc or x in NAT ) by XBOOLE_0:def 3;
hence ( x is Int_position or x = IC SCMPDS or x is Instruction-Location of SCMPDS ) by AMI_1:def 4, SCMPDS_2:9, TARSKI:def 1; :: thesis: verum