take i = (DataLoc 0 ,0 ) := 0 ; :: thesis: ( i is No-StopCode & i is shiftable & i is parahalting )
A1: InsCode i = 2 by SCMPDS_2:23;
InsCode (halt SCMPDS ) = 0 by SCMPDS_2:21, SCMPDS_2:93;
hence ( i is No-StopCode & i is shiftable & i is parahalting ) by A1, Def1, Def2, Lm1; :: thesis: verum