let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being good Program of SCM+FSA
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0)
let s be State of SCM+FSA; :: thesis: for I being good Program of SCM+FSA
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0)
let I be good Program of SCM+FSA; :: thesis: for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0)
let m be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) implies for n being Element of NAT st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0) )
assume A1: for n being Element of NAT st n < m holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ; :: thesis: for n being Element of NAT st n <= m holds
(Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0)
let n be Element of NAT ; :: thesis: ( n <= m implies (Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0) )
A2: not I destroys intloc 0 by SCMFSA7B:def 5;
assume n <= m ; :: thesis: (Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0)
hence (Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0) by A1, A2, Th94; :: thesis: verum