theorem Th4: :: RELOC:4

for I being Instruction of SCM
for k being Element of NAT st not not InsCode I = 0 & ... & not InsCode I = 5 holds
IncAddr (I,k) = I