set M = STC N;
the Instructions of (STC N) = {[1,0 ],[0 ,0 ]} by Def11;
then reconsider I = [0 ,0 ] as Instruction of (STC N) by TARSKI:def 2;
take I ; :: according to AMI_1:def 9 :: thesis: I is halting
InsCode I = 0 by MCART_1:def 1;
hence I is halting by Th20; :: thesis: verum