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