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