theorem :: SCMFSA_4:4

for k being Nat
for i being Instruction of SCM+FSA st not InsCode i in {6,7,8} holds
IncAddr (i,k) = i