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 destroysdestroy 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