YES Problem: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Proof: DP Processor: DPs: a__f#(X) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) TDG Processor: DPs: a__f#(X) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) graph: a__if#(false(),X,Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(false(),X,Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__if#(false(),X,Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X2) a__if#(false(),X,Y) -> mark#(Y) -> mark#(f(X)) -> a__f#(mark(X)) a__if#(false(),X,Y) -> mark#(Y) -> mark#(f(X)) -> mark#(X) a__if#(true(),X,Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__if#(true(),X,Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__if#(true(),X,Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) a__if#(true(),X,Y) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) a__if#(true(),X,Y) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) -> a__if#(false(),X,Y) -> mark#(Y) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) -> a__if#(true(),X,Y) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) -> a__f#(X) -> a__if#(mark(X),c(),f(true())) mark#(f(X)) -> a__f#(mark(X)) -> a__f#(X) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) -> a__if#(false(),X,Y) -> mark#(Y) a__f#(X) -> a__if#(mark(X),c(),f(true())) -> a__if#(true(),X,Y) -> mark#(X) a__f#(X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) a__f#(X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__f#(X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) a__f#(X) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) a__f#(X) -> mark#(X) -> mark#(f(X)) -> mark#(X) Arctic Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = x1 + x2 + 6, [mark#](x0) = x0, [a__f#](x0) = x0 + 6, [if](x0, x1, x2) = x0 + 5x1 + x2 + 6, [false] = 0, [a__if](x0, x1, x2) = x0 + 5x1 + x2 + 6, [f](x0) = x0 + 6, [true] = 0, [c] = 0, [mark](x0) = x0 + 1, [a__f](x0) = x0 + 6 orientation: a__f#(X) = X + 6 >= X = mark#(X) a__f#(X) = X + 6 >= 6 = a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) = X + Y + 6 >= X = mark#(X) a__if#(false(),X,Y) = X + Y + 6 >= Y = mark#(Y) mark#(f(X)) = X + 6 >= X = mark#(X) mark#(f(X)) = X + 6 >= X + 6 = a__f#(mark(X)) mark#(if(X1,X2,X3)) = X1 + 5X2 + X3 + 6 >= X2 = mark#(X2) mark#(if(X1,X2,X3)) = X1 + 5X2 + X3 + 6 >= X1 = mark#(X1) mark#(if(X1,X2,X3)) = X1 + 5X2 + X3 + 6 >= X2 + X3 + 6 = a__if#(mark(X1),mark(X2),X3) a__f(X) = X + 6 >= X + 6 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = 5X + Y + 6 >= X + 1 = mark(X) a__if(false(),X,Y) = 5X + Y + 6 >= Y + 1 = mark(Y) mark(f(X)) = X + 6 >= X + 6 = a__f(mark(X)) mark(if(X1,X2,X3)) = X1 + 5X2 + X3 + 6 >= X1 + 5X2 + X3 + 6 = a__if(mark(X1),mark(X2),X3) mark(c()) = 1 >= 0 = c() mark(true()) = 1 >= 0 = true() mark(false()) = 1 >= 0 = false() a__f(X) = X + 6 >= X + 6 = f(X) a__if(X1,X2,X3) = X1 + 5X2 + X3 + 6 >= X1 + 5X2 + X3 + 6 = if(X1,X2,X3) problem: DPs: a__f#(X) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = x0 + 7x1 + 5x2, [mark#](x0) = 5x0 + 0, [a__f#](x0) = 5x0 + 7, [if](x0, x1, x2) = 1x0 + 2x1 + x2, [false] = 5, [a__if](x0, x1, x2) = 1x0 + 2x1 + x2, [f](x0) = 2x0 + 2, [true] = 0, [c] = 0, [mark](x0) = x0, [a__f](x0) = 2x0 + 2 orientation: a__f#(X) = 5X + 7 >= 5X + 0 = mark#(X) a__f#(X) = 5X + 7 >= X + 7 = a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) = 7X + 5Y + 0 >= 5X + 0 = mark#(X) a__if#(false(),X,Y) = 7X + 5Y + 5 >= 5Y + 0 = mark#(Y) mark#(f(X)) = 7X + 7 >= 5X + 0 = mark#(X) mark#(f(X)) = 7X + 7 >= 5X + 7 = a__f#(mark(X)) mark#(if(X1,X2,X3)) = 6X1 + 7X2 + 5X3 + 0 >= 5X1 + 0 = mark#(X1) mark#(if(X1,X2,X3)) = 6X1 + 7X2 + 5X3 + 0 >= X1 + 7X2 + 5X3 = a__if#(mark(X1),mark(X2),X3) a__f(X) = 2X + 2 >= 1X + 2 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = 2X + Y + 1 >= X = mark(X) a__if(false(),X,Y) = 2X + Y + 6 >= Y = mark(Y) mark(f(X)) = 2X + 2 >= 2X + 2 = a__f(mark(X)) mark(if(X1,X2,X3)) = 1X1 + 2X2 + X3 >= 1X1 + 2X2 + X3 = a__if(mark(X1),mark(X2),X3) mark(c()) = 0 >= 0 = c() mark(true()) = 0 >= 0 = true() mark(false()) = 5 >= 5 = false() a__f(X) = 2X + 2 >= 2X + 2 = f(X) a__if(X1,X2,X3) = 1X1 + 2X2 + X3 >= 1X1 + 2X2 + X3 = if(X1,X2,X3) problem: DPs: a__f#(X) -> mark#(X) a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = x0 + x1 + x2 + 0, [mark#](x0) = x0, [a__f#](x0) = 1x0 + 1, [if](x0, x1, x2) = x0 + x1 + x2 + 0, [false] = 0, [a__if](x0, x1, x2) = x0 + x1 + x2 + 0, [f](x0) = 1x0 + 1, [true] = 0, [c] = 0, [mark](x0) = x0 + 0, [a__f](x0) = 1x0 + 1 orientation: a__f#(X) = 1X + 1 >= X = mark#(X) a__f#(X) = 1X + 1 >= X + 1 = a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) = X + Y + 0 >= X = mark#(X) a__if#(false(),X,Y) = X + Y + 0 >= Y = mark#(Y) mark#(f(X)) = 1X + 1 >= 1X + 1 = a__f#(mark(X)) mark#(if(X1,X2,X3)) = X1 + X2 + X3 + 0 >= X1 = mark#(X1) mark#(if(X1,X2,X3)) = X1 + X2 + X3 + 0 >= X1 + X2 + X3 + 0 = a__if#(mark(X1),mark(X2),X3) a__f(X) = 1X + 1 >= X + 1 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = X + Y + 0 >= X + 0 = mark(X) a__if(false(),X,Y) = X + Y + 0 >= Y + 0 = mark(Y) mark(f(X)) = 1X + 1 >= 1X + 1 = a__f(mark(X)) mark(if(X1,X2,X3)) = X1 + X2 + X3 + 0 >= X1 + X2 + X3 + 0 = a__if(mark(X1),mark(X2),X3) mark(c()) = 0 >= 0 = c() mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__f(X) = 1X + 1 >= 1X + 1 = f(X) a__if(X1,X2,X3) = X1 + X2 + X3 + 0 >= X1 + X2 + X3 + 0 = if(X1,X2,X3) problem: DPs: a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = 1x0 + x1 + x2 + 0, [mark#](x0) = x0 + 1, [a__f#](x0) = 4x0 + 4, [if](x0, x1, x2) = 4x0 + 4x1 + x2 + 4, [false] = 1, [a__if](x0, x1, x2) = 4x0 + 4x1 + x2 + 4, [f](x0) = 4x0 + 4, [true] = 0, [c] = 0, [mark](x0) = x0 + 0, [a__f](x0) = 4x0 + 4 orientation: a__f#(X) = 4X + 4 >= 1X + 4 = a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) = X + Y + 1 >= X + 1 = mark#(X) a__if#(false(),X,Y) = X + Y + 2 >= Y + 1 = mark#(Y) mark#(f(X)) = 4X + 4 >= 4X + 4 = a__f#(mark(X)) mark#(if(X1,X2,X3)) = 4X1 + 4X2 + X3 + 4 >= X1 + 1 = mark#(X1) mark#(if(X1,X2,X3)) = 4X1 + 4X2 + X3 + 4 >= 1X1 + X2 + X3 + 1 = a__if#(mark(X1),mark(X2),X3) a__f(X) = 4X + 4 >= 4X + 4 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = 4X + Y + 4 >= X + 0 = mark(X) a__if(false(),X,Y) = 4X + Y + 5 >= Y + 0 = mark(Y) mark(f(X)) = 4X + 4 >= 4X + 4 = a__f(mark(X)) mark(if(X1,X2,X3)) = 4X1 + 4X2 + X3 + 4 >= 4X1 + 4X2 + X3 + 4 = a__if(mark(X1),mark(X2),X3) mark(c()) = 0 >= 0 = c() mark(true()) = 0 >= 0 = true() mark(false()) = 1 >= 1 = false() a__f(X) = 4X + 4 >= 4X + 4 = f(X) a__if(X1,X2,X3) = 4X1 + 4X2 + X3 + 4 >= 4X1 + 4X2 + X3 + 4 = if(X1,X2,X3) problem: DPs: a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = 7x1 + x2 + 4, [mark#](x0) = x0, [a__f#](x0) = x0 + 7, [if](x0, x1, x2) = 7x1 + x2 + 4, [false] = 0, [a__if](x0, x1, x2) = 7x1 + x2 + 4, [f](x0) = x0 + 7, [true] = 0, [c] = 0, [mark](x0) = x0, [a__f](x0) = x0 + 7 orientation: a__f#(X) = X + 7 >= 7 = a__if#(mark(X),c(),f(true())) a__if#(true(),X,Y) = 7X + Y + 4 >= X = mark#(X) a__if#(false(),X,Y) = 7X + Y + 4 >= Y = mark#(Y) mark#(f(X)) = X + 7 >= X + 7 = a__f#(mark(X)) mark#(if(X1,X2,X3)) = 7X2 + X3 + 4 >= 7X2 + X3 + 4 = a__if#(mark(X1),mark(X2),X3) a__f(X) = X + 7 >= 7 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = 7X + Y + 4 >= X = mark(X) a__if(false(),X,Y) = 7X + Y + 4 >= Y = mark(Y) mark(f(X)) = X + 7 >= X + 7 = a__f(mark(X)) mark(if(X1,X2,X3)) = 7X2 + X3 + 4 >= 7X2 + X3 + 4 = a__if(mark(X1),mark(X2),X3) mark(c()) = 0 >= 0 = c() mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__f(X) = X + 7 >= X + 7 = f(X) a__if(X1,X2,X3) = 7X2 + X3 + 4 >= 7X2 + X3 + 4 = if(X1,X2,X3) problem: DPs: a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> a__f#(mark(X)) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),mark(X2),X3) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = x0 + x1 + x2 + 0, [mark#](x0) = x0, [a__f#](x0) = 3x0 + 4, [if](x0, x1, x2) = 3x0 + 2x1 + 1x2 + 4, [false] = 0, [a__if](x0, x1, x2) = 3x0 + 2x1 + 1x2 + 4, [f](x0) = 4x0 + 4, [true] = 0, [c] = 0, [mark](x0) = 1x0 + 1, [a__f](x0) = 4x0 + 5 orientation: a__f#(X) = 3X + 4 >= 1X + 4 = a__if#(mark(X),c(),f(true())) a__if#(false(),X,Y) = X + Y + 0 >= Y = mark#(Y) mark#(f(X)) = 4X + 4 >= 4X + 4 = a__f#(mark(X)) mark#(if(X1,X2,X3)) = 3X1 + 2X2 + 1X3 + 4 >= 1X1 + 1X2 + X3 + 1 = a__if#(mark(X1),mark(X2),X3) a__f(X) = 4X + 5 >= 4X + 5 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = 2X + 1Y + 4 >= 1X + 1 = mark(X) a__if(false(),X,Y) = 2X + 1Y + 4 >= 1Y + 1 = mark(Y) mark(f(X)) = 5X + 5 >= 5X + 5 = a__f(mark(X)) mark(if(X1,X2,X3)) = 4X1 + 3X2 + 2X3 + 5 >= 4X1 + 3X2 + 1X3 + 4 = a__if(mark(X1),mark(X2),X3) mark(c()) = 1 >= 0 = c() mark(true()) = 1 >= 0 = true() mark(false()) = 1 >= 0 = false() a__f(X) = 4X + 5 >= 4X + 4 = f(X) a__if(X1,X2,X3) = 3X1 + 2X2 + 1X3 + 4 >= 3X1 + 2X2 + 1X3 + 4 = if(X1,X2,X3) problem: DPs: a__f#(X) -> a__if#(mark(X),c(),f(true())) a__if#(false(),X,Y) -> mark#(Y) mark#(f(X)) -> a__f#(mark(X)) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [a__if#](x0, x1, x2) = x0 + 3x1 + 3x2 + 0, [mark#](x0) = 2x0 + 4, [a__f#](x0) = 2x0 + 4, [if](x0, x1, x2) = x0 + x1 + 2x2 + 1, [false] = 6, [a__if](x0, x1, x2) = x0 + x1 + 2x2 + 2, [f](x0) = x0, [true] = 0, [c] = 1, [mark](x0) = x0 + 2, [a__f](x0) = x0 + 2 orientation: a__f#(X) = 2X + 4 >= X + 4 = a__if#(mark(X),c(),f(true())) a__if#(false(),X,Y) = 3X + 3Y + 6 >= 2Y + 4 = mark#(Y) mark#(f(X)) = 2X + 4 >= 2X + 4 = a__f#(mark(X)) a__f(X) = X + 2 >= X + 2 = a__if(mark(X),c(),f(true())) a__if(true(),X,Y) = X + 2Y + 2 >= X + 2 = mark(X) a__if(false(),X,Y) = X + 2Y + 6 >= Y + 2 = mark(Y) mark(f(X)) = X + 2 >= X + 2 = a__f(mark(X)) mark(if(X1,X2,X3)) = X1 + X2 + 2X3 + 2 >= X1 + X2 + 2X3 + 2 = a__if(mark(X1),mark(X2),X3) mark(c()) = 2 >= 1 = c() mark(true()) = 2 >= 0 = true() mark(false()) = 6 >= 6 = false() a__f(X) = X + 2 >= X = f(X) a__if(X1,X2,X3) = X1 + X2 + 2X3 + 2 >= X1 + X2 + 2X3 + 1 = if(X1,X2,X3) problem: DPs: a__f#(X) -> a__if#(mark(X),c(),f(true())) mark#(f(X)) -> a__f#(mark(X)) TRS: a__f(X) -> a__if(mark(X),c(),f(true())) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(f(X)) -> a__f(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),mark(X2),X3) mark(c()) -> c() mark(true()) -> true() mark(false()) -> false() a__f(X) -> f(X) a__if(X1,X2,X3) -> if(X1,X2,X3) SCC Processor: #sccs: 0 #rules: 0 #arcs: 36/4