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