29.55/8.17	YES
29.55/8.17	
29.55/8.17	Proof:
29.55/8.18	This system is confluent.
29.55/8.18	By \cite{ALS94}, Theorem 4.1.
29.55/8.18	This system is of type 3 or smaller.
29.55/8.18	This system is strongly deterministic.
29.55/8.18	This system is quasi-decreasing.
29.55/8.18	By \cite{O02}, p. 214, Proposition 7.2.50.
29.55/8.18	This system is of type 3 or smaller.
29.55/8.18	This system is deterministic.
29.55/8.18	System R transformed to optimized U(R).
29.55/8.18	This system is terminating.
29.55/8.18	Call external tool:
29.55/8.18	./ttt2.sh
29.55/8.18	Input:
29.55/8.18	  qsort(cons(x, xs)) -> ?3(split(x, xs), x, xs)
29.55/8.18	  ?3(pair(ys, zs), x, xs) -> app(qsort(ys), cons(x, qsort(zs)))
29.55/8.18	  app(cons(x, xs), ys) -> cons(x, app(xs, ys))
29.55/8.18	  le(0, x) -> true
29.55/8.18	  split(x, nil) -> pair(nil, nil)
29.55/8.18	  qsort(nil) -> nil
29.55/8.18	  le(s(x), s(y)) -> le(x, y)
29.55/8.18	  le(s(x), 0) -> false
29.55/8.18	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
29.55/8.18	  ?1(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs)
29.55/8.18	  ?2(true, x, ys, y, zs, xs) -> pair(xs, cons(y, zs))
29.55/8.18	  app(nil, x) -> x
29.55/8.18	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
29.55/8.18	  ?1(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs)
29.55/8.18	  ?2(false, x, ys, y, zs, xs) -> pair(cons(y, xs), zs)
29.55/8.18	
29.55/8.18	 DP Processor:
29.55/8.18	  DPs:
29.55/8.18	   qsort#(cons(x,xs)) -> split#(x,xs)
29.55/8.18	   qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
29.55/8.18	   ?3#(pair(ys,zs),x,xs) -> qsort#(zs)
29.55/8.18	   ?3#(pair(ys,zs),x,xs) -> qsort#(ys)
29.55/8.18	   ?3#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
29.55/8.18	   app#(cons(x,xs),ys) -> app#(xs,ys)
29.55/8.18	   le#(s(x),s(y)) -> le#(x,y)
29.55/8.18	   split#(x,cons(y,ys)) -> split#(x,ys)
29.55/8.18	   split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
29.55/8.18	   ?1#(pair(xs,zs),x,y,ys) -> le#(x,y)
29.55/8.18	   ?1#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
29.55/8.18	  TRS:
29.55/8.18	   qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
29.55/8.18	   ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
29.55/8.18	   app(cons(x,xs),ys) -> cons(x,app(xs,ys))
29.55/8.18	   le(0(),x) -> true()
29.55/8.18	   split(x,nil()) -> pair(nil(),nil())
29.55/8.18	   qsort(nil()) -> nil()
29.55/8.18	   le(s(x),s(y)) -> le(x,y)
29.55/8.18	   le(s(x),0()) -> false()
29.55/8.18	   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
29.55/8.18	   ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
29.55/8.18	   ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
29.55/8.18	   app(nil(),x) -> x
29.55/8.18	   ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
29.55/8.18	  TDG Processor:
29.55/8.18	   DPs:
29.55/8.18	    qsort#(cons(x,xs)) -> split#(x,xs)
29.55/8.18	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
29.55/8.18	    ?3#(pair(ys,zs),x,xs) -> qsort#(zs)
29.55/8.18	    ?3#(pair(ys,zs),x,xs) -> qsort#(ys)
29.55/8.18	    ?3#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
29.55/8.18	    app#(cons(x,xs),ys) -> app#(xs,ys)
29.55/8.18	    le#(s(x),s(y)) -> le#(x,y)
29.55/8.18	    split#(x,cons(y,ys)) -> split#(x,ys)
29.55/8.18	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
29.55/8.18	    ?1#(pair(xs,zs),x,y,ys) -> le#(x,y)
29.55/8.18	    ?1#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
29.55/8.18	   TRS:
29.55/8.18	    qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
29.55/8.18	    ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
29.55/8.18	    app(cons(x,xs),ys) -> cons(x,app(xs,ys))
29.55/8.18	    le(0(),x) -> true()
29.55/8.18	    split(x,nil()) -> pair(nil(),nil())
29.55/8.18	    qsort(nil()) -> nil()
29.55/8.18	    le(s(x),s(y)) -> le(x,y)
29.55/8.18	    le(s(x),0()) -> false()
29.55/8.18	    split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
29.55/8.18	    ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
29.55/8.18	    ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
29.55/8.18	    app(nil(),x) -> x
29.55/8.18	    ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
29.55/8.18	   graph:
29.55/8.18	    ?1#(pair(xs,zs),x,y,ys) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
29.55/8.18	    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
29.55/8.18	    app#(cons(x,xs),ys) -> app#(xs,ys) ->
29.55/8.18	    app#(cons(x,xs),ys) -> app#(xs,ys)
29.55/8.18	    ?3#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) ->
29.55/8.18	    app#(cons(x,xs),ys) -> app#(xs,ys)
29.55/8.18	    ?3#(pair(ys,zs),x,xs) -> qsort#(zs) ->
29.55/8.18	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
29.55/8.18	    ?3#(pair(ys,zs),x,xs) -> qsort#(zs) ->
29.55/8.18	    qsort#(cons(x,xs)) -> split#(x,xs)
29.55/8.18	    ?3#(pair(ys,zs),x,xs) -> qsort#(ys) ->
29.55/8.18	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
29.94/8.20	    ?3#(pair(ys,zs),x,xs) -> qsort#(ys) ->
29.94/8.20	    qsort#(cons(x,xs)) -> split#(x,xs)
29.94/8.20	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
29.94/8.20	    ?1#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
29.94/8.20	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
29.94/8.20	    ?1#(pair(xs,zs),x,y,ys) -> le#(x,y)
29.94/8.20	    split#(x,cons(y,ys)) -> split#(x,ys) ->
29.94/8.20	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
29.94/8.20	    split#(x,cons(y,ys)) -> split#(x,ys) ->
29.94/8.20	    split#(x,cons(y,ys)) -> split#(x,ys)
29.94/8.20	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs) ->
29.94/8.20	    ?3#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
29.94/8.20	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs) ->
29.94/8.20	    ?3#(pair(ys,zs),x,xs) -> qsort#(ys)
29.94/8.20	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs) ->
29.94/8.20	    ?3#(pair(ys,zs),x,xs) -> qsort#(zs)
29.94/8.20	    qsort#(cons(x,xs)) -> split#(x,xs) ->
29.94/8.20	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
29.94/8.20	    qsort#(cons(x,xs)) -> split#(x,xs) -> split#(x,cons(y,ys)) -> split#(x,ys)
29.94/8.20	   SCC Processor:
29.94/8.20	    #sccs: 4
29.94/8.20	    #rules: 6
29.94/8.20	    #arcs: 17/121
29.94/8.20	    DPs:
29.94/8.20	     ?3#(pair(ys,zs),x,xs) -> qsort#(zs)
29.94/8.20	     qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
29.94/8.20	     ?3#(pair(ys,zs),x,xs) -> qsort#(ys)
29.94/8.20	    TRS:
29.94/8.20	     qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
29.94/8.20	     ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
29.94/8.20	     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
29.94/8.20	     le(0(),x) -> true()
29.94/8.20	     split(x,nil()) -> pair(nil(),nil())
29.94/8.20	     qsort(nil()) -> nil()
29.94/8.20	     le(s(x),s(y)) -> le(x,y)
29.94/8.20	     le(s(x),0()) -> false()
29.94/8.20	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
29.94/8.20	     ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
29.94/8.20	     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
29.94/8.20	     app(nil(),x) -> x
29.94/8.20	     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
29.94/8.20	    Subterm Criterion Processor:
29.94/8.20	     simple projection:
29.94/8.20	      pi(cons) = [0,0,1,1,1]
29.94/8.20	      pi(split) = [1,1]
29.94/8.20	      pi(pair) = [0,1]
29.94/8.20	      pi(?1) = [0,0,0,2,2,2]
29.94/8.20	      pi(?2) = [3,3,4,4,4,5,5,5]
29.94/8.20	      pi(qsort#) = [0,0]
29.94/8.20	      pi(?3#) = [0,0,0]
29.94/8.20	     problem:
29.94/8.20	      DPs:
29.94/8.20	       
29.94/8.20	      TRS:
29.94/8.20	       qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
29.94/8.20	       ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
29.94/8.20	       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
29.94/8.20	       le(0(),x) -> true()
29.94/8.20	       split(x,nil()) -> pair(nil(),nil())
29.94/8.20	       qsort(nil()) -> nil()
29.94/8.20	       le(s(x),s(y)) -> le(x,y)
29.94/8.20	       le(s(x),0()) -> false()
29.94/8.20	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
29.94/8.20	       ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
29.94/8.20	       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
29.94/8.20	       app(nil(),x) -> x
29.94/8.20	       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
29.94/8.20	     Qed
29.94/8.20	    
29.94/8.20	    DPs:
29.94/8.20	     split#(x,cons(y,ys)) -> split#(x,ys)
29.94/8.20	    TRS:
29.94/8.20	     qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
29.94/8.20	     ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
29.94/8.20	     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
29.94/8.20	     le(0(),x) -> true()
29.94/8.20	     split(x,nil()) -> pair(nil(),nil())
29.94/8.20	     qsort(nil()) -> nil()
29.94/8.20	     le(s(x),s(y)) -> le(x,y)
29.94/8.20	     le(s(x),0()) -> false()
29.94/8.20	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
29.94/8.20	     ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
29.94/8.20	     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
29.94/8.20	     app(nil(),x) -> x
29.94/8.20	     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
29.94/8.20	    Subterm Criterion Processor:
29.94/8.20	     simple projection:
29.94/8.20	      pi(split#) = 1
29.94/8.20	     problem:
29.94/8.20	      DPs:
29.94/8.20	       
29.94/8.20	      TRS:
29.94/8.20	       qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
29.94/8.20	       ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
29.94/8.20	       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
29.94/8.20	       le(0(),x) -> true()
29.94/8.20	       split(x,nil()) -> pair(nil(),nil())
29.94/8.20	       qsort(nil()) -> nil()
29.94/8.20	       le(s(x),s(y)) -> le(x,y)
29.94/8.20	       le(s(x),0()) -> false()
29.94/8.20	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
29.94/8.20	       ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
29.94/8.20	       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
29.94/8.20	       app(nil(),x) -> x
29.94/8.20	       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
29.94/8.20	     Qed
29.94/8.20	    
29.94/8.20	    DPs:
29.94/8.20	     app#(cons(x,xs),ys) -> app#(xs,ys)
29.94/8.20	    TRS:
29.94/8.20	     qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
29.94/8.20	     ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
29.94/8.20	     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
29.94/8.20	     le(0(),x) -> true()
29.94/8.20	     split(x,nil()) -> pair(nil(),nil())
29.94/8.20	     qsort(nil()) -> nil()
29.94/8.20	     le(s(x),s(y)) -> le(x,y)
29.94/8.20	     le(s(x),0()) -> false()
29.94/8.20	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
29.94/8.20	     ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
29.94/8.20	     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
29.94/8.20	     app(nil(),x) -> x
29.94/8.20	     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
29.94/8.20	    Subterm Criterion Processor:
29.94/8.20	     simple projection:
29.94/8.20	      pi(app#) = 0
29.94/8.20	     problem:
29.94/8.20	      DPs:
29.94/8.20	       
29.94/8.20	      TRS:
29.94/8.20	       qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
29.94/8.20	       ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
29.94/8.20	       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
29.94/8.20	       le(0(),x) -> true()
29.94/8.20	       split(x,nil()) -> pair(nil(),nil())
29.94/8.20	       qsort(nil()) -> nil()
29.94/8.20	       le(s(x),s(y)) -> le(x,y)
29.94/8.20	       le(s(x),0()) -> false()
29.94/8.20	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
29.94/8.20	       ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
29.94/8.20	       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
29.94/8.20	       app(nil(),x) -> x
29.94/8.20	       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
29.94/8.20	     Qed
29.94/8.20	    
30.05/8.28	    DPs:
30.05/8.28	     le#(s(x),s(y)) -> le#(x,y)
30.05/8.28	    TRS:
30.05/8.28	     qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
30.05/8.28	     ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
30.05/8.28	     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
30.05/8.28	     le(0(),x) -> true()
30.05/8.28	     split(x,nil()) -> pair(nil(),nil())
30.05/8.28	     qsort(nil()) -> nil()
30.05/8.28	     le(s(x),s(y)) -> le(x,y)
30.05/8.28	     le(s(x),0()) -> false()
30.05/8.28	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
30.05/8.28	     ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
30.05/8.28	     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
30.05/8.28	     app(nil(),x) -> x
30.05/8.28	     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
30.05/8.28	    Subterm Criterion Processor:
30.05/8.28	     simple projection:
30.05/8.28	      pi(le#) = 0
30.05/8.28	     problem:
30.05/8.28	      DPs:
30.05/8.28	       
30.05/8.28	      TRS:
30.05/8.28	       qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
30.05/8.28	       ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
30.05/8.28	       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
30.05/8.28	       le(0(),x) -> true()
30.05/8.28	       split(x,nil()) -> pair(nil(),nil())
30.05/8.28	       qsort(nil()) -> nil()
30.05/8.28	       le(s(x),s(y)) -> le(x,y)
30.05/8.28	       le(s(x),0()) -> false()
30.05/8.28	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
30.05/8.28	       ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
30.05/8.28	       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
30.05/8.28	       app(nil(),x) -> x
30.05/8.28	       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
30.05/8.28	     Qed
30.05/8.28	All 2 critical pairs are joinable.
30.05/8.28	Overlap: (rule1: split(z', cons($1, y')) -> pair(cons($1, x'), z) <= split(z', y') = pair(x', z), le(z', $1) = false, rule2: split($3, cons($5, $4)) -> pair($6, cons($5, $2)) <= split($3, $4) = pair($6, $2), le($3, $5) = true, pos: ε, mgu: {($3,z'), ($5,$1), ($4,y')})
30.05/8.28	CP: pair($6, cons($1, $2)) = pair(cons($1, x'), z) <= split(z', y') = pair(x', z), le(z', $1) = false, split(z', y') = pair($6, $2), le(z', $1) = true
30.05/8.28	This critical pair is unfeasible.
30.05/8.28	Overlap: (rule1: split(z', cons($1, y')) -> pair(x', cons($1, z)) <= split(z', y') = pair(x', z), le(z', $1) = true, rule2: split($3, cons($5, $4)) -> pair(cons($5, $6), $2) <= split($3, $4) = pair($6, $2), le($3, $5) = false, pos: ε, mgu: {($3,z'), ($5,$1), ($4,y')})
30.05/8.28	CP: pair(cons($1, $6), $2) = pair(x', cons($1, z)) <= split(z', y') = pair(x', z), le(z', $1) = true, split(z', y') = pair($6, $2), le(z', $1) = false
30.05/8.28	This critical pair is unfeasible.
30.05/8.28	
32.02/8.77	EOF