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