theorem Th18: :: SCMRING3:19

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 7 holds
ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1