let s be State of SCM+FSA; :: thesis: for I being good Program of SCM+FSA st I is_closed_on s holds
for k being Element of NAT holds (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) . (intloc 0) = s . (intloc 0)
let I be good Program of SCM+FSA; :: thesis: ( I is_closed_on s implies for k being Element of NAT holds (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) . (intloc 0) = s . (intloc 0) )
assume A1: I is_closed_on s ; :: thesis: for k being Element of NAT holds (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) . (intloc 0) = s . (intloc 0)
let k be Element of NAT ; :: thesis: (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) . (intloc 0) = s . (intloc 0)
not I destroys intloc 0 by SCMFSA7B:def 5;
hence (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) . (intloc 0) = s . (intloc 0) by A1, SCMFSA7B:27; :: thesis: verum