26.96/7.70 YES 26.96/7.70 26.96/7.70 Problem: 26.96/7.70 le(0(), x) -> true() 26.96/7.70 le(s(x), 0()) -> false() 26.96/7.70 le(s(x), s(y)) -> le(x, y) 26.96/7.70 app(nil(), x) -> x 26.96/7.70 app(cons(x, xs), ys) -> cons(x, app(xs, ys)) 26.96/7.70 split(x, nil()) -> pair(nil(), nil()) 26.96/7.70 qsort(nil()) -> nil() 26.96/7.70 split(x, cons(y, ys)) -> pair(xs, cons(y, zs)) <= split(x, ys) = pair(xs, zs), le(x, y) = true() 26.96/7.70 split(x, cons(y, ys)) -> pair(cons(y, xs), zs) <= split(x, ys) = pair(xs, zs), le(x, y) = false() 26.96/7.70 qsort(cons(x, xs)) -> app(qsort(ys), cons(x, qsort(zs))) <= split(x, xs) = pair(ys, zs) 26.96/7.70 26.96/7.70 Proof: 26.96/7.70 This system is confluent. 26.96/7.70 By \cite{ALS94}, Theorem 4.1. 26.96/7.70 This system is of type 3 or smaller. 26.96/7.70 This system is strongly deterministic. 26.96/7.70 All 2 critical pairs are joinable. 26.96/7.70 CP: 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(): 26.96/7.70 This critical pair is unfeasible. 26.96/7.70 CP: 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(): 26.96/7.70 This critical pair is unfeasible. 26.96/7.70 This system is quasi-decreasing. 26.96/7.70 By \cite{O02}, p. 214, Proposition 7.2.50. 26.96/7.70 This system is of type 3 or smaller. 26.96/7.70 This system is deterministic. 26.96/7.70 System R transformed to optimized U(R). 26.96/7.70 This system is terminating. 26.96/7.70 Call external tool: 26.96/7.70 ./ttt2.sh 26.96/7.70 Input: 26.96/7.70 le(0(), x) -> true() 26.96/7.70 le(s(x), 0()) -> false() 26.96/7.70 le(s(x), s(y)) -> le(x, y) 26.96/7.70 app(nil(), x) -> x 26.96/7.70 app(cons(x, xs), ys) -> cons(x, app(xs, ys)) 26.96/7.70 split(x, nil()) -> pair(nil(), nil()) 26.96/7.70 qsort(nil()) -> nil() 26.96/7.70 ?2(true(), x, ys, y, zs, xs) -> pair(xs, cons(y, zs)) 26.96/7.70 ?3(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs) 26.96/7.70 split(x, cons(y, ys)) -> ?3(split(x, ys), x, y, ys) 26.96/7.70 ?2(false(), x, ys, y, zs, xs) -> pair(cons(y, xs), zs) 26.96/7.70 ?1(pair(ys, zs), x, xs) -> app(qsort(ys), cons(x, qsort(zs))) 26.96/7.70 qsort(cons(x, xs)) -> ?1(split(x, xs), x, xs) 26.96/7.70 26.96/7.70 DP Processor: 26.96/7.70 DPs: 26.96/7.70 le#(s(x),s(y)) -> le#(x,y) 26.96/7.70 app#(cons(x,xs),ys) -> app#(xs,ys) 26.96/7.70 ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) 26.96/7.70 ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) 26.96/7.70 split#(x,cons(y,ys)) -> split#(x,ys) 26.96/7.70 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 26.96/7.70 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 26.96/7.70 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 26.96/7.70 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 26.96/7.70 qsort#(cons(x,xs)) -> split#(x,xs) 26.96/7.70 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 26.96/7.70 TRS: 26.96/7.70 le(0(),x) -> true() 26.96/7.70 le(s(x),0()) -> false() 26.96/7.70 le(s(x),s(y)) -> le(x,y) 26.96/7.70 app(nil(),x) -> x 26.96/7.70 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 26.96/7.70 split(x,nil()) -> pair(nil(),nil()) 26.96/7.70 qsort(nil()) -> nil() 26.96/7.70 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 26.96/7.70 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 26.96/7.70 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 26.96/7.70 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 26.96/7.70 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 26.96/7.70 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 26.96/7.70 TDG Processor: 26.96/7.70 DPs: 26.96/7.70 le#(s(x),s(y)) -> le#(x,y) 26.96/7.70 app#(cons(x,xs),ys) -> app#(xs,ys) 26.96/7.70 ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) 26.96/7.70 ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) 27.39/7.72 split#(x,cons(y,ys)) -> split#(x,ys) 27.39/7.72 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 27.39/7.72 qsort#(cons(x,xs)) -> split#(x,xs) 27.39/7.72 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 27.39/7.72 TRS: 27.39/7.72 le(0(),x) -> true() 27.39/7.72 le(s(x),0()) -> false() 27.39/7.72 le(s(x),s(y)) -> le(x,y) 27.39/7.72 app(nil(),x) -> x 27.39/7.72 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 27.39/7.72 split(x,nil()) -> pair(nil(),nil()) 27.39/7.72 qsort(nil()) -> nil() 27.39/7.72 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.39/7.72 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.39/7.72 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.39/7.72 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.39/7.72 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 27.39/7.72 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 27.39/7.72 graph: 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) -> 27.39/7.72 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) -> 27.39/7.72 qsort#(cons(x,xs)) -> split#(x,xs) 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) -> 27.39/7.72 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) -> 27.39/7.72 qsort#(cons(x,xs)) -> split#(x,xs) 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) -> 27.39/7.72 app#(cons(x,xs),ys) -> app#(xs,ys) 27.39/7.72 ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) -> 27.39/7.72 le#(s(x),s(y)) -> le#(x,y) 27.39/7.72 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 27.39/7.72 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 27.39/7.72 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 27.39/7.72 qsort#(cons(x,xs)) -> split#(x,xs) -> 27.39/7.72 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 27.39/7.72 qsort#(cons(x,xs)) -> split#(x,xs) -> 27.39/7.72 split#(x,cons(y,ys)) -> split#(x,ys) 27.39/7.72 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) -> 27.39/7.72 ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) 27.39/7.72 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) -> 27.39/7.72 ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) 27.39/7.72 split#(x,cons(y,ys)) -> split#(x,ys) -> 27.39/7.72 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 27.39/7.72 split#(x,cons(y,ys)) -> split#(x,ys) -> 27.39/7.72 split#(x,cons(y,ys)) -> split#(x,ys) 27.39/7.72 app#(cons(x,xs),ys) -> app#(xs,ys) -> 27.39/7.72 app#(cons(x,xs),ys) -> app#(xs,ys) 27.39/7.72 le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) 27.39/7.72 SCC Processor: 27.39/7.72 #sccs: 4 27.39/7.72 #rules: 6 27.39/7.72 #arcs: 17/121 27.39/7.72 DPs: 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 27.39/7.72 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 27.39/7.72 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 27.39/7.72 TRS: 27.39/7.72 le(0(),x) -> true() 27.39/7.72 le(s(x),0()) -> false() 27.39/7.72 le(s(x),s(y)) -> le(x,y) 27.39/7.72 app(nil(),x) -> x 27.39/7.72 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 27.39/7.72 split(x,nil()) -> pair(nil(),nil()) 27.39/7.72 qsort(nil()) -> nil() 27.39/7.72 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.39/7.72 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.39/7.72 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.39/7.72 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.39/7.72 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 27.39/7.73 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 27.39/7.73 Usable Rule Processor: 27.39/7.73 DPs: 27.39/7.73 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 27.39/7.73 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 27.39/7.73 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 27.39/7.73 TRS: 27.39/7.73 split(x,nil()) -> pair(nil(),nil()) 27.39/7.73 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.39/7.73 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.39/7.73 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.39/7.73 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.39/7.73 le(0(),x) -> true() 27.39/7.73 le(s(x),0()) -> false() 27.39/7.73 le(s(x),s(y)) -> le(x,y) 27.39/7.73 KBO Processor: 27.39/7.73 argument filtering: 27.39/7.73 pi(0) = [] 27.39/7.73 pi(le) = [] 27.39/7.73 pi(true) = [] 27.39/7.73 pi(s) = [] 27.39/7.73 pi(false) = [] 27.39/7.73 pi(nil) = [] 27.39/7.73 pi(cons) = [0,1] 27.39/7.73 pi(split) = [0,1] 27.39/7.73 pi(pair) = [0,1] 27.39/7.73 pi(?2) = [0,3,4,5] 27.39/7.73 pi(?3) = [0,2] 27.39/7.73 pi(qsort#) = [0] 27.39/7.73 pi(?1#) = 0 27.39/7.73 usable rules: 27.39/7.73 split(x,nil()) -> pair(nil(),nil()) 27.70/7.83 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.70/7.83 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.70/7.83 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.70/7.83 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.70/7.83 le(0(),x) -> true() 27.70/7.83 le(s(x),0()) -> false() 27.70/7.83 le(s(x),s(y)) -> le(x,y) 27.70/7.83 weight function: 27.70/7.83 w0 = 1 27.70/7.83 w(qsort#) = w(pair) = w(split) = w(nil) = w(false) = w(s) = w( 27.70/7.83 true) = w(le) = w(0) = 1 27.70/7.83 w(?1#) = w(?3) = w(?2) = w(cons) = 0 27.70/7.83 precedence: 27.70/7.83 qsort# ~ cons ~ nil ~ s ~ 0 > split > ?3 > ?2 ~ le > ?1# ~ pair ~ false ~ true 27.70/7.83 problem: 27.70/7.83 DPs: 27.70/7.83 27.70/7.83 TRS: 27.70/7.83 split(x,nil()) -> pair(nil(),nil()) 27.70/7.83 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.70/7.83 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.70/7.83 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.70/7.83 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.70/7.83 le(0(),x) -> true() 27.70/7.83 le(s(x),0()) -> false() 27.70/7.83 le(s(x),s(y)) -> le(x,y) 27.70/7.83 Qed 27.70/7.83 27.70/7.83 DPs: 27.70/7.83 app#(cons(x,xs),ys) -> app#(xs,ys) 27.70/7.83 TRS: 27.70/7.83 le(0(),x) -> true() 27.70/7.83 le(s(x),0()) -> false() 27.70/7.83 le(s(x),s(y)) -> le(x,y) 27.70/7.83 app(nil(),x) -> x 27.70/7.83 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 27.70/7.83 split(x,nil()) -> pair(nil(),nil()) 27.70/7.83 qsort(nil()) -> nil() 27.70/7.83 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.70/7.83 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.70/7.83 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.70/7.83 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.70/7.83 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 27.70/7.83 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 27.70/7.83 Subterm Criterion Processor: 27.70/7.83 simple projection: 27.70/7.83 pi(app#) = 0 27.70/7.83 problem: 27.70/7.83 DPs: 27.70/7.83 27.70/7.83 TRS: 27.70/7.83 le(0(),x) -> true() 27.70/7.83 le(s(x),0()) -> false() 27.70/7.83 le(s(x),s(y)) -> le(x,y) 27.70/7.83 app(nil(),x) -> x 27.70/7.83 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 27.70/7.83 split(x,nil()) -> pair(nil(),nil()) 27.70/7.83 qsort(nil()) -> nil() 27.70/7.83 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.70/7.83 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.70/7.83 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.70/7.83 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.70/7.83 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 27.70/7.83 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 27.70/7.83 Qed 27.70/7.83 27.70/7.83 DPs: 27.70/7.83 split#(x,cons(y,ys)) -> split#(x,ys) 27.70/7.83 TRS: 27.70/7.83 le(0(),x) -> true() 27.70/7.83 le(s(x),0()) -> false() 27.70/7.83 le(s(x),s(y)) -> le(x,y) 27.70/7.83 app(nil(),x) -> x 27.70/7.83 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 27.70/7.83 split(x,nil()) -> pair(nil(),nil()) 27.70/7.83 qsort(nil()) -> nil() 27.70/7.83 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.70/7.83 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.70/7.83 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.70/7.83 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.70/7.83 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 27.70/7.83 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 27.70/7.83 Subterm Criterion Processor: 27.70/7.83 simple projection: 27.70/7.83 pi(split#) = 1 27.70/7.83 problem: 27.70/7.83 DPs: 27.70/7.83 27.70/7.83 TRS: 27.70/7.83 le(0(),x) -> true() 27.70/7.83 le(s(x),0()) -> false() 27.70/7.83 le(s(x),s(y)) -> le(x,y) 27.70/7.83 app(nil(),x) -> x 27.70/7.83 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 27.70/7.83 split(x,nil()) -> pair(nil(),nil()) 27.70/7.83 qsort(nil()) -> nil() 27.70/7.83 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 27.70/7.83 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 27.70/7.83 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 27.70/7.83 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 27.70/7.83 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 27.70/7.83 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 27.70/7.83 Qed 27.70/7.83 27.70/7.83 DPs: 27.70/7.83 le#(s(x),s(y)) -> le#(x,y) 27.70/7.83 TRS: 27.70/7.83 le(0(),x) -> true() 28.01/8.00 le(s(x),0()) -> false() 28.01/8.00 le(s(x),s(y)) -> le(x,y) 28.01/8.00 app(nil(),x) -> x 28.01/8.00 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 28.01/8.00 split(x,nil()) -> pair(nil(),nil()) 28.01/8.00 qsort(nil()) -> nil() 28.01/8.00 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 28.01/8.00 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 28.01/8.00 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 28.01/8.00 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 28.01/8.00 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 28.01/8.00 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 28.01/8.00 Subterm Criterion Processor: 28.01/8.00 simple projection: 28.01/8.00 pi(le#) = 0 28.01/8.00 problem: 28.01/8.00 DPs: 28.01/8.00 28.01/8.00 TRS: 28.01/8.00 le(0(),x) -> true() 28.01/8.00 le(s(x),0()) -> false() 28.01/8.00 le(s(x),s(y)) -> le(x,y) 28.01/8.00 app(nil(),x) -> x 28.01/8.00 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 28.01/8.00 split(x,nil()) -> pair(nil(),nil()) 28.01/8.00 qsort(nil()) -> nil() 28.01/8.00 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 28.01/8.00 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 28.01/8.00 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 28.01/8.00 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 28.01/8.00 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 28.01/8.00 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 28.01/8.00 Qed 28.01/8.00 30.06/8.48 EOF