the haltF of (SCM R) = [0,{},{}] by Def1;
hence the haltF of (SCM R) is halting by Th21; :: according to EXTPRO_1:def 4 :: thesis: verum