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