MAYBE Problem: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) Proof: DP Processor: DPs: i#(x,x) -> i#(a(),b()) g#(x,x) -> g#(a(),b()) h#(s(f(x))) -> h#(f(x)) f#(s(x)) -> h#(s(x)) f#(s(x)) -> f#(h(s(x))) f#(g(s(x),y)) -> g#(x,s(y)) f#(g(s(x),y)) -> f#(g(x,s(y))) h#(g(x,s(y))) -> g#(s(x),y) h#(g(x,s(y))) -> h#(g(s(x),y)) h#(i(x,y)) -> h#(y) h#(i(x,y)) -> h#(h(y)) h#(i(x,y)) -> i#(c(),h(h(y))) h#(i(x,y)) -> i#(i(c(),h(h(y))),x) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) TRS: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) TDG Processor: DPs: i#(x,x) -> i#(a(),b()) g#(x,x) -> g#(a(),b()) h#(s(f(x))) -> h#(f(x)) f#(s(x)) -> h#(s(x)) f#(s(x)) -> f#(h(s(x))) f#(g(s(x),y)) -> g#(x,s(y)) f#(g(s(x),y)) -> f#(g(x,s(y))) h#(g(x,s(y))) -> g#(s(x),y) h#(g(x,s(y))) -> h#(g(s(x),y)) h#(i(x,y)) -> h#(y) h#(i(x,y)) -> h#(h(y)) h#(i(x,y)) -> i#(c(),h(h(y))) h#(i(x,y)) -> i#(i(c(),h(h(y))),x) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) TRS: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) graph: f#(s(x)) -> f#(h(s(x))) -> f#(g(s(x),y)) -> f#(g(x,s(y))) f#(s(x)) -> f#(h(s(x))) -> f#(g(s(x),y)) -> g#(x,s(y)) f#(s(x)) -> f#(h(s(x))) -> f#(s(x)) -> f#(h(s(x))) f#(s(x)) -> f#(h(s(x))) -> f#(s(x)) -> h#(s(x)) f#(s(x)) -> h#(s(x)) -> h#(i(x,y)) -> i#(i(c(),h(h(y))),x) f#(s(x)) -> h#(s(x)) -> h#(i(x,y)) -> i#(c(),h(h(y))) f#(s(x)) -> h#(s(x)) -> h#(i(x,y)) -> h#(h(y)) f#(s(x)) -> h#(s(x)) -> h#(i(x,y)) -> h#(y) f#(s(x)) -> h#(s(x)) -> h#(g(x,s(y))) -> h#(g(s(x),y)) f#(s(x)) -> h#(s(x)) -> h#(g(x,s(y))) -> g#(s(x),y) f#(s(x)) -> h#(s(x)) -> h#(s(f(x))) -> h#(f(x)) f#(g(s(x),y)) -> f#(g(x,s(y))) -> f#(g(s(x),y)) -> f#(g(x,s(y))) f#(g(s(x),y)) -> f#(g(x,s(y))) -> f#(g(s(x),y)) -> g#(x,s(y)) f#(g(s(x),y)) -> f#(g(x,s(y))) -> f#(s(x)) -> f#(h(s(x))) f#(g(s(x),y)) -> f#(g(x,s(y))) -> f#(s(x)) -> h#(s(x)) f#(g(s(x),y)) -> g#(x,s(y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) f#(g(s(x),y)) -> g#(x,s(y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) f#(g(s(x),y)) -> g#(x,s(y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) f#(g(s(x),y)) -> g#(x,s(y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) f#(g(s(x),y)) -> g#(x,s(y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) f#(g(s(x),y)) -> g#(x,s(y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) f#(g(s(x),y)) -> g#(x,s(y)) -> g#(x,x) -> g#(a(),b()) h#(s(f(x))) -> h#(f(x)) -> h#(i(x,y)) -> i#(i(c(),h(h(y))),x) h#(s(f(x))) -> h#(f(x)) -> h#(i(x,y)) -> i#(c(),h(h(y))) h#(s(f(x))) -> h#(f(x)) -> h#(i(x,y)) -> h#(h(y)) h#(s(f(x))) -> h#(f(x)) -> h#(i(x,y)) -> h#(y) h#(s(f(x))) -> h#(f(x)) -> h#(g(x,s(y))) -> h#(g(s(x),y)) h#(s(f(x))) -> h#(f(x)) -> h#(g(x,s(y))) -> g#(s(x),y) h#(s(f(x))) -> h#(f(x)) -> h#(s(f(x))) -> h#(f(x)) h#(g(x,s(y))) -> h#(g(s(x),y)) -> h#(i(x,y)) -> i#(i(c(),h(h(y))),x) h#(g(x,s(y))) -> h#(g(s(x),y)) -> h#(i(x,y)) -> i#(c(),h(h(y))) h#(g(x,s(y))) -> h#(g(s(x),y)) -> h#(i(x,y)) -> h#(h(y)) h#(g(x,s(y))) -> h#(g(s(x),y)) -> h#(i(x,y)) -> h#(y) h#(g(x,s(y))) -> h#(g(s(x),y)) -> h#(g(x,s(y))) -> h#(g(s(x),y)) h#(g(x,s(y))) -> h#(g(s(x),y)) -> h#(g(x,s(y))) -> g#(s(x),y) h#(g(x,s(y))) -> h#(g(s(x),y)) -> h#(s(f(x))) -> h#(f(x)) h#(g(x,s(y))) -> g#(s(x),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) h#(g(x,s(y))) -> g#(s(x),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) h#(g(x,s(y))) -> g#(s(x),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) h#(g(x,s(y))) -> g#(s(x),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) h#(g(x,s(y))) -> g#(s(x),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) h#(g(x,s(y))) -> g#(s(x),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) h#(g(x,s(y))) -> g#(s(x),y) -> g#(x,x) -> g#(a(),b()) h#(i(x,y)) -> h#(h(y)) -> h#(i(x,y)) -> i#(i(c(),h(h(y))),x) h#(i(x,y)) -> h#(h(y)) -> h#(i(x,y)) -> i#(c(),h(h(y))) h#(i(x,y)) -> h#(h(y)) -> h#(i(x,y)) -> h#(h(y)) h#(i(x,y)) -> h#(h(y)) -> h#(i(x,y)) -> h#(y) h#(i(x,y)) -> h#(h(y)) -> h#(g(x,s(y))) -> h#(g(s(x),y)) h#(i(x,y)) -> h#(h(y)) -> h#(g(x,s(y))) -> g#(s(x),y) h#(i(x,y)) -> h#(h(y)) -> h#(s(f(x))) -> h#(f(x)) h#(i(x,y)) -> h#(y) -> h#(i(x,y)) -> i#(i(c(),h(h(y))),x) h#(i(x,y)) -> h#(y) -> h#(i(x,y)) -> i#(c(),h(h(y))) h#(i(x,y)) -> h#(y) -> h#(i(x,y)) -> h#(h(y)) h#(i(x,y)) -> h#(y) -> h#(i(x,y)) -> h#(y) h#(i(x,y)) -> h#(y) -> h#(g(x,s(y))) -> h#(g(s(x),y)) h#(i(x,y)) -> h#(y) -> h#(g(x,s(y))) -> g#(s(x),y) h#(i(x,y)) -> h#(y) -> h#(s(f(x))) -> h#(f(x)) h#(i(x,y)) -> i#(c(),h(h(y))) -> i#(x,x) -> i#(a(),b()) h#(i(x,y)) -> i#(i(c(),h(h(y))),x) -> i#(x,x) -> i#(a(),b()) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) -> g#(x,x) -> g#(a(),b()) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) -> g#(x,x) -> g#(a(),b()) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) -> g#(x,x) -> g#(a(),b()) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) -> g#(x,x) -> g#(a(),b()) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) -> g#(x,x) -> g#(a(),b()) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) -> g#(x,x) -> g#(a(),b()) g#(x,x) -> g#(a(),b()) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) g#(x,x) -> g#(a(),b()) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(x,x) -> g#(a(),b()) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(x,x) -> g#(a(),b()) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(x,x) -> g#(a(),b()) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(x,x) -> g#(a(),b()) -> g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(x,x) -> g#(a(),b()) -> g#(x,x) -> g#(a(),b()) i#(x,x) -> i#(a(),b()) -> i#(x,x) -> i#(a(),b()) Restore Modifier: DPs: i#(x,x) -> i#(a(),b()) g#(x,x) -> g#(a(),b()) h#(s(f(x))) -> h#(f(x)) f#(s(x)) -> h#(s(x)) f#(s(x)) -> f#(h(s(x))) f#(g(s(x),y)) -> g#(x,s(y)) f#(g(s(x),y)) -> f#(g(x,s(y))) h#(g(x,s(y))) -> g#(s(x),y) h#(g(x,s(y))) -> h#(g(s(x),y)) h#(i(x,y)) -> h#(y) h#(i(x,y)) -> h#(h(y)) h#(i(x,y)) -> i#(c(),h(h(y))) h#(i(x,y)) -> i#(i(c(),h(h(y))),x) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) TRS: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) SCC Processor: #sccs: 4 #rules: 14 #arcs: 109/361 DPs: f#(s(x)) -> f#(h(s(x))) f#(g(s(x),y)) -> f#(g(x,s(y))) TRS: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) Open DPs: h#(s(f(x))) -> h#(f(x)) h#(g(x,s(y))) -> h#(g(s(x),y)) h#(i(x,y)) -> h#(y) h#(i(x,y)) -> h#(h(y)) TRS: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) Open DPs: i#(x,x) -> i#(a(),b()) TRS: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) Open DPs: g#(x,x) -> g#(a(),b()) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),y) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(b(),g(b(),y)) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(x,g(b(),g(b(),y))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(x,g(b(),g(b(),y)))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(x,g(b(),g(b(),y))))) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) TRS: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) Open