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()) 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)))))) CDG Processor: 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)))))) graph: Qed 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)))))) CDG Processor: 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)))))) graph: 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#(i(x,y)) -> h#(y) h#(i(x,y)) -> h#(h(y)) -> h#(i(x,y)) -> h#(h(y)) h#(i(x,y)) -> h#(y) -> h#(s(f(x))) -> h#(f(x)) h#(i(x,y)) -> h#(y) -> h#(g(x,s(y))) -> h#(g(s(x),y)) h#(i(x,y)) -> h#(y) -> h#(i(x,y)) -> h#(y) h#(i(x,y)) -> h#(y) -> h#(i(x,y)) -> h#(h(y)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 7/16 DPs: h#(i(x,y)) -> h#(h(y)) h#(i(x,y)) -> 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)))))) Matrix Interpretation Processor: dim=2 interpretation: [h#](x0) = [1 0]x0 + [1], [0] [c] = [0], [0 1] [h](x0) = [3 0]x0, [2 0] [s](x0) = [0 0]x0, [1 0] [f](x0) = [0 0]x0, [0 0] [1] [g](x0, x1) = [1 0]x1 + [0], [0] [b] = [0], [0] [a] = [0], [0 0] [1 1] [1] [i](x0, x1) = [1 1]x0 + [0 0]x1 + [1] orientation: h#(i(x,y)) = [1 1]y + [2] >= [0 1]y + [1] = h#(h(y)) h#(i(x,y)) = [1 1]y + [2] >= [1 0]y + [1] = h#(y) [1 1] [1] [1] i(x,x) = [1 1]x + [1] >= [1] = i(a(),b()) [0 0] [1] [1] g(x,x) = [1 0]x + [0] >= [0] = g(a(),b()) [0 0] [0 0] h(s(f(x))) = [6 0]x >= [3 0]x = h(f(x)) [2 0] [0] f(s(x)) = [0 0]x >= [0] = s(s(f(h(s(x))))) [1] [1] f(g(s(x),y)) = [0] >= [0] = f(g(x,s(y))) [2 0] [0] [1 0] [0] h(g(x,s(y))) = [0 0]y + [3] >= [0 0]y + [3] = h(g(s(x),y)) [1 1] [0 0] [1] [1 1] [0 0] [1] h(i(x,y)) = [0 0]x + [3 3]y + [3] >= [0 0]x + [3 3]y + [3] = i(i(c(),h(h(y))),x) [1] [1] g(a(),g(x,g(b(),g(a(),g(x,y))))) = [1] >= [1] = g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) problem: DPs: 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)))))) Qed 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)))))) EDG Processor: 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)))))) graph: Qed 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)))))) EDG Processor: 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)))))) graph: 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#(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(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(),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#(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(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#(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#(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#(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#(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#(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#(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#(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#(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)))))) CDG Processor: 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)))))) graph: 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()) SCC Processor: #sccs: 1 #rules: 3 #arcs: 22/49 DPs: 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)))) 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