YES Problem: f(a(),x) -> g(a(),x) g(a(),x) -> f(b(),x) f(a(),x) -> f(b(),x) Proof: DP Processor: DPs: f#(a(),x) -> g#(a(),x) g#(a(),x) -> f#(b(),x) f#(a(),x) -> f#(b(),x) TRS: f(a(),x) -> g(a(),x) g(a(),x) -> f(b(),x) f(a(),x) -> f(b(),x) Usable Rule Processor: DPs: f#(a(),x) -> g#(a(),x) g#(a(),x) -> f#(b(),x) f#(a(),x) -> f#(b(),x) TRS: LPO Processor: argument filtering: pi(a) = [] pi(b) = [] pi(f#) = [0] pi(g#) = [] usable rules: precedence: a > g# > f# ~ b problem: DPs: TRS: Qed