reconsider I = [0 ,{} ] as Instruction of SCM by AMI_2:2;
take I ; :: according to AMI_1:def 9 :: thesis: I is halting
thus I is halting by Lm2; :: thesis: verum