section ‹Deciding RPO-constraints is NP-hard› text ‹We show that for a given an RPO it is NP-hard to decide whether two terms are in relation, following a proof in \<^cite>‹"RPO_NPC"›.› theory RPO_NP_Hard imports Multiset_Ordering_NP_Hard Weighted_Path_Order.RPO begin subsection ‹Definition of the Encoding›