let I be Program of SCM+FSA ; :: thesis: for n being Element of NAT holds dom I misses dom (Start-At (insloc n))
let n be Element of NAT ; :: thesis: dom I misses dom (Start-At (insloc n))
A1: dom (Start-At (insloc n)) = {(IC SCM+FSA )} by FUNCOP_1:19;
A2: dom I c= NAT by RELAT_1:def 18;
assume (dom I) /\ (dom (Start-At (insloc n))) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being set such that
A3: x in (dom I) /\ (dom (Start-At (insloc n))) by XBOOLE_0:def 1;
( x in dom I & x in dom (Start-At (insloc n)) ) by A3, XBOOLE_0:def 4;
then IC SCM+FSA in dom I by A1, TARSKI:def 1;
then reconsider l = IC SCM+FSA as Instruction-Location of SCM+FSA by A2, AMI_1:def 4;
l = IC SCM+FSA ;
hence contradiction by AMI_1:48; :: thesis: verum