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