for a, b being Data-Location holds not a := b is halting by Lm4;