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 A1: Initialized (f .--> w) c= s ; :: thesis: ( s . f = w & s . (intloc 0) = 1 )
reconsider pt = Initialized (f .--> w) as PartState of SCM+FSA ;
A2: f in dom (f .--> w) by TARSKI:def 1;
A3: f in dom pt by A2, FUNCT_4:12;
A4: intloc 0 in dom pt by Th4;
ex i being 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 A5: not f in dom ((intloc 0) .--> 1) ;
A6: 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 A7: not f in dom (Initialize ((intloc 0) .--> 1)) by A5, A6, XBOOLE_0:def 3;
thus s . f = pt . f by A1, A3, GRFUNC_1:2
.= (f .--> w) . f by A7, FUNCT_4:11
.= w by FUNCOP_1:72 ; :: thesis: s . (intloc 0) = 1
thus s . (intloc 0) = (Initialized (f .--> w)) . (intloc 0) by A1, A4, GRFUNC_1:2
.= 1 by Th12, Th10, FUNCT_4:13 ; :: thesis: verum