let a be Int-Location ; :: thesis: for il being Instruction-Location of SCM+FSA holds a >0_goto il = [8,<*il,a*>]
let il be Instruction-Location of SCM+FSA ; :: thesis: a >0_goto il = [8,<*il,a*>]
ex A being Data-Location ex L being Instruction-Location of SCM 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