theorem Th17: :: SCMRING3:18

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 6 holds
ex i2 being Nat st I = goto (i2,R)