4.78/2.26	YES
4.78/2.26	
4.78/2.27	Proof:
4.78/2.27	This system is confluent.
4.78/2.27	By \cite{ALS94}, Theorem 4.1.
4.78/2.27	This system is of type 3 or smaller.
4.78/2.28	This system is strongly deterministic.
4.78/2.28	This system is quasi-decreasing.
4.78/2.28	By \cite{A14}, Theorem 11.5.9.
4.78/2.28	This system is of type 3 or smaller.
4.78/2.28	This system is deterministic.
4.78/2.28	System R transformed to V(R) + Emb.
4.78/2.28	This system is terminating.
4.78/2.28	Call external tool:
4.78/2.28	./ttt2.sh
4.78/2.28	Input:
4.78/2.28	(VAR X Y x y)
4.78/2.28	(RULES
4.78/2.28	  plus(0, X) -> X
4.78/2.28	  plus(s(X), Y) -> plus(X, s(Y))
4.78/2.28	  fib(0) -> pair(s(0), 0)
4.78/2.28	  fib(s(X)) -> pair(plus(fib(X), fib(X)), fib(X))
4.78/2.28	  fib(s(X)) -> plus(fib(X), fib(X))
4.78/2.28	  fib(s(X)) -> fib(X)
4.78/2.28	  pair(x, y) -> x
4.78/2.28	  pair(x, y) -> y
4.78/2.28	  s(x) -> x
4.78/2.28	  fib(x) -> x
4.78/2.28	  plus(x, y) -> x
4.78/2.28	  plus(x, y) -> y
4.78/2.28	)
4.78/2.28	
4.78/2.28	 DP Processor:
4.78/2.28	  DPs:
4.78/2.28	   plus#(s(X),Y) -> s#(Y)
4.78/2.28	   plus#(s(X),Y) -> plus#(X,s(Y))
4.78/2.28	   fib#(0()) -> s#(0())
4.78/2.28	   fib#(0()) -> pair#(s(0()),0())
4.78/2.28	   fib#(s(X)) -> fib#(X)
4.78/2.28	   fib#(s(X)) -> plus#(fib(X),fib(X))
4.78/2.28	   fib#(s(X)) -> pair#(plus(fib(X),fib(X)),fib(X))
4.78/2.28	  TRS:
4.78/2.28	   plus(0(),X) -> X
4.78/2.28	   plus(s(X),Y) -> plus(X,s(Y))
4.78/2.28	   fib(0()) -> pair(s(0()),0())
4.78/2.28	   fib(s(X)) -> pair(plus(fib(X),fib(X)),fib(X))
4.78/2.28	   fib(s(X)) -> plus(fib(X),fib(X))
4.78/2.28	   fib(s(X)) -> fib(X)
4.78/2.28	   pair(x,y) -> x
4.78/2.28	   pair(x,y) -> y
4.78/2.28	   s(x) -> x
4.78/2.28	   fib(x) -> x
4.78/2.28	   plus(x,y) -> x
4.78/2.28	   plus(x,y) -> y
4.78/2.28	  TDG Processor:
4.78/2.28	   DPs:
4.78/2.28	    plus#(s(X),Y) -> s#(Y)
4.78/2.28	    plus#(s(X),Y) -> plus#(X,s(Y))
4.78/2.28	    fib#(0()) -> s#(0())
4.78/2.28	    fib#(0()) -> pair#(s(0()),0())
4.78/2.28	    fib#(s(X)) -> fib#(X)
4.78/2.28	    fib#(s(X)) -> plus#(fib(X),fib(X))
4.78/2.28	    fib#(s(X)) -> pair#(plus(fib(X),fib(X)),fib(X))
4.78/2.28	   TRS:
4.78/2.28	    plus(0(),X) -> X
4.78/2.28	    plus(s(X),Y) -> plus(X,s(Y))
4.78/2.28	    fib(0()) -> pair(s(0()),0())
4.78/2.28	    fib(s(X)) -> pair(plus(fib(X),fib(X)),fib(X))
4.78/2.28	    fib(s(X)) -> plus(fib(X),fib(X))
4.78/2.28	    fib(s(X)) -> fib(X)
4.78/2.28	    pair(x,y) -> x
4.78/2.28	    pair(x,y) -> y
4.78/2.28	    s(x) -> x
4.78/2.28	    fib(x) -> x
4.78/2.28	    plus(x,y) -> x
4.78/2.28	    plus(x,y) -> y
4.78/2.28	   graph:
4.78/2.28	    fib#(s(X)) -> fib#(X) -> fib#(s(X)) -> pair#(plus(fib(X),fib(X)),fib(X))
4.78/2.28	    fib#(s(X)) -> fib#(X) -> fib#(s(X)) -> plus#(fib(X),fib(X))
4.78/2.28	    fib#(s(X)) -> fib#(X) -> fib#(s(X)) -> fib#(X)
4.78/2.28	    fib#(s(X)) -> fib#(X) -> fib#(0()) -> pair#(s(0()),0())
4.78/2.28	    fib#(s(X)) -> fib#(X) -> fib#(0()) -> s#(0())
4.78/2.28	    fib#(s(X)) -> plus#(fib(X),fib(X)) ->
4.78/2.28	    plus#(s(X),Y) -> plus#(X,s(Y))
4.78/2.28	    fib#(s(X)) -> plus#(fib(X),fib(X)) -> plus#(s(X),Y) -> s#(Y)
4.78/2.28	    plus#(s(X),Y) -> plus#(X,s(Y)) -> plus#(s(X),Y) -> plus#(X,s(Y))
4.78/2.28	    plus#(s(X),Y) -> plus#(X,s(Y)) -> plus#(s(X),Y) -> s#(Y)
4.78/2.28	   SCC Processor:
4.78/2.28	    #sccs: 2
4.78/2.28	    #rules: 2
4.78/2.28	    #arcs: 9/49
4.78/2.28	    DPs:
4.78/2.28	     fib#(s(X)) -> fib#(X)
4.78/2.28	    TRS:
4.78/2.28	     plus(0(),X) -> X
4.78/2.28	     plus(s(X),Y) -> plus(X,s(Y))
4.78/2.28	     fib(0()) -> pair(s(0()),0())
4.78/2.28	     fib(s(X)) -> pair(plus(fib(X),fib(X)),fib(X))
4.78/2.28	     fib(s(X)) -> plus(fib(X),fib(X))
4.78/2.28	     fib(s(X)) -> fib(X)
4.78/2.28	     pair(x,y) -> x
4.78/2.28	     pair(x,y) -> y
4.78/2.28	     s(x) -> x
4.78/2.28	     fib(x) -> x
4.78/2.28	     plus(x,y) -> x
4.78/2.28	     plus(x,y) -> y
4.78/2.28	    Subterm Criterion Processor:
4.78/2.28	     simple projection:
4.78/2.28	      pi(fib#) = 0
4.78/2.28	     problem:
4.78/2.28	      DPs:
4.78/2.28	       
4.78/2.28	      TRS:
4.78/2.28	       plus(0(),X) -> X
4.78/2.28	       plus(s(X),Y) -> plus(X,s(Y))
4.78/2.28	       fib(0()) -> pair(s(0()),0())
4.78/2.28	       fib(s(X)) -> pair(plus(fib(X),fib(X)),fib(X))
4.78/2.28	       fib(s(X)) -> plus(fib(X),fib(X))
4.78/2.28	       fib(s(X)) -> fib(X)
4.78/2.28	       pair(x,y) -> x
4.78/2.28	       pair(x,y) -> y
4.78/2.28	       s(x) -> x
4.78/2.28	       fib(x) -> x
4.78/2.28	       plus(x,y) -> x
4.78/2.28	       plus(x,y) -> y
4.78/2.28	     Qed
4.78/2.28	    
4.78/2.28	    DPs:
4.78/2.28	     plus#(s(X),Y) -> plus#(X,s(Y))
4.78/2.28	    TRS:
4.78/2.28	     plus(0(),X) -> X
4.78/2.28	     plus(s(X),Y) -> plus(X,s(Y))
4.78/2.28	     fib(0()) -> pair(s(0()),0())
4.78/2.28	     fib(s(X)) -> pair(plus(fib(X),fib(X)),fib(X))
4.78/2.28	     fib(s(X)) -> plus(fib(X),fib(X))
4.78/2.28	     fib(s(X)) -> fib(X)
4.78/2.28	     pair(x,y) -> x
4.78/2.28	     pair(x,y) -> y
4.78/2.28	     s(x) -> x
4.78/2.28	     fib(x) -> x
4.78/2.28	     plus(x,y) -> x
4.78/2.28	     plus(x,y) -> y
4.78/2.28	    Subterm Criterion Processor:
4.78/2.28	     simple projection:
4.78/2.28	      pi(plus#) = 0
4.78/2.28	     problem:
4.78/2.28	      DPs:
4.78/2.28	       
4.78/2.28	      TRS:
4.78/2.28	       plus(0(),X) -> X
4.78/2.28	       plus(s(X),Y) -> plus(X,s(Y))
4.78/2.28	       fib(0()) -> pair(s(0()),0())
4.78/2.28	       fib(s(X)) -> pair(plus(fib(X),fib(X)),fib(X))
4.78/2.28	       fib(s(X)) -> plus(fib(X),fib(X))
4.78/2.28	       fib(s(X)) -> fib(X)
4.78/2.28	       pair(x,y) -> x
4.78/2.28	       pair(x,y) -> y
4.78/2.28	       s(x) -> x
4.78/2.28	       fib(x) -> x
4.78/2.28	       plus(x,y) -> x
4.78/2.28	       plus(x,y) -> y
4.78/2.28	     Qed
4.78/2.28	All 0 critical pairs are joinable.
4.78/2.28	
5.08/2.30	EOF