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))))))))))))))))))))))))))))))))))))) 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))))))))))))))))))))))))))))))))))))) 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)))))))))))))))))))))))))))))))))))) 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))))))))))))))))))))))))))))))))))))) 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)))))))))))))))))))))))))))))))))))) 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))))))))))))))))))))))))))))))))))))) 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#(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#(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)))))))))))))))))))))))))))))))))))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 42/196 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))))))))))))))))))))))))))))))))))))) 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))))))))))))))))))))))))))))))))))))) interpretation: [1#](x0) = 7x0 + 0, [0](x0) = 3x0 + 5, [2](x0) = -3x0 + 0, [1](x0) = x0 + 1 orientation: 1#(2(1(0(x1)))) = 7x1 + 9 >= 4x1 + 7 = 1#(2(1(x1))) 1#(2(1(0(x1)))) = 7x1 + 9 >= 4x1 + 8 = 1#(1(2(1(x1)))) 1#(2(1(0(x1)))) = 7x1 + 9 >= 7x1 + 0 = 1#(x1) 1(2(1(0(x1)))) = x1 + 2 >= -3x1 + 2 = 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -3x1 + 2 = 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -3x1 + 2 = 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -3x1 + 2 = 2(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 + 2 >= -3x1 + 2 = 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 + 2 >= -3x1 + 2 = 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 + 2 >= -3x1 + 2 = 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 + 2 >= -3x1 + 2 = 2(1(0(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 + 2 >= -3x1 + 2 = 2(1(0(2(1(0(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 + 2 >= -3x1 + 2 = 2(1(0(2(1(0(2(1(0(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))))))))))))))))))))))))))))))))))))) 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))))))))))))))))))))))))))))))))))))) 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))))))))))))))))))))))))))))))))))))) 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))))))))))))))))))))))))))))))))))))) graph: Qed