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