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