let lb be Nat; :: thesis: for a being Int-Location holds InsCode (a >0_goto lb) = 8
let a be Int-Location; :: thesis: InsCode (a >0_goto lb) = 8
ex A being Data-Location st
( a = A & a >0_goto lb = A >0_goto lb ) by Def13;
hence InsCode (a >0_goto lb) = 8 ; :: thesis: verum