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