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