MAYBE Problem: purge(nil()) -> nil() purge(.(x,y)) -> .(x,purge(remove(x,y))) remove(x,nil()) -> nil() remove(x,.(y,z)) -> if(=(x,y),remove(x,z),.(y,remove(x,z))) Proof: DP Processor: DPs: purge#(.(x,y)) -> remove#(x,y) purge#(.(x,y)) -> purge#(remove(x,y)) remove#(x,.(y,z)) -> remove#(x,z) TRS: purge(nil()) -> nil() purge(.(x,y)) -> .(x,purge(remove(x,y))) remove(x,nil()) -> nil() remove(x,.(y,z)) -> if(=(x,y),remove(x,z),.(y,remove(x,z))) Usable Rule Processor: DPs: purge#(.(x,y)) -> remove#(x,y) purge#(.(x,y)) -> purge#(remove(x,y)) remove#(x,.(y,z)) -> remove#(x,z) TRS: f8(x,y) -> x f8(x,y) -> y remove(x,nil()) -> nil() remove(x,.(y,z)) -> if(=(x,y),remove(x,z),.(y,remove(x,z))) TDG Processor: DPs: purge#(.(x,y)) -> remove#(x,y) purge#(.(x,y)) -> purge#(remove(x,y)) remove#(x,.(y,z)) -> remove#(x,z) TRS: f8(x,y) -> x f8(x,y) -> y remove(x,nil()) -> nil() remove(x,.(y,z)) -> if(=(x,y),remove(x,z),.(y,remove(x,z))) graph: remove#(x,.(y,z)) -> remove#(x,z) -> remove#(x,.(y,z)) -> remove#(x,z) purge#(.(x,y)) -> remove#(x,y) -> remove#(x,.(y,z)) -> remove#(x,z) purge#(.(x,y)) -> purge#(remove(x,y)) -> purge#(.(x,y)) -> purge#(remove(x,y)) purge#(.(x,y)) -> purge#(remove(x,y)) -> purge#(.(x,y)) -> remove#(x,y) Restore Modifier: DPs: purge#(.(x,y)) -> remove#(x,y) purge#(.(x,y)) -> purge#(remove(x,y)) remove#(x,.(y,z)) -> remove#(x,z) TRS: purge(nil()) -> nil() purge(.(x,y)) -> .(x,purge(remove(x,y))) remove(x,nil()) -> nil() remove(x,.(y,z)) -> if(=(x,y),remove(x,z),.(y,remove(x,z))) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/9 DPs: purge#(.(x,y)) -> purge#(remove(x,y)) TRS: purge(nil()) -> nil() purge(.(x,y)) -> .(x,purge(remove(x,y))) remove(x,nil()) -> nil() remove(x,.(y,z)) -> if(=(x,y),remove(x,z),.(y,remove(x,z))) Open DPs: remove#(x,.(y,z)) -> remove#(x,z) TRS: purge(nil()) -> nil() purge(.(x,y)) -> .(x,purge(remove(x,y))) remove(x,nil()) -> nil() remove(x,.(y,z)) -> if(=(x,y),remove(x,z),.(y,remove(x,z))) Open