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