MAYBE Problem: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(nil()) -> tt() a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isNeList(V) -> a__isQid(V) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(nil()) -> tt() a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isQid(X)) -> a__isQid(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a____(X1,X2) -> __(X1,X2) a__and(X1,X2) -> and(X1,X2) a__isList(X) -> isList(X) a__isNeList(X) -> isNeList(X) a__isQid(X) -> isQid(X) a__isNePal(X) -> isNePal(X) a__isPal(X) -> isPal(X) Proof: RT Transformation Processor: strict: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(nil()) -> tt() a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isNeList(V) -> a__isQid(V) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(nil()) -> tt() a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isQid(X)) -> a__isQid(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a____(X1,X2) -> __(X1,X2) a__and(X1,X2) -> and(X1,X2) a__isList(X) -> isList(X) a__isNeList(X) -> isNeList(X) a__isQid(X) -> isQid(X) a__isNePal(X) -> isNePal(X) a__isPal(X) -> isPal(X) weak: Matrix Interpretation Processor: dimension: 1 interpretation: [isNePal](x0) = x0 + 23, [isQid](x0) = x0 + 8, [and](x0, x1) = x0 + x1 + 2, [u] = 1, [o] = 18, [i] = 27, [e] = 0, [a] = 0, [a__isPal](x0) = x0 + 26, [isPal](x0) = x0 + 24, [a__isNePal](x0) = x0 + 16, [isNeList](x0) = x0 + 8, [a__isQid](x0) = x0 + 12, [isList](x0) = x0 + 17, [a__isNeList](x0) = x0 + 19, [a__isList](x0) = x0 + 16, [a__and](x0, x1) = x0 + x1 + 4, [tt] = 18, [nil] = 17, [mark](x0) = x0 + 1, [a____](x0, x1) = x0 + x1 + 12, [__](x0, x1) = x0 + x1 + 14 orientation: a____(__(X,Y),Z) = X + Y + Z + 26 >= X + Y + Z + 27 = a____(mark(X),a____(mark(Y),mark(Z))) a____(X,nil()) = X + 29 >= X + 1 = mark(X) a____(nil(),X) = X + 29 >= X + 1 = mark(X) a__and(tt(),X) = X + 22 >= X + 1 = mark(X) a__isList(V) = V + 16 >= V + 19 = a__isNeList(V) a__isList(nil()) = 33 >= 18 = tt() a__isList(__(V1,V2)) = V1 + V2 + 30 >= V1 + V2 + 37 = a__and(a__isList(V1),isList(V2)) a__isNeList(V) = V + 19 >= V + 12 = a__isQid(V) a__isNeList(__(V1,V2)) = V1 + V2 + 33 >= V1 + V2 + 28 = a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) = V1 + V2 + 33 >= V1 + V2 + 40 = a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) = V + 16 >= V + 12 = a__isQid(V) a__isNePal(__(I,__(P,I))) = 2I + P + 44 >= I + P + 40 = a__and(a__isQid(I),isPal(P)) a__isPal(V) = V + 26 >= V + 16 = a__isNePal(V) a__isPal(nil()) = 43 >= 18 = tt() a__isQid(a()) = 12 >= 18 = tt() a__isQid(e()) = 12 >= 18 = tt() a__isQid(i()) = 39 >= 18 = tt() a__isQid(o()) = 30 >= 18 = tt() a__isQid(u()) = 13 >= 18 = tt() mark(__(X1,X2)) = X1 + X2 + 15 >= X1 + X2 + 14 = a____(mark(X1),mark(X2)) mark(and(X1,X2)) = X1 + X2 + 3 >= X1 + X2 + 5 = a__and(mark(X1),X2) mark(isList(X)) = X + 18 >= X + 16 = a__isList(X) mark(isNeList(X)) = X + 9 >= X + 19 = a__isNeList(X) mark(isQid(X)) = X + 9 >= X + 12 = a__isQid(X) mark(isNePal(X)) = X + 24 >= X + 16 = a__isNePal(X) mark(isPal(X)) = X + 25 >= X + 26 = a__isPal(X) mark(nil()) = 18 >= 17 = nil() mark(tt()) = 19 >= 18 = tt() mark(a()) = 1 >= 0 = a() mark(e()) = 1 >= 0 = e() mark(i()) = 28 >= 27 = i() mark(o()) = 19 >= 18 = o() mark(u()) = 2 >= 1 = u() a____(X1,X2) = X1 + X2 + 12 >= X1 + X2 + 14 = __(X1,X2) a__and(X1,X2) = X1 + X2 + 4 >= X1 + X2 + 2 = and(X1,X2) a__isList(X) = X + 16 >= X + 17 = isList(X) a__isNeList(X) = X + 19 >= X + 8 = isNeList(X) a__isQid(X) = X + 12 >= X + 8 = isQid(X) a__isNePal(X) = X + 16 >= X + 23 = isNePal(X) a__isPal(X) = X + 26 >= X + 24 = isPal(X) problem: strict: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) -> a__isNeList(V) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(u()) -> tt() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isNeList(X)) -> a__isNeList(X) mark(isQid(X)) -> a__isQid(X) mark(isPal(X)) -> a__isPal(X) a____(X1,X2) -> __(X1,X2) a__isList(X) -> isList(X) a__isNePal(X) -> isNePal(X) weak: a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__and(tt(),X) -> mark(X) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(nil()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(isList(X)) -> a__isList(X) mark(isNePal(X)) -> a__isNePal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a__and(X1,X2) -> and(X1,X2) a__isNeList(X) -> isNeList(X) a__isQid(X) -> isQid(X) a__isPal(X) -> isPal(X) Matrix Interpretation Processor: dimension: 1 interpretation: [isNePal](x0) = x0 + 17, [isQid](x0) = x0 + 3, [and](x0, x1) = x0 + x1, [u] = 16, [o] = 18, [i] = 1, [e] = 8, [a] = 2, [a__isPal](x0) = x0 + 20, [isPal](x0) = x0 + 3, [a__isNePal](x0) = x0 + 3, [isNeList](x0) = x0 + 3, [a__isQid](x0) = x0 + 3, [isList](x0) = x0 + 9, [a__isNeList](x0) = x0 + 3, [a__isList](x0) = x0, [a__and](x0, x1) = x0 + x1 + 4, [tt] = 4, [nil] = 15, [mark](x0) = x0 + 4, [a____](x0, x1) = x0 + x1 + 24, [__](x0, x1) = x0 + x1 + 28 orientation: a____(__(X,Y),Z) = X + Y + Z + 52 >= X + Y + Z + 60 = a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) = V >= V + 3 = a__isNeList(V) a__isList(__(V1,V2)) = V1 + V2 + 28 >= V1 + V2 + 13 = a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) = V1 + V2 + 31 >= V1 + V2 + 16 = a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) = 5 >= 4 = tt() a__isQid(e()) = 11 >= 4 = tt() a__isQid(u()) = 19 >= 4 = tt() mark(and(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 8 = a__and(mark(X1),X2) mark(isNeList(X)) = X + 7 >= X + 3 = a__isNeList(X) mark(isQid(X)) = X + 7 >= X + 3 = a__isQid(X) mark(isPal(X)) = X + 7 >= X + 20 = a__isPal(X) a____(X1,X2) = X1 + X2 + 24 >= X1 + X2 + 28 = __(X1,X2) a__isList(X) = X >= X + 9 = isList(X) a__isNePal(X) = X + 3 >= X + 17 = isNePal(X) a____(X,nil()) = X + 39 >= X + 4 = mark(X) a____(nil(),X) = X + 39 >= X + 4 = mark(X) a__and(tt(),X) = X + 8 >= X + 4 = mark(X) a__isList(nil()) = 15 >= 4 = tt() a__isNeList(V) = V + 3 >= V + 3 = a__isQid(V) a__isNeList(__(V1,V2)) = V1 + V2 + 31 >= V1 + V2 + 7 = a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) = V + 3 >= V + 3 = a__isQid(V) a__isNePal(__(I,__(P,I))) = 2I + P + 59 >= I + P + 10 = a__and(a__isQid(I),isPal(P)) a__isPal(V) = V + 20 >= V + 3 = a__isNePal(V) a__isPal(nil()) = 35 >= 4 = tt() a__isQid(i()) = 4 >= 4 = tt() a__isQid(o()) = 21 >= 4 = tt() mark(__(X1,X2)) = X1 + X2 + 32 >= X1 + X2 + 32 = a____(mark(X1),mark(X2)) mark(isList(X)) = X + 13 >= X = a__isList(X) mark(isNePal(X)) = X + 21 >= X + 3 = a__isNePal(X) mark(nil()) = 19 >= 15 = nil() mark(tt()) = 8 >= 4 = tt() mark(a()) = 6 >= 2 = a() mark(e()) = 12 >= 8 = e() mark(i()) = 5 >= 1 = i() mark(o()) = 22 >= 18 = o() mark(u()) = 20 >= 16 = u() a__and(X1,X2) = X1 + X2 + 4 >= X1 + X2 = and(X1,X2) a__isNeList(X) = X + 3 >= X + 3 = isNeList(X) a__isQid(X) = X + 3 >= X + 3 = isQid(X) a__isPal(X) = X + 20 >= X + 3 = isPal(X) problem: strict: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) -> a__isNeList(V) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isPal(X)) -> a__isPal(X) a____(X1,X2) -> __(X1,X2) a__isList(X) -> isList(X) a__isNePal(X) -> isNePal(X) weak: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(u()) -> tt() mark(isNeList(X)) -> a__isNeList(X) mark(isQid(X)) -> a__isQid(X) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__and(tt(),X) -> mark(X) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(nil()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(isList(X)) -> a__isList(X) mark(isNePal(X)) -> a__isNePal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a__and(X1,X2) -> and(X1,X2) a__isNeList(X) -> isNeList(X) a__isQid(X) -> isQid(X) a__isPal(X) -> isPal(X) Matrix Interpretation Processor: dimension: 1 interpretation: [isNePal](x0) = x0 + 12, [isQid](x0) = x0 + 2, [and](x0, x1) = x0 + x1 + 3, [u] = 1, [o] = 1, [i] = 16, [e] = 1, [a] = 1, [a__isPal](x0) = x0 + 16, [isPal](x0) = x0 + 1, [a__isNePal](x0) = x0 + 12, [isNeList](x0) = x0 + 2, [a__isQid](x0) = x0 + 2, [isList](x0) = x0 + 4, [a__isNeList](x0) = x0 + 2, [a__isList](x0) = x0 + 4, [a__and](x0, x1) = x0 + x1 + 20, [tt] = 3, [nil] = 0, [mark](x0) = x0, [a____](x0, x1) = x0 + x1, [__](x0, x1) = x0 + x1 + 24 orientation: a____(__(X,Y),Z) = X + Y + Z + 24 >= X + Y + Z = a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) = V + 4 >= V + 2 = a__isNeList(V) mark(and(X1,X2)) = X1 + X2 + 3 >= X1 + X2 + 20 = a__and(mark(X1),X2) mark(isPal(X)) = X + 1 >= X + 16 = a__isPal(X) a____(X1,X2) = X1 + X2 >= X1 + X2 + 24 = __(X1,X2) a__isList(X) = X + 4 >= X + 4 = isList(X) a__isNePal(X) = X + 12 >= X + 12 = isNePal(X) a__isList(__(V1,V2)) = V1 + V2 + 28 >= V1 + V2 + 28 = a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) = V1 + V2 + 26 >= V1 + V2 + 26 = a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) = 3 >= 3 = tt() a__isQid(e()) = 3 >= 3 = tt() a__isQid(u()) = 3 >= 3 = tt() mark(isNeList(X)) = X + 2 >= X + 2 = a__isNeList(X) mark(isQid(X)) = X + 2 >= X + 2 = a__isQid(X) a____(X,nil()) = X >= X = mark(X) a____(nil(),X) = X >= X = mark(X) a__and(tt(),X) = X + 23 >= X = mark(X) a__isList(nil()) = 4 >= 3 = tt() a__isNeList(V) = V + 2 >= V + 2 = a__isQid(V) a__isNeList(__(V1,V2)) = V1 + V2 + 26 >= V1 + V2 + 26 = a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) = V + 12 >= V + 2 = a__isQid(V) a__isNePal(__(I,__(P,I))) = 2I + P + 60 >= I + P + 23 = a__and(a__isQid(I),isPal(P)) a__isPal(V) = V + 16 >= V + 12 = a__isNePal(V) a__isPal(nil()) = 16 >= 3 = tt() a__isQid(i()) = 18 >= 3 = tt() a__isQid(o()) = 3 >= 3 = tt() mark(__(X1,X2)) = X1 + X2 + 24 >= X1 + X2 = a____(mark(X1),mark(X2)) mark(isList(X)) = X + 4 >= X + 4 = a__isList(X) mark(isNePal(X)) = X + 12 >= X + 12 = a__isNePal(X) mark(nil()) = 0 >= 0 = nil() mark(tt()) = 3 >= 3 = tt() mark(a()) = 1 >= 1 = a() mark(e()) = 1 >= 1 = e() mark(i()) = 16 >= 16 = i() mark(o()) = 1 >= 1 = o() mark(u()) = 1 >= 1 = u() a__and(X1,X2) = X1 + X2 + 20 >= X1 + X2 + 3 = and(X1,X2) a__isNeList(X) = X + 2 >= X + 2 = isNeList(X) a__isQid(X) = X + 2 >= X + 2 = isQid(X) a__isPal(X) = X + 16 >= X + 1 = isPal(X) problem: strict: mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(isPal(X)) -> a__isPal(X) a____(X1,X2) -> __(X1,X2) a__isList(X) -> isList(X) a__isNePal(X) -> isNePal(X) weak: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) -> a__isNeList(V) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(u()) -> tt() mark(isNeList(X)) -> a__isNeList(X) mark(isQid(X)) -> a__isQid(X) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__and(tt(),X) -> mark(X) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(nil()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(isList(X)) -> a__isList(X) mark(isNePal(X)) -> a__isNePal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a__and(X1,X2) -> and(X1,X2) a__isNeList(X) -> isNeList(X) a__isQid(X) -> isQid(X) a__isPal(X) -> isPal(X) Matrix Interpretation Processor: dimension: 1 interpretation: [isNePal](x0) = x0 + 6, [isQid](x0) = x0, [and](x0, x1) = x0 + x1 + 5, [u] = 4, [o] = 10, [i] = 16, [e] = 16, [a] = 12, [a__isPal](x0) = x0 + 6, [isPal](x0) = x0 + 6, [a__isNePal](x0) = x0 + 6, [isNeList](x0) = x0 + 4, [a__isQid](x0) = x0, [isList](x0) = x0 + 12, [a__isNeList](x0) = x0 + 4, [a__isList](x0) = x0 + 8, [a__and](x0, x1) = x0 + x1 + 5, [tt] = 4, [nil] = 2, [mark](x0) = x0 + 1, [a____](x0, x1) = x0 + x1, [__](x0, x1) = x0 + x1 + 25 orientation: mark(and(X1,X2)) = X1 + X2 + 6 >= X1 + X2 + 6 = a__and(mark(X1),X2) mark(isPal(X)) = X + 7 >= X + 6 = a__isPal(X) a____(X1,X2) = X1 + X2 >= X1 + X2 + 25 = __(X1,X2) a__isList(X) = X + 8 >= X + 12 = isList(X) a__isNePal(X) = X + 6 >= X + 6 = isNePal(X) a____(__(X,Y),Z) = X + Y + Z + 25 >= X + Y + Z + 3 = a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) = V + 8 >= V + 4 = a__isNeList(V) a__isList(__(V1,V2)) = V1 + V2 + 33 >= V1 + V2 + 25 = a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) = V1 + V2 + 29 >= V1 + V2 + 21 = a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) = 12 >= 4 = tt() a__isQid(e()) = 16 >= 4 = tt() a__isQid(u()) = 4 >= 4 = tt() mark(isNeList(X)) = X + 5 >= X + 4 = a__isNeList(X) mark(isQid(X)) = X + 1 >= X = a__isQid(X) a____(X,nil()) = X + 2 >= X + 1 = mark(X) a____(nil(),X) = X + 2 >= X + 1 = mark(X) a__and(tt(),X) = X + 9 >= X + 1 = mark(X) a__isList(nil()) = 10 >= 4 = tt() a__isNeList(V) = V + 4 >= V = a__isQid(V) a__isNeList(__(V1,V2)) = V1 + V2 + 29 >= V1 + V2 + 17 = a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) = V + 6 >= V = a__isQid(V) a__isNePal(__(I,__(P,I))) = 2I + P + 56 >= I + P + 11 = a__and(a__isQid(I),isPal(P)) a__isPal(V) = V + 6 >= V + 6 = a__isNePal(V) a__isPal(nil()) = 8 >= 4 = tt() a__isQid(i()) = 16 >= 4 = tt() a__isQid(o()) = 10 >= 4 = tt() mark(__(X1,X2)) = X1 + X2 + 26 >= X1 + X2 + 2 = a____(mark(X1),mark(X2)) mark(isList(X)) = X + 13 >= X + 8 = a__isList(X) mark(isNePal(X)) = X + 7 >= X + 6 = a__isNePal(X) mark(nil()) = 3 >= 2 = nil() mark(tt()) = 5 >= 4 = tt() mark(a()) = 13 >= 12 = a() mark(e()) = 17 >= 16 = e() mark(i()) = 17 >= 16 = i() mark(o()) = 11 >= 10 = o() mark(u()) = 5 >= 4 = u() a__and(X1,X2) = X1 + X2 + 5 >= X1 + X2 + 5 = and(X1,X2) a__isNeList(X) = X + 4 >= X + 4 = isNeList(X) a__isQid(X) = X >= X = isQid(X) a__isPal(X) = X + 6 >= X + 6 = isPal(X) problem: strict: mark(and(X1,X2)) -> a__and(mark(X1),X2) a____(X1,X2) -> __(X1,X2) a__isList(X) -> isList(X) a__isNePal(X) -> isNePal(X) weak: mark(isPal(X)) -> a__isPal(X) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) -> a__isNeList(V) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(u()) -> tt() mark(isNeList(X)) -> a__isNeList(X) mark(isQid(X)) -> a__isQid(X) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__and(tt(),X) -> mark(X) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(nil()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(isList(X)) -> a__isList(X) mark(isNePal(X)) -> a__isNePal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a__and(X1,X2) -> and(X1,X2) a__isNeList(X) -> isNeList(X) a__isQid(X) -> isQid(X) a__isPal(X) -> isPal(X) Matrix Interpretation Processor: dimension: 1 interpretation: [isNePal](x0) = x0, [isQid](x0) = x0, [and](x0, x1) = x0 + x1, [u] = 8, [o] = 4, [i] = 8, [e] = 6, [a] = 18, [a__isPal](x0) = x0 + 4, [isPal](x0) = x0 + 2, [a__isNePal](x0) = x0 + 2, [isNeList](x0) = x0, [a__isQid](x0) = x0, [isList](x0) = x0 + 1, [a__isNeList](x0) = x0 + 4, [a__isList](x0) = x0 + 4, [a__and](x0, x1) = x0 + x1 + 4, [tt] = 0, [nil] = 16, [mark](x0) = x0 + 4, [a____](x0, x1) = x0 + x1 + 1, [__](x0, x1) = x0 + x1 + 13 orientation: mark(and(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 8 = a__and(mark(X1),X2) a____(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 13 = __(X1,X2) a__isList(X) = X + 4 >= X + 1 = isList(X) a__isNePal(X) = X + 2 >= X = isNePal(X) mark(isPal(X)) = X + 6 >= X + 4 = a__isPal(X) a____(__(X,Y),Z) = X + Y + Z + 14 >= X + Y + Z + 14 = a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) = V + 4 >= V + 4 = a__isNeList(V) a__isList(__(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 9 = a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 9 = a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) = 18 >= 0 = tt() a__isQid(e()) = 6 >= 0 = tt() a__isQid(u()) = 8 >= 0 = tt() mark(isNeList(X)) = X + 4 >= X + 4 = a__isNeList(X) mark(isQid(X)) = X + 4 >= X = a__isQid(X) a____(X,nil()) = X + 17 >= X + 4 = mark(X) a____(nil(),X) = X + 17 >= X + 4 = mark(X) a__and(tt(),X) = X + 4 >= X + 4 = mark(X) a__isList(nil()) = 20 >= 0 = tt() a__isNeList(V) = V + 4 >= V = a__isQid(V) a__isNeList(__(V1,V2)) = V1 + V2 + 17 >= V1 + V2 + 8 = a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) = V + 2 >= V = a__isQid(V) a__isNePal(__(I,__(P,I))) = 2I + P + 28 >= I + P + 6 = a__and(a__isQid(I),isPal(P)) a__isPal(V) = V + 4 >= V + 2 = a__isNePal(V) a__isPal(nil()) = 20 >= 0 = tt() a__isQid(i()) = 8 >= 0 = tt() a__isQid(o()) = 4 >= 0 = tt() mark(__(X1,X2)) = X1 + X2 + 17 >= X1 + X2 + 9 = a____(mark(X1),mark(X2)) mark(isList(X)) = X + 5 >= X + 4 = a__isList(X) mark(isNePal(X)) = X + 4 >= X + 2 = a__isNePal(X) mark(nil()) = 20 >= 16 = nil() mark(tt()) = 4 >= 0 = tt() mark(a()) = 22 >= 18 = a() mark(e()) = 10 >= 6 = e() mark(i()) = 12 >= 8 = i() mark(o()) = 8 >= 4 = o() mark(u()) = 12 >= 8 = u() a__and(X1,X2) = X1 + X2 + 4 >= X1 + X2 = and(X1,X2) a__isNeList(X) = X + 4 >= X = isNeList(X) a__isQid(X) = X >= X = isQid(X) a__isPal(X) = X + 4 >= X + 2 = isPal(X) problem: strict: mark(and(X1,X2)) -> a__and(mark(X1),X2) a____(X1,X2) -> __(X1,X2) weak: a__isList(X) -> isList(X) a__isNePal(X) -> isNePal(X) mark(isPal(X)) -> a__isPal(X) a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a__isList(V) -> a__isNeList(V) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(u()) -> tt() mark(isNeList(X)) -> a__isNeList(X) mark(isQid(X)) -> a__isQid(X) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__and(tt(),X) -> mark(X) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(nil()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(isList(X)) -> a__isList(X) mark(isNePal(X)) -> a__isNePal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a__and(X1,X2) -> and(X1,X2) a__isNeList(X) -> isNeList(X) a__isQid(X) -> isQid(X) a__isPal(X) -> isPal(X) Open