:: deftheorem defines := SCMFSA_7:def 4 :
for f being FinSeq-Location
for p being FinSequence of INT holds f := p = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA);