21.94/6.53	YES
21.94/6.53	
21.94/6.53	Proof:
21.94/6.53	This system is confluent.
21.94/6.53	By \cite{ALS94}, Theorem 4.1.
21.94/6.53	This system is of type 3 or smaller.
21.94/6.53	This system is strongly deterministic.
21.94/6.53	This system is quasi-decreasing.
21.94/6.53	By \cite{O02}, p. 214, Proposition 7.2.50.
21.94/6.53	This system is of type 3 or smaller.
21.94/6.53	This system is deterministic.
21.94/6.53	System R transformed to optimized U(R).
21.94/6.53	This system is terminating.
21.94/6.53	Call external tool:
21.94/6.53	./ttt2.sh
21.94/6.53	Input:
21.94/6.53	(VAR x ys y zs xs)
21.94/6.53	(RULES
21.94/6.53	  qsort(cons(x, xs)) -> ?3(split(x, xs), x, xs)
21.94/6.53	  ?3(pair(ys, zs), x, xs) -> app(qsort(ys), cons(x, qsort(zs)))
21.94/6.53	  app(cons(x, xs), ys) -> cons(x, app(xs, ys))
21.94/6.53	  le(0, x) -> true
21.94/6.53	  split(x, nil) -> pair(nil, nil)
21.94/6.53	  qsort(nil) -> nil
21.94/6.53	  le(s(x), s(y)) -> le(x, y)
21.94/6.53	  le(s(x), 0) -> false
21.94/6.53	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
21.94/6.53	  ?1(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs)
21.94/6.53	  ?2(true, x, ys, y, zs, xs) -> pair(xs, cons(y, zs))
21.94/6.53	  app(nil, x) -> x
21.94/6.53	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
21.94/6.53	  ?1(pair(xs, zs), x, y, ys) -> ?2(le(x, y), x, ys, y, zs, xs)
21.94/6.53	  ?2(false, x, ys, y, zs, xs) -> pair(cons(y, xs), zs)
21.94/6.53	)
21.94/6.53	
21.94/6.53	 DP Processor:
21.94/6.53	  DPs:
21.94/6.53	   qsort#(cons(x,xs)) -> split#(x,xs)
21.94/6.53	   qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
21.94/6.53	   ?3#(pair(ys,zs),x,xs) -> qsort#(zs)
21.94/6.53	   ?3#(pair(ys,zs),x,xs) -> qsort#(ys)
21.94/6.53	   ?3#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
21.94/6.53	   app#(cons(x,xs),ys) -> app#(xs,ys)
21.94/6.53	   le#(s(x),s(y)) -> le#(x,y)
21.94/6.53	   split#(x,cons(y,ys)) -> split#(x,ys)
21.94/6.53	   split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
21.94/6.53	   ?1#(pair(xs,zs),x,y,ys) -> le#(x,y)
21.94/6.53	   ?1#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
21.94/6.53	  TRS:
21.94/6.53	   qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.53	   ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.53	   app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.53	   le(0(),x) -> true()
21.94/6.53	   split(x,nil()) -> pair(nil(),nil())
21.94/6.53	   qsort(nil()) -> nil()
21.94/6.53	   le(s(x),s(y)) -> le(x,y)
21.94/6.53	   le(s(x),0()) -> false()
21.94/6.53	   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.53	   ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.53	   ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.53	   app(nil(),x) -> x
21.94/6.53	   ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.53	  TDG Processor:
21.94/6.53	   DPs:
21.94/6.53	    qsort#(cons(x,xs)) -> split#(x,xs)
21.94/6.53	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
21.94/6.53	    ?3#(pair(ys,zs),x,xs) -> qsort#(zs)
21.94/6.53	    ?3#(pair(ys,zs),x,xs) -> qsort#(ys)
21.94/6.53	    ?3#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
21.94/6.53	    app#(cons(x,xs),ys) -> app#(xs,ys)
21.94/6.53	    le#(s(x),s(y)) -> le#(x,y)
21.94/6.53	    split#(x,cons(y,ys)) -> split#(x,ys)
21.94/6.53	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
21.94/6.53	    ?1#(pair(xs,zs),x,y,ys) -> le#(x,y)
21.94/6.53	    ?1#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
21.94/6.53	   TRS:
21.94/6.53	    qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.53	    ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.53	    app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.53	    le(0(),x) -> true()
21.94/6.53	    split(x,nil()) -> pair(nil(),nil())
21.94/6.53	    qsort(nil()) -> nil()
21.94/6.53	    le(s(x),s(y)) -> le(x,y)
21.94/6.53	    le(s(x),0()) -> false()
21.94/6.53	    split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.53	    ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.53	    ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.54	    app(nil(),x) -> x
21.94/6.54	    ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.54	   graph:
21.94/6.54	    ?1#(pair(xs,zs),x,y,ys) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
21.94/6.54	    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
21.94/6.54	    app#(cons(x,xs),ys) -> app#(xs,ys) ->
21.94/6.54	    app#(cons(x,xs),ys) -> app#(xs,ys)
21.94/6.54	    ?3#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs))) ->
21.94/6.54	    app#(cons(x,xs),ys) -> app#(xs,ys)
21.94/6.54	    ?3#(pair(ys,zs),x,xs) -> qsort#(zs) ->
21.94/6.54	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
21.94/6.54	    ?3#(pair(ys,zs),x,xs) -> qsort#(zs) ->
21.94/6.54	    qsort#(cons(x,xs)) -> split#(x,xs)
21.94/6.54	    ?3#(pair(ys,zs),x,xs) -> qsort#(ys) ->
21.94/6.54	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
21.94/6.54	    ?3#(pair(ys,zs),x,xs) -> qsort#(ys) ->
21.94/6.54	    qsort#(cons(x,xs)) -> split#(x,xs)
21.94/6.54	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
21.94/6.54	    ?1#(pair(xs,zs),x,y,ys) -> ?2#(le(x,y),x,ys,y,zs,xs)
21.94/6.54	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
21.94/6.54	    ?1#(pair(xs,zs),x,y,ys) -> le#(x,y)
21.94/6.54	    split#(x,cons(y,ys)) -> split#(x,ys) ->
21.94/6.54	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
21.94/6.54	    split#(x,cons(y,ys)) -> split#(x,ys) ->
21.94/6.54	    split#(x,cons(y,ys)) -> split#(x,ys)
21.94/6.54	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs) ->
21.94/6.54	    ?3#(pair(ys,zs),x,xs) -> app#(qsort(ys),cons(x,qsort(zs)))
21.94/6.54	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs) ->
21.94/6.54	    ?3#(pair(ys,zs),x,xs) -> qsort#(ys)
21.94/6.54	    qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs) ->
21.94/6.54	    ?3#(pair(ys,zs),x,xs) -> qsort#(zs)
21.94/6.54	    qsort#(cons(x,xs)) -> split#(x,xs) ->
21.94/6.54	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
21.94/6.54	    qsort#(cons(x,xs)) -> split#(x,xs) -> split#(x,cons(y,ys)) -> split#(x,ys)
21.94/6.54	   SCC Processor:
21.94/6.54	    #sccs: 4
21.94/6.54	    #rules: 6
21.94/6.54	    #arcs: 17/121
21.94/6.54	    DPs:
21.94/6.54	     ?3#(pair(ys,zs),x,xs) -> qsort#(zs)
21.94/6.54	     qsort#(cons(x,xs)) -> ?3#(split(x,xs),x,xs)
21.94/6.54	     ?3#(pair(ys,zs),x,xs) -> qsort#(ys)
21.94/6.54	    TRS:
21.94/6.54	     qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.54	     ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.54	     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.54	     le(0(),x) -> true()
21.94/6.54	     split(x,nil()) -> pair(nil(),nil())
21.94/6.54	     qsort(nil()) -> nil()
21.94/6.54	     le(s(x),s(y)) -> le(x,y)
21.94/6.54	     le(s(x),0()) -> false()
21.94/6.54	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.54	     ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.54	     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.54	     app(nil(),x) -> x
21.94/6.54	     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.54	    Subterm Criterion Processor:
21.94/6.54	     simple projection:
21.94/6.54	      pi(cons) = [0,0,1,1,1]
21.94/6.54	      pi(split) = [1,1]
21.94/6.54	      pi(pair) = [0,1]
21.94/6.54	      pi(?1) = [0,0,0,2,2,2]
21.94/6.54	      pi(?2) = [3,3,4,4,4,5,5,5]
21.94/6.54	      pi(qsort#) = [0,0]
21.94/6.54	      pi(?3#) = [0,0,0]
21.94/6.54	     problem:
21.94/6.54	      DPs:
21.94/6.54	       
21.94/6.54	      TRS:
21.94/6.54	       qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.54	       ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.54	       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.54	       le(0(),x) -> true()
21.94/6.54	       split(x,nil()) -> pair(nil(),nil())
21.94/6.54	       qsort(nil()) -> nil()
21.94/6.54	       le(s(x),s(y)) -> le(x,y)
21.94/6.54	       le(s(x),0()) -> false()
21.94/6.54	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.54	       ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.54	       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.54	       app(nil(),x) -> x
21.94/6.54	       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.54	     Qed
21.94/6.54	    
21.94/6.54	    DPs:
21.94/6.54	     split#(x,cons(y,ys)) -> split#(x,ys)
21.94/6.54	    TRS:
21.94/6.54	     qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.54	     ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.54	     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.54	     le(0(),x) -> true()
21.94/6.54	     split(x,nil()) -> pair(nil(),nil())
21.94/6.54	     qsort(nil()) -> nil()
21.94/6.54	     le(s(x),s(y)) -> le(x,y)
21.94/6.54	     le(s(x),0()) -> false()
21.94/6.54	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.54	     ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.54	     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.54	     app(nil(),x) -> x
21.94/6.54	     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.54	    Subterm Criterion Processor:
21.94/6.54	     simple projection:
21.94/6.54	      pi(split#) = 1
21.94/6.54	     problem:
21.94/6.54	      DPs:
21.94/6.54	       
21.94/6.54	      TRS:
21.94/6.54	       qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.54	       ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.54	       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.54	       le(0(),x) -> true()
21.94/6.54	       split(x,nil()) -> pair(nil(),nil())
21.94/6.54	       qsort(nil()) -> nil()
21.94/6.56	       le(s(x),s(y)) -> le(x,y)
21.94/6.56	       le(s(x),0()) -> false()
21.94/6.56	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.56	       ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.56	       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.56	       app(nil(),x) -> x
21.94/6.56	       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.56	     Qed
21.94/6.56	    
21.94/6.56	    DPs:
21.94/6.56	     app#(cons(x,xs),ys) -> app#(xs,ys)
21.94/6.56	    TRS:
21.94/6.56	     qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.56	     ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.56	     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.56	     le(0(),x) -> true()
21.94/6.56	     split(x,nil()) -> pair(nil(),nil())
21.94/6.56	     qsort(nil()) -> nil()
21.94/6.56	     le(s(x),s(y)) -> le(x,y)
21.94/6.56	     le(s(x),0()) -> false()
21.94/6.56	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.56	     ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.56	     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.56	     app(nil(),x) -> x
21.94/6.56	     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.56	    Subterm Criterion Processor:
21.94/6.56	     simple projection:
21.94/6.56	      pi(app#) = 0
21.94/6.56	     problem:
21.94/6.56	      DPs:
21.94/6.56	       
21.94/6.56	      TRS:
21.94/6.56	       qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.56	       ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.56	       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.56	       le(0(),x) -> true()
21.94/6.56	       split(x,nil()) -> pair(nil(),nil())
21.94/6.56	       qsort(nil()) -> nil()
21.94/6.56	       le(s(x),s(y)) -> le(x,y)
21.94/6.56	       le(s(x),0()) -> false()
21.94/6.56	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.56	       ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.56	       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.56	       app(nil(),x) -> x
21.94/6.56	       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.56	     Qed
21.94/6.56	    
21.94/6.56	    DPs:
21.94/6.56	     le#(s(x),s(y)) -> le#(x,y)
21.94/6.56	    TRS:
21.94/6.56	     qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.56	     ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.56	     app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.56	     le(0(),x) -> true()
21.94/6.56	     split(x,nil()) -> pair(nil(),nil())
21.94/6.56	     qsort(nil()) -> nil()
21.94/6.56	     le(s(x),s(y)) -> le(x,y)
21.94/6.56	     le(s(x),0()) -> false()
21.94/6.56	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.56	     ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.56	     ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.56	     app(nil(),x) -> x
21.94/6.56	     ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.56	    Subterm Criterion Processor:
21.94/6.56	     simple projection:
21.94/6.56	      pi(le#) = 0
21.94/6.56	     problem:
21.94/6.56	      DPs:
21.94/6.56	       
21.94/6.56	      TRS:
21.94/6.56	       qsort(cons(x,xs)) -> ?3(split(x,xs),x,xs)
21.94/6.56	       ?3(pair(ys,zs),x,xs) -> app(qsort(ys),cons(x,qsort(zs)))
21.94/6.56	       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
21.94/6.56	       le(0(),x) -> true()
21.94/6.56	       split(x,nil()) -> pair(nil(),nil())
21.94/6.56	       qsort(nil()) -> nil()
21.94/6.56	       le(s(x),s(y)) -> le(x,y)
21.94/6.56	       le(s(x),0()) -> false()
21.94/6.56	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
21.94/6.56	       ?1(pair(xs,zs),x,y,ys) -> ?2(le(x,y),x,ys,y,zs,xs)
21.94/6.56	       ?2(true(),x,ys,y,zs,xs) -> pair(xs,cons(y,zs))
21.94/6.56	       app(nil(),x) -> x
21.94/6.56	       ?2(false(),x,ys,y,zs,xs) -> pair(cons(y,xs),zs)
21.94/6.56	     Qed
21.94/6.56	All 2 critical pairs are joinable.
21.94/6.56	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: {(z',$3), ($1,$5), (y',$4)})
21.94/6.56	CP: pair($6, cons($5, $2)) = pair(cons($5, x'), z) <= split($3, $4) = pair(x', z), le($3, $5) = false, split($3, $4) = pair($6, $2), le($3, $5) = true
21.94/6.56	This critical pair is unfeasible.
21.94/6.56	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: {(z',$3), ($1,$5), (y',$4)})
21.94/6.56	CP: pair(cons($5, $6), $2) = pair(x', cons($5, z)) <= split($3, $4) = pair(x', z), le($3, $5) = true, split($3, $4) = pair($6, $2), le($3, $5) = false
21.94/6.56	This critical pair is unfeasible.
21.94/6.56	
23.69/7.03	EOF