let k, loc be Element of NAT ; :: thesis: for a being Data-Location holds IncAddr (a >0_goto loc),k = a >0_goto (loc + k)
let a be Data-Location ; :: thesis: IncAddr (a >0_goto loc),k = a >0_goto (loc + k)
A1: (@ (a >0_goto loc)) cjump_address = loc by AMI_5:57;
( InsCode (a >0_goto loc) = 8 & ((@ (a >0_goto loc)) cond_address ) @ = a ) by AMI_5:57, MCART_1:7;
hence IncAddr (a >0_goto loc),k = a >0_goto (loc + k) by A1, Def3; :: thesis: verum