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