take i = (DataLoc 0 ,0 ) := 1; :: thesis: i is shiftable
InsCode i = 2 by SCMPDS_2:23;
hence i is shiftable by Def13; :: thesis: verum