set S1 = {(IC )};

set S2 = SCM-Data-Loc ;

set S3 = NAT ;

let s be State of SCMPDS; :: thesis: for x being set holds

( not x in dom s or x is Int_position or x = IC )

let x be set ; :: thesis: ( not x in dom s or x is Int_position or x = IC )

assume A1: x in dom s ; :: thesis: ( x is Int_position or x = IC )

dom s = the carrier of SCMPDS by PARTFUN1:def 2;

then x in {(IC )} \/ SCM-Data-Loc by A1, SCMPDS_2:84, STRUCT_0:4;

then ( x in {(IC )} or x in SCM-Data-Loc ) by XBOOLE_0:def 3;

hence ( x is Int_position or x = IC ) by AMI_2:def 16, TARSKI:def 1; :: thesis: verum

set S2 = SCM-Data-Loc ;

set S3 = NAT ;

let s be State of SCMPDS; :: thesis: for x being set holds

( not x in dom s or x is Int_position or x = IC )

let x be set ; :: thesis: ( not x in dom s or x is Int_position or x = IC )

assume A1: x in dom s ; :: thesis: ( x is Int_position or x = IC )

dom s = the carrier of SCMPDS by PARTFUN1:def 2;

then x in {(IC )} \/ SCM-Data-Loc by A1, SCMPDS_2:84, STRUCT_0:4;

then ( x in {(IC )} or x in SCM-Data-Loc ) by XBOOLE_0:def 3;

hence ( x is Int_position or x = IC ) by AMI_2:def 16, TARSKI:def 1; :: thesis: verum