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 Restore Modifier: 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 SCC Processor: #sccs: 1 #rules: 5 #arcs: 25/25 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 Open