let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
for k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds
(Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
for k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds
(Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a
let I be Program of SCM+FSA; :: thesis: for a being Int-Location st not I destroys a holds
for k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds
(Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a
let a be Int-Location; :: thesis: ( not I destroys a implies for k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds
(Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a )
assume A1: not I destroys a ; :: thesis: for k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds
(Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a
set s1 = Initialize s;
set P1 = P +* I;
A2: I c= P +* I by FUNCT_4:25;
let k be Element of NAT ; :: thesis: ( IC (Comput ((P +* I),(Initialize s),k)) in dom I implies (Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a )
assume A3: IC (Comput ((P +* I),(Initialize s),k)) in dom I ; :: thesis: (Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a
set l = IC (Comput ((P +* I),(Initialize s),k));
(P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) = I . (IC (Comput ((P +* I),(Initialize s),k))) by A3, A2, GRFUNC_1:2;
then (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) in rng I by A3, FUNCT_1:def 3;
then A4: not (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) destroys a by A1;
thus (Comput ((P +* I),(Initialize s),(k + 1))) . a = (Following ((P +* I),(Comput ((P +* I),(Initialize s),k)))) . a by EXTPRO_1:3
.= (Exec (((P +* I) . (IC (Comput ((P +* I),(Initialize s),k)))),(Comput ((P +* I),(Initialize s),k)))) . a by PBOOLE:143
.= (Comput ((P +* I),(Initialize s),k)) . a by A4, SCMFSA7B:20 ; :: thesis: verum