YES Problem: 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1)))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))) 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))) Proof: String Reversal Processor: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) DP Processor: DPs: 1#(2(1(0(x1)))) -> 1#(x1) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) 1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1)))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) EDG Processor: DPs: 1#(2(1(0(x1)))) -> 1#(x1) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) 1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1)))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) graph: 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(x1) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1)))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(x1) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1)))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(x1) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1)))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 48/256 DPs: 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) 1#(2(1(0(x1)))) -> 1#(x1) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {5} transitions: 20(7) -> 8* 20(21) -> 22* 20(83) -> 84* 20(18) -> 19* 20(80) -> 81* 10(20) -> 21* 10(15) -> 16* 10(82) -> 83* 10(77) -> 78* 10(17) -> 18* 10(79) -> 80* 10(6) -> 7* 10(8) -> 9* 00(19) -> 20* 00(81) -> 82* 00(16) -> 17* 00(78) -> 79* 1{#,1}(133) -> 134* 1{#,1}(33) -> 34* 11(30) -> 31* 11(132) -> 133* 11(92) -> 93* 11(87) -> 88* 11(57) -> 58* 11(32) -> 33* 11(89) -> 90* 11(151) -> 152* 11(183) -> 184* 11(130) -> 131* 21(131) -> 132* 21(31) -> 32* 21(93) -> 94* 21(90) -> 91* 01(91) -> 92* 01(88) -> 89* 01(105) -> 106* f50() -> 6* 1{#,0}(45) -> 46* 1{#,0}(47) -> 48* 1{#,0}(216) -> 217* 1{#,0}(9) -> 5* 1{#,0}(181) -> 182* 1{#,0}(166) -> 167* 1{#,0}(120) -> 121* 9 -> 15* 16 -> 120,57 19 -> 7,16,47,30 22 -> 9* 32 -> 45* 33 -> 87,77 34 -> 182,121,48,5 46 -> 182,121,48,5 48 -> 5* 58 -> 31* 78 -> 216,183 81 -> 181,130 84 -> 16* 94 -> 131,58,105,31 106 -> 92* 121 -> 48,5 132 -> 166* 133 -> 151* 134 -> 121* 152 -> 88* 167 -> 121,48 182 -> 121,48 184 -> 31* 217 -> 182,121 problem: DPs: 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(x1) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2 ( 1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) Restore Modifier: DPs: 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(x1) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2 ( 1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) EDG Processor: DPs: 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(x1) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0( 2 ( 1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) graph: 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(x1) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(2(1(x1))) 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(x1) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: f150() -> 2* 20(45) -> 46* 20(20) -> 21* 20(77) -> 78* 20(57) -> 58* 20(17) -> 18* 20(139) -> 140* 20(109) -> 110* 20(89) -> 90* 20(24) -> 25* 20(161) -> 162* 20(136) -> 137* 20(131) -> 132* 20(61) -> 62* 20(41) -> 42* 20(158) -> 159* 20(153) -> 154* 20(93) -> 94* 20(73) -> 74* 20(3) -> 4* 20(105) -> 106* 10(60) -> 61* 10(40) -> 41* 10(167) -> 168* 10(157) -> 158* 10(152) -> 153* 10(132) -> 133* 10(92) -> 93* 10(72) -> 73* 10(2) -> 3* 10(154) -> 155* 10(104) -> 105* 10(44) -> 45* 10(19) -> 20* 10(14) -> 15* 10(76) -> 77* 10(56) -> 57* 10(16) -> 17* 10(173) -> 174* 10(138) -> 139* 10(133) -> 134* 10(108) -> 109* 10(88) -> 89* 10(23) -> 24* 10(13) -> 14* 10(160) -> 161* 10(155) -> 156* 10(135) -> 136* 10(130) -> 131* 00(75) -> 76* 00(55) -> 56* 00(15) -> 16* 00(137) -> 138* 00(107) -> 108* 00(87) -> 88* 00(22) -> 23* 00(159) -> 160* 00(134) -> 135* 00(59) -> 60* 00(39) -> 40* 00(156) -> 157* 00(91) -> 92* 00(71) -> 72* 00(163) -> 164* 00(103) -> 104* 00(43) -> 44* 00(18) -> 19* 1{#,0}(7) -> 8* 1{#,0}(4) -> 1* 1 -> 8* 2 -> 7* 4 -> 13* 8 -> 1* 15 -> 152* 18 -> 15,130 21 -> 14,22,3 25 -> 39,3 42 -> 43,3 46 -> 55,3 58 -> 59,3 62 -> 71,3 74 -> 75,3 78 -> 87,3 90 -> 91,3 94 -> 103,3 106 -> 107,3 110 -> 3* 134 -> 173* 137 -> 167* 140 -> 15* 162 -> 168,153,163,131 164 -> 160* 168 -> 153* 174 -> 153* problem: DPs: 1#(2(1(0(x1)))) -> 1#(x1) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1( 0 ( 2 ( 1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) Restore Modifier: DPs: 1#(2(1(0(x1)))) -> 1#(x1) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1( 0 ( 2 ( 1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) EDG Processor: DPs: 1#(2(1(0(x1)))) -> 1#(x1) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1 ( 0 ( 2 ( 1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) graph: 1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(x1) CDG Processor: DPs: 1#(2(1(0(x1)))) -> 1#(x1) TRS: 1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2( 1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2( 1 ( 0 ( 2 ( 1 ( 0 ( 2 ( 1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))) graph: Qed