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