Claus's theorem states that if the accessibility problem for k-rule semi-Thue systems is undecidable, then so is the Post Correspondence Problem over an alphabet of k+4 letters. The transfer is proved as two independent many-one reductions through the Generalized Post Correspondence Problem: accessibility for k rules reduces to GPCP over k+2 letters, and GPCP over k letters reduces to PCP over k+2 letters. Both turn on encoding devices worth learning in their own right - embedding an arbitrary alphabet into an infinite comma-free binary code so that derivations survive translation, and an accordion lemma that uses an unbordered delimiter word to compress a whole derivation chain into a single correspondence solution.
A semi-Thue system is a finite set of rewriting rules (s,t) over an alphabet, where one word is derivable from another when repeatedly replacing an occurrence of some rule's left side by its right si…