7.03/2.67	YES
7.03/2.67	
7.03/2.67	Proof:
7.03/2.67	This system is confluent.
7.03/2.67	By \cite{ALS94}, Theorem 4.1.
7.03/2.67	This system is of type 3 or smaller.
7.03/2.67	This system is strongly deterministic.
7.03/2.67	This system is quasi-decreasing.
7.03/2.67	By \cite{O02}, p. 214, Proposition 7.2.50.
7.03/2.67	This system is of type 3 or smaller.
7.03/2.67	This system is deterministic.
7.03/2.67	System R transformed to optimized U(R).
7.03/2.67	This system is terminating.
7.03/2.67	Call external tool:
7.03/2.67	./ttt2.sh
7.03/2.67	Input:
7.03/2.67	(VAR zs2 x ys zs1 y)
7.03/2.67	(RULES
7.03/2.67	  le(0, y) -> true
7.03/2.67	  split(x, nil) -> tp2(nil, nil)
7.03/2.67	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
7.03/2.67	  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
7.03/2.67	  ?2(true, zs2, x, ys, zs1, y) -> tp2(zs1, cons(y, zs2))
7.03/2.67	  le(s(x), s(y)) -> le(x, y)
7.03/2.67	  split(x, cons(y, ys)) -> ?1(split(x, ys), x, y, ys)
7.03/2.67	  ?1(tp2(zs1, zs2), x, y, ys) -> ?2(le(x, y), zs2, x, ys, zs1, y)
7.03/2.67	  ?2(false, zs2, x, ys, zs1, y) -> tp2(cons(y, zs1), zs2)
7.03/2.67	  le(s(x), 0) -> false
7.03/2.67	)
7.03/2.67	
7.03/2.67	 DP Processor:
7.03/2.67	  DPs:
7.03/2.67	   split#(x,cons(y,ys)) -> split#(x,ys)
7.03/2.67	   split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
7.03/2.67	   ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
7.03/2.67	   ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
7.03/2.67	   le#(s(x),s(y)) -> le#(x,y)
7.03/2.67	  TRS:
7.03/2.67	   le(0(),y) -> true()
7.03/2.67	   split(x,nil()) -> tp2(nil(),nil())
7.03/2.67	   split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.03/2.67	   ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.03/2.67	   ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.03/2.67	   le(s(x),s(y)) -> le(x,y)
7.03/2.67	   ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.03/2.67	   le(s(x),0()) -> false()
7.03/2.67	  TDG Processor:
7.03/2.67	   DPs:
7.03/2.67	    split#(x,cons(y,ys)) -> split#(x,ys)
7.03/2.67	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
7.03/2.67	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
7.03/2.67	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
7.03/2.67	    le#(s(x),s(y)) -> le#(x,y)
7.03/2.67	   TRS:
7.03/2.67	    le(0(),y) -> true()
7.03/2.67	    split(x,nil()) -> tp2(nil(),nil())
7.03/2.67	    split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.03/2.67	    ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.03/2.67	    ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.03/2.67	    le(s(x),s(y)) -> le(x,y)
7.03/2.67	    ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.03/2.67	    le(s(x),0()) -> false()
7.03/2.67	   graph:
7.03/2.67	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y) ->
7.03/2.67	    le#(s(x),s(y)) -> le#(x,y)
7.03/2.67	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
7.03/2.67	    ?1#(tp2(zs1,zs2),x,y,ys) -> ?2#(le(x,y),zs2,x,ys,zs1,y)
7.03/2.67	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys) ->
7.03/2.67	    ?1#(tp2(zs1,zs2),x,y,ys) -> le#(x,y)
7.03/2.67	    split#(x,cons(y,ys)) -> split#(x,ys) ->
7.03/2.67	    split#(x,cons(y,ys)) -> ?1#(split(x,ys),x,y,ys)
7.03/2.67	    split#(x,cons(y,ys)) -> split#(x,ys) ->
7.03/2.67	    split#(x,cons(y,ys)) -> split#(x,ys)
7.03/2.67	    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
7.03/2.67	   SCC Processor:
7.03/2.67	    #sccs: 2
7.03/2.67	    #rules: 2
7.03/2.67	    #arcs: 6/25
7.03/2.67	    DPs:
7.03/2.67	     split#(x,cons(y,ys)) -> split#(x,ys)
7.03/2.67	    TRS:
7.03/2.67	     le(0(),y) -> true()
7.03/2.67	     split(x,nil()) -> tp2(nil(),nil())
7.03/2.67	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.03/2.67	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.03/2.67	     ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.03/2.67	     le(s(x),s(y)) -> le(x,y)
7.03/2.67	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.03/2.67	     le(s(x),0()) -> false()
7.03/2.67	    Subterm Criterion Processor:
7.03/2.67	     simple projection:
7.03/2.67	      pi(split#) = 1
7.03/2.67	     problem:
7.03/2.67	      DPs:
7.03/2.67	       
7.03/2.67	      TRS:
7.03/2.67	       le(0(),y) -> true()
7.03/2.67	       split(x,nil()) -> tp2(nil(),nil())
7.03/2.67	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.03/2.67	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.03/2.67	       ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.03/2.67	       le(s(x),s(y)) -> le(x,y)
7.03/2.67	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.03/2.67	       le(s(x),0()) -> false()
7.03/2.67	     Qed
7.03/2.67	    
7.03/2.67	    DPs:
7.03/2.67	     le#(s(x),s(y)) -> le#(x,y)
7.03/2.67	    TRS:
7.03/2.67	     le(0(),y) -> true()
7.03/2.67	     split(x,nil()) -> tp2(nil(),nil())
7.03/2.67	     split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.03/2.67	     ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.03/2.68	     ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.20/2.70	     le(s(x),s(y)) -> le(x,y)
7.20/2.70	     ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.20/2.70	     le(s(x),0()) -> false()
7.20/2.70	    Subterm Criterion Processor:
7.20/2.70	     simple projection:
7.20/2.70	      pi(le#) = 0
7.20/2.70	     problem:
7.20/2.70	      DPs:
7.20/2.70	       
7.20/2.70	      TRS:
7.20/2.70	       le(0(),y) -> true()
7.20/2.70	       split(x,nil()) -> tp2(nil(),nil())
7.20/2.70	       split(x,cons(y,ys)) -> ?1(split(x,ys),x,y,ys)
7.20/2.70	       ?1(tp2(zs1,zs2),x,y,ys) -> ?2(le(x,y),zs2,x,ys,zs1,y)
7.20/2.70	       ?2(true(),zs2,x,ys,zs1,y) -> tp2(zs1,cons(y,zs2))
7.20/2.70	       le(s(x),s(y)) -> le(x,y)
7.20/2.70	       ?2(false(),zs2,x,ys,zs1,y) -> tp2(cons(y,zs1),zs2)
7.20/2.70	       le(s(x),0()) -> false()
7.20/2.70	     Qed
7.20/2.70	All 2 critical pairs are joinable.
7.20/2.70	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.20/2.70	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.20/2.70	This critical pair is unfeasible.
7.20/2.70	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.20/2.70	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.20/2.70	This critical pair is unfeasible.
7.20/2.70	
7.20/2.73	EOF