set I = the haltF of (STC N);
the haltF of (STC N) = [0 ,0 ,0 ] by Def11;
then InsCode the haltF of (STC N) = 0 by RECDEF_2:def 1;
hence the haltF of (STC N) is halting by Th20; :: according to AMI_1:def 9 :: thesis: verum