1.22/1.35 NO 1.22/1.35 1.22/1.35 Problem: 1.22/1.35 a(b(x)) -> b(c(x)) 1.22/1.35 a(c(x)) -> c(a(x)) 1.22/1.35 b(b(x)) -> a(c(x)) 1.22/1.35 c(b(x)) -> b(c(x)) 1.22/1.35 c(b(x)) -> c(c(x)) 1.22/1.35 c(c(x)) -> c(b(x)) 1.22/1.35 0(1(2(x))) -> 2(0(1(x))) 1.22/1.35 2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x)))))))))))) 1.22/1.35 1.22/1.35 Proof: 1.22/1.35 sorted: (order-sorted) 1.22/1.35 0:0(1(2(x))) -> 2(0(1(x))) 1.22/1.35 2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x)))))))))))) 1.22/1.35 1:a(b(x)) -> b(c(x)) 1.22/1.35 a(c(x)) -> c(a(x)) 1.22/1.35 b(b(x)) -> a(c(x)) 1.22/1.35 c(b(x)) -> b(c(x)) 1.22/1.35 c(b(x)) -> c(c(x)) 1.22/1.35 c(c(x)) -> c(b(x)) 1.22/1.35 ----- 1.22/1.35 sorts 1.22/1.35 [] 1.22/1.35 sort attachment (non-strict) 1.22/1.35 a : 1 -> 1 1.22/1.35 b : 1 -> 1 1.22/1.35 c : 1 -> 1 1.22/1.35 0 : 0 -> 0 1.22/1.35 1 : 0 -> 0 1.22/1.35 2 : 0 -> 0 1.22/1.35 ----- 1.22/1.35 0:0(1(2(x))) -> 2(0(1(x))) 1.22/1.35 2(2(2(2(2(2(2(1(1(1(1(2(x)))))))))))) -> 2(1(2(2(0(1(2(1(1(0(1(0(x)))))))))))) 1.22/1.35 Nonconfluence Processor: 1.22/1.35 terms: 2(0(1(1(2(2(2(0(1(1(1(0(1(0(x270)))))))))))))) *<- 0(1(2(2 1.22/1.35 ( 1.22/1.35 2 1.22/1.35 ( 1.22/1.35 2(2(2(2(1(1(1(1(2(x270)))))))))))))) ->* 1.22/1.35 2(2(2(2(2(2(2(0(1(1(1(1(1(2(x270)))))))))))))) 1.22/1.35 Qed 1.22/1.35 1.22/1.35 1.22/1.35 1:a(b(x)) -> b(c(x)) 1.22/1.35 a(c(x)) -> c(a(x)) 1.22/1.35 b(b(x)) -> a(c(x)) 1.22/1.35 c(b(x)) -> b(c(x)) 1.22/1.35 c(b(x)) -> c(c(x)) 1.22/1.35 c(c(x)) -> c(b(x)) 1.22/1.35 Open 1.22/1.35 1.22/1.35 EOF