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)))) Matrix Interpretation Processor: dim=4 interpretation: [0#](x0) = [0 0 0 1]x0, [1#](x0) = [0 0 0 1]x0, [0] [1] [R](x0) = [0] [0], [0 0 0 1] [0 0 0 1] [L](x0) = [0 0 0 1]x0 [0 0 0 0] , [0 0 1 0] [0] [0 0 0 1] [0] [0](x0) = [0 0 0 0]x0 + [1] [0 0 0 0] [0], [0 0 0 0] [0 0 0 0] [2](x0) = [0 0 0 0]x0 [0 1 1 0] , [0 0 0 0] [0] [0 1 1 0] [0] [1](x0) = [0 0 0 0]x0 + [1] [0 0 0 1] [0] orientation: 1#(2(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = 0#(1(x1)) 0#(2(0(x1))) = [0 0 0 1]x1 + [1] >= [0] = 1#(0(1(x1))) 1#(2(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = 1#(x1) 1#(2(1(x1))) = [0 1 1 0]x1 + [1] >= [0 1 1 0]x1 = 0#(2(x1)) 0#(2(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = 0#(1(x1)) 0#(2(0(x1))) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = 1#(x1) 0#(2(1(x1))) = [0 1 1 0]x1 + [1] >= [0] = 1#(0(2(x1))) 0#(2(1(x1))) = [0 1 1 0]x1 + [1] >= [0 1 1 0]x1 = 0#(2(x1)) [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] 1(2(1(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 2(0(2(x1))) [0 1 1 0] [1] [0 1 1 0] [1] [0 0 0 0] [0] [0 0 0 0] [0] [0 1 1 0] [1] [0 1 1 0] [1] 0(2(1(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 1(0(2(x1))) [0 0 0 0] [0] [0 0 0 0] [0] [0 1 1 0] [1] [0] [0 1 1 0] [1] [0] L(2(1(x1))) = [0 1 1 0]x1 + [1] >= [0] = L(1(0(2(x1)))) [0 0 0 0] [0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] 1(2(0(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [0] = 2(0(1(x1))) [0 0 0 1] [1] [0 0 0 1] [1] [0] [0] [0] [0] 1(2(R(x1))) = [1] >= [0] = 2(0(1(R(x1)))) [1] [1] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 1] [1] [0 0 0 1] [1] 0(2(0(x1))) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = 1(0(1(x1))) [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 1] [1] [0] [0 0 0 1] [1] [0] L(2(0(x1))) = [0 0 0 1]x1 + [1] >= [0] = L(1(0(1(x1)))) [0 0 0 0] [0] [0] [0] [0] [1] [1] 0(2(R(x1))) = [1] >= [1] = 1(0(1(R(x1)))) [0] [0] 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