theorem :: SCMFSA_2:88

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