YES Problem: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) Proof: DP Processor: DPs: g#(h(x1)) -> f#(s(x1)) g#(h(x1)) -> g#(f(s(x1))) f#(s(s(s(x1)))) -> h#(x1) f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(h(x1)) -> f#(s(h(x1))) f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) b#(a(x1)) -> b#(x1) b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(b(b(b(x1)))) -> a#(x1) TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) TDG Processor: DPs: g#(h(x1)) -> f#(s(x1)) g#(h(x1)) -> g#(f(s(x1))) f#(s(s(s(x1)))) -> h#(x1) f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(h(x1)) -> f#(s(h(x1))) f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) b#(a(x1)) -> b#(x1) b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(b(b(b(x1)))) -> a#(x1) TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) graph: a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(a(a(x1))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(x1))) -> b#(x1) -> b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> a#(a(b(x1))) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> a#(b(x1)) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> b#(x1) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(x1)) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> a#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(f(s(s(x1)))) -> f#(f(x1)) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(h(x1)) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> h#(x1) f#(f(s(s(x1)))) -> f#(x1) -> f#(f(s(s(x1)))) -> f#(f(x1)) f#(f(s(s(x1)))) -> f#(x1) -> f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(x1) -> f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) -> f#(h(x1)) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> h#(x1) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(f(s(s(x1)))) -> f#(f(x1)) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(f(s(s(x1)))) -> f#(x1) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(h(x1)) -> h#(f(s(h(x1)))) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(h(x1)) -> f#(s(h(x1))) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> h#(x1) f#(h(x1)) -> f#(s(h(x1))) -> f#(f(s(s(x1)))) -> f#(f(x1)) f#(h(x1)) -> f#(s(h(x1))) -> f#(f(s(s(x1)))) -> f#(x1) f#(h(x1)) -> f#(s(h(x1))) -> f#(h(x1)) -> h#(f(s(h(x1)))) f#(h(x1)) -> f#(s(h(x1))) -> f#(h(x1)) -> f#(s(h(x1))) f#(h(x1)) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(h(x1)) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(h(x1)) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> h#(x1) g#(h(x1)) -> f#(s(x1)) -> f#(f(s(s(x1)))) -> f#(f(x1)) g#(h(x1)) -> f#(s(x1)) -> f#(f(s(s(x1)))) -> f#(x1) g#(h(x1)) -> f#(s(x1)) -> f#(h(x1)) -> h#(f(s(h(x1)))) g#(h(x1)) -> f#(s(x1)) -> f#(h(x1)) -> f#(s(h(x1))) g#(h(x1)) -> f#(s(x1)) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) g#(h(x1)) -> f#(s(x1)) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) g#(h(x1)) -> f#(s(x1)) -> f#(s(s(s(x1)))) -> h#(x1) g#(h(x1)) -> g#(f(s(x1))) -> g#(h(x1)) -> g#(f(s(x1))) g#(h(x1)) -> g#(f(s(x1))) -> g#(h(x1)) -> f#(s(x1)) EDG Processor: DPs: g#(h(x1)) -> f#(s(x1)) g#(h(x1)) -> g#(f(s(x1))) f#(s(s(s(x1)))) -> h#(x1) f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(h(x1)) -> f#(s(h(x1))) f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) b#(a(x1)) -> b#(x1) b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(b(b(b(x1)))) -> a#(x1) TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) graph: a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(a(a(x1))) -> b#(x1) -> b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> b#(x1) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> a#(b(x1)) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> a#(a(b(x1))) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(x1) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(x1)) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> a#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> h#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(h(x1)) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(f(s(s(x1)))) -> f#(f(x1)) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> h#(x1) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) -> f#(h(x1)) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(x1) -> f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) -> f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(x1) -> f#(f(s(s(x1)))) -> f#(f(x1)) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> h#(x1) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(s(s(s(x1)))) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(h(x1)) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> h#(x1) f#(h(x1)) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(h(x1)) -> f#(s(h(x1))) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) g#(h(x1)) -> f#(s(x1)) -> f#(s(s(s(x1)))) -> h#(x1) g#(h(x1)) -> f#(s(x1)) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) g#(h(x1)) -> f#(s(x1)) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) g#(h(x1)) -> g#(f(s(x1))) -> g#(h(x1)) -> f#(s(x1)) g#(h(x1)) -> g#(f(s(x1))) -> g#(h(x1)) -> g#(f(s(x1))) CDG Processor: DPs: g#(h(x1)) -> f#(s(x1)) g#(h(x1)) -> g#(f(s(x1))) f#(s(s(s(x1)))) -> h#(x1) f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(h(x1)) -> f#(s(h(x1))) f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) b#(a(x1)) -> b#(x1) b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(b(b(b(x1)))) -> a#(x1) TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) graph: a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> b#(x1) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(a(a(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(a(a(x1))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(x1))) -> b#(x1) -> b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> a#(a(b(x1))) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> a#(b(x1)) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(x1))) -> b#(x1) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(x1))) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(x1)) b#(a(x1)) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> a#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(f(s(s(x1)))) -> f#(f(x1)) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(h(x1)) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(f(x1)) -> f#(s(s(s(x1)))) -> h#(x1) f#(f(s(s(x1)))) -> f#(x1) -> f#(f(s(s(x1)))) -> f#(f(x1)) f#(f(s(s(x1)))) -> f#(x1) -> f#(f(s(s(x1)))) -> f#(x1) f#(f(s(s(x1)))) -> f#(x1) -> f#(h(x1)) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) -> f#(h(x1)) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> h#(f(s(h(x1)))) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> f#(s(h(x1))) f#(f(s(s(x1)))) -> f#(x1) -> f#(s(s(s(x1)))) -> h#(x1) g#(h(x1)) -> g#(f(s(x1))) -> g#(h(x1)) -> g#(f(s(x1))) g#(h(x1)) -> g#(f(s(x1))) -> g#(h(x1)) -> f#(s(x1)) SCC Processor: #sccs: 3 #rules: 10 #arcs: 41/256 DPs: g#(h(x1)) -> g#(f(s(x1))) TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) Matrix Interpretation Processor: dim=3 interpretation: [g#](x0) = [0 1 0]x0, [0 2 0] [b](x0) = [1 0 0]x0 [0 0 1] , [0] [a](x0) = [0] [0], [0 2 0] [f](x0) = [0 2 0]x0 [2 0 0] , [0 0 0] [0] [s](x0) = [0 0 1]x0 + [0] [0 1 0] [1], [0 2 0] [g](x0) = [0 3 1]x0 [0 0 0] , [1 0 0] [0] [h](x0) = [0 1 2]x0 + [1] [0 0 1] [0] orientation: g#(h(x1)) = [0 1 2]x1 + [1] >= [0 0 2]x1 = g#(f(s(x1))) [0 2 4] [2] [0 0 4] g(h(x1)) = [0 3 7]x1 + [3] >= [0 0 6]x1 = g(f(s(x1))) [0 0 0] [0] [0 0 0] [0 0 2] [2] [0 0 2] [0] f(s(s(s(x1)))) = [0 0 2]x1 + [2] >= [0 0 2]x1 + [1] = h(f(s(h(x1)))) [0 0 0] [0] [0 0 0] [0] [0 2 4] [2] [0 0 2] [0] f(h(x1)) = [0 2 4]x1 + [2] >= [0 0 2]x1 + [1] = h(f(s(h(x1)))) [2 0 0] [0] [0 0 0] [0] [1 0 0] [0] h(x1) = [0 1 2]x1 + [1] >= x1 = x1 [0 0 1] [0] [0 4 0] [4] [0 0 0] [0] f(f(s(s(x1)))) = [0 4 0]x1 + [4] >= [0 4 0]x1 + [1] = s(s(s(f(f(x1))))) [0 4 0] [4] [0 4 0] [2] [0] [0] b(a(x1)) = [0] >= [0] = a(b(x1)) [0] [0] [0] [0] a(a(a(x1))) = [0] >= [0] = b(a(a(b(x1)))) [0] [0] [4 0 0] [0] b(b(b(b(x1)))) = [0 4 0]x1 >= [0] = a(x1) [0 0 1] [0] problem: DPs: TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) Qed DPs: f#(f(s(s(x1)))) -> f#(f(x1)) f#(f(s(s(x1)))) -> f#(x1) TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) Matrix Interpretation Processor: dim=3 interpretation: [f#](x0) = [2 0 0]x0, [0 0 0] [0] [b](x0) = [0 0 1]x0 + [0] [0 0 0] [1], [0] [a](x0) = [1] [1], [2 0 0] [f](x0) = [2 0 0]x0 [0 2 0] , [0 0 1] [0] [s](x0) = [0 0 0]x0 + [0] [1 0 0] [1], [0 0 2] [1] [g](x0) = [0 0 0]x0 + [3] [0 1 3] [1], [1 0 1] [2] [h](x0) = [0 1 0]x0 + [0] [0 0 1] [0] orientation: f#(f(s(s(x1)))) = [4 0 0]x1 + [4] >= [4 0 0]x1 = f#(f(x1)) f#(f(s(s(x1)))) = [4 0 0]x1 + [4] >= [2 0 0]x1 = f#(x1) [0 0 2] [1] [0 0 0] [1] g(h(x1)) = [0 0 0]x1 + [3] >= [0 0 0]x1 + [3] = g(f(s(x1))) [0 1 3] [1] [0 0 2] [1] [0 0 2] [2] [0 0 2] [2] f(s(s(s(x1)))) = [0 0 2]x1 + [2] >= [0 0 2]x1 + [0] = h(f(s(h(x1)))) [0 0 0] [0] [0 0 0] [0] [2 0 2] [4] [0 0 2] [2] f(h(x1)) = [2 0 2]x1 + [4] >= [0 0 2]x1 + [0] = h(f(s(h(x1)))) [0 2 0] [0] [0 0 0] [0] [1 0 1] [2] h(x1) = [0 1 0]x1 + [0] >= x1 = x1 [0 0 1] [0] [4 0 0] [4] [4 0 0] [1] f(f(s(s(x1)))) = [4 0 0]x1 + [4] >= [0 0 0]x1 + [0] = s(s(s(f(f(x1))))) [4 0 0] [4] [4 0 0] [2] [0] [0] b(a(x1)) = [1] >= [1] = a(b(x1)) [1] [1] [0] [0] a(a(a(x1))) = [1] >= [1] = b(a(a(b(x1)))) [1] [1] [0] [0] b(b(b(b(x1)))) = [1] >= [1] = a(x1) [1] [1] problem: DPs: TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) Qed DPs: a#(a(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) b#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(x1))) a#(a(a(x1))) -> b#(a(a(b(x1)))) b#(b(b(b(x1)))) -> a#(x1) TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) Matrix Interpretation Processor: dim=1 interpretation: [a#](x0) = 2x0 + 16, [b#](x0) = 2x0 + 13, [b](x0) = x0 + 1, [a](x0) = x0 + 3, [f](x0) = 0, [s](x0) = 0, [g](x0) = 3, [h](x0) = 8x0 orientation: a#(a(a(x1))) = 2x1 + 28 >= 2x1 + 18 = a#(b(x1)) a#(a(a(x1))) = 2x1 + 28 >= 2x1 + 13 = b#(x1) b#(a(x1)) = 2x1 + 19 >= 2x1 + 13 = b#(x1) b#(a(x1)) = 2x1 + 19 >= 2x1 + 18 = a#(b(x1)) a#(a(a(x1))) = 2x1 + 28 >= 2x1 + 24 = a#(a(b(x1))) a#(a(a(x1))) = 2x1 + 28 >= 2x1 + 27 = b#(a(a(b(x1)))) b#(b(b(b(x1)))) = 2x1 + 19 >= 2x1 + 16 = a#(x1) g(h(x1)) = 3 >= 3 = g(f(s(x1))) f(s(s(s(x1)))) = 0 >= 0 = h(f(s(h(x1)))) f(h(x1)) = 0 >= 0 = h(f(s(h(x1)))) h(x1) = 8x1 >= x1 = x1 f(f(s(s(x1)))) = 0 >= 0 = s(s(s(f(f(x1))))) b(a(x1)) = x1 + 4 >= x1 + 4 = a(b(x1)) a(a(a(x1))) = x1 + 9 >= x1 + 8 = b(a(a(b(x1)))) b(b(b(b(x1)))) = x1 + 4 >= x1 + 3 = a(x1) problem: DPs: TRS: g(h(x1)) -> g(f(s(x1))) f(s(s(s(x1)))) -> h(f(s(h(x1)))) f(h(x1)) -> h(f(s(h(x1)))) h(x1) -> x1 f(f(s(s(x1)))) -> s(s(s(f(f(x1))))) b(a(x1)) -> a(b(x1)) a(a(a(x1))) -> b(a(a(b(x1)))) b(b(b(b(x1)))) -> a(x1) Qed