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