InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence (fa,a) := c is No-StopCode by COMPOS_0:def 12; :: thesis: verum