let s be State of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 implies DataPart (IExec (Stop SCM+FSA ),s) = DataPart s )
set D = Int-Locations \/ FinSeq-Locations ;
assume A1: s . (intloc 0 ) = 1 ; :: thesis: DataPart (IExec (Stop SCM+FSA ),s) = DataPart s
thus DataPart (IExec (Stop SCM+FSA ),s) = DataPart ((Initialize s) +* (Start-At 0 ,SCM+FSA )) by SCMFSA8C:38
.= DataPart (Initialize s) by SCMFSA8A:10
.= DataPart s by A1, SCMFSA8C:27 ; :: thesis: verum