MAYBE Problem: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y Proof: DP Processor: DPs: c#(c(c(y))) -> c#(a(y,0())) c#(c(c(y))) -> c#(c(a(y,0()))) c#(a(a(0(),x),y)) -> c#(0()) c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y EDG Processor: DPs: c#(c(c(y))) -> c#(a(y,0())) c#(c(c(y))) -> c#(c(a(y,0()))) c#(a(a(0(),x),y)) -> c#(0()) c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y graph: c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(c(c(y))) -> c#(a(y,0())) c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(c(c(y))) -> c#(c(a(y,0()))) c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(a(a(0(),x),y)) -> c#(0()) c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(0())) -> c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(c(c(y))) -> c#(a(y,0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(c(c(y))) -> c#(c(a(y,0()))) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(a(a(0(),x),y)) -> c#(0()) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) -> c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(0()) c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(c(0())) c#(c(c(y))) -> c#(a(y,0())) -> c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(c(c(y))) -> c#(a(y,0())) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(c(c(y))) -> c#(c(a(y,0()))) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(0()) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(c(0())) c#(c(c(y))) -> c#(c(a(y,0()))) -> c#(a(a(0(),x),y)) -> c#(c(c(0()))) SCC Processor: #sccs: 1 #rules: 4 #arcs: 18/25 DPs: c#(a(a(0(),x),y)) -> c#(c(0())) c#(a(a(0(),x),y)) -> c#(c(c(0()))) c#(c(c(y))) -> c#(c(a(y,0()))) c#(c(c(y))) -> c#(a(y,0())) TRS: c(c(c(y))) -> c(c(a(y,0()))) c(a(a(0(),x),y)) -> a(c(c(c(0()))),y) c(y) -> y Open