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 (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 (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 (Initialized I) +* (f .--> w) c= s holds
( s . f = w & s . (intloc 0 ) = 1 )
let I be Program of SCM+FSA ; :: thesis: ( (Initialized I) +* (f .--> w) c= s implies ( s . f = w & s . (intloc 0 ) = 1 ) )
set t = f .--> w;
set p = Initialized I;
assume A1: (Initialized I) +* (f .--> w) c= s ; :: thesis: ( s . f = w & s . (intloc 0 ) = 1 )
A2: dom (f .--> w) = {f} by FUNCOP_1:19;
then A3: f in dom (f .--> w) by TARSKI:def 1;
intloc 0 <> f by SCMFSA_2:83;
then A4: not intloc 0 in dom (f .--> w) by A2, TARSKI:def 1;
intloc 0 in dom (Initialized I) by SCMFSA6A:45;
then A5: intloc 0 in dom ((Initialized I) +* (f .--> w)) by FUNCT_4:13;
f .--> w c= (Initialized I) +* (f .--> w) by FUNCT_4:26;
then f .--> w c= s by A1, XBOOLE_1:1;
hence s . f = (f .--> w) . f by A3, GRFUNC_1:8
.= w by FUNCOP_1:87 ;
:: thesis: s . (intloc 0 ) = 1
thus s . (intloc 0 ) = ((Initialized I) +* (f .--> w)) . (intloc 0 ) by A1, A5, GRFUNC_1:8
.= (Initialized I) . (intloc 0 ) by A4, FUNCT_4:12
.= 1 by SCMFSA6A:46 ; :: thesis: verum