let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for a being read-write Int-Location
for k being Integer holds
( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
let s be State of SCM+FSA; for a being read-write Int-Location
for k being Integer holds
( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
let a be read-write Int-Location; for k being Integer holds
( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
let k be Integer; ( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
set s1 = s +* (Initialize ((intloc 0) .--> 1));
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:
a := k c= P +* (a := k)
by FUNCT_4:25;
thus (IExec ((a := k),P,s)) . a =
(Result ((P +* (a := k)),s1)) . a
.=
k
by A1, A2, SCMFSA_7:6
; ( ( for b being read-write Int-Location st b <> a holds
(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )
hereby for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f
let b be
read-write Int-Location;
( b <> a implies (IExec ((a := k),P,s)) . b = s . b )assume A3:
b <> a
;
(IExec ((a := k),P,s)) . b = s . b
(
b <> intloc 0 &
b <> IC )
by SCMFSA_2:56;
then A4:
not
b in dom (Initialize ((intloc 0) .--> 1))
by SCMFSA_M:11, TARSKI:def 2;
thus (IExec ((a := k),P,s)) . b =
(Result ((P +* (a := k)),s1)) . b
.=
s1 . b
by A1, A2, A3, SCMFSA_7:6
.=
s . b
by A4, FUNCT_4:11
;
verum
end;
let f be FinSeq-Location ; (IExec ((a := k),P,s)) . f = s . f
( f <> intloc 0 & f <> IC )
by SCMFSA_2:57, SCMFSA_2:58;
then A5:
not f in dom (Initialize ((intloc 0) .--> 1))
by SCMFSA_M:11, TARSKI:def 2;
thus (IExec ((a := k),P,s)) . f =
(Result ((P +* (a := k)),s1)) . f
.=
s1 . f
by A1, A2, SCMFSA_7:6
.=
s . f
by A5, FUNCT_4:11
; verum