MAYBE Problem: ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) Proof: DP Processor: DPs: ap#(ap(ff(),x),x) -> ap#(cons(),x) ap#(ap(ff(),x),x) -> ap#(ap(cons(),x),nil()) ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) TRS: ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) EDG Processor: DPs: ap#(ap(ff(),x),x) -> ap#(cons(),x) ap#(ap(ff(),x),x) -> ap#(ap(cons(),x),nil()) ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) TRS: ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) graph: ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) -> ap#(ap(ff(),x),x) -> ap#(cons(),x) ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) -> ap#(ap(ff(),x),x) -> ap#(ap(cons(),x),nil()) ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) -> ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) -> ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) -> ap#(ap(ff(),x),x) -> ap#(cons(),x) ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) -> ap#(ap(ff(),x),x) -> ap#(ap(cons(),x),nil()) ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) -> ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) -> ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) SCC Processor: #sccs: 1 #rules: 2 #arcs: 8/16 DPs: ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x)) TRS: ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil())) Open