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