YES Problem: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) active#(f(X1,X2)) -> active#(X1) active#(f(X1,X2)) -> f#(active(X1),X2) active#(g(X)) -> active#(X) active#(g(X)) -> g#(active(X)) f#(mark(X1),X2) -> f#(X1,X2) g#(mark(X)) -> g#(X) proper#(f(X1,X2)) -> proper#(X2) proper#(f(X1,X2)) -> proper#(X1) proper#(f(X1,X2)) -> f#(proper(X1),proper(X2)) proper#(g(X)) -> proper#(X) proper#(g(X)) -> g#(proper(X)) f#(ok(X1),ok(X2)) -> f#(X1,X2) g#(ok(X)) -> g#(X) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) TDG Processor: DPs: active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) active#(f(X1,X2)) -> active#(X1) active#(f(X1,X2)) -> f#(active(X1),X2) active#(g(X)) -> active#(X) active#(g(X)) -> g#(active(X)) f#(mark(X1),X2) -> f#(X1,X2) g#(mark(X)) -> g#(X) proper#(f(X1,X2)) -> proper#(X2) proper#(f(X1,X2)) -> proper#(X1) proper#(f(X1,X2)) -> f#(proper(X1),proper(X2)) proper#(g(X)) -> proper#(X) proper#(g(X)) -> g#(proper(X)) f#(ok(X1),ok(X2)) -> f#(X1,X2) g#(ok(X)) -> g#(X) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X)) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X) top#(ok(X)) -> active#(X) -> active#(g(X)) -> g#(active(X)) top#(ok(X)) -> active#(X) -> active#(g(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(f(X1,X2)) -> f#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(f(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> top#(proper(X)) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(g(X)) -> g#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(g(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(f(X1,X2)) -> f#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(f(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(f(X1,X2)) -> proper#(X2) proper#(f(X1,X2)) -> proper#(X2) -> proper#(g(X)) -> g#(proper(X)) proper#(f(X1,X2)) -> proper#(X2) -> proper#(g(X)) -> proper#(X) proper#(f(X1,X2)) -> proper#(X2) -> proper#(f(X1,X2)) -> f#(proper(X1),proper(X2)) proper#(f(X1,X2)) -> proper#(X2) -> proper#(f(X1,X2)) -> proper#(X1) proper#(f(X1,X2)) -> proper#(X2) -> proper#(f(X1,X2)) -> proper#(X2) proper#(f(X1,X2)) -> proper#(X1) -> proper#(g(X)) -> g#(proper(X)) proper#(f(X1,X2)) -> proper#(X1) -> proper#(g(X)) -> proper#(X) proper#(f(X1,X2)) -> proper#(X1) -> proper#(f(X1,X2)) -> f#(proper(X1),proper(X2)) proper#(f(X1,X2)) -> proper#(X1) -> proper#(f(X1,X2)) -> proper#(X1) proper#(f(X1,X2)) -> proper#(X1) -> proper#(f(X1,X2)) -> proper#(X2) proper#(f(X1,X2)) -> f#(proper(X1),proper(X2)) -> f#(ok(X1),ok(X2)) -> f#(X1,X2) proper#(f(X1,X2)) -> f#(proper(X1),proper(X2)) -> f#(mark(X1),X2) -> f#(X1,X2) proper#(g(X)) -> proper#(X) -> proper#(g(X)) -> g#(proper(X)) proper#(g(X)) -> proper#(X) -> proper#(g(X)) -> proper#(X) proper#(g(X)) -> proper#(X) -> proper#(f(X1,X2)) -> f#(proper(X1),proper(X2)) proper#(g(X)) -> proper#(X) -> proper#(f(X1,X2)) -> proper#(X1) proper#(g(X)) -> proper#(X) -> proper#(f(X1,X2)) -> proper#(X2) proper#(g(X)) -> g#(proper(X)) -> g#(ok(X)) -> g#(X) proper#(g(X)) -> g#(proper(X)) -> g#(mark(X)) -> g#(X) g#(ok(X)) -> g#(X) -> g#(ok(X)) -> g#(X) g#(ok(X)) -> g#(X) -> g#(mark(X)) -> g#(X) g#(mark(X)) -> g#(X) -> g#(ok(X)) -> g#(X) g#(mark(X)) -> g#(X) -> g#(mark(X)) -> g#(X) f#(ok(X1),ok(X2)) -> f#(X1,X2) -> f#(ok(X1),ok(X2)) -> f#(X1,X2) f#(ok(X1),ok(X2)) -> f#(X1,X2) -> f#(mark(X1),X2) -> f#(X1,X2) f#(mark(X1),X2) -> f#(X1,X2) -> f#(ok(X1),ok(X2)) -> f#(X1,X2) f#(mark(X1),X2) -> f#(X1,X2) -> f#(mark(X1),X2) -> f#(X1,X2) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(ok(X1),ok(X2)) -> f#(X1,X2) active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) -> f#(mark(X1),X2) -> f#(X1,X2) active#(f(X1,X2)) -> f#(active(X1),X2) -> f#(ok(X1),ok(X2)) -> f#(X1,X2) active#(f(X1,X2)) -> f#(active(X1),X2) -> f#(mark(X1),X2) -> f#(X1,X2) active#(f(X1,X2)) -> active#(X1) -> active#(g(X)) -> g#(active(X)) active#(f(X1,X2)) -> active#(X1) -> active#(g(X)) -> active#(X) active#(f(X1,X2)) -> active#(X1) -> active#(f(X1,X2)) -> f#(active(X1),X2) active#(f(X1,X2)) -> active#(X1) -> active#(f(X1,X2)) -> active#(X1) active#(f(X1,X2)) -> active#(X1) -> active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) active#(g(X)) -> g#(active(X)) -> g#(ok(X)) -> g#(X) active#(g(X)) -> g#(active(X)) -> g#(mark(X)) -> g#(X) active#(g(X)) -> active#(X) -> active#(g(X)) -> g#(active(X)) active#(g(X)) -> active#(X) -> active#(g(X)) -> active#(X) active#(g(X)) -> active#(X) -> active#(f(X1,X2)) -> f#(active(X1),X2) active#(g(X)) -> active#(X) -> active#(f(X1,X2)) -> active#(X1) active#(g(X)) -> active#(X) -> active#(f(g(X),Y)) -> f#(X,f(g(X),Y)) SCC Processor: #sccs: 5 #rules: 11 #arcs: 61/324 DPs: top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [top#](x0) = 1/2x0 + 3, [top](x0) = 2x0, [ok](x0) = 2x0 + 1, [proper](x0) = 3x0 + 2, [mark](x0) = 3x0 + 3, [active](x0) = 2x0, [f](x0, x1) = 5/2x0 + 3/2, [g](x0) = 3x0 + 2 orientation: top#(ok(X)) = X + 7/2 >= X + 3 = top#(active(X)) top#(mark(X)) = 3/2X + 9/2 >= 3/2X + 4 = top#(proper(X)) active(f(g(X),Y)) = 15X + 13 >= 15/2X + 15/2 = mark(f(X,f(g(X),Y))) active(f(X1,X2)) = 5X1 + 3 >= 5X1 + 3/2 = f(active(X1),X2) active(g(X)) = 6X + 4 >= 6X + 2 = g(active(X)) f(mark(X1),X2) = 15/2X1 + 9 >= 15/2X1 + 15/2 = mark(f(X1,X2)) g(mark(X)) = 9X + 11 >= 9X + 9 = mark(g(X)) proper(f(X1,X2)) = 15/2X1 + 13/2 >= 15/2X1 + 13/2 = f(proper(X1),proper(X2)) proper(g(X)) = 9X + 8 >= 9X + 8 = g(proper(X)) f(ok(X1),ok(X2)) = 5X1 + 4 >= 5X1 + 4 = ok(f(X1,X2)) g(ok(X)) = 6X + 5 >= 6X + 5 = ok(g(X)) top(mark(X)) = 6X + 6 >= 6X + 4 = top(proper(X)) top(ok(X)) = 4X + 2 >= 4X = top(active(X)) problem: DPs: TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: active#(f(X1,X2)) -> active#(X1) active#(g(X)) -> active#(X) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [active#](x0) = 2x0 + 4, [top](x0) = 3, [ok](x0) = 4x0 + 4, [proper](x0) = 4x0, [mark](x0) = 0, [active](x0) = x0, [f](x0, x1) = 2x0 + 1, [g](x0) = 4x0 + 2 orientation: active#(f(X1,X2)) = 4X1 + 6 >= 2X1 + 4 = active#(X1) active#(g(X)) = 8X + 8 >= 2X + 4 = active#(X) active(f(g(X),Y)) = 8X + 5 >= 0 = mark(f(X,f(g(X),Y))) active(f(X1,X2)) = 2X1 + 1 >= 2X1 + 1 = f(active(X1),X2) active(g(X)) = 4X + 2 >= 4X + 2 = g(active(X)) f(mark(X1),X2) = 1 >= 0 = mark(f(X1,X2)) g(mark(X)) = 2 >= 0 = mark(g(X)) proper(f(X1,X2)) = 8X1 + 4 >= 8X1 + 1 = f(proper(X1),proper(X2)) proper(g(X)) = 16X + 8 >= 16X + 2 = g(proper(X)) f(ok(X1),ok(X2)) = 8X1 + 9 >= 8X1 + 8 = ok(f(X1,X2)) g(ok(X)) = 16X + 18 >= 16X + 12 = ok(g(X)) top(mark(X)) = 3 >= 3 = top(proper(X)) top(ok(X)) = 3 >= 3 = top(active(X)) problem: DPs: TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: proper#(f(X1,X2)) -> proper#(X2) proper#(f(X1,X2)) -> proper#(X1) proper#(g(X)) -> proper#(X) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) KBO Processor: argument filtering: pi(g) = [0] pi(f) = [0,1] pi(active) = 0 pi(mark) = [] pi(proper) = 0 pi(ok) = 0 pi(top) = [] pi(proper#) = [0] weight function: w0 = 1 w(proper#) = w(top) = w(ok) = w(proper) = w(mark) = w(active) = w(f) = 1 w(g) = 0 precedence: proper# ~ top ~ ok ~ proper ~ f ~ g > mark ~ active problem: DPs: TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: g#(mark(X)) -> g#(X) g#(ok(X)) -> g#(X) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [g#](x0) = 5x0, [top](x0) = 5, [ok](x0) = x0 + 3, [proper](x0) = 4x0 + 3, [mark](x0) = x0 + 1, [active](x0) = 2x0, [f](x0, x1) = 4x0 + x1 + 4, [g](x0) = 2x0 + 1 orientation: g#(mark(X)) = 5X + 5 >= 5X = g#(X) g#(ok(X)) = 5X + 15 >= 5X = g#(X) active(f(g(X),Y)) = 16X + 2Y + 16 >= 12X + Y + 13 = mark(f(X,f(g(X),Y))) active(f(X1,X2)) = 8X1 + 2X2 + 8 >= 8X1 + X2 + 4 = f(active(X1),X2) active(g(X)) = 4X + 2 >= 4X + 1 = g(active(X)) f(mark(X1),X2) = 4X1 + X2 + 8 >= 4X1 + X2 + 5 = mark(f(X1,X2)) g(mark(X)) = 2X + 3 >= 2X + 2 = mark(g(X)) proper(f(X1,X2)) = 16X1 + 4X2 + 19 >= 16X1 + 4X2 + 19 = f(proper(X1),proper(X2)) proper(g(X)) = 8X + 7 >= 8X + 7 = g(proper(X)) f(ok(X1),ok(X2)) = 4X1 + X2 + 19 >= 4X1 + X2 + 7 = ok(f(X1,X2)) g(ok(X)) = 2X + 7 >= 2X + 4 = ok(g(X)) top(mark(X)) = 5 >= 5 = top(proper(X)) top(ok(X)) = 5 >= 5 = top(active(X)) problem: DPs: TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: f#(mark(X1),X2) -> f#(X1,X2) f#(ok(X1),ok(X2)) -> f#(X1,X2) TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [f#](x0, x1) = x0, [top](x0) = 2, [ok](x0) = x0 + 1/2, [proper](x0) = x0, [mark](x0) = x0 + 5/2, [active](x0) = 3x0, [f](x0, x1) = 2x0 + x1, [g](x0) = x0 + 3/2 orientation: f#(mark(X1),X2) = X1 + 5/2 >= X1 = f#(X1,X2) f#(ok(X1),ok(X2)) = X1 + 1/2 >= X1 = f#(X1,X2) active(f(g(X),Y)) = 6X + 3Y + 9 >= 4X + Y + 11/2 = mark(f(X,f(g(X),Y))) active(f(X1,X2)) = 6X1 + 3X2 >= 6X1 + X2 = f(active(X1),X2) active(g(X)) = 3X + 9/2 >= 3X + 3/2 = g(active(X)) f(mark(X1),X2) = 2X1 + X2 + 5 >= 2X1 + X2 + 5/2 = mark(f(X1,X2)) g(mark(X)) = X + 4 >= X + 4 = mark(g(X)) proper(f(X1,X2)) = 2X1 + X2 >= 2X1 + X2 = f(proper(X1),proper(X2)) proper(g(X)) = X + 3/2 >= X + 3/2 = g(proper(X)) f(ok(X1),ok(X2)) = 2X1 + X2 + 3/2 >= 2X1 + X2 + 1/2 = ok(f(X1,X2)) g(ok(X)) = X + 2 >= X + 2 = ok(g(X)) top(mark(X)) = 2 >= 2 = top(proper(X)) top(ok(X)) = 2 >= 2 = top(active(X)) problem: DPs: TRS: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y))) active(f(X1,X2)) -> f(active(X1),X2) active(g(X)) -> g(active(X)) f(mark(X1),X2) -> mark(f(X1,X2)) g(mark(X)) -> mark(g(X)) proper(f(X1,X2)) -> f(proper(X1),proper(X2)) proper(g(X)) -> g(proper(X)) f(ok(X1),ok(X2)) -> ok(f(X1,X2)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed