11.69/3.55	YES
11.69/3.55	
11.69/3.55	Problem:
11.69/3.55	split(x, nil()) -> tp2(nil(), nil())
11.69/3.55	split(x, cons(y, ys)) -> tp2(zs1, cons(y, zs2)) <= split(x, ys) = tp2(zs1, zs2), le(x, y) = true()
11.69/3.55	split(x, cons(y, ys)) -> tp2(cons(y, zs1), zs2) <= split(x, ys) = tp2(zs1, zs2), le(x, y) = false()
11.69/3.55	le(0(), y) -> true()
11.69/3.55	le(s(x), 0()) -> false()
11.69/3.55	le(s(x), s(y)) -> le(x, y)
11.69/3.55	
11.69/3.55	Proof:
11.69/3.55	This system is confluent.
11.69/3.55	By \cite{ALS94}, Theorem 4.1.
11.69/3.55	This system is of type 3 or smaller.
11.69/3.55	This system is strongly deterministic.
11.69/3.55	All 2 critical pairs are joinable.
11.69/3.55	CP: tp2($7, cons($6, y)) = tp2(cons($6, x), $3) <= split($5, $8) = tp2(x, $3), le($5, $6) = false(), split($5, $8) = tp2($7, y), le($5, $6) = true():
11.69/3.55	This critical pair is unfeasible.
11.69/3.55	CP: tp2(cons($6, $7), y) = tp2(x, cons($6, $3)) <= split($5, $8) = tp2(x, $3), le($5, $6) = true(), split($5, $8) = tp2($7, y), le($5, $6) = false():
11.69/3.55	This critical pair is unfeasible.
11.69/3.55	This system is quasi-decreasing.
11.69/3.55	By \cite{O02}, p. 214, Proposition 7.2.50.
11.69/3.55	This system is of type 3 or smaller.
11.69/3.55	This system is deterministic.
11.69/3.55	System R transformed to U(R).
11.69/3.55	This system is terminating.
11.69/3.55	Call external tool:
11.69/3.55	./ttt2.sh
11.69/3.55	Input:
11.69/3.55	  split(x, nil()) -> tp2(nil(), nil())
11.69/3.55	  ?4(true(), zs2, x, ys, zs1, y) -> tp2(zs1, cons(y, zs2))
11.69/3.55	  ?3(tp2(zs1, zs2), x, y, ys) -> ?4(le(x, y), zs2, x, ys, zs1, y)
11.69/3.55	  split(x, cons(y, ys)) -> ?3(split(x, ys), x, y, ys)
11.69/3.55	  ?2(false(), zs2, x, ys, zs1, y) -> tp2(cons(y, zs1), zs2)
11.69/3.55	  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
11.69/3.55	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
11.69/3.55	  le(0(), y) -> true()
11.69/3.55	  le(s(x), 0()) -> false()
11.69/3.55	  le(s(x), s(y)) -> le(x, y)
11.69/3.55	
11.69/3.55	 DP Processor:
11.69/3.55	  DPs:
11.69/3.55	   ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.69/3.55	   ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	   split#(x,cons(y,ys)) -> split#(x,ys)
11.69/3.55	   split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
11.69/3.55	   ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.69/3.55	   ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	   split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
11.69/3.55	   le#(s(x),s(y)) -> le#(x,y)
11.69/3.55	  TRS:
11.69/3.55	   split(x,nil()) -> tp2(nil(),nil())
11.69/3.55	   ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.69/3.55	   ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	   split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.69/3.55	   ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.69/3.55	   ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.69/3.55	   le(0(),y) -> true()
11.69/3.55	   le(s(x),0()) -> false()
11.69/3.55	   le(s(x),s(y)) -> le(x,y)
11.69/3.55	  TDG Processor:
11.69/3.55	   DPs:
11.69/3.55	    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.69/3.55	    ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	    split#(x,cons(y,ys)) -> split#(x,ys)
11.69/3.55	    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
11.69/3.55	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.69/3.55	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
11.69/3.55	    le#(s(x),s(y)) -> le#(x,y)
11.69/3.55	   TRS:
11.69/3.55	    split(x,nil()) -> tp2(nil(),nil())
11.69/3.55	    ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.69/3.55	    ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	    split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.69/3.55	    ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.69/3.55	    ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	    split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.69/3.55	    le(0(),y) -> true()
11.69/3.55	    le(s(x),0()) -> false()
11.69/3.55	    le(s(x),s(y)) -> le(x,y)
11.69/3.55	   graph:
11.69/3.55	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
11.69/3.55	    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
11.69/3.55	    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) ->
11.69/3.55	    le#(s(x),s(y)) -> le#(x,y)
11.69/3.55	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
11.69/3.55	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
11.69/3.55	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.69/3.55	    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ->
11.69/3.55	    ?3#(tp2(zs1,zs2),x,y,ys) -> ?4#(le(x,y),zs2,x,ys,zs1,y)
11.69/3.55	    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys) ->
11.69/3.55	    ?3#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
11.69/3.55	    split#(x,cons(y,ys)) -> split#(x,ys) ->
11.69/3.55	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
11.69/3.55	    split#(x,cons(y,ys)) -> split#(x,ys) ->
11.69/3.55	    split#(x,cons(y,ys)) -> ?3#(split(x,ys),x,y,ys)
11.69/3.55	    split#(x,cons(y,ys)) -> split#(x,ys) -> split#(x,cons(y,ys)) -> split#(x,ys)
11.69/3.55	   SCC Processor:
11.69/3.56	    #sccs: 2
11.69/3.56	    #rules: 2
11.69/3.56	    #arcs: 10/64
11.69/3.56	    DPs:
11.69/3.56	     split#(x,cons(y,ys)) -> split#(x,ys)
11.69/3.56	    TRS:
11.69/3.56	     split(x,nil()) -> tp2(nil(),nil())
11.69/3.56	     ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.69/3.56	     ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.69/3.56	     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.69/3.56	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.69/3.56	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.69/3.56	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.69/3.56	     le(0(),y) -> true()
11.69/3.56	     le(s(x),0()) -> false()
11.69/3.56	     le(s(x),s(y)) -> le(x,y)
11.69/3.56	    Subterm Criterion Processor:
11.69/3.56	     simple projection:
11.69/3.56	      pi(split#) = 1
11.69/3.56	     problem:
11.69/3.56	      DPs:
11.69/3.56	       
11.69/3.56	      TRS:
11.69/3.56	       split(x,nil()) -> tp2(nil(),nil())
11.69/3.56	       ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.69/3.56	       ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.69/3.56	       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.69/3.56	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.69/3.56	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.69/3.56	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.69/3.56	       le(0(),y) -> true()
11.69/3.56	       le(s(x),0()) -> false()
11.69/3.56	       le(s(x),s(y)) -> le(x,y)
11.69/3.56	     Qed
11.69/3.56	    
11.69/3.56	    DPs:
11.69/3.56	     le#(s(x),s(y)) -> le#(x,y)
11.69/3.56	    TRS:
11.69/3.56	     split(x,nil()) -> tp2(nil(),nil())
11.69/3.56	     ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.69/3.56	     ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.69/3.56	     split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.69/3.56	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.69/3.56	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.69/3.56	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.69/3.56	     le(0(),y) -> true()
11.69/3.56	     le(s(x),0()) -> false()
11.69/3.56	     le(s(x),s(y)) -> le(x,y)
11.69/3.56	    Subterm Criterion Processor:
11.69/3.56	     simple projection:
11.69/3.56	      pi(le#) = 0
11.69/3.56	     problem:
11.69/3.56	      DPs:
11.69/3.56	       
11.69/3.56	      TRS:
11.69/3.56	       split(x,nil()) -> tp2(nil(),nil())
11.69/3.56	       ?4(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
11.69/3.56	       ?3(tp2(zs1,zs2),x,y,ys) -> ?4(le(x,y),zs2,x,ys,zs1,y)
11.69/3.56	       split(x,cons(y,ys)) -> ?3(split(x,ys),x,y,ys)
11.69/3.56	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
11.69/3.56	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
11.69/3.56	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
11.69/3.56	       le(0(),y) -> true()
11.69/3.56	       le(s(x),0()) -> false()
11.69/3.56	       le(s(x),s(y)) -> le(x,y)
11.69/3.56	     Qed
11.69/3.56	
13.23/4.02	EOF