MAYBE Problem: f(h(x)) -> f(i(x)) f(i(x)) -> a() i(x) -> h(x) Proof: DP Processor: DPs: f#(h(x)) -> i#(x) f#(h(x)) -> f#(i(x)) TRS: f(h(x)) -> f(i(x)) f(i(x)) -> a() i(x) -> h(x) Usable Rule Processor: DPs: f#(h(x)) -> i#(x) f#(h(x)) -> f#(i(x)) TRS: i(x) -> h(x) ADG Processor: DPs: f#(h(x)) -> i#(x) f#(h(x)) -> f#(i(x)) TRS: i(x) -> h(x) graph: f#(h(x)) -> f#(i(x)) -> f#(h(x)) -> i#(x) f#(h(x)) -> f#(i(x)) -> f#(h(x)) -> f#(i(x)) Restore Modifier: DPs: f#(h(x)) -> i#(x) f#(h(x)) -> f#(i(x)) TRS: f(h(x)) -> f(i(x)) f(i(x)) -> a() i(x) -> h(x) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: f#(h(x)) -> f#(i(x)) TRS: f(h(x)) -> f(i(x)) f(i(x)) -> a() i(x) -> h(x) Open