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 )
let x be set ; :: thesis: ( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )
assume A1: x in dom s ; :: thesis: ( x is Int-Location or x is FinSeq-Location or x = IC )
x in (Data-Locations ) \/ {(IC )} by A1, MEMSTR_0:13;
then ( x in Data-Locations or x in {(IC )} ) by XBOOLE_0:def 3;
then ( x in Int-Locations or x in FinSeq-Locations or x = IC ) by SCMFSA_2:100, TARSKI:def 1, XBOOLE_0:def 3;
hence ( x is Int-Location or x is FinSeq-Location or x = IC ) by AMI_2:def 16, SCMFSA_2:def 5; :: thesis: verum