0.00/0.56 YES 0.00/0.56 0.00/0.56 Problem: 0.00/0.56 plus(0(), X) -> X 0.00/0.56 plus(s(X), Y) -> plus(X, s(Y)) 0.00/0.56 fib(0()) -> pair(s(0()), 0()) 0.00/0.56 fib(s(X)) -> pair(W, Y) <= fib(X) = pair(Y, Z), plus(Y, Z) = W 0.00/0.56 0.00/0.56 Proof: 0.00/0.56 This system is confluent. 0.00/0.56 By \cite{SMI95}, Corollary 4.7 or 5.3. 0.00/0.56 This system is oriented. 0.00/0.56 This system is of type 3 or smaller. 0.00/0.56 This system is right-stable. 0.00/0.56 This system is properly oriented. 0.00/0.56 This is an overlay system. 0.00/0.56 This system is left-linear. 0.00/0.56 All 0 critical pairs are trivial or infeasible. 0.00/0.56 0.00/0.58 EOF