for R being Ring
for I being Instruction of (SCM R) st I is halting holds
I = halt (SCM R) by Lm10;