let w be FinSequence of INT ; :: thesis: for f being FinSeq-Location
for s being State of SCM+FSA
for I being Program of 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
for I being Program of st Initialized (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 st Initialized (f .--> w) c= s holds
( s . f = w & s . (intloc 0) = 1 )
let I be Program of ; :: thesis: ( Initialized (f .--> w) c= s implies ( s . f = w & s . (intloc 0) = 1 ) )
set t = f .--> w;
set p = Initialized (f .--> w);
B0: Initialized (f .--> w) = (f .--> w) +* (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:def 3;
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 ;
dom (f .--> w) = {f} by FUNCOP_1:13;
then f in dom (f .--> w) by TARSKI:def 1;
then C3: f in dom pt by B0, FUNCT_4:12;
B3: f in dom pt by C3;
intloc 0 in dom (Initialized (f .--> w)) by SCMFSA6A:10;
then B5: intloc 0 in dom pt ;
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 Y1: not f in dom ((intloc 0) .--> 1) by FUNCOP_1:13;
Y2: 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 YY: not f in dom (Initialize ((intloc 0) .--> 1)) by Y1, Y2, XBOOLE_0:def 3;
thus s . f = pt . f by A1, B3, GRFUNC_1:2
.= pt . f
.= (f .--> w) . f by B0, YY, FUNCT_4:11
.= w by FUNCOP_1:72 ; :: thesis: s . (intloc 0) = 1
thus s . (intloc 0) = pt . (intloc 0) by A1, B5, GRFUNC_1:2
.= pt . (intloc 0)
.= (Initialized (f .--> w)) . (intloc 0)
.= (Initialize ((intloc 0) .--> 1)) . (intloc 0) by B0, FUNCT_4:13, SCMFSA6A:41
.= 1 by SCMFSA6A:43 ; :: thesis: verum