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) = [7,<*i1*>,<*a*>] `2_3 by Th7
.= <*i1*> ; :: thesis: verum