let i1 be Nat; :: thesis: for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>
let a be Int-Location; :: thesis: JumpPart (a >0_goto i1) = <*i1*>
thus JumpPart (a >0_goto i1) = [8,<*i1*>,<*a*>] `2_3 by Th8
.= <*i1*> ; :: thesis: verum