We present a termination proof for the Battle of Hercules and Hydra represented as a rewrite system with AC symbols. Our proof employs type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-RPO.

翻译：我们给出了以带AC符号的重写系统表示的赫拉克勒斯与海德拉之战的终止性证明。该证明将类型引入与多类语义标记技术相结合，适用于AC重写及AC-RPO。