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 (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),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 (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),n) . (intloc 0 ) = s . (intloc 0 )
let m be Element of NAT ; :: thesis: ( ( for n being Element of NAT st n < m holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ) implies for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),n) . (intloc 0 ) = s . (intloc 0 ) )
assume A1: for n being Element of NAT st n < m holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I ; :: thesis: for n being Element of NAT st n <= m holds
(Computation (s +* (I +* (Start-At (insloc 0 )))),n) . (intloc 0 ) = s . (intloc 0 )
let n be Element of NAT ; :: thesis: ( n <= m implies (Computation (s +* (I +* (Start-At (insloc 0 )))),n) . (intloc 0 ) = s . (intloc 0 ) )
assume A2: n <= m ; :: thesis: (Computation (s +* (I +* (Start-At (insloc 0 )))),n) . (intloc 0 ) = s . (intloc 0 )
I does_not_destroy intloc 0 by SCMFSA7B:def 5;
hence (Computation (s +* (I +* (Start-At (insloc 0 )))),n) . (intloc 0 ) = s . (intloc 0 ) by A1, A2, Th94; :: thesis: verum