theorem Th30: :: SCMFSA_2:37

for ins being Instruction of SCM+FSA st InsCode ins = 8 holds
ex lb being Nat ex da being Int-Location st ins = da >0_goto lb