set p = Load i;

now :: thesis: for x being Nat st x in dom (Load i) holds

(Load i) . x <> halt SCMPDS

hence
Load i is halt-free
; :: thesis: verum(Load i) . x <> halt SCMPDS

let x be Nat; :: thesis: ( x in dom (Load i) implies (Load i) . x <> halt SCMPDS )

assume x in dom (Load i) ; :: thesis: (Load i) . x <> halt SCMPDS

then x = 0 by COMPOS_1:50;

then (Load i) . x = i ;

hence (Load i) . x <> halt SCMPDS by COMPOS_0:def 12; :: thesis: verum

end;assume x in dom (Load i) ; :: thesis: (Load i) . x <> halt SCMPDS

then x = 0 by COMPOS_1:50;

then (Load i) . x = i ;

hence (Load i) . x <> halt SCMPDS by COMPOS_0:def 12; :: thesis: verum