let s be State of SCM+FSA; :: thesis: for x being set holds
( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC or x is Element of NAT )
let x be set ; :: thesis: ( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC or x is Element of NAT )
assume A1: x in dom s ; :: thesis: ( x is Int-Location or x is FinSeq-Location or x = IC or x is Element of NAT )
dom s = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
then ( x in (Data-Locations SCM+FSA) \/ {(IC )} or x in NAT ) by A1, XBOOLE_0:def 3;
then ( x in Data-Locations SCM+FSA or x in {(IC )} or x in NAT ) by XBOOLE_0:def 3;
then ( x in Int-Locations or x in FinSeq-Locations or x = IC or x is Element of NAT ) by TARSKI:def 1, XBOOLE_0:def 3, SCMFSA_2:127;
hence ( x is Int-Location or x is FinSeq-Location or x = IC or x is Element of NAT ) by SCMFSA_2:11, SCMFSA_2:12; :: thesis: verum