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