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 :: thesis: for x being Nat st x in dom II holds
II . x <> halt SCMPDS

let x be 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:13;
then x = 0 by TARSKI:def 1;
then A1: II . x = (DataLoc (0,0)) := 0 ;
InsCode ((DataLoc (0,0)) := 0) = 2 by SCMPDS_2:14;
hence II . x <> halt SCMPDS by A1; :: thesis: verum

end;

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