0.00/0.67 NO 0.00/0.67 0.00/0.67 Problem: 0.00/0.67 up(x) -> x 0.00/0.67 down(x) -> x 0.00/0.67 up(x) -> up(s(x)) 0.00/0.67 down(s(x)) -> down(x) 0.00/0.67 between(x, y, z) -> true() <= up(x) = y, down(z) = y 0.00/0.67 0.00/0.67 Proof: 0.00/0.67 This system is not confluent. 0.00/0.68 This system is oriented. 0.00/0.68 For the unconditional CP x = up(s(x)) the left- and right-hand sides are not joinable wrt R_u. 0.00/0.68 Call external tool: 0.00/0.68 ./csi.sh 0.00/0.68 Input: 0.00/0.68 up(x) -> x 0.00/0.68 down(x) -> x 0.00/0.68 up(x) -> up(s(x)) 0.00/0.68 down(s(x)) -> down(x) 0.00/0.68 between(x, y, z) -> true() 0.00/0.68 0.00/0.68 Nonconfluence Processor: 0.00/0.68 terms: f5() *<- f5() ->* up(s(f5())) 0.00/0.68 Qed 0.00/0.68 0.00/0.68 first automaton: 0.00/0.68 final states: {1} 0.00/0.68 transitions: 0.00/0.68 f5() -> 1* 0.00/0.68 0.00/0.68 second automaton: 0.00/0.68 final states: {2} 0.00/0.68 transitions: 0.00/0.68 up(4) -> 2* 0.00/0.68 s(4) -> 4* 0.00/0.68 s(3) -> 4* 0.00/0.68 f5() -> 3* 0.00/0.68 4 -> 2* 0.00/0.68 0.00/0.86 EOF