MAYBE Problem: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Proof: DP Processor: DPs: leq#(s(X),s(Y)) -> leq#(X,Y) if#(true(),X,Y) -> activate#(X) if#(false(),X,Y) -> activate#(Y) diff#(X,Y) -> leq#(X,Y) diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__diff(X1,X2)) -> activate#(X2) activate#(n__diff(X1,X2)) -> activate#(X1) activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__p(X)) -> activate#(X) activate#(n__p(X)) -> p#(activate(X)) TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X TDG Processor: DPs: leq#(s(X),s(Y)) -> leq#(X,Y) if#(true(),X,Y) -> activate#(X) if#(false(),X,Y) -> activate#(Y) diff#(X,Y) -> leq#(X,Y) diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__diff(X1,X2)) -> activate#(X2) activate#(n__diff(X1,X2)) -> activate#(X1) activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__p(X)) -> activate#(X) activate#(n__p(X)) -> p#(activate(X)) TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X graph: diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) -> if#(false(),X,Y) -> activate#(Y) diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) -> if#(true(),X,Y) -> activate#(X) diff#(X,Y) -> leq#(X,Y) -> leq#(s(X),s(Y)) -> leq#(X,Y) activate#(n__s(X)) -> activate#(X) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__p(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__s(X)) -> activate#(X) -> activate#(n__diff(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__diff(X1,X2)) -> activate#(X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) -> diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) -> diff#(X,Y) -> leq#(X,Y) activate#(n__diff(X1,X2)) -> activate#(X2) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__diff(X1,X2)) -> activate#(X2) -> activate#(n__p(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> activate#(X2) -> activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__diff(X1,X2)) -> activate#(X2) -> activate#(n__diff(X1,X2)) -> activate#(X1) activate#(n__diff(X1,X2)) -> activate#(X2) -> activate#(n__diff(X1,X2)) -> activate#(X2) activate#(n__diff(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__diff(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> activate#(X2) -> activate#(n__0()) -> 0#() activate#(n__diff(X1,X2)) -> activate#(X1) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__diff(X1,X2)) -> activate#(X1) -> activate#(n__p(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> activate#(X1) -> activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__diff(X1,X2)) -> activate#(X1) -> activate#(n__diff(X1,X2)) -> activate#(X1) activate#(n__diff(X1,X2)) -> activate#(X1) -> activate#(n__diff(X1,X2)) -> activate#(X2) activate#(n__diff(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__diff(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__p(X)) -> activate#(X) -> activate#(n__p(X)) -> p#(activate(X)) activate#(n__p(X)) -> activate#(X) -> activate#(n__p(X)) -> activate#(X) activate#(n__p(X)) -> activate#(X) -> activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__p(X)) -> activate#(X) -> activate#(n__diff(X1,X2)) -> activate#(X1) activate#(n__p(X)) -> activate#(X) -> activate#(n__diff(X1,X2)) -> activate#(X2) activate#(n__p(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__p(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__p(X)) -> activate#(X) -> activate#(n__0()) -> 0#() if#(false(),X,Y) -> activate#(Y) -> activate#(n__p(X)) -> p#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__diff(X1,X2)) -> activate#(X1) if#(false(),X,Y) -> activate#(Y) -> activate#(n__diff(X1,X2)) -> activate#(X2) if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__0()) -> 0#() if#(true(),X,Y) -> activate#(X) -> activate#(n__p(X)) -> p#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__p(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) if#(true(),X,Y) -> activate#(X) -> activate#(n__diff(X1,X2)) -> activate#(X1) if#(true(),X,Y) -> activate#(X) -> activate#(n__diff(X1,X2)) -> activate#(X2) if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__0()) -> 0#() leq#(s(X),s(Y)) -> leq#(X,Y) -> leq#(s(X),s(Y)) -> leq#(X,Y) SCC Processor: #sccs: 2 #rules: 9 #arcs: 54/169 DPs: diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> activate#(X2) activate#(n__diff(X1,X2)) -> activate#(X1) activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [diff#](x0, x1) = 1x0 + x1 + 0, [activate#](x0) = x0, [if#](x0, x1, x2) = x1 + x2 + 0, [n__s](x0) = x0 + 0, [n__diff](x0, x1) = 1x0 + x1 + 0, [n__p](x0) = x0, [n__0] = 0, [diff](x0, x1) = 1x0 + x1 + 0, [activate](x0) = x0, [if](x0, x1, x2) = x0 + x1 + x2, [false] = 0, [true] = 0, [leq](x0, x1) = x0 + x1, [s](x0) = x0 + 0, [p](x0) = x0, [0] = 0 orientation: diff#(X,Y) = 1X + Y + 0 >= 1X + Y + 0 = if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) if#(true(),X,Y) = X + Y + 0 >= X = activate#(X) activate#(n__s(X)) = X + 0 >= X = activate#(X) activate#(n__diff(X1,X2)) = 1X1 + X2 + 0 >= X2 = activate#(X2) activate#(n__diff(X1,X2)) = 1X1 + X2 + 0 >= X1 = activate#(X1) activate#(n__diff(X1,X2)) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = diff#(activate(X1),activate(X2)) activate#(n__p(X)) = X >= X = activate#(X) if#(false(),X,Y) = X + Y + 0 >= Y = activate#(Y) p(0()) = 0 >= 0 = 0() p(s(X)) = X + 0 >= X = X leq(0(),Y) = Y + 0 >= 0 = true() leq(s(X),0()) = X + 0 >= 0 = false() leq(s(X),s(Y)) = X + Y + 0 >= X + Y = leq(X,Y) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) diff(X,Y) = 1X + Y + 0 >= 1X + Y + 0 = if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() = 0 >= 0 = n__0() s(X) = X + 0 >= X + 0 = n__s(X) diff(X1,X2) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = n__diff(X1,X2) p(X) = X >= X = n__p(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__diff(X1,X2)) = 1X1 + X2 + 0 >= 1X1 + X2 + 0 = diff(activate(X1),activate(X2)) activate(n__p(X)) = X >= X = p(activate(X)) activate(X) = X >= X = X problem: DPs: diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> activate#(X2) activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [diff#](x0, x1) = 2x1 + 0, [activate#](x0) = x0, [if#](x0, x1, x2) = x0 + x1 + x2 + 0, [n__s](x0) = x0 + 0, [n__diff](x0, x1) = 2x1 + 0, [n__p](x0) = x0, [n__0] = 0, [diff](x0, x1) = 2x1 + 0, [activate](x0) = x0, [if](x0, x1, x2) = x0 + x1 + x2 + 0, [false] = 0, [true] = 0, [leq](x0, x1) = 0, [s](x0) = x0 + 0, [p](x0) = x0, [0] = 0 orientation: diff#(X,Y) = 2Y + 0 >= 2Y + 0 = if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) if#(true(),X,Y) = X + Y + 0 >= X = activate#(X) activate#(n__s(X)) = X + 0 >= X = activate#(X) activate#(n__diff(X1,X2)) = 2X2 + 0 >= X2 = activate#(X2) activate#(n__diff(X1,X2)) = 2X2 + 0 >= 2X2 + 0 = diff#(activate(X1),activate(X2)) activate#(n__p(X)) = X >= X = activate#(X) if#(false(),X,Y) = X + Y + 0 >= Y = activate#(Y) p(0()) = 0 >= 0 = 0() p(s(X)) = X + 0 >= X = X leq(0(),Y) = 0 >= 0 = true() leq(s(X),0()) = 0 >= 0 = false() leq(s(X),s(Y)) = 0 >= 0 = leq(X,Y) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) diff(X,Y) = 2Y + 0 >= 2Y + 0 = if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() = 0 >= 0 = n__0() s(X) = X + 0 >= X + 0 = n__s(X) diff(X1,X2) = 2X2 + 0 >= 2X2 + 0 = n__diff(X1,X2) p(X) = X >= X = n__p(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__diff(X1,X2)) = 2X2 + 0 >= 2X2 + 0 = diff(activate(X1),activate(X2)) activate(n__p(X)) = X >= X = p(activate(X)) activate(X) = X >= X = X problem: DPs: diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) activate#(n__p(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [diff#](x0, x1) = 4x1 + 4, [activate#](x0) = 4x0 + 4, [if#](x0, x1, x2) = x0 + 4x1 + 4x2 + 4, [n__s](x0) = x0, [n__diff](x0, x1) = x1, [n__p](x0) = 3x0 + 3, [n__0] = 0, [diff](x0, x1) = x1 + 0, [activate](x0) = x0 + 0, [if](x0, x1, x2) = x0 + x1 + x2 + 0, [false] = 0, [true] = 0, [leq](x0, x1) = x1 + 0, [s](x0) = x0 + 0, [p](x0) = 3x0 + 3, [0] = 0 orientation: diff#(X,Y) = 4Y + 4 >= 4Y + 4 = if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) if#(true(),X,Y) = 4X + 4Y + 4 >= 4X + 4 = activate#(X) activate#(n__s(X)) = 4X + 4 >= 4X + 4 = activate#(X) activate#(n__diff(X1,X2)) = 4X2 + 4 >= 4X2 + 4 = diff#(activate(X1),activate(X2)) activate#(n__p(X)) = 7X + 7 >= 4X + 4 = activate#(X) if#(false(),X,Y) = 4X + 4Y + 4 >= 4Y + 4 = activate#(Y) p(0()) = 3 >= 0 = 0() p(s(X)) = 3X + 3 >= X = X leq(0(),Y) = Y + 0 >= 0 = true() leq(s(X),0()) = 0 >= 0 = false() leq(s(X),s(Y)) = Y + 0 >= Y + 0 = leq(X,Y) if(true(),X,Y) = X + Y + 0 >= X + 0 = activate(X) if(false(),X,Y) = X + Y + 0 >= Y + 0 = activate(Y) diff(X,Y) = Y + 0 >= Y + 0 = if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() = 0 >= 0 = n__0() s(X) = X + 0 >= X = n__s(X) diff(X1,X2) = X2 + 0 >= X2 = n__diff(X1,X2) p(X) = 3X + 3 >= 3X + 3 = n__p(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__diff(X1,X2)) = X2 + 0 >= X2 + 0 = diff(activate(X1),activate(X2)) activate(n__p(X)) = 3X + 3 >= 3X + 3 = p(activate(X)) activate(X) = X + 0 >= X = X problem: DPs: diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) if#(false(),X,Y) -> activate#(Y) TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [diff#](x0, x1) = 4x0 + 6x1 + 5, [activate#](x0) = x0 + 5, [if#](x0, x1, x2) = x0 + 1x1 + x2 + 0, [n__s](x0) = x0 + 4, [n__diff](x0, x1) = 4x0 + 6x1 + 4, [n__p](x0) = x0 + 0, [n__0] = 4, [diff](x0, x1) = 4x0 + 6x1 + 4, [activate](x0) = x0, [if](x0, x1, x2) = x1 + x2 + 0, [false] = 6, [true] = 7, [leq](x0, x1) = 3x0, [s](x0) = x0 + 4, [p](x0) = x0 + 0, [0] = 4 orientation: diff#(X,Y) = 4X + 6Y + 5 >= 4X + 6Y + 5 = if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) if#(true(),X,Y) = 1X + Y + 7 >= X + 5 = activate#(X) activate#(n__s(X)) = X + 5 >= X + 5 = activate#(X) activate#(n__diff(X1,X2)) = 4X1 + 6X2 + 5 >= 4X1 + 6X2 + 5 = diff#(activate(X1),activate(X2)) if#(false(),X,Y) = 1X + Y + 6 >= Y + 5 = activate#(Y) p(0()) = 4 >= 4 = 0() p(s(X)) = X + 4 >= X = X leq(0(),Y) = 7 >= 7 = true() leq(s(X),0()) = 3X + 7 >= 6 = false() leq(s(X),s(Y)) = 3X + 7 >= 3X = leq(X,Y) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) diff(X,Y) = 4X + 6Y + 4 >= 4X + 6Y + 4 = if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() = 4 >= 4 = n__0() s(X) = X + 4 >= X + 4 = n__s(X) diff(X1,X2) = 4X1 + 6X2 + 4 >= 4X1 + 6X2 + 4 = n__diff(X1,X2) p(X) = X + 0 >= X + 0 = n__p(X) activate(n__0()) = 4 >= 4 = 0() activate(n__s(X)) = X + 4 >= X + 4 = s(activate(X)) activate(n__diff(X1,X2)) = 4X1 + 6X2 + 4 >= 4X1 + 6X2 + 4 = diff(activate(X1),activate(X2)) activate(n__p(X)) = X + 0 >= X + 0 = p(activate(X)) activate(X) = X >= X = X problem: DPs: diff#(X,Y) -> if#(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) activate#(n__s(X)) -> activate#(X) activate#(n__diff(X1,X2)) -> diff#(activate(X1),activate(X2)) if#(false(),X,Y) -> activate#(Y) TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Open DPs: leq#(s(X),s(Y)) -> leq#(X,Y) TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Subterm Criterion Processor: simple projection: pi(leq#) = 1 problem: DPs: TRS: p(0()) -> 0() p(s(X)) -> X leq(0(),Y) -> true() leq(s(X),0()) -> false() leq(s(X),s(Y)) -> leq(X,Y) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) diff(X,Y) -> if(leq(X,Y),n__0(),n__s(n__diff(n__p(X),Y))) 0() -> n__0() s(X) -> n__s(X) diff(X1,X2) -> n__diff(X1,X2) p(X) -> n__p(X) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__diff(X1,X2)) -> diff(activate(X1),activate(X2)) activate(n__p(X)) -> p(activate(X)) activate(X) -> X Qed