MAYBE Problem: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(d(x)) -> x g(c(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Proof: DP Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(x) TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(d(x)) -> x g(c(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) EDG Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(x) TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(d(x)) -> x g(c(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) graph: g#(h(x)) -> g#(x) -> g#(c(h(0()))) -> g#(d(1())) g#(h(x)) -> g#(x) -> g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(x) -> g#(h(x)) -> g#(x) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/25 DPs: g#(h(x)) -> g#(x) TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(d(x)) -> x g(c(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Open