theorem Th37: :: SCMFSA10:37

for il, i1 being Nat
for a being Int-Location holds NIC ((a >0_goto i1),il) = {i1,(il + 1)}