InsCode (halt SCM+FSA) = 0 ;
hence fa :=<0,...,0> a is No-StopCode ; :: thesis: verum