let a be Int-Location; :: thesis: for il being Nat holds a >0_goto il = [8,<*il*>,<*a*>]
let il be Nat; :: thesis: a >0_goto il = [8,<*il*>,<*a*>]
ex A being Data-Location st
( A = a & A >0_goto il = a >0_goto il ) by SCMFSA_2:def 15;
hence a >0_goto il = [8,<*il*>,<*a*>] ; :: thesis: verum