theorem :: SCMFSA_2:95

for I being Instruction of SCM+FSA st InsCode I = 0 holds
I = halt SCM+FSA by Th85;