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)))))))))))))))))))))))))))))))))))))))))))))) 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(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)))))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))))) 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(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)))))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))))))))))) 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(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)))))))))))))))))))))))))))))))))))))))))))))) 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(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#(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(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#(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(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))))))))))))))))))))))))))))))))))))))))))))) 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(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))))))))))))))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 54/324 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)))))))))))))))))))))))))))))))))))))))))))))) 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(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))))))))))))))))))))))))))))))))))))) 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)))))))))))))))))))))))))))))))))))))))))))))) 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(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))))) interpretation: [1#](x0) = x0 + 0, [0](x0) = 12x0 + 14, [2](x0) = -12x0 + 0, [1](x0) = x0 + 1 orientation: 1#(2(1(0(x1)))) = x1 + 2 >= -12x1 + 0 = 1#(2(1(x1))) 1#(2(1(0(x1)))) = x1 + 2 >= -12x1 + 1 = 1#(1(2(1(x1)))) 1#(2(1(0(x1)))) = x1 + 2 >= x1 + 0 = 1#(x1) 1(2(1(0(x1)))) = x1 + 2 >= -12x1 + 2 = 2(1(0(2(1(0(1(1(2(1(x1)))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -12x1 + 2 = 2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -12x1 + 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 >= -12x1 + 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 >= -12x1 + 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 >= -12x1 + 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 >= -12x1 + 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 >= -12x1 + 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 >= -12x1 + 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 >= -12x1 + 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))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -12x1 + 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(2(1 ( 0 ( 1 ( 1 ( 2(1(x1)))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -12x1 + 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(2(1 ( 0 ( 2 ( 1 ( 0 ( 1 ( 1 ( 2(1(x1))))))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -12x1 + 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(2(1 ( 0 ( 2 ( 1 ( 0 ( 2 ( 1 ( 0 ( 1 ( 1 ( 2(1(x1)))))))))))))))))))))))))))))))))))))))))))))) 1(2(1(0(x1)))) = x1 + 2 >= -12x1 + 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(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)))))))))))))))))))))))))))))))))))))))))))))) 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(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)))))))))))))))))))))))))))))))))))))))))))))) 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(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)))))))))))))))))))))))))))))))))))))))))))))) 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(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)))))))))))))))))))))))))))))))))))))))))))))) 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(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))))) graph: Qed