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