let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for s being State of SCM+FSA
for I being Program of SCM+FSA st NPP ((Initialized I) +* (f .--> w)) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let f be FinSeq-Location ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st NPP ((Initialized I) +* (f .--> w)) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st NPP ((Initialized I) +* (f .--> w)) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let I be Program of SCM+FSA; :: thesis: ( NPP ((Initialized I) +* (f .--> w)) c= s implies ( s . f = w & s . (intloc 0) = 1 ) )
set t = f .--> w;
set p = Initialized I;
assume A1: NPP ((Initialized I) +* (f .--> w)) c= s ; :: thesis: ( s . f = w & s . (intloc 0) = 1 )
reconsider pt = (Initialized I) +* (f .--> w) as PartState of SCM+FSA ;
A2: dom (f .--> w) = {f} by FUNCOP_1:19;
then A3: f in dom (f .--> w) by TARSKI:def 1;
then C3: f in dom pt by FUNCT_4:13;
f in FinSeq-Locations by SCMFSA_2:10;
then X2: f in Data-Locations SCM+FSA by SCMFSA_2:127, XBOOLE_0:def 3;
then B3: f in dom (NPP pt) by C3, COMPOS_1:219;
intloc 0 <> f by SCMFSA_2:83;
then A4: not intloc 0 in dom (f .--> w) by A2, TARSKI:def 1;
intloc 0 in Int-Locations by SCMFSA_2:9;
then X1: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:127, XBOOLE_0:def 3;
intloc 0 in dom (Initialized I) by SCMFSA6A:45;
then intloc 0 in dom ((Initialized I) +* (f .--> w)) by FUNCT_4:13;
then B5: intloc 0 in dom (NPP pt) by X1, COMPOS_1:219;
thus s . f = (NPP pt) . f by A1, B3, GRFUNC_1:8
.= pt . f by X2, COMPOS_1:218
.= (f .--> w) . f by A3, FUNCT_4:14
.= w by FUNCOP_1:87 ; :: thesis: s . (intloc 0) = 1
thus s . (intloc 0) = (NPP pt) . (intloc 0) by A1, B5, GRFUNC_1:8
.= pt . (intloc 0) by X1, COMPOS_1:218
.= (Initialized I) . (intloc 0) by A4, FUNCT_4:12
.= 1 by SCMFSA6A:46 ; :: thesis: verum