MAYBE Problem: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) Proof: DP Processor: DPs: half#(s(s(x))) -> half#(x) log#(s(s(x))) -> half#(x) log#(s(s(x))) -> log#(s(half(x))) TRS: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) ADG Processor: DPs: half#(s(s(x))) -> half#(x) log#(s(s(x))) -> half#(x) log#(s(s(x))) -> log#(s(half(x))) TRS: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) graph: log#(s(s(x))) -> log#(s(half(x))) -> log#(s(s(x))) -> half#(x) log#(s(s(x))) -> log#(s(half(x))) -> log#(s(s(x))) -> log#(s(half(x))) log#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x) half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/9 DPs: log#(s(s(x))) -> log#(s(half(x))) TRS: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) Open DPs: half#(s(s(x))) -> half#(x) TRS: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) Open