take i = (DataLoc (0,0)) := 0; :: thesis: ( i is No-StopCode & i is shiftable & i is parahalting )

InsCode i = 2 by SCMPDS_2:14;

then i <> halt SCMPDS ;

hence i is No-StopCode ; :: thesis: ( i is shiftable & i is parahalting )

thus ( i is shiftable & i is parahalting ) by Lm2; :: thesis: verum

InsCode i = 2 by SCMPDS_2:14;

then i <> halt SCMPDS ;

hence i is No-StopCode ; :: thesis: ( i is shiftable & i is parahalting )

thus ( i is shiftable & i is parahalting ) by Lm2; :: thesis: verum