theorem :: SCMFSA_2:89

for f being FinSeq-Location
for c being Int-Location holds not c :=len f is halting ;