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