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: not I destroys 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