let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (IExec ((Stop SCM+FSA),p,s)) = DataPart s
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 implies DataPart (IExec ((Stop SCM+FSA),p,s)) = DataPart s )
assume A1: s . (intloc 0) = 1 ; :: thesis: DataPart (IExec ((Stop SCM+FSA),p,s)) = DataPart s
thus DataPart (IExec ((Stop SCM+FSA),p,s)) = DataPart (Initialized s) by SCMFSA8C:14
.= DataPart s by A1, SCMFSA_M:19 ; :: thesis: verum