YES Proof: This system is confluent. By \cite{ALS94}, Theorem 4.1. This system is of type 3 or smaller. This system is strongly deterministic. All 2 critical pairs are joinable. pair($4, cons($8, $7)) = pair(cons($8, y), $3) <= split($5, x) = pair(y, $3), le($5, $8) = false, split($5, x) = pair($4, $7), le($5, $8) = true: This critical pair is unfeasible. pair(cons($8, $4), $7) = pair(y, cons($8, $3)) <= split($5, x) = pair(y, $3), le($5, $8) = true, split($5, x) = pair($4, $7), le($5, $8) = false: This critical pair is unfeasible. This system is of type 3 or smaller. This system is deterministic. By \cite{O02}, p. 214, Proposition 7.2.50. This system is of type 3 or smaller. This system is deterministic. System R transformed to optimized U(R). Call external tool: ttt2 - trs 30 Input: le(0, x) -> true le(s(x), 0) -> false le(s(x), s(y)) -> le(x, y) app(nil, x) -> x app(cons(x, xs), ys) -> cons(x, app(xs, ys)) split(x, nil) -> pair(nil, nil) qsort(nil) -> nil ?2(true, x, ys, y, zs, xs) -> pair(xs, cons(y, zs)) ?3(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs) split(x, cons(y, ys)) -> ?3(split(x, ys), x, y, ys) ?2(false, x, ys, y, zs, xs) -> pair(cons(y, xs), zs) ?1(pair(ys, zs), x, xs) -> app(qsort(ys), cons(x, qsort(zs))) qsort(cons(x, xs)) -> ?1(split(x, xs), x, xs) DP Processor: DPs: le#(s(x),s(y)) -> le#(x,y) app#(cons(x,xs),ys) -> app#(xs,ys) ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) split#(x,cons(y,ys)) -> split#(x,ys) split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ?1#(pair(ys,zs),x,xs) -> qsort#(zs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) qsort#(cons(x,xs)) -> split#(x,xs) qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) TDG Processor: DPs: le#(s(x),s(y)) -> le#(x,y) app#(cons(x,xs),ys) -> app#(xs,ys) ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) split#(x,cons(y,ys)) -> split#(x,ys) split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ?1#(pair(ys,zs),x,xs) -> qsort#(zs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) qsort#(cons(x,xs)) -> split#(x,xs) qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) graph: ?1#(pair(ys,zs),x,xs) -> qsort#(zs) -> qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) ?1#(pair(ys,zs),x,xs) -> qsort#(zs) -> qsort#(cons(x,xs)) -> split#(x,xs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) -> qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) -> qsort#(cons(x,xs)) -> split#(x,xs) ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) -> app#(cons(x,xs),ys) -> app#(xs,ys) ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> ?1#(pair(ys,zs),x,xs) -> qsort#(ys) qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> ?1#(pair(ys,zs),x,xs) -> qsort#(zs) qsort#(cons(x,xs)) -> split#(x,xs) -> split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) qsort#(cons(x,xs)) -> split#(x,xs) -> split#(x,cons(y,ys)) -> split#(x,ys) split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) -> ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) -> ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) split#(x,cons(y,ys)) -> split#(x,ys) -> split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) split#(x,cons(y,ys)) -> split#(x,ys) -> split#(x,cons(y,ys)) -> split#(x,ys) app#(cons(x,xs),ys) -> app#(xs,ys) -> app#(cons(x,xs),ys) -> app#(xs,ys) le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) SCC Processor: #sccs: 4 #rules: 6 #arcs: 17/121 DPs: ?1#(pair(ys,zs),x,xs) -> qsort#(zs) qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) Usable Rule Processor: DPs: ?1#(pair(ys,zs),x,xs) -> qsort#(zs) qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) TRS: split(x,nil()) -> pair(nil(),nil()) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) Matrix Interpretation Processor: dim=2 usable rules: split(x,nil()) -> pair(nil(),nil()) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) interpretation: [2] [false] = [0], [0 2] [split](x0, x1) = [0 2]x1, [2] [le](x0, x1) = [0], [0] [s](x0) = [0], [qsort#](x0) = [0 2]x0, [0] [nil] = [0], [0] [0] = [0], [0 0] [0] [cons](x0, x1) = [1 1]x1 + [1], [?1#](x0, x1, x2) = [1 0]x0, [0 1] [2 0] [2] [?3](x0, x1, x2, x3) = [0 1]x0 + [1 0]x3 + [2], [1 0] [2 0] [2 2] [2 2] [?2](x0, x1, x2, x3, x4, x5) = [1 0]x0 + [0 0]x2 + [2 2]x4 + [2 2]x5, [0 2] [0 2] [pair](x0, x1) = [2 2]x0 + [2 2]x1, [2] [true] = [0] orientation: ?1#(pair(ys,zs),x,xs) = [0 2]ys + [0 2]zs >= [0 2]zs = qsort#(zs) qsort#(cons(x,xs)) = [2 2]xs + [2] >= [0 2]xs = ?1#(split(x,xs),x,xs) ?1#(pair(ys,zs),x,xs) = [0 2]ys + [0 2]zs >= [0 2]ys = qsort#(ys) [0] [0] split(x,nil()) = [0] >= [0] = pair(nil(),nil()) [2 2] [2] [2 2] [2] split(x,cons(y,ys)) = [2 2]ys + [2] >= [1 2]ys + [2] = ?3(split(x,ys),x,y,ys) [2 2] [2 0] [2 2] [2] [2 2] [2 0] [2 2] [2] ?3(pair(xs,zs),x,y,ys) = [2 2]xs + [1 0]ys + [2 2]zs + [2] >= [2 2]xs + [0 0]ys + [2 2]zs + [2] = ?2(le(x,y),x,ys,y,zs,xs) [2 2] [2 0] [2 2] [2] [0 2] [2 2] [2] ?2(true(),x,ys,y,zs,xs) = [2 2]xs + [0 0]ys + [2 2]zs + [2] >= [2 2]xs + [2 2]zs + [2] = pair(xs,cons(y,zs)) [2 2] [2 0] [2 2] [2] [2 2] [0 2] [2] ?2(false(),x,ys,y,zs,xs) = [2 2]xs + [0 0]ys + [2 2]zs + [2] >= [2 2]xs + [2 2]zs + [2] = pair(cons(y,xs),zs) [2] [2] le(0(),x) = [0] >= [0] = true() [2] [2] le(s(x),0()) = [0] >= [0] = false() [2] [2] le(s(x),s(y)) = [0] >= [0] = le(x,y) problem: DPs: ?1#(pair(ys,zs),x,xs) -> qsort#(zs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) TRS: split(x,nil()) -> pair(nil(),nil()) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) Restore Modifier: DPs: ?1#(pair(ys,zs),x,xs) -> qsort#(zs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) EDG Processor: DPs: ?1#(pair(ys,zs),x,xs) -> qsort#(zs) ?1#(pair(ys,zs),x,xs) -> qsort#(ys) TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) graph: Qed DPs: app#(cons(x,xs),ys) -> app#(xs,ys) TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) Subterm Criterion Processor: simple projection: pi(app#) = 0 problem: DPs: TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) Qed DPs: split#(x,cons(y,ys)) -> split#(x,ys) TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) Subterm Criterion Processor: simple projection: pi(split#) = 1 problem: DPs: TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) Qed DPs: le#(s(x),s(y)) -> le#(x,y) TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) Subterm Criterion Processor: simple projection: pi(le#) = 0 problem: DPs: TRS: le(0(),x) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) app(nil(),x) -> x app(cons(x,xs),ys) -> cons(x,app(xs,ys)) split(x,nil()) -> pair(nil(),nil()) qsort(nil()) -> nil() ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) Qed