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)) Matrix Interpretation Processor: dim=1 interpretation: [q3#](x0) = 8x0, [q2#](x0) = 2x0 + 3, [1'#](x0) = 4x0 + 8, [0#](x0) = 2x0 + 4, [0'#](x0) = 4x0, [q1#](x0) = 2x0 + 6, [q0#](x0) = 2x0 + 1, [q4](x0) = x0, [b](x0) = 4x0 + 18, [q3](x0) = x0, [q2](x0) = 2x0 + 5, [1](x0) = 8x0 + 13, [1'](x0) = 4x0 + 4, [0'](x0) = 4x0, [q1](x0) = x0, [q0](x0) = 2x0, [0](x0) = 2x0 + 4 orientation: q0#(0(x1)) = 4x1 + 9 >= 2x1 + 6 = q1#(x1) q0#(0(x1)) = 4x1 + 9 >= 4x1 = 0'#(q1(x1)) q1#(0(x1)) = 4x1 + 14 >= 2x1 + 6 = q1#(x1) q1#(0(x1)) = 4x1 + 14 >= 2x1 + 4 = 0#(q1(x1)) q1#(1'(x1)) = 8x1 + 14 >= 2x1 + 6 = q1#(x1) q1#(1'(x1)) = 8x1 + 14 >= 4x1 + 8 = 1'#(q1(x1)) 0#(q1(1(x1))) = 16x1 + 30 >= 4x1 + 8 = 1'#(x1) 0#(q1(1(x1))) = 16x1 + 30 >= 8x1 + 12 = 0#(1'(x1)) 0#(q1(1(x1))) = 16x1 + 30 >= 16x1 + 27 = q2#(0(1'(x1))) 0'#(q1(1(x1))) = 32x1 + 52 >= 4x1 + 8 = 1'#(x1) 0'#(q1(1(x1))) = 32x1 + 52 >= 16x1 + 16 = 0'#(1'(x1)) 0'#(q1(1(x1))) = 32x1 + 52 >= 32x1 + 35 = q2#(0'(1'(x1))) 1'#(q1(1(x1))) = 32x1 + 60 >= 4x1 + 8 = 1'#(x1) 1'#(q1(1(x1))) = 32x1 + 60 >= 16x1 + 24 = 1'#(1'(x1)) 1'#(q1(1(x1))) = 32x1 + 60 >= 32x1 + 43 = q2#(1'(1'(x1))) 0#(q2(0(x1))) = 8x1 + 30 >= 4x1 + 12 = 0#(0(x1)) 0#(q2(0(x1))) = 8x1 + 30 >= 8x1 + 27 = q2#(0(0(x1))) 0'#(q2(0(x1))) = 16x1 + 52 >= 8x1 + 16 = 0'#(0(x1)) 0'#(q2(0(x1))) = 16x1 + 52 >= 16x1 + 35 = q2#(0'(0(x1))) 1'#(q2(0(x1))) = 16x1 + 60 >= 8x1 + 24 = 1'#(0(x1)) 1'#(q2(0(x1))) = 16x1 + 60 >= 16x1 + 43 = q2#(1'(0(x1))) 0#(q2(1'(x1))) = 16x1 + 30 >= 8x1 + 12 = 0#(1'(x1)) 0#(q2(1'(x1))) = 16x1 + 30 >= 16x1 + 27 = q2#(0(1'(x1))) 0'#(q2(1'(x1))) = 32x1 + 52 >= 16x1 + 16 = 0'#(1'(x1)) 0'#(q2(1'(x1))) = 32x1 + 52 >= 32x1 + 35 = q2#(0'(1'(x1))) 1'#(q2(1'(x1))) = 32x1 + 60 >= 16x1 + 24 = 1'#(1'(x1)) 1'#(q2(1'(x1))) = 32x1 + 60 >= 32x1 + 43 = q2#(1'(1'(x1))) q2#(0'(x1)) = 8x1 + 3 >= 2x1 + 1 = q0#(x1) q2#(0'(x1)) = 8x1 + 3 >= 8x1 = 0'#(q0(x1)) q0#(1'(x1)) = 8x1 + 9 >= 8x1 = q3#(x1) q0#(1'(x1)) = 8x1 + 9 >= 4x1 + 8 = 1'#(q3(x1)) q3#(1'(x1)) = 32x1 + 32 >= 8x1 = q3#(x1) q3#(1'(x1)) = 32x1 + 32 >= 4x1 + 8 = 1'#(q3(x1)) q0(0(x1)) = 4x1 + 8 >= 4x1 = 0'(q1(x1)) q1(0(x1)) = 2x1 + 4 >= 2x1 + 4 = 0(q1(x1)) q1(1'(x1)) = 4x1 + 4 >= 4x1 + 4 = 1'(q1(x1)) 0(q1(1(x1))) = 16x1 + 30 >= 16x1 + 29 = q2(0(1'(x1))) 0'(q1(1(x1))) = 32x1 + 52 >= 32x1 + 37 = q2(0'(1'(x1))) 1'(q1(1(x1))) = 32x1 + 56 >= 32x1 + 45 = q2(1'(1'(x1))) 0(q2(0(x1))) = 8x1 + 30 >= 8x1 + 29 = q2(0(0(x1))) 0'(q2(0(x1))) = 16x1 + 52 >= 16x1 + 37 = q2(0'(0(x1))) 1'(q2(0(x1))) = 16x1 + 56 >= 16x1 + 45 = q2(1'(0(x1))) 0(q2(1'(x1))) = 16x1 + 30 >= 16x1 + 29 = q2(0(1'(x1))) 0'(q2(1'(x1))) = 32x1 + 52 >= 32x1 + 37 = q2(0'(1'(x1))) 1'(q2(1'(x1))) = 32x1 + 56 >= 32x1 + 45 = q2(1'(1'(x1))) q2(0'(x1)) = 8x1 + 5 >= 8x1 = 0'(q0(x1)) q0(1'(x1)) = 8x1 + 8 >= 4x1 + 4 = 1'(q3(x1)) q3(1'(x1)) = 4x1 + 4 >= 4x1 + 4 = 1'(q3(x1)) q3(b(x1)) = 4x1 + 18 >= 4x1 + 18 = b(q4(x1)) problem: DPs: 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)) Qed