YES Problem: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) Proof: DP Processor: DPs: 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> L#(1(0(2(x1)))) 1#(2(0(x1))) -> 1#(x1) 1#(2(0(x1))) -> 0#(1(x1)) 1#(2(R(x1))) -> 1#(R(x1)) 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> L#(1(0(1(x1)))) 0#(2(R(x1))) -> 1#(R(x1)) 0#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(R(x1))) -> 1#(0(1(R(x1)))) TRS: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) TDG Processor: DPs: 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> L#(1(0(2(x1)))) 1#(2(0(x1))) -> 1#(x1) 1#(2(0(x1))) -> 0#(1(x1)) 1#(2(R(x1))) -> 1#(R(x1)) 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> L#(1(0(1(x1)))) 0#(2(R(x1))) -> 1#(R(x1)) 0#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(R(x1))) -> 1#(0(1(R(x1)))) TRS: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) graph: L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(0(x1))) -> L#(1(0(1(x1)))) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(1(x1))) -> L#(1(0(2(x1)))) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(1(x1))) -> 1#(0(2(x1))) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(1(x1))) -> 0#(2(x1)) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) L#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(R(x1))) -> 0#(1(R(x1))) L#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(R(x1))) -> 1#(R(x1)) L#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(1(x1))) -> 0#(2(x1)) L#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 0#(1(R(x1))) L#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 1#(R(x1)) L#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 1#(x1) -> 1#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(0(x1))) -> L#(1(0(1(x1)))) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(0(x1))) -> 1#(0(1(x1))) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(0(x1))) -> 0#(1(x1)) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(0(x1))) -> 1#(x1) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(1(x1))) -> L#(1(0(2(x1)))) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(x1) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(R(x1))) -> 0#(1(R(x1))) L#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(R(x1))) -> 1#(R(x1)) L#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(0(x1))) -> 0#(1(x1)) L#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(0(x1))) -> 1#(x1) L#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) 0#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(R(x1))) -> 1#(R(x1)) 0#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 0#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(0(x1))) -> 1#(x1) 0#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 0#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(1(x1))) -> 0#(2(x1)) 0#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(R(x1))) -> 1#(R(x1)) 0#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(0(x1))) -> 1#(x1) 0#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(R(x1))) -> 1#(0(1(R(x1)))) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(R(x1))) -> 1#(0(1(R(x1)))) -> 1#(2(R(x1))) -> 1#(R(x1)) 0#(2(R(x1))) -> 1#(0(1(R(x1)))) -> 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(R(x1))) -> 1#(0(1(R(x1)))) -> 1#(2(0(x1))) -> 1#(x1) 0#(2(R(x1))) -> 1#(0(1(R(x1)))) -> 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) 0#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(R(x1))) -> 1#(R(x1)) 0#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 1#(R(x1)) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(x1) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(R(x1))) -> 1#(R(x1)) 0#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(0(x1))) -> 1#(x1) 0#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(1(x1))) -> 0#(2(x1)) 1#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) 1#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(R(x1))) -> 0#(1(R(x1))) 1#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(R(x1))) -> 1#(R(x1)) 1#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 1#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(0(x1))) -> 0#(1(x1)) 1#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(0(x1))) -> 1#(x1) 1#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 1#(2(R(x1))) -> 0#(1(R(x1))) -> 0#(2(1(x1))) -> 0#(2(x1)) 1#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 1#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(R(x1))) -> 1#(R(x1)) 1#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(0(x1))) -> 0#(1(x1)) 1#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(0(x1))) -> 1#(x1) 1#(2(R(x1))) -> 1#(R(x1)) -> 1#(2(1(x1))) -> 0#(2(x1)) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(x1) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 1#(R(x1)) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 0#(1(x1)) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 1#(x1) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(1(x1))) -> 0#(2(x1)) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(x1) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) EDG Processor: DPs: 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> L#(1(0(2(x1)))) 1#(2(0(x1))) -> 1#(x1) 1#(2(0(x1))) -> 0#(1(x1)) 1#(2(R(x1))) -> 1#(R(x1)) 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> L#(1(0(1(x1)))) 0#(2(R(x1))) -> 1#(R(x1)) 0#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(R(x1))) -> 1#(0(1(R(x1)))) TRS: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) graph: L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(1(x1))) -> 0#(2(x1)) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(1(x1))) -> 1#(0(2(x1))) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(1(x1))) -> L#(1(0(2(x1)))) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> L#(1(0(1(x1)))) -> L#(2(0(x1))) -> L#(1(0(1(x1)))) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) L#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(1(x1))) -> 0#(2(x1)) L#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 1#(x1) -> 1#(2(1(x1))) -> 0#(2(x1)) L#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 1#(x1) L#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 0#(1(x1)) L#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 1#(R(x1)) L#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 0#(1(R(x1))) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(1(x1))) -> L#(1(0(2(x1)))) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(0(x1))) -> 1#(x1) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(0(x1))) -> 0#(1(x1)) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(0(x1))) -> 1#(0(1(x1))) L#(2(1(x1))) -> L#(1(0(2(x1)))) -> L#(2(0(x1))) -> L#(1(0(1(x1)))) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(x1) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) L#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) L#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(1(x1))) -> 0#(2(x1)) L#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(0(x1))) -> 1#(x1) L#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 0#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 1#(0(1(x1))) -> 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 1#(x1) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 1#(R(x1)) 0#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(x1) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) 0#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) 0#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(0(x1))) -> 1#(x1) 0#(2(1(x1))) -> 1#(0(2(x1))) -> 1#(2(0(x1))) -> 0#(1(x1)) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(x1) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) 1#(2(0(x1))) -> 0#(1(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(1(x1))) -> 0#(2(x1)) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 1#(x1) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(0(x1))) -> 0#(1(x1)) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 1#(R(x1)) 1#(2(0(x1))) -> 1#(x1) -> 1#(2(R(x1))) -> 0#(1(R(x1))) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 0#(2(x1)) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(1(x1))) -> 1#(0(2(x1))) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(x1) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 0#(1(x1)) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(0(x1))) -> 1#(0(1(x1))) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(R(x1)) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 0#(1(R(x1))) 1#(2(1(x1))) -> 0#(2(x1)) -> 0#(2(R(x1))) -> 1#(0(1(R(x1)))) SCC Processor: #sccs: 2 #rules: 10 #arcs: 80/400 DPs: L#(2(0(x1))) -> L#(1(0(1(x1)))) L#(2(1(x1))) -> L#(1(0(2(x1)))) TRS: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) KBO Processor: argument filtering: pi(1) = 0 pi(2) = [] pi(0) = [] pi(L) = [] pi(R) = [] pi(L#) = [0] weight function: w0 = 1 w(L#) = w(R) = w(L) = w(0) = w(2) = 1 w(1) = 0 precedence: L# ~ L ~ 2 > R ~ 0 ~ 1 problem: DPs: TRS: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) Qed DPs: 1#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(0(1(x1))) 1#(2(0(x1))) -> 1#(x1) 1#(2(1(x1))) -> 0#(2(x1)) 0#(2(0(x1))) -> 0#(1(x1)) 0#(2(0(x1))) -> 1#(x1) 0#(2(1(x1))) -> 1#(0(2(x1))) 0#(2(1(x1))) -> 0#(2(x1)) TRS: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) Arctic Interpretation Processor: dimension: 1 interpretation: [0#](x0) = x0, [1#](x0) = x0, [R](x0) = 12x0 + 15, [L](x0) = 0, [0](x0) = x0, [2](x0) = 4x0, [1](x0) = 2x0 orientation: 1#(2(0(x1))) = 4x1 >= 2x1 = 0#(1(x1)) 0#(2(0(x1))) = 4x1 >= 2x1 = 1#(0(1(x1))) 1#(2(0(x1))) = 4x1 >= x1 = 1#(x1) 1#(2(1(x1))) = 6x1 >= 4x1 = 0#(2(x1)) 0#(2(0(x1))) = 4x1 >= 2x1 = 0#(1(x1)) 0#(2(0(x1))) = 4x1 >= x1 = 1#(x1) 0#(2(1(x1))) = 6x1 >= 4x1 = 1#(0(2(x1))) 0#(2(1(x1))) = 6x1 >= 4x1 = 0#(2(x1)) 1(2(1(x1))) = 8x1 >= 8x1 = 2(0(2(x1))) 0(2(1(x1))) = 6x1 >= 6x1 = 1(0(2(x1))) L(2(1(x1))) = 0 >= 0 = L(1(0(2(x1)))) 1(2(0(x1))) = 6x1 >= 6x1 = 2(0(1(x1))) 1(2(R(x1))) = 18x1 + 21 >= 18x1 + 21 = 2(0(1(R(x1)))) 0(2(0(x1))) = 4x1 >= 4x1 = 1(0(1(x1))) L(2(0(x1))) = 0 >= 0 = L(1(0(1(x1)))) 0(2(R(x1))) = 16x1 + 19 >= 16x1 + 19 = 1(0(1(R(x1)))) problem: DPs: TRS: 1(2(1(x1))) -> 2(0(2(x1))) 0(2(1(x1))) -> 1(0(2(x1))) L(2(1(x1))) -> L(1(0(2(x1)))) 1(2(0(x1))) -> 2(0(1(x1))) 1(2(R(x1))) -> 2(0(1(R(x1)))) 0(2(0(x1))) -> 1(0(1(x1))) L(2(0(x1))) -> L(1(0(1(x1)))) 0(2(R(x1))) -> 1(0(1(R(x1)))) Qed