MAYBE Problem: rev(xs) -> revtl(xs,nil()) revtl(nil(),ys) -> ys revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys)) Proof: DP Processor: DPs: rev#(xs) -> revtl#(xs,nil()) revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys)) TRS: rev(xs) -> revtl(xs,nil()) revtl(nil(),ys) -> ys revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys)) EDG Processor: DPs: rev#(xs) -> revtl#(xs,nil()) revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys)) TRS: rev(xs) -> revtl(xs,nil()) revtl(nil(),ys) -> ys revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys)) graph: revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys)) -> revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys)) rev#(xs) -> revtl#(xs,nil()) -> revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys)) TRS: rev(xs) -> revtl(xs,nil()) revtl(nil(),ys) -> ys revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys)) Open