take the halting Instruction of S ; :: thesis: the halting Instruction of S is IC-relocable
thus the halting Instruction of S is IC-relocable ; :: thesis: verum