theorem Th29: :: SCMFSA_2:36

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