theorem :: SCMFSA_2:24

for lb being Nat
for a being Int-Location holds InsCode (a =0_goto lb) = 7