42.77/11.80 YES 42.77/11.80 42.77/11.80 Problem: 42.77/11.80 le(0(), x) -> true() 42.77/11.80 le(s(x), 0()) -> false() 42.77/11.80 le(s(x), s(y)) -> le(x, y) 42.77/11.80 app(nil(), x) -> x 42.77/11.80 app(cons(x, xs), ys) -> cons(x, app(xs, ys)) 42.77/11.80 split(x, nil()) -> pair(nil(), nil()) 42.77/11.80 qsort(nil()) -> nil() 42.77/11.80 split(x, cons(y, ys)) -> pair(xs, cons(y, zs)) <= split(x, ys) = pair(xs, zs), le(x, y) = true() 42.77/11.80 split(x, cons(y, ys)) -> pair(cons(y, xs), zs) <= split(x, ys) = pair(xs, zs), le(x, y) = false() 42.77/11.80 qsort(cons(x, xs)) -> app(qsort(ys), cons(x, qsort(zs))) <= split(x, xs) = pair(ys, zs) 42.77/11.80 42.77/11.80 Proof: 42.77/11.80 This system is confluent. 42.77/11.80 By \cite{SMI95}, Corollary 4.7 or 5.3. 42.77/11.80 This system is oriented. 42.77/11.80 This system is of type 3 or smaller. 42.77/11.80 This system is right-stable. 42.77/11.80 This system is properly oriented. 42.77/11.80 This is an overlay system. 42.77/11.80 This system is left-linear. 42.77/11.80 All 2 critical pairs are trivial or infeasible. 42.77/11.80 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(): 42.77/11.80 This critical pair is infeasible. 42.77/11.80 This critical pair is conditional. 42.77/11.80 This critical pair has some non-trivial conditions. 42.77/11.80 This system is of type 3 or smaller. 42.77/11.80 This system is deterministic. 42.77/11.80 This system is quasi-decreasing. 42.77/11.80 By \cite{O02}, p. 214, Proposition 7.2.50. 42.77/11.80 This system is of type 3 or smaller. 42.77/11.80 This system is deterministic. 42.77/11.80 System R transformed to optimized U(R). 42.77/11.80 This system is terminating. 42.77/11.80 Call external tool: 42.77/11.80 ./ttt2.sh 42.77/11.80 Input: 42.77/11.80 le(0(), x) -> true() 42.77/11.80 le(s(x), 0()) -> false() 42.77/11.80 le(s(x), s(y)) -> le(x, y) 42.77/11.80 app(nil(), x) -> x 42.77/11.80 app(cons(x, xs), ys) -> cons(x, app(xs, ys)) 42.77/11.80 split(x, nil()) -> pair(nil(), nil()) 42.77/11.80 qsort(nil()) -> nil() 42.77/11.80 ?2(true(), x, ys, y, zs, xs) -> pair(xs, cons(y, zs)) 42.77/11.80 ?3(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs) 42.77/11.80 split(x, cons(y, ys)) -> ?3(split(x, ys), x, y, ys) 42.77/11.80 ?2(false(), x, ys, y, zs, xs) -> pair(cons(y, xs), zs) 42.77/11.80 ?1(pair(ys, zs), x, xs) -> app(qsort(ys), cons(x, qsort(zs))) 42.77/11.80 qsort(cons(x, xs)) -> ?1(split(x, xs), x, xs) 42.77/11.80 42.77/11.80 DP Processor: 42.77/11.80 DPs: 42.77/11.80 le#(s(x),s(y)) -> le#(x,y) 42.77/11.80 app#(cons(x,xs),ys) -> app#(xs,ys) 42.77/11.80 ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) 42.77/11.80 ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) 42.77/11.80 split#(x,cons(y,ys)) -> split#(x,ys) 42.77/11.80 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 42.77/11.80 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 42.77/11.80 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 42.77/11.80 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 42.77/11.80 qsort#(cons(x,xs)) -> split#(x,xs) 42.77/11.80 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 42.77/11.80 TRS: 42.77/11.80 le(0(),x) -> true() 42.77/11.80 le(s(x),0()) -> false() 42.77/11.80 le(s(x),s(y)) -> le(x,y) 42.77/11.80 app(nil(),x) -> x 42.77/11.80 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 42.77/11.80 split(x,nil()) -> pair(nil(),nil()) 42.77/11.80 qsort(nil()) -> nil() 42.77/11.80 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 42.77/11.80 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 42.77/11.80 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 42.77/11.80 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 42.77/11.80 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 42.77/11.80 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 42.77/11.80 TDG Processor: 42.77/11.80 DPs: 42.77/11.80 le#(s(x),s(y)) -> le#(x,y) 42.77/11.80 app#(cons(x,xs),ys) -> app#(xs,ys) 42.77/11.80 ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) 42.97/11.89 ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) 43.40/12.03 split#(x,cons(y,ys)) -> split#(x,ys) 43.40/12.03 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 43.40/12.03 qsort#(cons(x,xs)) -> split#(x,xs) 43.40/12.03 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 43.40/12.03 TRS: 43.40/12.03 le(0(),x) -> true() 43.40/12.03 le(s(x),0()) -> false() 43.40/12.03 le(s(x),s(y)) -> le(x,y) 43.40/12.03 app(nil(),x) -> x 43.40/12.03 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 43.40/12.03 split(x,nil()) -> pair(nil(),nil()) 43.40/12.03 qsort(nil()) -> nil() 43.40/12.03 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 43.40/12.03 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 43.40/12.03 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 43.40/12.03 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 43.40/12.03 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 43.40/12.03 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 43.40/12.03 graph: 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) -> 43.40/12.03 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) -> 43.40/12.03 qsort#(cons(x,xs)) -> split#(x,xs) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) -> 43.40/12.03 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) -> 43.40/12.03 qsort#(cons(x,xs)) -> split#(x,xs) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) -> 43.40/12.03 app#(cons(x,xs),ys) -> app#(xs,ys) 43.40/12.03 ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) -> 43.40/12.03 le#(s(x),s(y)) -> le#(x,y) 43.40/12.03 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 43.40/12.03 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 43.40/12.03 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 43.40/12.03 qsort#(cons(x,xs)) -> split#(x,xs) -> 43.40/12.03 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 43.40/12.03 qsort#(cons(x,xs)) -> split#(x,xs) -> 43.40/12.03 split#(x,cons(y,ys)) -> split#(x,ys) 43.40/12.03 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) -> 43.40/12.03 ?3#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs) 43.40/12.03 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) -> 43.40/12.03 ?3#(pair(xs,zs),x,y,ys) -> le#(x,y) 43.40/12.03 split#(x,cons(y,ys)) -> split#(x,ys) -> 43.40/12.03 split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) 43.40/12.03 split#(x,cons(y,ys)) -> split#(x,ys) -> 43.40/12.03 split#(x,cons(y,ys)) -> split#(x,ys) 43.40/12.03 app#(cons(x,xs),ys) -> app#(xs,ys) -> 43.40/12.03 app#(cons(x,xs),ys) -> app#(xs,ys) 43.40/12.03 le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) 43.40/12.03 SCC Processor: 43.40/12.03 #sccs: 4 43.40/12.03 #rules: 6 43.40/12.03 #arcs: 17/121 43.40/12.03 DPs: 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 43.40/12.03 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 43.40/12.03 TRS: 43.40/12.03 le(0(),x) -> true() 43.40/12.03 le(s(x),0()) -> false() 43.40/12.03 le(s(x),s(y)) -> le(x,y) 43.40/12.03 app(nil(),x) -> x 43.40/12.03 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 43.40/12.03 split(x,nil()) -> pair(nil(),nil()) 43.40/12.03 qsort(nil()) -> nil() 43.40/12.03 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 43.40/12.03 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 43.40/12.03 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 43.40/12.03 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 43.40/12.03 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 43.40/12.03 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 43.40/12.03 Usable Rule Processor: 43.40/12.03 DPs: 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 43.40/12.03 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 43.40/12.03 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 43.40/12.03 TRS: 43.40/12.03 split(x,nil()) -> pair(nil(),nil()) 43.40/12.03 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 43.40/12.03 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 43.40/12.03 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 43.40/12.03 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 43.40/12.03 le(0(),x) -> true() 43.40/12.03 le(s(x),0()) -> false() 43.40/12.03 le(s(x),s(y)) -> le(x,y) 43.40/12.03 KBO Processor: 43.40/12.03 argument filtering: 43.40/12.03 pi(0) = [] 43.40/12.03 pi(le) = [] 43.40/12.03 pi(true) = [] 43.40/12.03 pi(s) = [] 43.40/12.03 pi(false) = [] 43.40/12.03 pi(nil) = [] 43.40/12.03 pi(cons) = [0,1] 43.40/12.03 pi(split) = [0,1] 43.40/12.03 pi(pair) = [0,1] 43.40/12.03 pi(?2) = [0,3,4,5] 43.40/12.03 pi(?3) = [0,2] 43.40/12.03 pi(qsort#) = [0] 43.40/12.03 pi(?1#) = 0 43.40/12.03 usable rules: 43.40/12.03 split(x,nil()) -> pair(nil(),nil()) 43.40/12.03 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 43.40/12.03 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 43.40/12.03 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 43.40/12.03 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 43.40/12.03 le(0(),x) -> true() 43.40/12.03 le(s(x),0()) -> false() 43.40/12.03 le(s(x),s(y)) -> le(x,y) 43.40/12.03 weight function: 43.40/12.03 w0 = 1 43.40/12.03 w(qsort#) = w(pair) = w(split) = w(nil) = w(false) = w(s) = w( 43.40/12.03 true) = w(le) = w(0) = 1 43.40/12.03 w(?1#) = w(?3) = w(?2) = w(cons) = 0 44.10/12.15 precedence: 44.10/12.15 qsort# ~ cons ~ nil ~ s ~ 0 > split > ?3 > ?2 ~ le > ?1# ~ pair ~ false ~ true 44.10/12.15 problem: 44.10/12.15 DPs: 44.10/12.15 44.10/12.15 TRS: 44.10/12.15 split(x,nil()) -> pair(nil(),nil()) 44.10/12.15 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 44.10/12.15 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 44.10/12.15 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.15 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.15 le(0(),x) -> true() 44.10/12.15 le(s(x),0()) -> false() 44.10/12.15 le(s(x),s(y)) -> le(x,y) 44.10/12.15 Qed 44.10/12.15 44.10/12.15 DPs: 44.10/12.15 app#(cons(x,xs),ys) -> app#(xs,ys) 44.10/12.15 TRS: 44.10/12.15 le(0(),x) -> true() 44.10/12.15 le(s(x),0()) -> false() 44.10/12.15 le(s(x),s(y)) -> le(x,y) 44.10/12.15 app(nil(),x) -> x 44.10/12.15 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 44.10/12.15 split(x,nil()) -> pair(nil(),nil()) 44.10/12.15 qsort(nil()) -> nil() 44.10/12.15 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.15 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 44.10/12.15 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 44.10/12.15 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.15 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 44.10/12.15 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 44.10/12.15 Subterm Criterion Processor: 44.10/12.15 simple projection: 44.10/12.15 pi(app#) = 0 44.10/12.15 problem: 44.10/12.15 DPs: 44.10/12.15 44.10/12.15 TRS: 44.10/12.15 le(0(),x) -> true() 44.10/12.15 le(s(x),0()) -> false() 44.10/12.15 le(s(x),s(y)) -> le(x,y) 44.10/12.15 app(nil(),x) -> x 44.10/12.15 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 44.10/12.15 split(x,nil()) -> pair(nil(),nil()) 44.10/12.15 qsort(nil()) -> nil() 44.10/12.15 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.15 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 44.10/12.15 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 44.10/12.15 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.15 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 44.10/12.15 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 44.10/12.15 Qed 44.10/12.15 44.10/12.15 DPs: 44.10/12.15 split#(x,cons(y,ys)) -> split#(x,ys) 44.10/12.15 TRS: 44.10/12.15 le(0(),x) -> true() 44.10/12.15 le(s(x),0()) -> false() 44.10/12.15 le(s(x),s(y)) -> le(x,y) 44.10/12.15 app(nil(),x) -> x 44.10/12.15 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 44.10/12.15 split(x,nil()) -> pair(nil(),nil()) 44.10/12.15 qsort(nil()) -> nil() 44.10/12.15 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.15 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 44.10/12.15 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 44.10/12.15 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.15 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 44.10/12.15 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 44.10/12.15 Subterm Criterion Processor: 44.10/12.15 simple projection: 44.10/12.15 pi(split#) = 1 44.10/12.15 problem: 44.10/12.15 DPs: 44.10/12.15 44.10/12.15 TRS: 44.10/12.15 le(0(),x) -> true() 44.10/12.15 le(s(x),0()) -> false() 44.10/12.15 le(s(x),s(y)) -> le(x,y) 44.10/12.15 app(nil(),x) -> x 44.10/12.15 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 44.10/12.15 split(x,nil()) -> pair(nil(),nil()) 44.10/12.15 qsort(nil()) -> nil() 44.10/12.15 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.15 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 44.10/12.15 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 44.10/12.15 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.15 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 44.10/12.15 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 44.10/12.15 Qed 44.10/12.15 44.10/12.15 DPs: 44.10/12.15 le#(s(x),s(y)) -> le#(x,y) 44.10/12.15 TRS: 44.10/12.15 le(0(),x) -> true() 44.10/12.15 le(s(x),0()) -> false() 44.10/12.15 le(s(x),s(y)) -> le(x,y) 44.10/12.15 app(nil(),x) -> x 44.10/12.15 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 44.10/12.15 split(x,nil()) -> pair(nil(),nil()) 44.10/12.15 qsort(nil()) -> nil() 44.10/12.15 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.15 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 44.10/12.15 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 44.10/12.15 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.15 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 44.10/12.15 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 44.10/12.15 Subterm Criterion Processor: 44.10/12.15 simple projection: 44.10/12.22 pi(le#) = 0 44.10/12.22 problem: 44.10/12.22 DPs: 44.10/12.22 44.10/12.22 TRS: 44.10/12.22 le(0(),x) -> true() 44.10/12.22 le(s(x),0()) -> false() 44.10/12.22 le(s(x),s(y)) -> le(x,y) 44.10/12.22 app(nil(),x) -> x 44.10/12.22 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 44.10/12.22 split(x,nil()) -> pair(nil(),nil()) 44.10/12.22 qsort(nil()) -> nil() 44.10/12.22 ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.22 ?3(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys) 44.10/12.22 ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.22 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 44.10/12.22 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 44.10/12.22 Qed 44.10/12.22 This critical pair is unfeasible. 44.10/12.22 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(): 44.10/12.22 This critical pair is infeasible. 44.10/12.22 This critical pair is conditional. 44.10/12.22 This critical pair has some non-trivial conditions. 44.10/12.22 This system is of type 3 or smaller. 44.10/12.22 This system is deterministic. 44.10/12.22 This system is quasi-decreasing. 44.10/12.22 By \cite{O02}, p. 214, Proposition 7.2.50. 44.10/12.22 This system is of type 3 or smaller. 44.10/12.22 This system is deterministic. 44.10/12.22 System R transformed to U(R). 44.10/12.22 This system is terminating. 44.10/12.22 Call external tool: 44.10/12.22 ./ttt2.sh 44.10/12.22 Input: 44.10/12.22 le(0(), x) -> true() 44.10/12.22 le(s(x), 0()) -> false() 44.10/12.22 le(s(x), s(y)) -> le(x, y) 44.10/12.22 app(nil(), x) -> x 44.10/12.22 app(cons(x, xs), ys) -> cons(x, app(xs, ys)) 44.10/12.22 split(x, nil()) -> pair(nil(), nil()) 44.10/12.22 qsort(nil()) -> nil() 44.10/12.22 ?5(true(), x, ys, y, zs, xs) -> pair(xs, cons(y, zs)) 44.10/12.22 ?4(pair(xs, zs), x, y, ys) -> ?5(le(x, y), x, ys, y, zs, xs) 44.10/12.22 split(x, cons(y, ys)) -> ?4(split(x, ys), x, y, ys) 44.10/12.22 ?3(false(), x, ys, y, zs, xs) -> pair(cons(y, xs), zs) 44.10/12.22 ?2(pair(xs, zs), x, y, ys) -> ?3(le(x, y), x, ys, y, zs, xs) 44.10/12.22 split(x, cons(y, ys)) -> ?2(split(x, ys), x, y, ys) 44.10/12.22 ?1(pair(ys, zs), x, xs) -> app(qsort(ys), cons(x, qsort(zs))) 44.10/12.22 qsort(cons(x, xs)) -> ?1(split(x, xs), x, xs) 44.10/12.22 44.10/12.22 DP Processor: 44.10/12.22 DPs: 44.10/12.22 le#(s(x),s(y)) -> le#(x,y) 44.10/12.22 app#(cons(x,xs),ys) -> app#(xs,ys) 44.10/12.22 ?4#(pair(xs,zs),x,y,ys) -> le#(x,y) 44.10/12.22 ?4#(pair(xs,zs),x,y,ys) -> ?5#(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split#(x,cons(y,ys)) -> split#(x,ys) 44.10/12.22 split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys) 44.10/12.22 ?2#(pair(xs,zs),x,y,ys) -> le#(x,y) 44.10/12.22 ?2#(pair(xs,zs),x,y,ys) -> ?3#(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) 44.10/12.22 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 44.10/12.22 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 44.10/12.22 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 44.10/12.22 qsort#(cons(x,xs)) -> split#(x,xs) 44.10/12.22 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 44.10/12.22 TRS: 44.10/12.22 le(0(),x) -> true() 44.10/12.22 le(s(x),0()) -> false() 44.10/12.22 le(s(x),s(y)) -> le(x,y) 44.10/12.22 app(nil(),x) -> x 44.10/12.22 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 44.10/12.22 split(x,nil()) -> pair(nil(),nil()) 44.10/12.22 qsort(nil()) -> nil() 44.10/12.22 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.22 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 44.10/12.22 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.22 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 44.10/12.22 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 44.10/12.22 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 44.10/12.22 TDG Processor: 44.10/12.22 DPs: 44.10/12.22 le#(s(x),s(y)) -> le#(x,y) 44.10/12.22 app#(cons(x,xs),ys) -> app#(xs,ys) 44.10/12.22 ?4#(pair(xs,zs),x,y,ys) -> le#(x,y) 44.10/12.22 ?4#(pair(xs,zs),x,y,ys) -> ?5#(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split#(x,cons(y,ys)) -> split#(x,ys) 44.10/12.22 split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys) 44.10/12.22 ?2#(pair(xs,zs),x,y,ys) -> le#(x,y) 44.10/12.22 ?2#(pair(xs,zs),x,y,ys) -> ?3#(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) 44.10/12.22 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 44.10/12.22 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 44.10/12.22 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 44.10/12.22 qsort#(cons(x,xs)) -> split#(x,xs) 44.10/12.22 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 44.10/12.22 TRS: 44.10/12.22 le(0(),x) -> true() 44.10/12.22 le(s(x),0()) -> false() 44.10/12.22 le(s(x),s(y)) -> le(x,y) 44.10/12.22 app(nil(),x) -> x 44.10/12.22 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 44.10/12.22 split(x,nil()) -> pair(nil(),nil()) 44.10/12.22 qsort(nil()) -> nil() 44.10/12.22 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 44.10/12.22 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 44.10/12.22 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 44.10/12.22 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 44.10/12.22 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 44.10/12.22 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 44.10/12.22 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 44.10/12.22 graph: 44.10/12.22 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) -> 44.10/12.22 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) -> 45.22/12.29 qsort#(cons(x,xs)) -> split#(x,xs) 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) -> 45.22/12.29 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) -> 45.22/12.29 qsort#(cons(x,xs)) -> split#(x,xs) 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) -> 45.22/12.29 app#(cons(x,xs),ys) -> app#(xs,ys) 45.22/12.29 ?2#(pair(xs,zs),x,y,ys) -> le#(x,y) -> 45.22/12.29 le#(s(x),s(y)) -> le#(x,y) 45.22/12.29 ?4#(pair(xs,zs),x,y,ys) -> le#(x,y) -> 45.22/12.29 le#(s(x),s(y)) -> le#(x,y) 45.22/12.29 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) 45.22/12.29 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 45.22/12.29 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) -> 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 45.22/12.29 qsort#(cons(x,xs)) -> split#(x,xs) -> 45.22/12.29 split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) 45.22/12.29 qsort#(cons(x,xs)) -> split#(x,xs) -> 45.22/12.29 split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys) 45.22/12.29 qsort#(cons(x,xs)) -> split#(x,xs) -> 45.22/12.29 split#(x,cons(y,ys)) -> split#(x,ys) 45.22/12.29 split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) -> 45.22/12.29 ?2#(pair(xs,zs),x,y,ys) -> ?3#(le(x,y),x,ys,y,zs,xs) 45.22/12.29 split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) -> 45.22/12.29 ?2#(pair(xs,zs),x,y,ys) -> le#(x,y) 45.22/12.29 split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys) -> 45.22/12.29 ?4#(pair(xs,zs),x,y,ys) -> ?5#(le(x,y),x,ys,y,zs,xs) 45.22/12.29 split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys) -> 45.22/12.29 ?4#(pair(xs,zs),x,y,ys) -> le#(x,y) 45.22/12.29 split#(x,cons(y,ys)) -> split#(x,ys) -> 45.22/12.29 split#(x,cons(y,ys)) -> ?2#(split(x,ys),x,y,ys) 45.22/12.29 split#(x,cons(y,ys)) -> split#(x,ys) -> 45.22/12.29 split#(x,cons(y,ys)) -> ?4#(split(x,ys),x,y,ys) 45.22/12.29 split#(x,cons(y,ys)) -> split#(x,ys) -> 45.22/12.29 split#(x,cons(y,ys)) -> split#(x,ys) 45.22/12.29 app#(cons(x,xs),ys) -> app#(xs,ys) -> 45.22/12.29 app#(cons(x,xs),ys) -> app#(xs,ys) 45.22/12.29 le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y) 45.22/12.29 SCC Processor: 45.22/12.29 #sccs: 4 45.22/12.29 #rules: 6 45.22/12.29 #arcs: 22/196 45.22/12.29 DPs: 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 45.22/12.29 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 45.22/12.29 TRS: 45.22/12.29 le(0(),x) -> true() 45.22/12.29 le(s(x),0()) -> false() 45.22/12.29 le(s(x),s(y)) -> le(x,y) 45.22/12.29 app(nil(),x) -> x 45.22/12.29 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 45.22/12.29 split(x,nil()) -> pair(nil(),nil()) 45.22/12.29 qsort(nil()) -> nil() 45.22/12.29 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 45.22/12.29 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 45.22/12.29 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 45.22/12.29 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 45.22/12.29 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 45.22/12.29 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 45.22/12.29 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 45.22/12.29 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 45.22/12.29 Usable Rule Processor: 45.22/12.29 DPs: 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(zs) 45.22/12.29 qsort#(cons(x,xs)) -> ?1#(split(x,xs),x,xs) 45.22/12.29 ?1#(pair(ys,zs),x,xs) -> qsort#(ys) 45.22/12.29 TRS: 45.22/12.29 split(x,nil()) -> pair(nil(),nil()) 45.22/12.29 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 45.22/12.29 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 45.22/12.29 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 45.22/12.29 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 45.22/12.29 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 45.22/12.29 le(0(),x) -> true() 45.22/12.29 le(s(x),0()) -> false() 45.22/12.29 le(s(x),s(y)) -> le(x,y) 45.22/12.29 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 45.74/12.36 KBO Processor: 45.74/12.36 argument filtering: 45.74/12.36 pi(0) = [] 45.74/12.36 pi(le) = [] 45.74/12.36 pi(true) = [] 45.74/12.36 pi(s) = 0 45.74/12.36 pi(false) = [] 45.74/12.36 pi(nil) = [] 45.74/12.36 pi(cons) = [0,1] 45.74/12.36 pi(split) = [0,1] 45.74/12.36 pi(pair) = [0,1] 45.74/12.36 pi(?5) = [0,3,4,5] 45.74/12.36 pi(?4) = [0,2] 45.74/12.36 pi(?3) = [0,3,4,5] 45.74/12.36 pi(?2) = [0,2] 45.74/12.36 pi(qsort#) = 0 45.74/12.36 pi(?1#) = 0 45.74/12.36 usable rules: 45.74/12.36 split(x,nil()) -> pair(nil(),nil()) 45.74/12.36 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 45.74/12.36 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 45.74/12.36 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 45.74/12.36 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 45.74/12.36 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 45.74/12.36 le(0(),x) -> true() 45.74/12.36 le(s(x),0()) -> false() 45.74/12.36 le(s(x),s(y)) -> le(x,y) 45.74/12.36 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 45.74/12.36 weight function: 45.74/12.36 w0 = 1 45.74/12.36 w(qsort#) = w(?2) = w(?3) = w(?4) = w(?5) = w(pair) = w(split) = w( 45.74/12.36 cons) = w(nil) = w(false) = w(s) = w(true) = w(le) = w(0) = 1 45.74/12.36 w(?1#) = 0 45.74/12.36 precedence: 45.74/12.36 cons ~ nil ~ 0 > split > ?2 ~ ?4 ~ le > ?3 ~ ?5 > ?1# ~ qsort# ~ pair ~ false ~ s ~ true 45.74/12.36 problem: 45.74/12.36 DPs: 45.74/12.36 45.74/12.36 TRS: 45.74/12.36 split(x,nil()) -> pair(nil(),nil()) 45.74/12.36 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 45.74/12.36 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 45.74/12.36 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 45.74/12.36 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 45.74/12.36 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 45.74/12.36 le(0(),x) -> true() 45.74/12.36 le(s(x),0()) -> false() 45.74/12.36 le(s(x),s(y)) -> le(x,y) 45.74/12.36 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 45.74/12.36 Qed 46.41/12.52 46.41/12.52 DPs: 46.41/12.52 app#(cons(x,xs),ys) -> app#(xs,ys) 46.41/12.52 TRS: 46.41/12.52 le(0(),x) -> true() 46.41/12.52 le(s(x),0()) -> false() 46.41/12.52 le(s(x),s(y)) -> le(x,y) 46.41/12.52 app(nil(),x) -> x 46.41/12.52 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 46.41/12.52 split(x,nil()) -> pair(nil(),nil()) 46.41/12.52 qsort(nil()) -> nil() 46.41/12.52 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 46.41/12.52 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 46.41/12.52 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 46.41/12.52 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 46.41/12.52 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 46.41/12.52 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 46.41/12.52 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 46.41/12.52 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 46.41/12.52 Subterm Criterion Processor: 46.41/12.52 simple projection: 46.41/12.52 pi(app#) = 0 46.41/12.52 problem: 46.41/12.52 DPs: 46.41/12.52 46.41/12.52 TRS: 46.41/12.52 le(0(),x) -> true() 46.41/12.52 le(s(x),0()) -> false() 46.41/12.52 le(s(x),s(y)) -> le(x,y) 46.41/12.52 app(nil(),x) -> x 46.41/12.52 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 46.41/12.52 split(x,nil()) -> pair(nil(),nil()) 46.41/12.52 qsort(nil()) -> nil() 46.41/12.52 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 46.41/12.52 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 46.41/12.52 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 46.41/12.52 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 46.41/12.52 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 46.41/12.52 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 46.41/12.52 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 46.41/12.52 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 46.41/12.52 Qed 46.41/12.52 46.41/12.52 DPs: 46.41/12.52 split#(x,cons(y,ys)) -> split#(x,ys) 46.41/12.52 TRS: 46.41/12.52 le(0(),x) -> true() 46.41/12.52 le(s(x),0()) -> false() 46.41/12.52 le(s(x),s(y)) -> le(x,y) 46.41/12.52 app(nil(),x) -> x 46.41/12.52 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 46.41/12.52 split(x,nil()) -> pair(nil(),nil()) 46.41/12.52 qsort(nil()) -> nil() 46.41/12.52 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 46.41/12.52 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 46.41/12.52 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 46.41/12.52 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 46.41/12.52 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 46.41/12.52 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 46.41/12.52 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 46.41/12.52 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 46.41/12.52 Subterm Criterion Processor: 46.41/12.52 simple projection: 46.41/12.52 pi(split#) = 1 46.41/12.52 problem: 46.41/12.52 DPs: 46.41/12.52 46.41/12.52 TRS: 46.41/12.52 le(0(),x) -> true() 46.41/12.52 le(s(x),0()) -> false() 46.41/12.52 le(s(x),s(y)) -> le(x,y) 46.41/12.52 app(nil(),x) -> x 46.41/12.52 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 46.41/12.52 split(x,nil()) -> pair(nil(),nil()) 46.41/12.52 qsort(nil()) -> nil() 46.41/12.52 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 46.41/12.52 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 46.41/12.52 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 46.41/12.52 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 46.41/12.52 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 46.41/12.52 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 46.41/12.52 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 46.41/12.52 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 46.41/12.52 Qed 46.41/12.52 46.41/12.52 DPs: 46.41/12.52 le#(s(x),s(y)) -> le#(x,y) 46.41/12.52 TRS: 46.41/12.52 le(0(),x) -> true() 46.41/12.52 le(s(x),0()) -> false() 46.41/12.52 le(s(x),s(y)) -> le(x,y) 46.41/12.52 app(nil(),x) -> x 46.41/12.52 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 46.41/12.52 split(x,nil()) -> pair(nil(),nil()) 46.41/12.52 qsort(nil()) -> nil() 46.41/12.56 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 46.41/12.56 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 46.41/12.56 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 46.41/12.56 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 46.41/12.56 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 46.41/12.56 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 46.41/12.56 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 46.41/12.56 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 46.41/12.56 Subterm Criterion Processor: 46.41/12.56 simple projection: 46.41/12.56 pi(le#) = 0 46.41/12.56 problem: 46.41/12.56 DPs: 46.41/12.56 46.41/12.56 TRS: 46.41/12.56 le(0(),x) -> true() 46.41/12.56 le(s(x),0()) -> false() 46.41/12.56 le(s(x),s(y)) -> le(x,y) 46.41/12.56 app(nil(),x) -> x 46.41/12.56 app(cons(x,xs),ys) -> cons(x,app(xs,ys)) 46.41/12.56 split(x,nil()) -> pair(nil(),nil()) 46.41/12.56 qsort(nil()) -> nil() 46.41/12.56 ?5(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs)) 46.41/12.56 ?4(pair(xs,zs),x,y,ys) -> ?5(le(x,y),x,ys,y,zs,xs) 46.41/12.56 split(x,cons(y,ys)) -> ?4(split(x,ys),x,y,ys) 46.41/12.56 ?3(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs) 46.41/12.56 ?2(pair(xs,zs),x,y,ys) -> ?3(le(x,y),x,ys,y,zs,xs) 46.41/12.56 split(x,cons(y,ys)) -> ?2(split(x,ys),x,y,ys) 46.41/12.56 ?1(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs))) 46.41/12.56 qsort(cons(x,xs)) -> ?1(split(x,xs),x,xs) 46.41/12.56 Qed 46.41/12.56 This critical pair is unfeasible. 46.41/12.56 47.98/12.98 EOF