let P be Instruction-Sequence of SCM+FSA; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (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 ; :: thesis: ( ( 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 ) )

( 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 ; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( (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 ; :: thesis: ( ( 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 :: thesis: for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f

let f be FinSeq-Location ; :: thesis: (IExec ((a := k),P,s)) . f = s . flet b be read-write Int-Location; :: thesis: ( b <> a implies (IExec ((a := k),P,s)) . b = s . b )

assume A3: b <> a ; :: thesis: (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 ; :: thesis: verum

end;assume A3: b <> a ; :: thesis: (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 ; :: thesis: verum

( 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 ; :: thesis: verum