YES Problem: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) Proof: DP Processor: DPs: q0#(0(x1)) -> q1#(x1) q0#(0(x1)) -> 0'#(q1(x1)) q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) 0#(q1(1(x1))) -> 1'#(x1) 0#(q1(1(x1))) -> 0#(1'(x1)) 0#(q1(1(x1))) -> q2#(0(1'(x1))) 0'#(q1(1(x1))) -> 1'#(x1) 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(x1) 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) q0#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) Matrix Interpretation Processor: dim=3 interpretation: [q3#](x0) = [1 0 1]x0, [q2#](x0) = [1 0 0]x0 + [1], [1'#](x0) = [1 1 0]x0, [0#](x0) = [1 1 0]x0, [0'#](x0) = [1 1 0]x0, [q1#](x0) = [1 1 1]x0, [q0#](x0) = [1 1 1]x0, [0 0 0] [q4](x0) = [1 0 0]x0 [0 1 0] , [0 0 0] [b](x0) = [0 0 0]x0 [1 1 1] , [0 0 0] [q3](x0) = [0 0 0]x0 [0 0 1] , [1 0 1] [1] [q2](x0) = [0 1 1]x0 + [0] [0 0 0] [0], [1 1 1] [1] [1](x0) = [0 1 1]x0 + [1] [0 0 0] [0], [1 1 0] [0] [1'](x0) = [1 0 0]x0 + [0] [0 0 1] [1], [1 1 1] [0'](x0) = [0 0 0]x0 [0 0 0] , [1 1 0] [q1](x0) = [1 0 0]x0 [0 0 1] , [1 1 0] [q0](x0) = [0 0 0]x0 [0 0 1] , [1 1 1] [0] [0](x0) = [1 0 0]x0 + [0] [0 0 0] [1] orientation: q0#(0(x1)) = [2 1 1]x1 + [1] >= [1 1 1]x1 = q1#(x1) q0#(0(x1)) = [2 1 1]x1 + [1] >= [2 1 0]x1 = 0'#(q1(x1)) q1#(0(x1)) = [2 1 1]x1 + [1] >= [1 1 1]x1 = q1#(x1) q1#(0(x1)) = [2 1 1]x1 + [1] >= [2 1 0]x1 = 0#(q1(x1)) q1#(1'(x1)) = [2 1 1]x1 + [1] >= [1 1 1]x1 = q1#(x1) q1#(1'(x1)) = [2 1 1]x1 + [1] >= [2 1 0]x1 = 1'#(q1(x1)) 0#(q1(1(x1))) = [2 3 3]x1 + [3] >= [1 1 0]x1 = 1'#(x1) 0#(q1(1(x1))) = [2 3 3]x1 + [3] >= [2 1 0]x1 = 0#(1'(x1)) 0#(q1(1(x1))) = [2 3 3]x1 + [3] >= [2 1 1]x1 + [2] = q2#(0(1'(x1))) 0'#(q1(1(x1))) = [2 3 3]x1 + [3] >= [1 1 0]x1 = 1'#(x1) 0'#(q1(1(x1))) = [2 3 3]x1 + [3] >= [2 1 0]x1 = 0'#(1'(x1)) 0'#(q1(1(x1))) = [2 3 3]x1 + [3] >= [2 1 1]x1 + [2] = q2#(0'(1'(x1))) 1'#(q1(1(x1))) = [2 3 3]x1 + [3] >= [1 1 0]x1 = 1'#(x1) 1'#(q1(1(x1))) = [2 3 3]x1 + [3] >= [2 1 0]x1 = 1'#(1'(x1)) 1'#(q1(1(x1))) = [2 3 3]x1 + [3] >= [2 1 0]x1 + [1] = q2#(1'(1'(x1))) 0#(q2(0(x1))) = [2 1 1]x1 + [3] >= [2 1 1]x1 = 0#(0(x1)) 0#(q2(0(x1))) = [2 1 1]x1 + [3] >= [2 1 1]x1 + [2] = q2#(0(0(x1))) 0'#(q2(0(x1))) = [2 1 1]x1 + [3] >= [2 1 1]x1 = 0'#(0(x1)) 0'#(q2(0(x1))) = [2 1 1]x1 + [3] >= [2 1 1]x1 + [2] = q2#(0'(0(x1))) 1'#(q2(0(x1))) = [2 1 1]x1 + [3] >= [2 1 1]x1 = 1'#(0(x1)) 1'#(q2(0(x1))) = [2 1 1]x1 + [3] >= [2 1 1]x1 + [1] = q2#(1'(0(x1))) 0#(q2(1'(x1))) = [2 1 2]x1 + [3] >= [2 1 0]x1 = 0#(1'(x1)) 0#(q2(1'(x1))) = [2 1 2]x1 + [3] >= [2 1 1]x1 + [2] = q2#(0(1'(x1))) 0'#(q2(1'(x1))) = [2 1 2]x1 + [3] >= [2 1 0]x1 = 0'#(1'(x1)) 0'#(q2(1'(x1))) = [2 1 2]x1 + [3] >= [2 1 1]x1 + [2] = q2#(0'(1'(x1))) 1'#(q2(1'(x1))) = [2 1 2]x1 + [3] >= [2 1 0]x1 = 1'#(1'(x1)) 1'#(q2(1'(x1))) = [2 1 2]x1 + [3] >= [2 1 0]x1 + [1] = q2#(1'(1'(x1))) q2#(0'(x1)) = [1 1 1]x1 + [1] >= [1 1 1]x1 = q0#(x1) q2#(0'(x1)) = [1 1 1]x1 + [1] >= [1 1 0]x1 = 0'#(q0(x1)) q0#(1'(x1)) = [2 1 1]x1 + [1] >= [1 0 1]x1 = q3#(x1) q0#(1'(x1)) = [2 1 1]x1 + [1] >= [0] = 1'#(q3(x1)) q3#(1'(x1)) = [1 1 1]x1 + [1] >= [1 0 1]x1 = q3#(x1) q3#(1'(x1)) = [1 1 1]x1 + [1] >= [0] = 1'#(q3(x1)) [2 1 1] [0] [2 1 1] q0(0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0'(q1(x1)) [0 0 0] [1] [0 0 0] [2 1 1] [0] [2 1 1] [0] q1(0(x1)) = [1 1 1]x1 + [0] >= [1 1 0]x1 + [0] = 0(q1(x1)) [0 0 0] [1] [0 0 0] [1] [2 1 0] [0] [2 1 0] [0] q1(1'(x1)) = [1 1 0]x1 + [0] >= [1 1 0]x1 + [0] = 1'(q1(x1)) [0 0 1] [1] [0 0 1] [1] [2 3 3] [3] [2 1 1] [3] 0(q1(1(x1))) = [1 2 2]x1 + [2] >= [1 1 0]x1 + [1] = q2(0(1'(x1))) [0 0 0] [1] [0 0 0] [0] [2 3 3] [3] [2 1 1] [2] 0'(q1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0'(1'(x1))) [0 0 0] [0] [0 0 0] [0] [2 3 3] [3] [2 1 1] [3] 1'(q1(1(x1))) = [1 2 2]x1 + [2] >= [1 1 1]x1 + [2] = q2(1'(1'(x1))) [0 0 0] [1] [0 0 0] [0] [2 1 1] [3] [2 1 1] [3] 0(q2(0(x1))) = [1 1 1]x1 + [2] >= [1 1 1]x1 + [1] = q2(0(0(x1))) [0 0 0] [1] [0 0 0] [0] [2 1 1] [3] [2 1 1] [2] 0'(q2(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0'(0(x1))) [0 0 0] [0] [0 0 0] [0] [2 1 1] [3] [2 1 1] [3] 1'(q2(0(x1))) = [1 1 1]x1 + [2] >= [1 1 1]x1 + [2] = q2(1'(0(x1))) [0 0 0] [1] [0 0 0] [0] [2 1 2] [3] [2 1 1] [3] 0(q2(1'(x1))) = [1 1 1]x1 + [2] >= [1 1 0]x1 + [1] = q2(0(1'(x1))) [0 0 0] [1] [0 0 0] [0] [2 1 2] [3] [2 1 1] [2] 0'(q2(1'(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0'(1'(x1))) [0 0 0] [0] [0 0 0] [0] [2 1 2] [3] [2 1 1] [3] 1'(q2(1'(x1))) = [1 1 1]x1 + [2] >= [1 1 1]x1 + [2] = q2(1'(1'(x1))) [0 0 0] [1] [0 0 0] [0] [1 1 1] [1] [1 1 1] q2(0'(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = 0'(q0(x1)) [0 0 0] [0] [0 0 0] [2 1 0] [0] [0 0 0] [0] q0(1'(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1'(q3(x1)) [0 0 1] [1] [0 0 1] [1] [0 0 0] [0] [0 0 0] [0] q3(1'(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1'(q3(x1)) [0 0 1] [1] [0 0 1] [1] [0 0 0] [0 0 0] q3(b(x1)) = [0 0 0]x1 >= [0 0 0]x1 = b(q4(x1)) [1 1 1] [1 1 0] problem: DPs: TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) Qed