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