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