MAYBE Problem: f(X,g(X)) -> f(1(),g(X)) g(1()) -> g(0()) Proof: DP Processor: DPs: f#(X,g(X)) -> f#(1(),g(X)) g#(1()) -> g#(0()) TRS: f(X,g(X)) -> f(1(),g(X)) g(1()) -> g(0()) CDG Processor: DPs: f#(X,g(X)) -> f#(1(),g(X)) g#(1()) -> g#(0()) TRS: f(X,g(X)) -> f(1(),g(X)) g(1()) -> g(0()) graph: f#(X,g(X)) -> f#(1(),g(X)) -> f#(X,g(X)) -> f#(1(),g(X)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/4 DPs: f#(X,g(X)) -> f#(1(),g(X)) TRS: f(X,g(X)) -> f(1(),g(X)) g(1()) -> g(0()) Open