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