MAYBE Problem: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) Proof: DP Processor: DPs: app#(cons(x,xs),ys) -> app#(xs,ys) rev#(cons(x,xs)) -> rev#(cons(x,nil())) shuffle#(cons(x,xs)) -> rev#(xs) shuffle#(cons(x,xs)) -> shuffle#(rev(xs)) TRS: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) TDG Processor: DPs: app#(cons(x,xs),ys) -> app#(xs,ys) rev#(cons(x,xs)) -> rev#(cons(x,nil())) shuffle#(cons(x,xs)) -> rev#(xs) shuffle#(cons(x,xs)) -> shuffle#(rev(xs)) TRS: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) graph: shuffle#(cons(x,xs)) -> shuffle#(rev(xs)) -> shuffle#(cons(x,xs)) -> shuffle#(rev(xs)) shuffle#(cons(x,xs)) -> shuffle#(rev(xs)) -> shuffle#(cons(x,xs)) -> rev#(xs) shuffle#(cons(x,xs)) -> rev#(xs) -> rev#(cons(x,xs)) -> rev#(cons(x,nil())) rev#(cons(x,xs)) -> rev#(cons(x,nil())) -> rev#(cons(x,xs)) -> rev#(cons(x,nil())) app#(cons(x,xs),ys) -> app#(xs,ys) -> app#(cons(x,xs),ys) -> app#(xs,ys) CDG Processor: DPs: app#(cons(x,xs),ys) -> app#(xs,ys) rev#(cons(x,xs)) -> rev#(cons(x,nil())) shuffle#(cons(x,xs)) -> rev#(xs) shuffle#(cons(x,xs)) -> shuffle#(rev(xs)) TRS: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) graph: shuffle#(cons(x,xs)) -> rev#(xs) -> rev#(cons(x,xs)) -> rev#(cons(x,nil())) rev#(cons(x,xs)) -> rev#(cons(x,nil())) -> rev#(cons(x,xs)) -> rev#(cons(x,nil())) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/16 DPs: rev#(cons(x,xs)) -> rev#(cons(x,nil())) TRS: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) rev(nil()) -> nil() rev(cons(x,xs)) -> append(xs,rev(cons(x,nil()))) shuffle(nil()) -> nil() shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs))) Open