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