IC SCM in dom p by COMPOS_1:def 16;
hence Relocated (p,k) is halting by Th38; :: thesis: verum