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))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))) 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(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)))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))) 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(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)))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))) 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(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#(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(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#(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(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)))))))))))))))))))))))))))))))))))))))))) 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(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 51/289 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))))))))))))))))))))))))))))))))))))))))))) 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(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(187) -> 188* 11(132) -> 133* 11(92) -> 93* 11(87) -> 88* 11(57) -> 58* 11(32) -> 33* 11(89) -> 90* 11(155) -> 156* 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}(209) -> 210* 1{#,0}(159) -> 160* 1{#,0}(9) -> 5* 1{#,0}(185) -> 186* 1{#,0}(120) -> 121* 9 -> 15* 16 -> 120,57 19 -> 7,16,47,30 22 -> 9* 32 -> 45* 33 -> 87,77 34 -> 186,121,48,5 46 -> 186,121,48,5 48 -> 5* 58 -> 31* 78 -> 209,187 81 -> 185,130 84 -> 16* 94 -> 131,58,105,31 106 -> 92* 121 -> 48,5 132 -> 159* 133 -> 155* 134 -> 121* 156 -> 88* 160 -> 121,48 186 -> 121,48 188 -> 31* 210 -> 186,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))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))) 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(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) Arctic Interpretation Processor: dimension: 1 usable rules: 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))))))))))))))))))))))))))))))))))))))))))) 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(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))))))) interpretation: [1#](x0) = x0 + 4, [0](x0) = 2x0 + 8, [2](x0) = -2x0 + 2, [1](x0) = x0 orientation: 1#(2(1(0(x1)))) = x1 + 6 >= -2x1 + 4 = 1#(2(1(x1))) 1#(2(1(0(x1)))) = x1 + 6 >= x1 + 4 = 1#(x1) 1(2(1(0(x1)))) = x1 + 6 >= -2x1 + 6 = 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) = x1 + 6 >= -2x1 + 6 = 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) = x1 + 6 >= -2x1 + 6 = 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) = x1 + 6 >= -2x1 + 6 = 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)))) = x1 + 6 >= -2x1 + 6 = 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)))) = x1 + 6 >= -2x1 + 6 = 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)))) = x1 + 6 >= -2x1 + 6 = 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)))) = x1 + 6 >= -2x1 + 6 = 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)))) = x1 + 6 >= -2x1 + 6 = 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)))) = x1 + 6 >= -2x1 + 6 = 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)))) = x1 + 6 >= -2x1 + 6 = 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)))) = x1 + 6 >= -2x1 + 6 = 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))))))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) = x1 + 6 >= -2x1 + 6 = 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 ( 2 ( 1 ( 0 ( 1 ( 1 ( 2(1(x1)))))))))))))))))))))))))))))))))))))))))))))) 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))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))) 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(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))))))) graph: Qed