0.00/1.01	YES
0.00/1.01	
0.00/1.01	Problem:
0.00/1.01	add(x, 0()) -> x
0.00/1.01	add(x, s(y)) -> s(z) <= add(x, y) = z
0.00/1.01	
0.00/1.01	Proof:
0.00/1.01	This system is confluent.
0.00/1.01	By \cite{ALS94}, Theorem 4.1.
0.00/1.01	This system is of type 3 or smaller.
0.00/1.01	This system is strongly deterministic.
0.00/1.01	All 0 critical pairs are joinable.
0.00/1.01	This system is quasi-decreasing.
0.00/1.01	By \cite{O02}, p. 214, Proposition 7.2.50.
0.00/1.01	This system is of type 3 or smaller.
0.00/1.01	This system is deterministic.
0.00/1.01	System R transformed to optimized U(R).
0.00/1.01	This system is terminating.
0.00/1.01	Call external tool:
0.00/1.01	./ttt2.sh
0.00/1.01	Input:
0.00/1.01	  add(x, 0()) -> x
0.00/1.01	  ?1(z, x, y) -> s(z)
0.00/1.01	  add(x, s(y)) -> ?1(add(x, y), x, y)
0.00/1.01	
0.00/1.01	 DP Processor:
0.00/1.01	  DPs:
0.00/1.01	   add#(x,s(y)) -> add#(x,y)
0.00/1.01	   add#(x,s(y)) -> ?1#(add(x,y),x,y)
0.00/1.01	  TRS:
0.00/1.01	   add(x,0()) -> x
0.00/1.01	   ?1(z,x,y) -> s(z)
0.00/1.01	   add(x,s(y)) -> ?1(add(x,y),x,y)
0.00/1.01	  TDG Processor:
0.00/1.01	   DPs:
0.00/1.01	    add#(x,s(y)) -> add#(x,y)
0.00/1.01	    add#(x,s(y)) -> ?1#(add(x,y),x,y)
0.00/1.01	   TRS:
0.00/1.01	    add(x,0()) -> x
0.00/1.01	    ?1(z,x,y) -> s(z)
0.00/1.01	    add(x,s(y)) -> ?1(add(x,y),x,y)
0.00/1.01	   graph:
0.00/1.01	    add#(x,s(y)) -> add#(x,y) -> add#(x,s(y)) -> ?1#(add(x,y),x,y)
0.00/1.01	    add#(x,s(y)) -> add#(x,y) -> add#(x,s(y)) -> add#(x,y)
0.00/1.01	   SCC Processor:
0.00/1.01	    #sccs: 1
0.00/1.01	    #rules: 1
0.00/1.01	    #arcs: 2/4
0.00/1.01	    DPs:
0.00/1.01	     add#(x,s(y)) -> add#(x,y)
0.00/1.01	    TRS:
0.00/1.01	     add(x,0()) -> x
0.00/1.01	     ?1(z,x,y) -> s(z)
0.00/1.01	     add(x,s(y)) -> ?1(add(x,y),x,y)
0.00/1.01	    Subterm Criterion Processor:
0.00/1.01	     simple projection:
0.00/1.01	      pi(add#) = 1
0.00/1.01	     problem:
0.00/1.01	      DPs:
0.00/1.01	       
0.00/1.01	      TRS:
0.00/1.01	       add(x,0()) -> x
0.00/1.01	       ?1(z,x,y) -> s(z)
0.00/1.01	       add(x,s(y)) -> ?1(add(x,y),x,y)
0.00/1.01	     Qed
0.00/1.01	
2.27/1.05	EOF