theorem Th87: :: SCMFSA_2:94

for I being Instruction of SCM+FSA st I is halting holds
I = halt SCM+FSA by Lm1;