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