theorem :: SCMFSA_2:25

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