set I = halt (STC N);
InsCode (halt (STC N)) = 0 ;
hence halt (STC N) is halting by Th4; :: according to EXTPRO_1:def 4 :: thesis: verum