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