(Exec ((c :=len f), the State of SCM+FSA)) . (IC ) = (IC the State of SCM+FSA) + 1 by Th67;
hence not c :=len f is halting by Th71; :: thesis: verum