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