MAYBE Problem: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x Proof: DP Processor: DPs: a#(f(),0()) -> a#(s(),0()) a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) TRS: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x EDG Processor: DPs: a#(f(),0()) -> a#(s(),0()) a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) TRS: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x graph: a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) -> a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) -> a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) -> a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) -> a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),0()) -> a#(s(),0()) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) CDG Processor: DPs: a#(f(),0()) -> a#(s(),0()) a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) TRS: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x graph: a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(s(),a(s(),a(d(),a(p(),a(s(),x))))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(s(),a(d(),a(p(),a(s(),x)))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(d(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) -> a#(d(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(d(),a(f(),a(p(),a(s(),x)))) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),a(s(),x)) -> a#(p(),a(s(),x)) a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) -> a#(f(),0()) -> a#(s(),0()) SCC Processor: #sccs: 1 #rules: 1 #arcs: 8/64 DPs: a#(f(),a(s(),x)) -> a#(f(),a(p(),a(s(),x))) TRS: a(f(),0()) -> a(s(),0()) a(d(),0()) -> 0() a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x))))) a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x)))) a(p(),a(s(),x)) -> x Open