YES Problem: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) Proof: DP Processor: DPs: a#(b(x1)) -> a#(x1) a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> c#(b(a(x1))) b#(x1) -> a#(x1) c#(c(x1)) -> b#(x1) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) TDG Processor: DPs: a#(b(x1)) -> a#(x1) a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> c#(b(a(x1))) b#(x1) -> a#(x1) c#(c(x1)) -> b#(x1) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) graph: c#(c(x1)) -> b#(x1) -> b#(x1) -> a#(x1) b#(x1) -> a#(x1) -> a#(b(x1)) -> c#(b(a(x1))) b#(x1) -> a#(x1) -> a#(b(x1)) -> b#(a(x1)) b#(x1) -> a#(x1) -> a#(b(x1)) -> a#(x1) a#(b(x1)) -> c#(b(a(x1))) -> c#(c(x1)) -> b#(x1) a#(b(x1)) -> b#(a(x1)) -> b#(x1) -> a#(x1) a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> c#(b(a(x1))) a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> a#(x1) Arctic Interpretation Processor: dimension: 3 usable rules: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) interpretation: [c#](x0) = [0 1 1]x0 + [0], [b#](x0) = [-& 1 1 ]x0 + [0], [a#](x0) = [-& 1 0 ]x0 + [0], [-& 0 0 ] [0] [c](x0) = [1 1 0 ]x0 + [0] [0 0 1 ] [0], [1 0 0] [0] [b](x0) = [1 0 0]x0 + [0] [1 0 0] [0], [0 -& -&] [-&] [a](x0) = [1 0 0 ]x0 + [0 ] [1 0 0 ] [0 ] orientation: a#(b(x1)) = [2 1 1]x1 + [1] >= [-& 1 0 ]x1 + [0] = a#(x1) a#(b(x1)) = [2 1 1]x1 + [1] >= [2 1 1]x1 + [1] = b#(a(x1)) a#(b(x1)) = [2 1 1]x1 + [1] >= [2 1 1]x1 + [1] = c#(b(a(x1))) b#(x1) = [-& 1 1 ]x1 + [0] >= [-& 1 0 ]x1 + [0] = a#(x1) c#(c(x1)) = [2 2 2]x1 + [1] >= [-& 1 1 ]x1 + [0] = b#(x1) [0 -& -&] [-&] a(x1) = [1 0 0 ]x1 + [0 ] >= x1 = x1 [1 0 0 ] [0 ] [1 0 0] [0] [1 0 0] [0] a(b(x1)) = [2 1 1]x1 + [1] >= [2 1 1]x1 + [1] = c(b(a(x1))) [2 1 1] [1] [2 1 1] [1] [1 0 0] [0] [0 -& -&] [-&] b(x1) = [1 0 0]x1 + [0] >= [1 0 0 ]x1 + [0 ] = a(x1) [1 0 0] [0] [1 0 0 ] [0 ] [1 1 1] [0] [1 0 0] [0] c(c(x1)) = [2 2 1]x1 + [1] >= [1 0 0]x1 + [0] = b(x1) [1 1 2] [1] [1 0 0] [0] problem: DPs: a#(b(x1)) -> a#(x1) a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> c#(b(a(x1))) b#(x1) -> a#(x1) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) Restore Modifier: DPs: a#(b(x1)) -> a#(x1) a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> c#(b(a(x1))) b#(x1) -> a#(x1) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) EDG Processor: DPs: a#(b(x1)) -> a#(x1) a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> c#(b(a(x1))) b#(x1) -> a#(x1) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) graph: b#(x1) -> a#(x1) -> a#(b(x1)) -> a#(x1) b#(x1) -> a#(x1) -> a#(b(x1)) -> b#(a(x1)) b#(x1) -> a#(x1) -> a#(b(x1)) -> c#(b(a(x1))) a#(b(x1)) -> b#(a(x1)) -> b#(x1) -> a#(x1) a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> a#(x1) a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> a#(x1) -> a#(b(x1)) -> c#(b(a(x1))) SCC Processor: #sccs: 1 #rules: 3 #arcs: 7/16 DPs: b#(x1) -> a#(x1) a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> a#(x1) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) Arctic Interpretation Processor: dimension: 3 usable rules: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) interpretation: [b#](x0) = [0 0 1]x0 + [0], [a#](x0) = [0 -& 0 ]x0 + [0], [-& 0 0 ] [0 ] [c](x0) = [0 0 0 ]x0 + [0 ] [1 -& 0 ] [-&], [0 -& 0 ] [0] [b](x0) = [0 0 0 ]x0 + [0] [1 0 1 ] [1], [0 -& 0 ] [-&] [a](x0) = [0 0 0 ]x0 + [-&] [0 -& 0 ] [0 ] orientation: b#(x1) = [0 0 1]x1 + [0] >= [0 -& 0 ]x1 + [0] = a#(x1) a#(b(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 + [1] = b#(a(x1)) a#(b(x1)) = [1 0 1]x1 + [1] >= [0 -& 0 ]x1 + [0] = a#(x1) [0 -& 0 ] [-&] a(x1) = [0 0 0 ]x1 + [-&] >= x1 = x1 [0 -& 0 ] [0 ] [1 0 1] [1] [1 0 1] [1] a(b(x1)) = [1 0 1]x1 + [1] >= [1 0 1]x1 + [1] = c(b(a(x1))) [1 0 1] [1] [1 0 1] [1] [0 -& 0 ] [0] [0 -& 0 ] [-&] b(x1) = [0 0 0 ]x1 + [0] >= [0 0 0 ]x1 + [-&] = a(x1) [1 0 1 ] [1] [0 -& 0 ] [0 ] [1 0 0] [0] [0 -& 0 ] [0] c(c(x1)) = [1 0 0]x1 + [0] >= [0 0 0 ]x1 + [0] = b(x1) [1 1 1] [1] [1 0 1 ] [1] problem: DPs: b#(x1) -> a#(x1) a#(b(x1)) -> b#(a(x1)) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) Restore Modifier: DPs: b#(x1) -> a#(x1) a#(b(x1)) -> b#(a(x1)) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) EDG Processor: DPs: b#(x1) -> a#(x1) a#(b(x1)) -> b#(a(x1)) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) graph: b#(x1) -> a#(x1) -> a#(b(x1)) -> b#(a(x1)) a#(b(x1)) -> b#(a(x1)) -> b#(x1) -> a#(x1) Arctic Interpretation Processor: dimension: 4 usable rules: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) interpretation: [b#](x0) = [0 0 1 0]x0 + [1], [a#](x0) = [-& -& 0 -&]x0 + [0], [0 0 0 0 ] [1 ] [-& -& 0 0 ] [-&] [c](x0) = [0 1 0 0 ]x0 + [0 ] [0 0 0 0 ] [-&], [0 1 0 0 ] [0] [-& 0 0 -&] [0] [b](x0) = [0 1 1 0 ]x0 + [1] [-& 0 0 0 ] [1], [0 0 0 0 ] [0] [-& 0 0 -&] [0] [a](x0) = [-& 0 0 -&]x0 + [0] [-& 0 0 0 ] [1] orientation: b#(x1) = [0 0 1 0]x1 + [1] >= [-& -& 0 -&]x1 + [0] = a#(x1) a#(b(x1)) = [0 1 1 0]x1 + [1] >= [0 1 1 0]x1 + [1] = b#(a(x1)) [0 0 0 0 ] [0] [-& 0 0 -&] [0] a(x1) = [-& 0 0 -&]x1 + [0] >= x1 = x1 [-& 0 0 0 ] [1] [0 1 1 0] [1] [0 1 1 0] [1] [0 1 1 0] [1] [0 1 1 0] [1] a(b(x1)) = [0 1 1 0]x1 + [1] >= [0 1 1 0]x1 + [1] = c(b(a(x1))) [0 1 1 0] [1] [0 1 1 0] [1] [0 1 0 0 ] [0] [0 0 0 0 ] [0] [-& 0 0 -&] [0] [-& 0 0 -&] [0] b(x1) = [0 1 1 0 ]x1 + [1] >= [-& 0 0 -&]x1 + [0] = a(x1) [-& 0 0 0 ] [1] [-& 0 0 0 ] [1] [0 1 0 0] [1] [0 1 0 0 ] [0] [0 1 0 0] [0] [-& 0 0 -&] [0] c(c(x1)) = [0 1 1 1]x1 + [1] >= [0 1 1 0 ]x1 + [1] = b(x1) [0 1 0 0] [1] [-& 0 0 0 ] [1] problem: DPs: a#(b(x1)) -> b#(a(x1)) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) Restore Modifier: DPs: a#(b(x1)) -> b#(a(x1)) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) EDG Processor: DPs: a#(b(x1)) -> b#(a(x1)) TRS: a(x1) -> x1 a(b(x1)) -> c(b(a(x1))) b(x1) -> a(x1) c(c(x1)) -> b(x1) graph: Qed