:: deftheorem Def1 defines := SCMFSA_7:def 1 :
for a being Int-Location
for k being Integer
for b₃ being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds
( ( k > 0 implies ( b₃ = a := k iff ex k1 being Nat st
( k1 + 1 = k & b₃ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) ) & ( not k > 0 implies ( b₃ = a := k iff ex k1 being Nat st
( k1 + k = 1 & b₃ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) ) );