let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for s being State of SCM+FSA st Initialized (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 st Initialized (f .--> w) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let s be State of SCM+FSA; :: thesis: ( Initialized (f .--> w) c= s implies ( s . f = w & s . (intloc 0) = 1 ) )
set t = f .--> w;
set p = Initialized (f .--> w);
assume A2: Initialized (f .--> w) c= s ; :: thesis: ( s . f = w & s . (intloc 0) = 1 )
reconsider pt = Initialized (f .--> w) as PartState of SCM+FSA ;
dom (f .--> w) = {f} by FUNCOP_1:13;
then B3: f in dom (f .--> w) by TARSKI:def 1;
A4: f in dom pt by B3, FUNCT_4:12;
A5: intloc 0 in dom pt by Th4;
ex i being Element of NAT st f = fsloc i by SCMFSA_2:9;
then f <> intloc 0 by SCMFSA_2:99;
then not f in {(intloc 0)} by TARSKI:def 1;
then A6: not f in dom ((intloc 0) .--> 1) by FUNCOP_1:13;
A7: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
then A8: not f in dom (Initialize ((intloc 0) .--> 1)) by A6, A7, XBOOLE_0:def 3;
thus s . f = pt . f by A2, A4, GRFUNC_1:2
.= (f .--> w) . f by A8, FUNCT_4:11
.= w by FUNCOP_1:72 ; :: thesis: s . (intloc 0) = 1
thus s . (intloc 0) = (Initialized (f .--> w)) . (intloc 0) by A2, A5, GRFUNC_1:2
.= 1 by Th12, Th10, FUNCT_4:13 ; :: thesis: verum