MAYBE Problem: f(x,x) -> f(i(x),g(g(x))) f(x,y) -> x g(x) -> i(x) f(x,i(x)) -> f(x,x) f(i(x),i(g(x))) -> a() Proof: DP Processor: DPs: f#(x,x) -> g#(x) f#(x,x) -> g#(g(x)) f#(x,x) -> f#(i(x),g(g(x))) f#(x,i(x)) -> f#(x,x) TRS: f(x,x) -> f(i(x),g(g(x))) f(x,y) -> x g(x) -> i(x) f(x,i(x)) -> f(x,x) f(i(x),i(g(x))) -> a() Usable Rule Processor: DPs: f#(x,x) -> g#(x) f#(x,x) -> g#(g(x)) f#(x,x) -> f#(i(x),g(g(x))) f#(x,i(x)) -> f#(x,x) TRS: g(x) -> i(x) TDG Processor: DPs: f#(x,x) -> g#(x) f#(x,x) -> g#(g(x)) f#(x,x) -> f#(i(x),g(g(x))) f#(x,i(x)) -> f#(x,x) TRS: g(x) -> i(x) graph: f#(x,i(x)) -> f#(x,x) -> f#(x,i(x)) -> f#(x,x) f#(x,i(x)) -> f#(x,x) -> f#(x,x) -> f#(i(x),g(g(x))) f#(x,i(x)) -> f#(x,x) -> f#(x,x) -> g#(g(x)) f#(x,i(x)) -> f#(x,x) -> f#(x,x) -> g#(x) f#(x,x) -> f#(i(x),g(g(x))) -> f#(x,i(x)) -> f#(x,x) f#(x,x) -> f#(i(x),g(g(x))) -> f#(x,x) -> f#(i(x),g(g(x))) f#(x,x) -> f#(i(x),g(g(x))) -> f#(x,x) -> g#(g(x)) f#(x,x) -> f#(i(x),g(g(x))) -> f#(x,x) -> g#(x) Restore Modifier: DPs: f#(x,x) -> g#(x) f#(x,x) -> g#(g(x)) f#(x,x) -> f#(i(x),g(g(x))) f#(x,i(x)) -> f#(x,x) TRS: f(x,x) -> f(i(x),g(g(x))) f(x,y) -> x g(x) -> i(x) f(x,i(x)) -> f(x,x) f(i(x),i(g(x))) -> a() SCC Processor: #sccs: 1 #rules: 2 #arcs: 8/16 DPs: f#(x,i(x)) -> f#(x,x) f#(x,x) -> f#(i(x),g(g(x))) TRS: f(x,x) -> f(i(x),g(g(x))) f(x,y) -> x g(x) -> i(x) f(x,i(x)) -> f(x,x) f(i(x),i(g(x))) -> a() Open