IC (Exec ((a := b), the State of SCM+FSA)) = succ (IC the State of SCM+FSA) by Th63;
hence not a := b is halting by Th78; :: thesis: verum