let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for s being State of SCM+FSA
for I being Program of {INT,(INT *)} st (Initialized I) +* (f .--> w) c= s holds
I c= s
let f be FinSeq-Location ; :: thesis: for s being State of SCM+FSA
for I being Program of {INT,(INT *)} st (Initialized I) +* (f .--> w) c= s holds
I c= s
let s be State of SCM+FSA; :: thesis: for I being Program of {INT,(INT *)} st (Initialized I) +* (f .--> w) c= s holds
I c= s
let I be Program of {INT,(INT *)}; :: thesis: ( (Initialized I) +* (f .--> w) c= s implies I c= s )
set t = f .--> w;
set p = Initialized I;
assume A1: (Initialized I) +* (f .--> w) c= s ; :: thesis: I c= s
dom (Initialized I) misses dom (f .--> w) by Th46;
then A2: Initialized I c= (Initialized I) +* (f .--> w) by FUNCT_4:33;
I c= Initialized I by SCMFSA6A:26;
then I c= (Initialized I) +* (f .--> w) by A2, XBOOLE_1:1;
hence I c= s by A1, XBOOLE_1:1; :: thesis: verum