A1:
rng (Load i) = {i}
by AFINSQ_1:33;

now :: thesis: not halt S in rng (Load i)

hence
Load i is halt-free
; :: thesis: verumassume
halt S in rng (Load i)
; :: thesis: contradiction

then halt S = i by A1, TARSKI:def 1;

hence contradiction by COMPOS_0:def 12; :: thesis: verum

end;then halt S = i by A1, TARSKI:def 1;

hence contradiction by COMPOS_0:def 12; :: thesis: verum