YES Problem: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Proof: DP Processor: DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) EDG Processor: DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) graph: f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(f(f(a(),x),b()),b()) -> f#(x,b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(x,b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(a(),f(f(x,b()),b())) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) -> f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) -> f#(a(),f(a(),f(a(),f(x,b())))) -> f#(f(a(),f(a(),f(a(),x))),b()) SCC Processor: #sccs: 2 #rules: 6 #arcs: 28/64 DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),x) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Arctic Interpretation Processor: dimension: 1 usable rules: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) interpretation: [f#](x0, x1) = x1 + -16, [f](x0, x1) = x0 + 1x1 + 2, [b] = 0, [a] = 3 orientation: f#(a(),f(a(),f(a(),f(x,b())))) = 2x + 4 >= 2x + 4 = f#(a(),f(a(),f(a(),x))) f#(a(),f(a(),f(a(),f(x,b())))) = 2x + 4 >= 1x + 3 = f#(a(),f(a(),x)) f#(a(),f(a(),f(a(),f(x,b())))) = 2x + 4 >= x + -16 = f#(a(),x) f(a(),f(a(),f(a(),f(x,b())))) = 3x + 5 >= 3x + 5 = f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) = 1x + 3 >= 1x + 3 = f(f(a(),f(f(x,b()),b())),b()) problem: DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Restore Modifier: DPs: f#(a(),f(a(),f(a(),f(x,b())))) -> f#(a(),f(a(),f(a(),x))) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {1} transitions: f{#,1}(11,13) -> 1* a1() -> 11* f1(4,2) -> 11* f1(11,2) -> 11,13,12 f1(11,4) -> 12* f1(11,12) -> 13* f1(13,2) -> 11* f1(3,2) -> 11* f1(11,3) -> 12* f1(11,13) -> 11* f1(12,2) -> 11* f1(2,2) -> 11* b1() -> 2* f40() -> 2* f{#,0}(3,5) -> 1* a0() -> 3* f0(3,3) -> 4* f0(3,5) -> 3* f0(4,4) -> 3* f0(3,2) -> 4* f0(3,4) -> 3,5 f0(5,4) -> 3* f0(2,4) -> 3* b0() -> 4* 5 -> 4* problem: DPs: TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Qed DPs: f#(f(f(a(),x),b()),b()) -> f#(f(a(),f(f(x,b()),b())),b()) f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: f140() -> 3* f{#,0}(7,2) -> 1* a0() -> 6* f0(4,2) -> 5* f0(3,2) -> 4* f0(6,5) -> 7* f0(7,2) -> 5* f0(2,2) -> 4* b0() -> 2* 5 -> 4* problem: DPs: f#(f(f(a(),x),b()),b()) -> f#(f(x,b()),b()) f#(f(f(a(),x),b()),b()) -> f#(x,b()) TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Semantic Labeling Processor: dimension: 2 usable rules: interpretation: [1 0] [1 0] [f](x0, x1) = [0 0]x0 + [0 0]x1, [0] [b] = [1], [1] [a] = [0] labeled: f# usable (for model): f# f a b argument filtering: pi(a) = [] pi(b) = [] pi(f) = 1 pi(f#) = [] precedence: f# ~ f ~ b ~ a problem: DPs: TRS: f(a(),f(a(),f(a(),f(x,b())))) -> f(f(a(),f(a(),f(a(),x))),b()) f(f(f(a(),x),b()),b()) -> f(f(a(),f(f(x,b()),b())),b()) Qed