let t be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for I being Program of {INT,(INT *)} holds dom (Initialized I) misses dom (f .--> t)
let f be FinSeq-Location ; :: thesis: for I being Program of {INT,(INT *)} holds dom (Initialized I) misses dom (f .--> t)
let I be Program of {INT,(INT *)}; :: thesis: dom (Initialized I) misses dom (f .--> t)
set x = f .--> t;
A1: dom (f .--> t) = {f} by FUNCOP_1:19;
set DB = dom I;
set DI = dom (Initialized I);
A2: dom (Initialized I) = (dom I) \/ {(intloc 0),(IC SCM+FSA)} by Th41;
assume (dom (Initialized I)) /\ (dom (f .--> t)) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider y being set such that
A3: y in (dom (Initialized I)) /\ (dom (f .--> t)) by XBOOLE_0:def 1;
A4: y in dom (Initialized I) by A3, XBOOLE_0:def 4;
y in dom (f .--> t) by A3, XBOOLE_0:def 4;
then A5: y = f by A1, TARSKI:def 1;
A6: dom I c= NAT by RELAT_1:def 18;
not y in dom I by A5, A6, SCMFSA_2:85;
then y in {(intloc 0),(IC SCM+FSA)} by A2, A4, XBOOLE_0:def 3;
then ( y = intloc 0 or y = IC SCM+FSA ) by TARSKI:def 2;
hence contradiction by A5, SCMFSA_2:82, SCMFSA_2:83; :: thesis: verum