:: deftheorem defines jump_address SCMPDS_1:def 7 :
for s being SCM-State
for n being Integer holds jump_address (s,n) = |.((IC s) + n).|;