let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for f being FinSeq-Location
for p being FinSequence of INT holds
( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
let s be State of SCM+FSA; for f being FinSeq-Location
for p being FinSequence of INT holds
( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
let f be FinSeq-Location ; for p being FinSequence of INT holds
( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
let p be FinSequence of INT ; ( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
A1: (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) =
(Initialize ((intloc 0) .--> 1)) . (intloc 0)
by FUNCT_4:13, SCMFSA_M:10
.=
1
by SCMFSA_M:12
;
reconsider s1 = s +* (Initialize ((intloc 0) .--> 1)) as 0 -started State of SCM+FSA ;
A2:
f := p c= P +* (f := p)
by FUNCT_4:25;
thus (IExec ((f := p),P,s)) . f =
(Result ((P +* (f := p)),s1)) . f
.=
p
by A1, A2, SCMFSA_7:7
; ( ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g ) )
hereby for g being FinSeq-Location st g <> f holds
(IExec ((f := p),P,s)) . g = s . g
let a be
read-write Int-Location;
( a <> intloc 1 & a <> intloc 2 implies (IExec ((f := p),P,s)) . a = s . a )
(
a <> intloc 0 &
a <> IC )
by SCMFSA_2:56;
then A3:
not
a in dom (Initialize ((intloc 0) .--> 1))
by SCMFSA_M:11, TARSKI:def 2;
assume A4:
(
a <> intloc 1 &
a <> intloc 2 )
;
(IExec ((f := p),P,s)) . a = s . athus (IExec ((f := p),P,s)) . a =
(Result ((P +* (f := p)),(s +* (Initialize ((intloc 0) .--> 1))))) . a
.=
s1 . a
by A1, A2, A4, SCMFSA_7:7
.=
s . a
by A3, FUNCT_4:11
;
verum
end;
let g be FinSeq-Location ; ( g <> f implies (IExec ((f := p),P,s)) . g = s . g )
assume A5:
g <> f
; (IExec ((f := p),P,s)) . g = s . g
( g <> intloc 0 & g <> IC )
by SCMFSA_2:57, SCMFSA_2:58;
then A6:
not g in dom (Initialize ((intloc 0) .--> 1))
by SCMFSA_M:11, TARSKI:def 2;
thus (IExec ((f := p),P,s)) . g =
(Result ((P +* (f := p)),(s +* (Initialize ((intloc 0) .--> 1))))) . g
.=
s1 . g
by A1, A2, A5, SCMFSA_7:7
.=
s . g
by A6, FUNCT_4:11
; verum