7.27/2.74	YES
7.27/2.74	
7.27/2.74	Proof:
7.27/2.74	This system is confluent.
7.27/2.74	By \cite{ALS94}, Theorem 4.1.
7.27/2.74	This system is of type 3 or smaller.
7.27/2.74	This system is strongly deterministic.
7.27/2.74	This system is quasi-decreasing.
7.27/2.74	By \cite{O02}, p. 214, Proposition 7.2.50.
7.27/2.74	This system is of type 3 or smaller.
7.27/2.74	This system is deterministic.
7.27/2.74	System R transformed to optimized U(R).
7.27/2.74	This system is terminating.
7.27/2.74	Call external tool:
7.27/2.74	./ttt2.sh
7.27/2.74	Input:
7.27/2.74	(VAR zs2 x ys zs1 y)
7.27/2.74	(RULES
7.27/2.74	  le(0, y) -> true
7.27/2.74	  split(x, nil) -> tp2(nil, nil)
7.27/2.74	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
7.27/2.74	  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
7.27/2.74	  ?2(true, zs2, x, ys, zs1, y) -> tp2(zs1, cons(y, zs2))
7.27/2.74	  le(s(x), s(y)) -> le(x, y)
7.27/2.74	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
7.27/2.74	  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
7.27/2.74	  ?2(false, zs2, x, ys, zs1, y) -> tp2(cons(y, zs1), zs2)
7.27/2.74	  le(s(x), 0) -> false
7.27/2.74	)
7.27/2.74	
7.27/2.74	 DP Processor:
7.27/2.74	  DPs:
7.27/2.74	   split#(x,cons(y,ys)) -> split#(x,ys)
7.27/2.74	   split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
7.27/2.74	   ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
7.27/2.74	   ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
7.27/2.74	   le#(s(x),s(y)) -> le#(x,y)
7.27/2.74	  TRS:
7.27/2.74	   le(0(),y) -> true()
7.27/2.74	   split(x,nil()) -> tp2(nil(),nil())
7.27/2.74	   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.27/2.74	   ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.27/2.74	   ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.27/2.74	   le(s(x),s(y)) -> le(x,y)
7.27/2.74	   ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.27/2.74	   le(s(x),0()) -> false()
7.27/2.74	  TDG Processor:
7.27/2.74	   DPs:
7.27/2.74	    split#(x,cons(y,ys)) -> split#(x,ys)
7.27/2.74	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
7.27/2.74	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
7.27/2.74	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
7.27/2.74	    le#(s(x),s(y)) -> le#(x,y)
7.27/2.74	   TRS:
7.27/2.74	    le(0(),y) -> true()
7.27/2.74	    split(x,nil()) -> tp2(nil(),nil())
7.27/2.74	    split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.27/2.74	    ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.27/2.74	    ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.27/2.74	    le(s(x),s(y)) -> le(x,y)
7.27/2.74	    ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.27/2.74	    le(s(x),0()) -> false()
7.27/2.74	   graph:
7.27/2.74	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) ->
7.27/2.74	    le#(s(x),s(y)) -> le#(x,y)
7.27/2.74	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
7.27/2.74	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
7.27/2.74	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
7.27/2.74	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
7.27/2.74	    split#(x,cons(y,ys)) -> split#(x,ys) ->
7.27/2.74	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
7.27/2.74	    split#(x,cons(y,ys)) -> split#(x,ys) ->
7.27/2.74	    split#(x,cons(y,ys)) -> split#(x,ys)
7.27/2.74	    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
7.27/2.74	   SCC Processor:
7.27/2.74	    #sccs: 2
7.27/2.74	    #rules: 2
7.27/2.74	    #arcs: 6/25
7.27/2.74	    DPs:
7.27/2.74	     split#(x,cons(y,ys)) -> split#(x,ys)
7.27/2.74	    TRS:
7.27/2.74	     le(0(),y) -> true()
7.27/2.74	     split(x,nil()) -> tp2(nil(),nil())
7.27/2.74	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.27/2.74	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.27/2.74	     ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.27/2.74	     le(s(x),s(y)) -> le(x,y)
7.27/2.74	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.27/2.74	     le(s(x),0()) -> false()
7.27/2.74	    Subterm Criterion Processor:
7.27/2.74	     simple projection:
7.27/2.75	      pi(split#) = 1
7.27/2.75	     problem:
7.27/2.75	      DPs:
7.27/2.75	       
7.27/2.75	      TRS:
7.27/2.75	       le(0(),y) -> true()
7.27/2.75	       split(x,nil()) -> tp2(nil(),nil())
7.27/2.75	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.27/2.76	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.27/2.76	       ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.27/2.76	       le(s(x),s(y)) -> le(x,y)
7.27/2.76	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.27/2.76	       le(s(x),0()) -> false()
7.27/2.76	     Qed
7.27/2.76	    
7.27/2.76	    DPs:
7.27/2.76	     le#(s(x),s(y)) -> le#(x,y)
7.27/2.76	    TRS:
7.27/2.76	     le(0(),y) -> true()
7.27/2.76	     split(x,nil()) -> tp2(nil(),nil())
7.27/2.76	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.27/2.76	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.27/2.76	     ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.27/2.76	     le(s(x),s(y)) -> le(x,y)
7.27/2.76	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.27/2.76	     le(s(x),0()) -> false()
7.27/2.76	    Subterm Criterion Processor:
7.27/2.76	     simple projection:
7.27/2.76	      pi(le#) = 0
7.27/2.76	     problem:
7.27/2.76	      DPs:
7.27/2.76	       
7.27/2.76	      TRS:
7.27/2.76	       le(0(),y) -> true()
7.27/2.76	       split(x,nil()) -> tp2(nil(),nil())
7.27/2.76	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.27/2.76	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.27/2.76	       ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.27/2.76	       le(s(x),s(y)) -> le(x,y)
7.27/2.76	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.27/2.76	       le(s(x),0()) -> false()
7.27/2.76	     Qed
7.27/2.76	All 2 critical pairs are joinable.
7.27/2.76	Overlap: (rule1: split(z', cons(x', $1)) -> tp2(cons(x', y'), z) <= split(z', $1) = tp2(y', z), le(z', x') = false, rule2: split($3, cons($6, $5)) -> tp2($4, cons($6, $2)) <= split($3, $5) = tp2($4, $2), le($3, $6) = true, pos: ε, mgu: {(z',$3), (x',$6), ($1,$5)})
7.27/2.76	CP: tp2($4, cons($6, $2)) = tp2(cons($6, y'), z) <= split($3, $5) = tp2(y', z), le($3, $6) = false, split($3, $5) = tp2($4, $2), le($3, $6) = true
7.27/2.76	This critical pair is unfeasible.
7.27/2.76	Overlap: (rule1: split(z', cons(x', $1)) -> tp2(y', cons(x', z)) <= split(z', $1) = tp2(y', z), le(z', x') = true, rule2: split($3, cons($6, $5)) -> tp2(cons($6, $4), $2) <= split($3, $5) = tp2($4, $2), le($3, $6) = false, pos: ε, mgu: {(z',$3), (x',$6), ($1,$5)})
7.27/2.76	CP: tp2(cons($6, $4), $2) = tp2(y', cons($6, z)) <= split($3, $5) = tp2(y', z), le($3, $6) = true, split($3, $5) = tp2($4, $2), le($3, $6) = false
7.27/2.76	This critical pair is unfeasible.
7.27/2.76	
7.74/2.87	EOF