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

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 No-StopCode ) by Def3; :: thesis: verum