theorem :: SCMFSA_2:98
for i being Instruction of SCM
for I being Instruction of SCM+FSA st i = I & not i is halting holds
not I is halting by Th87, Th89;