:: deftheorem Def13 defines >0_goto SCMFSA_2:def 15 :
for la being Nat
for a being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = a >0_goto la iff ex A being Data-Location st
( a = A & b₃ = A >0_goto la ) );