MAYBE Problem: f(s(x),y,b()) -> f(g(h(x)),y,i(y)) g(h(x)) -> g(x) g(s(x)) -> s(x) g(0()) -> s(0()) h(0()) -> a() i(0()) -> b() i(s(y)) -> i(y) Proof: DP Processor: DPs: f#(s(x),y,b()) -> i#(y) f#(s(x),y,b()) -> h#(x) f#(s(x),y,b()) -> g#(h(x)) f#(s(x),y,b()) -> f#(g(h(x)),y,i(y)) g#(h(x)) -> g#(x) i#(s(y)) -> i#(y) TRS: f(s(x),y,b()) -> f(g(h(x)),y,i(y)) g(h(x)) -> g(x) g(s(x)) -> s(x) g(0()) -> s(0()) h(0()) -> a() i(0()) -> b() i(s(y)) -> i(y) CDG Processor: DPs: f#(s(x),y,b()) -> i#(y) f#(s(x),y,b()) -> h#(x) f#(s(x),y,b()) -> g#(h(x)) f#(s(x),y,b()) -> f#(g(h(x)),y,i(y)) g#(h(x)) -> g#(x) i#(s(y)) -> i#(y) TRS: f(s(x),y,b()) -> f(g(h(x)),y,i(y)) g(h(x)) -> g(x) g(s(x)) -> s(x) g(0()) -> s(0()) h(0()) -> a() i(0()) -> b() i(s(y)) -> i(y) graph: g#(h(x)) -> g#(x) -> g#(h(x)) -> g#(x) i#(s(y)) -> i#(y) -> i#(s(y)) -> i#(y) f#(s(x),y,b()) -> g#(h(x)) -> g#(h(x)) -> g#(x) f#(s(x),y,b()) -> i#(y) -> i#(s(y)) -> i#(y) f#(s(x),y,b()) -> f#(g(h(x)),y,i(y)) -> f#(s(x),y,b()) -> i#(y) f#(s(x),y,b()) -> f#(g(h(x)),y,i(y)) -> f#(s(x),y,b()) -> h#(x) f#(s(x),y,b()) -> f#(g(h(x)),y,i(y)) -> f#(s(x),y,b()) -> g#(h(x)) f#(s(x),y,b()) -> f#(g(h(x)),y,i(y)) -> f#(s(x),y,b()) -> f#(g(h(x)),y,i(y)) SCC Processor: #sccs: 3 #rules: 3 #arcs: 8/36 DPs: f#(s(x),y,b()) -> f#(g(h(x)),y,i(y)) TRS: f(s(x),y,b()) -> f(g(h(x)),y,i(y)) g(h(x)) -> g(x) g(s(x)) -> s(x) g(0()) -> s(0()) h(0()) -> a() i(0()) -> b() i(s(y)) -> i(y) Open DPs: i#(s(y)) -> i#(y) TRS: f(s(x),y,b()) -> f(g(h(x)),y,i(y)) g(h(x)) -> g(x) g(s(x)) -> s(x) g(0()) -> s(0()) h(0()) -> a() i(0()) -> b() i(s(y)) -> i(y) Open DPs: g#(h(x)) -> g#(x) TRS: f(s(x),y,b()) -> f(g(h(x)),y,i(y)) g(h(x)) -> g(x) g(s(x)) -> s(x) g(0()) -> s(0()) h(0()) -> a() i(0()) -> b() i(s(y)) -> i(y) Open