:: deftheorem Def12 defines =0_goto SCMFSA_2:def 14 :
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 ) );