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

assume A5: g <> f ; :: thesis: (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 ; :: thesis: verum

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; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( (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 ; :: thesis: ( ( 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 :: thesis: for g being FinSeq-Location st g <> f holds

(IExec ((f := p),P,s)) . g = s . g

let g be FinSeq-Location ; :: thesis: ( g <> f implies (IExec ((f := p),P,s)) . g = s . g )(IExec ((f := p),P,s)) . g = s . g

let a be read-write Int-Location; :: thesis: ( 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 ) ; :: thesis: (IExec ((f := p),P,s)) . a = s . a

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

end;( 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 ) ; :: thesis: (IExec ((f := p),P,s)) . a = s . a

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

assume A5: g <> f ; :: thesis: (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 ; :: thesis: verum