theorem :: SCMFSA_2:87

for f being FinSeq-Location
for a, c being Int-Location holds not c := (f,a) is halting ;