let k, loc be Element of NAT ; :: thesis: IncAddr (SCM-goto loc),k = SCM-goto (loc + k)
( InsCode (SCM-goto loc) = 6 & (@ (SCM-goto loc)) jump_address = loc ) by AMI_5:55, MCART_1:7;
hence IncAddr (SCM-goto loc),k = SCM-goto (loc + k) by Def3; :: thesis: verum