set ii = (DataLoc (0,0)) := 0;

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

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

hence
( II is parahalting & II is shiftable & II is halt-free )
; :: thesis: verumII . 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;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