let a, b be Int-Location ; :: thesis: JumpPart (AddTo a,b) = {}
thus JumpPart (AddTo a,b) = [2,{} ,<*a,b*>] `2_3 by Th10
.= {} by RECDEF_2:def 2 ; :: thesis: verum