:: deftheorem Def3 defines aSeq SCMFSA_7:def 3 :
for f being FinSeq-Location
for p being FinSequence of INT
for b₃ being XFinSequence of the InstructionsF of SCM+FSA holds
( b₃ = aSeq (f,p) iff ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b₃ = FlattenSeq pp ) );