YES Problem: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) Proof: DP Processor: DPs: q0#(0(x1)) -> q1#(x1) q0#(0(x1)) -> 0'#(q1(x1)) q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) 0#(q1(1(x1))) -> 1'#(x1) 0#(q1(1(x1))) -> 0#(1'(x1)) 0#(q1(1(x1))) -> q2#(0(1'(x1))) 0'#(q1(1(x1))) -> 1'#(x1) 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(x1) 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) q0#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) TDG Processor: DPs: q0#(0(x1)) -> q1#(x1) q0#(0(x1)) -> 0'#(q1(x1)) q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) 0#(q1(1(x1))) -> 1'#(x1) 0#(q1(1(x1))) -> 0#(1'(x1)) 0#(q1(1(x1))) -> q2#(0(1'(x1))) 0'#(q1(1(x1))) -> 1'#(x1) 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(x1) 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) q0#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) graph: q3#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q1(1(x1))) -> 1'#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q1(1(x1))) -> 0'#(1'(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q1(1(x1))) -> 1'#(x1) q2#(0'(x1)) -> q0#(x1) -> q0#(1'(x1)) -> 1'#(q3(x1)) q2#(0'(x1)) -> q0#(x1) -> q0#(1'(x1)) -> q3#(x1) q2#(0'(x1)) -> q0#(x1) -> q0#(0(x1)) -> 0'#(q1(x1)) q2#(0'(x1)) -> q0#(x1) -> q0#(0(x1)) -> q1#(x1) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q1(1(x1))) -> 1'#(x1) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q1(1(x1))) -> 1'#(x1) 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q1(1(x1))) -> 1'#(x1) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(x1) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q1(1(x1))) -> q2#(0(1'(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q1(1(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q1(1(x1))) -> 1'#(x1) 0#(q2(0(x1))) -> q2#(0(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q1(1(x1))) -> q2#(0(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q1(1(x1))) -> 0#(1'(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q1(1(x1))) -> 1'#(x1) 0#(q1(1(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q1(1(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(x1) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q1(1(x1))) -> q2#(0(1'(x1))) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q1(1(x1))) -> 0#(1'(x1)) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q1(1(x1))) -> 1'#(x1) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q1(1(x1))) -> 1'#(x1) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q1(1(x1))) -> 1'#(x1) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(x1) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q1(1(x1))) -> 1'#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q1(1(x1))) -> 1'#(x1) q1#(1'(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q1#(1'(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q1(1(x1))) -> q2#(0(1'(x1))) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q1(1(x1))) -> 0#(1'(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q1(1(x1))) -> 1'#(x1) q1#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q1#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q1#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q1#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q0#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> 1'#(q3(x1)) q0#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q1(1(x1))) -> 1'#(x1) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q1(1(x1))) -> 0'#(1'(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q1(1(x1))) -> 1'#(x1) q0#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q0#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q0#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q0#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) EDG Processor: DPs: q0#(0(x1)) -> q1#(x1) q0#(0(x1)) -> 0'#(q1(x1)) q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) 0#(q1(1(x1))) -> 1'#(x1) 0#(q1(1(x1))) -> 0#(1'(x1)) 0#(q1(1(x1))) -> q2#(0(1'(x1))) 0'#(q1(1(x1))) -> 1'#(x1) 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(x1) 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) q0#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) graph: q3#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q2#(0'(x1)) -> q0#(x1) -> q0#(0(x1)) -> q1#(x1) q2#(0'(x1)) -> q0#(x1) -> q0#(0(x1)) -> 0'#(q1(x1)) q2#(0'(x1)) -> q0#(x1) -> q0#(1'(x1)) -> q3#(x1) q2#(0'(x1)) -> q0#(x1) -> q0#(1'(x1)) -> 1'#(q3(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(x1) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0#(q2(0(x1))) -> q2#(0(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q2(0(x1))) -> q2#(0(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0#(q1(1(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q1(1(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(x1) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 0#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q1(1(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(x1) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 0'#(q1(1(x1))) -> 1'#(x1) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q1(1(x1))) -> 1'#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q1(1(x1))) -> 1'#(1'(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q1(1(x1))) -> q2#(1'(1'(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q1#(1'(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q1#(1'(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q1(1(x1))) -> 1'#(x1) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q1(1(x1))) -> 0#(1'(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q1(1(x1))) -> q2#(0(1'(x1))) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) q1#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q1#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q1#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q0#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> 1'#(q3(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q1(1(x1))) -> 1'#(x1) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q1(1(x1))) -> 0'#(1'(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q0#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q0#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q0#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q0#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [q3#](x0) = x0 + 0, [q2#](x0) = x0, [1'#](x0) = x0, [0#](x0) = x0, [0'#](x0) = x0 + 0, [q1#](x0) = x0, [q0#](x0) = x0 + 0, [q4](x0) = x0 + 2, [b](x0) = 0, [q3](x0) = 0, [q2](x0) = x0, [1](x0) = 6x0, [1'](x0) = x0, [0'](x0) = x0 + 0, [q1](x0) = x0, [q0](x0) = x0 + 0, [0](x0) = x0 orientation: q0#(0(x1)) = x1 + 0 >= x1 = q1#(x1) q0#(0(x1)) = x1 + 0 >= x1 + 0 = 0'#(q1(x1)) q1#(0(x1)) = x1 >= x1 = q1#(x1) q1#(0(x1)) = x1 >= x1 = 0#(q1(x1)) q1#(1'(x1)) = x1 >= x1 = q1#(x1) q1#(1'(x1)) = x1 >= x1 = 1'#(q1(x1)) 0#(q1(1(x1))) = 6x1 >= x1 = 1'#(x1) 0#(q1(1(x1))) = 6x1 >= x1 = 0#(1'(x1)) 0#(q1(1(x1))) = 6x1 >= x1 = q2#(0(1'(x1))) 0'#(q1(1(x1))) = 6x1 + 0 >= x1 = 1'#(x1) 0'#(q1(1(x1))) = 6x1 + 0 >= x1 + 0 = 0'#(1'(x1)) 0'#(q1(1(x1))) = 6x1 + 0 >= x1 + 0 = q2#(0'(1'(x1))) 1'#(q1(1(x1))) = 6x1 >= x1 = 1'#(x1) 1'#(q1(1(x1))) = 6x1 >= x1 = 1'#(1'(x1)) 1'#(q1(1(x1))) = 6x1 >= x1 = q2#(1'(1'(x1))) 0#(q2(0(x1))) = x1 >= x1 = 0#(0(x1)) 0#(q2(0(x1))) = x1 >= x1 = q2#(0(0(x1))) 0'#(q2(0(x1))) = x1 + 0 >= x1 + 0 = 0'#(0(x1)) 0'#(q2(0(x1))) = x1 + 0 >= x1 + 0 = q2#(0'(0(x1))) 1'#(q2(0(x1))) = x1 >= x1 = 1'#(0(x1)) 1'#(q2(0(x1))) = x1 >= x1 = q2#(1'(0(x1))) 0#(q2(1'(x1))) = x1 >= x1 = 0#(1'(x1)) 0#(q2(1'(x1))) = x1 >= x1 = q2#(0(1'(x1))) 0'#(q2(1'(x1))) = x1 + 0 >= x1 + 0 = 0'#(1'(x1)) 0'#(q2(1'(x1))) = x1 + 0 >= x1 + 0 = q2#(0'(1'(x1))) 1'#(q2(1'(x1))) = x1 >= x1 = 1'#(1'(x1)) 1'#(q2(1'(x1))) = x1 >= x1 = q2#(1'(1'(x1))) q2#(0'(x1)) = x1 + 0 >= x1 + 0 = q0#(x1) q2#(0'(x1)) = x1 + 0 >= x1 + 0 = 0'#(q0(x1)) q0#(1'(x1)) = x1 + 0 >= x1 + 0 = q3#(x1) q0#(1'(x1)) = x1 + 0 >= 0 = 1'#(q3(x1)) q3#(1'(x1)) = x1 + 0 >= x1 + 0 = q3#(x1) q3#(1'(x1)) = x1 + 0 >= 0 = 1'#(q3(x1)) q0(0(x1)) = x1 + 0 >= x1 + 0 = 0'(q1(x1)) q1(0(x1)) = x1 >= x1 = 0(q1(x1)) q1(1'(x1)) = x1 >= x1 = 1'(q1(x1)) 0(q1(1(x1))) = 6x1 >= x1 = q2(0(1'(x1))) 0'(q1(1(x1))) = 6x1 + 0 >= x1 + 0 = q2(0'(1'(x1))) 1'(q1(1(x1))) = 6x1 >= x1 = q2(1'(1'(x1))) 0(q2(0(x1))) = x1 >= x1 = q2(0(0(x1))) 0'(q2(0(x1))) = x1 + 0 >= x1 + 0 = q2(0'(0(x1))) 1'(q2(0(x1))) = x1 >= x1 = q2(1'(0(x1))) 0(q2(1'(x1))) = x1 >= x1 = q2(0(1'(x1))) 0'(q2(1'(x1))) = x1 + 0 >= x1 + 0 = q2(0'(1'(x1))) 1'(q2(1'(x1))) = x1 >= x1 = q2(1'(1'(x1))) q2(0'(x1)) = x1 + 0 >= x1 + 0 = 0'(q0(x1)) q0(1'(x1)) = x1 + 0 >= 0 = 1'(q3(x1)) q3(1'(x1)) = 0 >= 0 = 1'(q3(x1)) q3(b(x1)) = 0 >= 0 = b(q4(x1)) problem: DPs: q0#(0(x1)) -> q1#(x1) q0#(0(x1)) -> 0'#(q1(x1)) q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) q0#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) EDG Processor: DPs: q0#(0(x1)) -> q1#(x1) q0#(0(x1)) -> 0'#(q1(x1)) q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) 0'#(q1(1(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) q0#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) graph: q3#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q2#(0'(x1)) -> q0#(x1) -> q0#(1'(x1)) -> 1'#(q3(x1)) q2#(0'(x1)) -> q0#(x1) -> q0#(1'(x1)) -> q3#(x1) q2#(0'(x1)) -> q0#(x1) -> q0#(0(x1)) -> 0'#(q1(x1)) q2#(0'(x1)) -> q0#(x1) -> q0#(0(x1)) -> q1#(x1) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q1(1(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q1#(1'(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q1#(1'(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) q1#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q1#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q1#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q1#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q0#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> 1'#(q3(x1)) q0#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q1(1(x1))) -> q2#(0'(1'(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q1(1(x1))) -> 0'#(1'(x1)) q0#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q0#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q0#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q0#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [q3#](x0) = x0 + 0, [q2#](x0) = x0 + 0, [1'#](x0) = x0 + 0, [0#](x0) = 4x0 + 0, [0'#](x0) = 2x0 + 0, [q1#](x0) = x0 + 0, [q0#](x0) = x0 + 0, [q4](x0) = 0, [b](x0) = x0 + 0, [q3](x0) = x0, [q2](x0) = x0 + 0, [1](x0) = 13x0 + 3, [1'](x0) = x0, [0'](x0) = 2x0 + 0, [q1](x0) = x0, [q0](x0) = x0, [0](x0) = 4x0 + 0 orientation: q0#(0(x1)) = 4x1 + 0 >= x1 + 0 = q1#(x1) q0#(0(x1)) = 4x1 + 0 >= 2x1 + 0 = 0'#(q1(x1)) q1#(0(x1)) = 4x1 + 0 >= x1 + 0 = q1#(x1) q1#(0(x1)) = 4x1 + 0 >= 4x1 + 0 = 0#(q1(x1)) q1#(1'(x1)) = x1 + 0 >= x1 + 0 = q1#(x1) q1#(1'(x1)) = x1 + 0 >= x1 + 0 = 1'#(q1(x1)) 0'#(q1(1(x1))) = 15x1 + 5 >= 2x1 + 0 = 0'#(1'(x1)) 0'#(q1(1(x1))) = 15x1 + 5 >= 2x1 + 0 = q2#(0'(1'(x1))) 0#(q2(0(x1))) = 8x1 + 4 >= 8x1 + 4 = 0#(0(x1)) 0#(q2(0(x1))) = 8x1 + 4 >= 8x1 + 4 = q2#(0(0(x1))) 0'#(q2(0(x1))) = 6x1 + 2 >= 6x1 + 2 = 0'#(0(x1)) 0'#(q2(0(x1))) = 6x1 + 2 >= 6x1 + 2 = q2#(0'(0(x1))) 1'#(q2(0(x1))) = 4x1 + 0 >= 4x1 + 0 = 1'#(0(x1)) 1'#(q2(0(x1))) = 4x1 + 0 >= 4x1 + 0 = q2#(1'(0(x1))) 0#(q2(1'(x1))) = 4x1 + 4 >= 4x1 + 0 = 0#(1'(x1)) 0#(q2(1'(x1))) = 4x1 + 4 >= 4x1 + 0 = q2#(0(1'(x1))) 0'#(q2(1'(x1))) = 2x1 + 2 >= 2x1 + 0 = 0'#(1'(x1)) 0'#(q2(1'(x1))) = 2x1 + 2 >= 2x1 + 0 = q2#(0'(1'(x1))) 1'#(q2(1'(x1))) = x1 + 0 >= x1 + 0 = 1'#(1'(x1)) 1'#(q2(1'(x1))) = x1 + 0 >= x1 + 0 = q2#(1'(1'(x1))) q2#(0'(x1)) = 2x1 + 0 >= x1 + 0 = q0#(x1) q2#(0'(x1)) = 2x1 + 0 >= 2x1 + 0 = 0'#(q0(x1)) q0#(1'(x1)) = x1 + 0 >= x1 + 0 = q3#(x1) q0#(1'(x1)) = x1 + 0 >= x1 + 0 = 1'#(q3(x1)) q3#(1'(x1)) = x1 + 0 >= x1 + 0 = q3#(x1) q3#(1'(x1)) = x1 + 0 >= x1 + 0 = 1'#(q3(x1)) q0(0(x1)) = 4x1 + 0 >= 2x1 + 0 = 0'(q1(x1)) q1(0(x1)) = 4x1 + 0 >= 4x1 + 0 = 0(q1(x1)) q1(1'(x1)) = x1 >= x1 = 1'(q1(x1)) 0(q1(1(x1))) = 17x1 + 7 >= 4x1 + 0 = q2(0(1'(x1))) 0'(q1(1(x1))) = 15x1 + 5 >= 2x1 + 0 = q2(0'(1'(x1))) 1'(q1(1(x1))) = 13x1 + 3 >= x1 + 0 = q2(1'(1'(x1))) 0(q2(0(x1))) = 8x1 + 4 >= 8x1 + 4 = q2(0(0(x1))) 0'(q2(0(x1))) = 6x1 + 2 >= 6x1 + 2 = q2(0'(0(x1))) 1'(q2(0(x1))) = 4x1 + 0 >= 4x1 + 0 = q2(1'(0(x1))) 0(q2(1'(x1))) = 4x1 + 4 >= 4x1 + 0 = q2(0(1'(x1))) 0'(q2(1'(x1))) = 2x1 + 2 >= 2x1 + 0 = q2(0'(1'(x1))) 1'(q2(1'(x1))) = x1 + 0 >= x1 + 0 = q2(1'(1'(x1))) q2(0'(x1)) = 2x1 + 0 >= 2x1 + 0 = 0'(q0(x1)) q0(1'(x1)) = x1 >= x1 = 1'(q3(x1)) q3(1'(x1)) = x1 >= x1 = 1'(q3(x1)) q3(b(x1)) = x1 + 0 >= 0 = b(q4(x1)) problem: DPs: q0#(0(x1)) -> q1#(x1) q0#(0(x1)) -> 0'#(q1(x1)) q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) q0#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) EDG Processor: DPs: q0#(0(x1)) -> q1#(x1) q0#(0(x1)) -> 0'#(q1(x1)) q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> 1'#(q1(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> q2#(0(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) q0#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> 1'#(q3(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) graph: q3#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> q3#(x1) q3#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> 1'#(q3(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q3#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) q2#(0'(x1)) -> 0'#(q0(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q2#(0'(x1)) -> q0#(x1) -> q0#(0(x1)) -> q1#(x1) q2#(0'(x1)) -> q0#(x1) -> q0#(0(x1)) -> 0'#(q1(x1)) q2#(0'(x1)) -> q0#(x1) -> q0#(1'(x1)) -> q3#(x1) q2#(0'(x1)) -> q0#(x1) -> q0#(1'(x1)) -> 1'#(q3(x1)) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(1'(x1))) -> 1'#(1'(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 1'#(q2(0(x1))) -> q2#(1'(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) 1'#(q2(0(x1))) -> 1'#(0(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q2(1'(x1))) -> q2#(0(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(1'(x1))) -> 0#(1'(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0#(q2(0(x1))) -> q2#(0(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 0#(q2(0(x1))) -> q2#(0(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) 0#(q2(0(x1))) -> 0#(0(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(1'(x1))) -> 0'#(1'(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) -> q2#(0'(x1)) -> q0#(x1) 0'#(q2(0(x1))) -> q2#(0'(0(x1))) -> q2#(0'(x1)) -> 0'#(q0(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) 0'#(q2(0(x1))) -> 0'#(0(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q1#(1'(x1)) -> 1'#(q1(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q1#(1'(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q1#(1'(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q1#(1'(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q1#(1'(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(0(x1))) -> 0#(0(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(0(x1))) -> q2#(0(0(x1))) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(1'(x1))) -> 0#(1'(x1)) q1#(0(x1)) -> 0#(q1(x1)) -> 0#(q2(1'(x1))) -> q2#(0(1'(x1))) q1#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q1#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q1#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q1#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) q0#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> q3#(x1) q0#(1'(x1)) -> q3#(x1) -> q3#(1'(x1)) -> 1'#(q3(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> 1'#(0(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(0(x1))) -> q2#(1'(0(x1))) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> 1'#(1'(x1)) q0#(1'(x1)) -> 1'#(q3(x1)) -> 1'#(q2(1'(x1))) -> q2#(1'(1'(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(0(x1))) -> 0'#(0(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(0(x1))) -> q2#(0'(0(x1))) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(1'(x1))) -> 0'#(1'(x1)) q0#(0(x1)) -> 0'#(q1(x1)) -> 0'#(q2(1'(x1))) -> q2#(0'(1'(x1))) q0#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> q1#(x1) q0#(0(x1)) -> q1#(x1) -> q1#(0(x1)) -> 0#(q1(x1)) q0#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> q1#(x1) q0#(0(x1)) -> q1#(x1) -> q1#(1'(x1)) -> 1'#(q1(x1)) Arctic Interpretation Processor: dimension: 1 interpretation: [q3#](x0) = 11x0 + 0, [q2#](x0) = 4x0 + 0, [1'#](x0) = 4x0, [0#](x0) = 3x0 + 0, [0'#](x0) = 1x0, [q1#](x0) = 9x0, [q0#](x0) = 9x0, [q4](x0) = 1, [b](x0) = 1x0 + 2, [q3](x0) = x0, [q2](x0) = 14x0 + 0, [1](x0) = 11x0 + 13, [1'](x0) = 5x0 + 7, [0'](x0) = 5x0, [q1](x0) = 8x0 + 0, [q0](x0) = 8x0, [0](x0) = 5x0 + 12 orientation: q0#(0(x1)) = 14x1 + 21 >= 9x1 = q1#(x1) q0#(0(x1)) = 14x1 + 21 >= 9x1 + 1 = 0'#(q1(x1)) q1#(0(x1)) = 14x1 + 21 >= 9x1 = q1#(x1) q1#(0(x1)) = 14x1 + 21 >= 11x1 + 3 = 0#(q1(x1)) q1#(1'(x1)) = 14x1 + 16 >= 9x1 = q1#(x1) q1#(1'(x1)) = 14x1 + 16 >= 12x1 + 4 = 1'#(q1(x1)) 0#(q2(0(x1))) = 22x1 + 29 >= 8x1 + 15 = 0#(0(x1)) 0#(q2(0(x1))) = 22x1 + 29 >= 14x1 + 21 = q2#(0(0(x1))) 0'#(q2(0(x1))) = 20x1 + 27 >= 6x1 + 13 = 0'#(0(x1)) 0'#(q2(0(x1))) = 20x1 + 27 >= 14x1 + 21 = q2#(0'(0(x1))) 1'#(q2(0(x1))) = 23x1 + 30 >= 9x1 + 16 = 1'#(0(x1)) 1'#(q2(0(x1))) = 23x1 + 30 >= 14x1 + 21 = q2#(1'(0(x1))) 0#(q2(1'(x1))) = 22x1 + 24 >= 8x1 + 10 = 0#(1'(x1)) 0#(q2(1'(x1))) = 22x1 + 24 >= 14x1 + 16 = q2#(0(1'(x1))) 0'#(q2(1'(x1))) = 20x1 + 22 >= 6x1 + 8 = 0'#(1'(x1)) 0'#(q2(1'(x1))) = 20x1 + 22 >= 14x1 + 16 = q2#(0'(1'(x1))) 1'#(q2(1'(x1))) = 23x1 + 25 >= 9x1 + 11 = 1'#(1'(x1)) 1'#(q2(1'(x1))) = 23x1 + 25 >= 14x1 + 16 = q2#(1'(1'(x1))) q2#(0'(x1)) = 9x1 + 0 >= 9x1 = q0#(x1) q2#(0'(x1)) = 9x1 + 0 >= 9x1 = 0'#(q0(x1)) q0#(1'(x1)) = 14x1 + 16 >= 11x1 + 0 = q3#(x1) q0#(1'(x1)) = 14x1 + 16 >= 4x1 = 1'#(q3(x1)) q3#(1'(x1)) = 16x1 + 18 >= 11x1 + 0 = q3#(x1) q3#(1'(x1)) = 16x1 + 18 >= 4x1 = 1'#(q3(x1)) q0(0(x1)) = 13x1 + 20 >= 13x1 + 5 = 0'(q1(x1)) q1(0(x1)) = 13x1 + 20 >= 13x1 + 12 = 0(q1(x1)) q1(1'(x1)) = 13x1 + 15 >= 13x1 + 7 = 1'(q1(x1)) 0(q1(1(x1))) = 24x1 + 26 >= 24x1 + 26 = q2(0(1'(x1))) 0'(q1(1(x1))) = 24x1 + 26 >= 24x1 + 26 = q2(0'(1'(x1))) 1'(q1(1(x1))) = 24x1 + 26 >= 24x1 + 26 = q2(1'(1'(x1))) 0(q2(0(x1))) = 24x1 + 31 >= 24x1 + 31 = q2(0(0(x1))) 0'(q2(0(x1))) = 24x1 + 31 >= 24x1 + 31 = q2(0'(0(x1))) 1'(q2(0(x1))) = 24x1 + 31 >= 24x1 + 31 = q2(1'(0(x1))) 0(q2(1'(x1))) = 24x1 + 26 >= 24x1 + 26 = q2(0(1'(x1))) 0'(q2(1'(x1))) = 24x1 + 26 >= 24x1 + 26 = q2(0'(1'(x1))) 1'(q2(1'(x1))) = 24x1 + 26 >= 24x1 + 26 = q2(1'(1'(x1))) q2(0'(x1)) = 19x1 + 0 >= 13x1 = 0'(q0(x1)) q0(1'(x1)) = 13x1 + 15 >= 5x1 + 7 = 1'(q3(x1)) q3(1'(x1)) = 5x1 + 7 >= 5x1 + 7 = 1'(q3(x1)) q3(b(x1)) = 1x1 + 2 >= 2 = b(q4(x1)) problem: DPs: q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) EDG Processor: DPs: q2#(0'(x1)) -> q0#(x1) q2#(0'(x1)) -> 0'#(q0(x1)) TRS: q0(0(x1)) -> 0'(q1(x1)) q1(0(x1)) -> 0(q1(x1)) q1(1'(x1)) -> 1'(q1(x1)) 0(q1(1(x1))) -> q2(0(1'(x1))) 0'(q1(1(x1))) -> q2(0'(1'(x1))) 1'(q1(1(x1))) -> q2(1'(1'(x1))) 0(q2(0(x1))) -> q2(0(0(x1))) 0'(q2(0(x1))) -> q2(0'(0(x1))) 1'(q2(0(x1))) -> q2(1'(0(x1))) 0(q2(1'(x1))) -> q2(0(1'(x1))) 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 1'(q2(1'(x1))) -> q2(1'(1'(x1))) q2(0'(x1)) -> 0'(q0(x1)) q0(1'(x1)) -> 1'(q3(x1)) q3(1'(x1)) -> 1'(q3(x1)) q3(b(x1)) -> b(q4(x1)) graph: Qed