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