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:56;
( InsCode (a =0_goto loc) = 7 & ((@ (a =0_goto loc)) cond_address ) @ = a ) by AMI_5:56, MCART_1:7;
hence IncAddr (a =0_goto loc),k = a =0_goto (loc + k) by A1, Def3; :: thesis: verum