set ii = (DataLoc (0,0)) := 0;
take II = Load ((DataLoc (0,0)) := 0); :: thesis: ( II is parahalting & II is shiftable & II is halt-free )

now

let x be Element of NAT ; :: thesis: ( x in dom II implies II . x <> halt SCMPDS )
assume x in dom II ; :: thesis: II . x <> halt SCMPDS
then x in {0} by FUNCOP_1:19;
then x = 0 by TARSKI:def 1;
then A1: II . x = (DataLoc (0,0)) := 0 by FUNCOP_1:87;
InsCode ((DataLoc (0,0)) := 0) = 2 by SCMPDS_2:23;
hence II . x <> halt SCMPDS by A1, SCMPDS_2:21, SCMPDS_2:93; :: thesis: verum

end;

hence ( II is parahalting & II is shiftable & II is halt-free ) by Def3; :: thesis: verum