YES Problem: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Proof: DP Processor: DPs: r0#(0(x1)) -> r0#(x1) r0#(0(x1)) -> 0#(r0(x1)) r0#(1(x1)) -> r0#(x1) r0#(1(x1)) -> 1#(r0(x1)) r0#(m(x1)) -> r0#(x1) r0#(m(x1)) -> m#(r0(x1)) r1#(0(x1)) -> r1#(x1) r1#(0(x1)) -> 0#(r1(x1)) r1#(1(x1)) -> r1#(x1) r1#(1(x1)) -> 1#(r1(x1)) r1#(m(x1)) -> r1#(x1) r1#(m(x1)) -> m#(r1(x1)) r0#(b(x1)) -> 0#(b(x1)) r1#(b(x1)) -> 1#(b(x1)) 0#(qr(x1)) -> 0#(x1) 1#(qr(x1)) -> 1#(x1) m#(qr(x1)) -> m#(x1) 0#(ql(x1)) -> 0#(x1) 1#(ql(x1)) -> 1#(x1) b#(ql(0(x1))) -> r0#(x1) b#(ql(0(x1))) -> b#(r0(x1)) b#(ql(0(x1))) -> 0#(b(r0(x1))) b#(ql(1(x1))) -> r1#(x1) b#(ql(1(x1))) -> b#(r1(x1)) b#(ql(1(x1))) -> 1#(b(r1(x1))) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) TDG Processor: DPs: r0#(0(x1)) -> r0#(x1) r0#(0(x1)) -> 0#(r0(x1)) r0#(1(x1)) -> r0#(x1) r0#(1(x1)) -> 1#(r0(x1)) r0#(m(x1)) -> r0#(x1) r0#(m(x1)) -> m#(r0(x1)) r1#(0(x1)) -> r1#(x1) r1#(0(x1)) -> 0#(r1(x1)) r1#(1(x1)) -> r1#(x1) r1#(1(x1)) -> 1#(r1(x1)) r1#(m(x1)) -> r1#(x1) r1#(m(x1)) -> m#(r1(x1)) r0#(b(x1)) -> 0#(b(x1)) r1#(b(x1)) -> 1#(b(x1)) 0#(qr(x1)) -> 0#(x1) 1#(qr(x1)) -> 1#(x1) m#(qr(x1)) -> m#(x1) 0#(ql(x1)) -> 0#(x1) 1#(ql(x1)) -> 1#(x1) b#(ql(0(x1))) -> r0#(x1) b#(ql(0(x1))) -> b#(r0(x1)) b#(ql(0(x1))) -> 0#(b(r0(x1))) b#(ql(1(x1))) -> r1#(x1) b#(ql(1(x1))) -> b#(r1(x1)) b#(ql(1(x1))) -> 1#(b(r1(x1))) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) graph: b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(1(x1))) -> 1#(b(r1(x1))) b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(1(x1))) -> b#(r1(x1)) b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(1(x1))) -> r1#(x1) b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(0(x1))) -> 0#(b(r0(x1))) b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(0(x1))) -> b#(r0(x1)) b#(ql(1(x1))) -> b#(r1(x1)) -> b#(ql(0(x1))) -> r0#(x1) b#(ql(1(x1))) -> r1#(x1) -> r1#(b(x1)) -> 1#(b(x1)) b#(ql(1(x1))) -> r1#(x1) -> r1#(m(x1)) -> m#(r1(x1)) b#(ql(1(x1))) -> r1#(x1) -> r1#(m(x1)) -> r1#(x1) b#(ql(1(x1))) -> r1#(x1) -> r1#(1(x1)) -> 1#(r1(x1)) b#(ql(1(x1))) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1) b#(ql(1(x1))) -> r1#(x1) -> r1#(0(x1)) -> 0#(r1(x1)) b#(ql(1(x1))) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1) b#(ql(1(x1))) -> 1#(b(r1(x1))) -> 1#(ql(x1)) -> 1#(x1) b#(ql(1(x1))) -> 1#(b(r1(x1))) -> 1#(qr(x1)) -> 1#(x1) b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(1(x1))) -> 1#(b(r1(x1))) b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(1(x1))) -> b#(r1(x1)) b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(1(x1))) -> r1#(x1) b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(0(x1))) -> 0#(b(r0(x1))) b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(0(x1))) -> b#(r0(x1)) b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(0(x1))) -> r0#(x1) b#(ql(0(x1))) -> 0#(b(r0(x1))) -> 0#(ql(x1)) -> 0#(x1) b#(ql(0(x1))) -> 0#(b(r0(x1))) -> 0#(qr(x1)) -> 0#(x1) b#(ql(0(x1))) -> r0#(x1) -> r0#(b(x1)) -> 0#(b(x1)) b#(ql(0(x1))) -> r0#(x1) -> r0#(m(x1)) -> m#(r0(x1)) b#(ql(0(x1))) -> r0#(x1) -> r0#(m(x1)) -> r0#(x1) b#(ql(0(x1))) -> r0#(x1) -> r0#(1(x1)) -> 1#(r0(x1)) b#(ql(0(x1))) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1) b#(ql(0(x1))) -> r0#(x1) -> r0#(0(x1)) -> 0#(r0(x1)) b#(ql(0(x1))) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1) r1#(b(x1)) -> 1#(b(x1)) -> 1#(ql(x1)) -> 1#(x1) r1#(b(x1)) -> 1#(b(x1)) -> 1#(qr(x1)) -> 1#(x1) r1#(m(x1)) -> r1#(x1) -> r1#(b(x1)) -> 1#(b(x1)) r1#(m(x1)) -> r1#(x1) -> r1#(m(x1)) -> m#(r1(x1)) r1#(m(x1)) -> r1#(x1) -> r1#(m(x1)) -> r1#(x1) r1#(m(x1)) -> r1#(x1) -> r1#(1(x1)) -> 1#(r1(x1)) r1#(m(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1) r1#(m(x1)) -> r1#(x1) -> r1#(0(x1)) -> 0#(r1(x1)) r1#(m(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1) r1#(m(x1)) -> m#(r1(x1)) -> m#(qr(x1)) -> m#(x1) r1#(1(x1)) -> r1#(x1) -> r1#(b(x1)) -> 1#(b(x1)) r1#(1(x1)) -> r1#(x1) -> r1#(m(x1)) -> m#(r1(x1)) r1#(1(x1)) -> r1#(x1) -> r1#(m(x1)) -> r1#(x1) r1#(1(x1)) -> r1#(x1) -> r1#(1(x1)) -> 1#(r1(x1)) r1#(1(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1) r1#(1(x1)) -> r1#(x1) -> r1#(0(x1)) -> 0#(r1(x1)) r1#(1(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1) r1#(1(x1)) -> 1#(r1(x1)) -> 1#(ql(x1)) -> 1#(x1) r1#(1(x1)) -> 1#(r1(x1)) -> 1#(qr(x1)) -> 1#(x1) r1#(0(x1)) -> r1#(x1) -> r1#(b(x1)) -> 1#(b(x1)) r1#(0(x1)) -> r1#(x1) -> r1#(m(x1)) -> m#(r1(x1)) r1#(0(x1)) -> r1#(x1) -> r1#(m(x1)) -> r1#(x1) r1#(0(x1)) -> r1#(x1) -> r1#(1(x1)) -> 1#(r1(x1)) r1#(0(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1) r1#(0(x1)) -> r1#(x1) -> r1#(0(x1)) -> 0#(r1(x1)) r1#(0(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1) r1#(0(x1)) -> 0#(r1(x1)) -> 0#(ql(x1)) -> 0#(x1) r1#(0(x1)) -> 0#(r1(x1)) -> 0#(qr(x1)) -> 0#(x1) m#(qr(x1)) -> m#(x1) -> m#(qr(x1)) -> m#(x1) 1#(ql(x1)) -> 1#(x1) -> 1#(ql(x1)) -> 1#(x1) 1#(ql(x1)) -> 1#(x1) -> 1#(qr(x1)) -> 1#(x1) 1#(qr(x1)) -> 1#(x1) -> 1#(ql(x1)) -> 1#(x1) 1#(qr(x1)) -> 1#(x1) -> 1#(qr(x1)) -> 1#(x1) 0#(ql(x1)) -> 0#(x1) -> 0#(ql(x1)) -> 0#(x1) 0#(ql(x1)) -> 0#(x1) -> 0#(qr(x1)) -> 0#(x1) 0#(qr(x1)) -> 0#(x1) -> 0#(ql(x1)) -> 0#(x1) 0#(qr(x1)) -> 0#(x1) -> 0#(qr(x1)) -> 0#(x1) r0#(b(x1)) -> 0#(b(x1)) -> 0#(ql(x1)) -> 0#(x1) r0#(b(x1)) -> 0#(b(x1)) -> 0#(qr(x1)) -> 0#(x1) r0#(m(x1)) -> m#(r0(x1)) -> m#(qr(x1)) -> m#(x1) r0#(m(x1)) -> r0#(x1) -> r0#(b(x1)) -> 0#(b(x1)) r0#(m(x1)) -> r0#(x1) -> r0#(m(x1)) -> m#(r0(x1)) r0#(m(x1)) -> r0#(x1) -> r0#(m(x1)) -> r0#(x1) r0#(m(x1)) -> r0#(x1) -> r0#(1(x1)) -> 1#(r0(x1)) r0#(m(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1) r0#(m(x1)) -> r0#(x1) -> r0#(0(x1)) -> 0#(r0(x1)) r0#(m(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1) r0#(1(x1)) -> 1#(r0(x1)) -> 1#(ql(x1)) -> 1#(x1) r0#(1(x1)) -> 1#(r0(x1)) -> 1#(qr(x1)) -> 1#(x1) r0#(1(x1)) -> r0#(x1) -> r0#(b(x1)) -> 0#(b(x1)) r0#(1(x1)) -> r0#(x1) -> r0#(m(x1)) -> m#(r0(x1)) r0#(1(x1)) -> r0#(x1) -> r0#(m(x1)) -> r0#(x1) r0#(1(x1)) -> r0#(x1) -> r0#(1(x1)) -> 1#(r0(x1)) r0#(1(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1) r0#(1(x1)) -> r0#(x1) -> r0#(0(x1)) -> 0#(r0(x1)) r0#(1(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1) r0#(0(x1)) -> 0#(r0(x1)) -> 0#(ql(x1)) -> 0#(x1) r0#(0(x1)) -> 0#(r0(x1)) -> 0#(qr(x1)) -> 0#(x1) r0#(0(x1)) -> r0#(x1) -> r0#(b(x1)) -> 0#(b(x1)) r0#(0(x1)) -> r0#(x1) -> r0#(m(x1)) -> m#(r0(x1)) r0#(0(x1)) -> r0#(x1) -> r0#(m(x1)) -> r0#(x1) r0#(0(x1)) -> r0#(x1) -> r0#(1(x1)) -> 1#(r0(x1)) r0#(0(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1) r0#(0(x1)) -> r0#(x1) -> r0#(0(x1)) -> 0#(r0(x1)) r0#(0(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1) SCC Processor: #sccs: 6 #rules: 13 #arcs: 95/625 DPs: b#(ql(1(x1))) -> b#(r1(x1)) b#(ql(0(x1))) -> b#(r0(x1)) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = x0 + 1, [ql](x0) = x0, [qr](x0) = 0, [b](x0) = x0 + 1, [r1](x0) = x0, [m](x0) = 0, [1](x0) = 1x0 + 4, [r0](x0) = x0 + 0, [0](x0) = x0 orientation: b#(ql(1(x1))) = 1x1 + 4 >= x1 + 1 = b#(r1(x1)) b#(ql(0(x1))) = x1 + 1 >= x1 + 1 = b#(r0(x1)) r0(0(x1)) = x1 + 0 >= x1 + 0 = 0(r0(x1)) r0(1(x1)) = 1x1 + 4 >= 1x1 + 4 = 1(r0(x1)) r0(m(x1)) = 0 >= 0 = m(r0(x1)) r1(0(x1)) = x1 >= x1 = 0(r1(x1)) r1(1(x1)) = 1x1 + 4 >= 1x1 + 4 = 1(r1(x1)) r1(m(x1)) = 0 >= 0 = m(r1(x1)) r0(b(x1)) = x1 + 1 >= 0 = qr(0(b(x1))) r1(b(x1)) = x1 + 1 >= 0 = qr(1(b(x1))) 0(qr(x1)) = 0 >= 0 = qr(0(x1)) 1(qr(x1)) = 4 >= 0 = qr(1(x1)) m(qr(x1)) = 0 >= 0 = ql(m(x1)) 0(ql(x1)) = x1 >= x1 = ql(0(x1)) 1(ql(x1)) = 1x1 + 4 >= 1x1 + 4 = ql(1(x1)) b(ql(0(x1))) = x1 + 1 >= x1 + 1 = 0(b(r0(x1))) b(ql(1(x1))) = 1x1 + 4 >= 1x1 + 4 = 1(b(r1(x1))) problem: DPs: b#(ql(0(x1))) -> b#(r0(x1)) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) EDG Processor: DPs: b#(ql(0(x1))) -> b#(r0(x1)) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) graph: b#(ql(0(x1))) -> b#(r0(x1)) -> b#(ql(0(x1))) -> b#(r0(x1)) KBO Processor: argument filtering: pi(0) = [0] pi(r0) = 0 pi(1) = 0 pi(m) = [] pi(r1) = 0 pi(b) = [0] pi(qr) = [] pi(ql) = 0 pi(b#) = 0 weight function: w0 = 1 w(b#) = w(qr) = w(b) = w(m) = w(0) = 1 w(ql) = w(r1) = w(1) = w(r0) = 0 precedence: b# ~ b > ql ~ qr ~ r1 ~ m ~ 1 ~ r0 ~ 0 problem: DPs: TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Qed DPs: r1#(0(x1)) -> r1#(x1) r1#(1(x1)) -> r1#(x1) r1#(m(x1)) -> r1#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Arctic Interpretation Processor: dimension: 1 interpretation: [r1#](x0) = 1x0 + 0, [ql](x0) = 0, [qr](x0) = 0, [b](x0) = 0, [r1](x0) = 7x0 + 0, [m](x0) = 8x0 + 1, [1](x0) = x0, [r0](x0) = x0, [0](x0) = x0 orientation: r1#(0(x1)) = 1x1 + 0 >= 1x1 + 0 = r1#(x1) r1#(1(x1)) = 1x1 + 0 >= 1x1 + 0 = r1#(x1) r1#(m(x1)) = 9x1 + 2 >= 1x1 + 0 = r1#(x1) r0(0(x1)) = x1 >= x1 = 0(r0(x1)) r0(1(x1)) = x1 >= x1 = 1(r0(x1)) r0(m(x1)) = 8x1 + 1 >= 8x1 + 1 = m(r0(x1)) r1(0(x1)) = 7x1 + 0 >= 7x1 + 0 = 0(r1(x1)) r1(1(x1)) = 7x1 + 0 >= 7x1 + 0 = 1(r1(x1)) r1(m(x1)) = 15x1 + 8 >= 15x1 + 8 = m(r1(x1)) r0(b(x1)) = 0 >= 0 = qr(0(b(x1))) r1(b(x1)) = 7 >= 0 = qr(1(b(x1))) 0(qr(x1)) = 0 >= 0 = qr(0(x1)) 1(qr(x1)) = 0 >= 0 = qr(1(x1)) m(qr(x1)) = 8 >= 0 = ql(m(x1)) 0(ql(x1)) = 0 >= 0 = ql(0(x1)) 1(ql(x1)) = 0 >= 0 = ql(1(x1)) b(ql(0(x1))) = 0 >= 0 = 0(b(r0(x1))) b(ql(1(x1))) = 0 >= 0 = 1(b(r1(x1))) problem: DPs: r1#(0(x1)) -> r1#(x1) r1#(1(x1)) -> r1#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) EDG Processor: DPs: r1#(0(x1)) -> r1#(x1) r1#(1(x1)) -> r1#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) graph: r1#(1(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1) r1#(1(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1) r1#(0(x1)) -> r1#(x1) -> r1#(0(x1)) -> r1#(x1) r1#(0(x1)) -> r1#(x1) -> r1#(1(x1)) -> r1#(x1) CDG Processor: DPs: r1#(0(x1)) -> r1#(x1) r1#(1(x1)) -> r1#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) graph: Qed DPs: r0#(0(x1)) -> r0#(x1) r0#(1(x1)) -> r0#(x1) r0#(m(x1)) -> r0#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) KBO Processor: argument filtering: pi(0) = 0 pi(r0) = 0 pi(1) = 0 pi(m) = [0] pi(r1) = 0 pi(b) = [] pi(qr) = 0 pi(ql) = 0 pi(r0#) = 0 weight function: w0 = 1 w(r0#) = w(ql) = w(qr) = w(b) = w(r1) = w(m) = w(1) = w(r0) = w(0) = 1 precedence: r0# ~ ql ~ qr ~ b ~ r1 ~ m ~ 1 ~ r0 ~ 0 problem: DPs: r0#(0(x1)) -> r0#(x1) r0#(1(x1)) -> r0#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) EDG Processor: DPs: r0#(0(x1)) -> r0#(x1) r0#(1(x1)) -> r0#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) graph: r0#(1(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1) r0#(1(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1) r0#(0(x1)) -> r0#(x1) -> r0#(0(x1)) -> r0#(x1) r0#(0(x1)) -> r0#(x1) -> r0#(1(x1)) -> r0#(x1) CDG Processor: DPs: r0#(0(x1)) -> r0#(x1) r0#(1(x1)) -> r0#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) graph: Qed DPs: m#(qr(x1)) -> m#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Arctic Interpretation Processor: dimension: 1 interpretation: [m#](x0) = x0, [ql](x0) = x0, [qr](x0) = 7x0, [b](x0) = 0, [r1](x0) = 7, [m](x0) = 0, [1](x0) = x0, [r0](x0) = 15x0 + 12, [0](x0) = x0 orientation: m#(qr(x1)) = 7x1 >= x1 = m#(x1) r0(0(x1)) = 15x1 + 12 >= 15x1 + 12 = 0(r0(x1)) r0(1(x1)) = 15x1 + 12 >= 15x1 + 12 = 1(r0(x1)) r0(m(x1)) = 15 >= 0 = m(r0(x1)) r1(0(x1)) = 7 >= 7 = 0(r1(x1)) r1(1(x1)) = 7 >= 7 = 1(r1(x1)) r1(m(x1)) = 7 >= 0 = m(r1(x1)) r0(b(x1)) = 15 >= 7 = qr(0(b(x1))) r1(b(x1)) = 7 >= 7 = qr(1(b(x1))) 0(qr(x1)) = 7x1 >= 7x1 = qr(0(x1)) 1(qr(x1)) = 7x1 >= 7x1 = qr(1(x1)) m(qr(x1)) = 0 >= 0 = ql(m(x1)) 0(ql(x1)) = x1 >= x1 = ql(0(x1)) 1(ql(x1)) = x1 >= x1 = ql(1(x1)) b(ql(0(x1))) = 0 >= 0 = 0(b(r0(x1))) b(ql(1(x1))) = 0 >= 0 = 1(b(r1(x1))) problem: DPs: TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Qed DPs: 1#(qr(x1)) -> 1#(x1) 1#(ql(x1)) -> 1#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Arctic Interpretation Processor: dimension: 1 interpretation: [1#](x0) = x0, [ql](x0) = 1x0, [qr](x0) = 1x0, [b](x0) = x0, [r1](x0) = 1x0, [m](x0) = x0, [1](x0) = x0, [r0](x0) = 1x0, [0](x0) = x0 orientation: 1#(qr(x1)) = 1x1 >= x1 = 1#(x1) 1#(ql(x1)) = 1x1 >= x1 = 1#(x1) r0(0(x1)) = 1x1 >= 1x1 = 0(r0(x1)) r0(1(x1)) = 1x1 >= 1x1 = 1(r0(x1)) r0(m(x1)) = 1x1 >= 1x1 = m(r0(x1)) r1(0(x1)) = 1x1 >= 1x1 = 0(r1(x1)) r1(1(x1)) = 1x1 >= 1x1 = 1(r1(x1)) r1(m(x1)) = 1x1 >= 1x1 = m(r1(x1)) r0(b(x1)) = 1x1 >= 1x1 = qr(0(b(x1))) r1(b(x1)) = 1x1 >= 1x1 = qr(1(b(x1))) 0(qr(x1)) = 1x1 >= 1x1 = qr(0(x1)) 1(qr(x1)) = 1x1 >= 1x1 = qr(1(x1)) m(qr(x1)) = 1x1 >= 1x1 = ql(m(x1)) 0(ql(x1)) = 1x1 >= 1x1 = ql(0(x1)) 1(ql(x1)) = 1x1 >= 1x1 = ql(1(x1)) b(ql(0(x1))) = 1x1 >= 1x1 = 0(b(r0(x1))) b(ql(1(x1))) = 1x1 >= 1x1 = 1(b(r1(x1))) problem: DPs: TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) Qed DPs: 0#(qr(x1)) -> 0#(x1) 0#(ql(x1)) -> 0#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) KBO Processor: argument filtering: pi(0) = 0 pi(r0) = [0] pi(1) = 0 pi(m) = 0 pi(r1) = [0] pi(b) = [] pi(qr) = [0] pi(ql) = 0 pi(0#) = 0 weight function: w0 = 1 w(0#) = w(b) = w(r1) = w(r0) = 1 w(ql) = w(qr) = w(m) = w(1) = w(0) = 0 precedence: 1 > 0# ~ ql ~ qr ~ b ~ r1 ~ m ~ r0 ~ 0 problem: DPs: 0#(ql(x1)) -> 0#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) EDG Processor: DPs: 0#(ql(x1)) -> 0#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) graph: 0#(ql(x1)) -> 0#(x1) -> 0#(ql(x1)) -> 0#(x1) CDG Processor: DPs: 0#(ql(x1)) -> 0#(x1) TRS: r0(0(x1)) -> 0(r0(x1)) r0(1(x1)) -> 1(r0(x1)) r0(m(x1)) -> m(r0(x1)) r1(0(x1)) -> 0(r1(x1)) r1(1(x1)) -> 1(r1(x1)) r1(m(x1)) -> m(r1(x1)) r0(b(x1)) -> qr(0(b(x1))) r1(b(x1)) -> qr(1(b(x1))) 0(qr(x1)) -> qr(0(x1)) 1(qr(x1)) -> qr(1(x1)) m(qr(x1)) -> ql(m(x1)) 0(ql(x1)) -> ql(0(x1)) 1(ql(x1)) -> ql(1(x1)) b(ql(0(x1))) -> 0(b(r0(x1))) b(ql(1(x1))) -> 1(b(r1(x1))) graph: Qed