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