take i = (DataLoc (0,0)) := 0; :: thesis: ( i is No-StopCode & i is shiftable & i is parahalting )
A1: InsCode (halt SCMPDS) = 0 by COMPOS_1:70;
InsCode i = 2 by SCMPDS_2:14;
then i <> halt SCMPDS by A1;
hence i is No-StopCode by COMPOS_0:def 12; :: thesis: ( i is shiftable & i is parahalting )
thus ( i is shiftable & i is parahalting ) by Def2, Lm2; :: thesis: verum