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