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