MAYBE * Step 1: WeightGap MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(a__a) = [0] p(a__f) = [1] x1 + [0] p(a__g) = [1] x1 + [3] p(a__h) = [1] x1 + [0] p(b) = [0] p(f) = [1] x1 + [0] p(g) = [1] x1 + [0] p(h) = [1] x1 + [1] p(mark) = [1] x1 + [0] Following rules are strictly oriented: a__g(X1,X2) = [1] X1 + [3] > [1] X1 + [0] = g(X1,X2) a__g(a(),X) = [3] > [0] = a__f(b(),X) mark(h(X)) = [1] X + [1] > [1] X + [0] = a__h(mark(X)) Following rules are (at-least) weakly oriented: a__a() = [0] >= [0] = a() a__a() = [0] >= [0] = b() a__f(X,X) = [1] X + [0] >= [0] = a__h(a__a()) a__f(X1,X2) = [1] X1 + [0] >= [1] X1 + [0] = f(X1,X2) a__h(X) = [1] X + [0] >= [1] X + [3] = a__g(mark(X),X) a__h(X) = [1] X + [0] >= [1] X + [1] = h(X) mark(a()) = [0] >= [0] = a__a() mark(b()) = [0] >= [0] = b() mark(f(X1,X2)) = [1] X1 + [0] >= [1] X1 + [0] = a__f(mark(X1),X2) mark(g(X1,X2)) = [1] X1 + [0] >= [1] X1 + [3] = a__g(mark(X1),X2) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) - Weak TRS: a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(a__a) = [0] p(a__f) = [1] x1 + [0] p(a__g) = [1] x1 + [0] p(a__h) = [1] x1 + [0] p(b) = [0] p(f) = [1] x1 + [10] p(g) = [1] x1 + [0] p(h) = [1] x1 + [0] p(mark) = [1] x1 + [0] Following rules are strictly oriented: mark(f(X1,X2)) = [1] X1 + [10] > [1] X1 + [0] = a__f(mark(X1),X2) Following rules are (at-least) weakly oriented: a__a() = [0] >= [0] = a() a__a() = [0] >= [0] = b() a__f(X,X) = [1] X + [0] >= [0] = a__h(a__a()) a__f(X1,X2) = [1] X1 + [0] >= [1] X1 + [10] = f(X1,X2) a__g(X1,X2) = [1] X1 + [0] >= [1] X1 + [0] = g(X1,X2) a__g(a(),X) = [0] >= [0] = a__f(b(),X) a__h(X) = [1] X + [0] >= [1] X + [0] = a__g(mark(X),X) a__h(X) = [1] X + [0] >= [1] X + [0] = h(X) mark(a()) = [0] >= [0] = a__a() mark(b()) = [0] >= [0] = b() mark(g(X1,X2)) = [1] X1 + [0] >= [1] X1 + [0] = a__g(mark(X1),X2) mark(h(X)) = [1] X + [0] >= [1] X + [0] = a__h(mark(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(g(X1,X2)) -> a__g(mark(X1),X2) - Weak TRS: a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [4] p(a__a) = [0] p(a__f) = [1] x1 + [0] p(a__g) = [1] x1 + [0] p(a__h) = [1] x1 + [0] p(b) = [4] p(f) = [1] x1 + [8] p(g) = [1] x1 + [0] p(h) = [1] x1 + [5] p(mark) = [1] x1 + [0] Following rules are strictly oriented: mark(a()) = [4] > [0] = a__a() Following rules are (at-least) weakly oriented: a__a() = [0] >= [4] = a() a__a() = [0] >= [4] = b() a__f(X,X) = [1] X + [0] >= [0] = a__h(a__a()) a__f(X1,X2) = [1] X1 + [0] >= [1] X1 + [8] = f(X1,X2) a__g(X1,X2) = [1] X1 + [0] >= [1] X1 + [0] = g(X1,X2) a__g(a(),X) = [4] >= [4] = a__f(b(),X) a__h(X) = [1] X + [0] >= [1] X + [0] = a__g(mark(X),X) a__h(X) = [1] X + [0] >= [1] X + [5] = h(X) mark(b()) = [4] >= [4] = b() mark(f(X1,X2)) = [1] X1 + [8] >= [1] X1 + [0] = a__f(mark(X1),X2) mark(g(X1,X2)) = [1] X1 + [0] >= [1] X1 + [0] = a__g(mark(X1),X2) mark(h(X)) = [1] X + [5] >= [1] X + [0] = a__h(mark(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(b()) -> b() mark(g(X1,X2)) -> a__g(mark(X1),X2) - Weak TRS: a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) mark(a()) -> a__a() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [5] p(a__a) = [1] p(a__f) = [1] x1 + [0] p(a__g) = [1] x1 + [4] p(a__h) = [1] x1 + [0] p(b) = [2] p(f) = [0] p(g) = [0] p(h) = [1] x1 + [0] p(mark) = [4] Following rules are strictly oriented: mark(b()) = [4] > [2] = b() Following rules are (at-least) weakly oriented: a__a() = [1] >= [5] = a() a__a() = [1] >= [2] = b() a__f(X,X) = [1] X + [0] >= [1] = a__h(a__a()) a__f(X1,X2) = [1] X1 + [0] >= [0] = f(X1,X2) a__g(X1,X2) = [1] X1 + [4] >= [0] = g(X1,X2) a__g(a(),X) = [9] >= [2] = a__f(b(),X) a__h(X) = [1] X + [0] >= [8] = a__g(mark(X),X) a__h(X) = [1] X + [0] >= [1] X + [0] = h(X) mark(a()) = [4] >= [1] = a__a() mark(f(X1,X2)) = [4] >= [4] = a__f(mark(X1),X2) mark(g(X1,X2)) = [4] >= [8] = a__g(mark(X1),X2) mark(h(X)) = [4] >= [4] = a__h(mark(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: WeightGap MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(g(X1,X2)) -> a__g(mark(X1),X2) - Weak TRS: a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(a__a) = [0] p(a__f) = [1] x1 + [1] p(a__g) = [1] x1 + [1] p(a__h) = [1] x1 + [12] p(b) = [0] p(f) = [1] x1 + [8] p(g) = [1] x1 + [1] p(h) = [1] x1 + [12] p(mark) = [1] x1 + [0] Following rules are strictly oriented: a__h(X) = [1] X + [12] > [1] X + [1] = a__g(mark(X),X) Following rules are (at-least) weakly oriented: a__a() = [0] >= [0] = a() a__a() = [0] >= [0] = b() a__f(X,X) = [1] X + [1] >= [12] = a__h(a__a()) a__f(X1,X2) = [1] X1 + [1] >= [1] X1 + [8] = f(X1,X2) a__g(X1,X2) = [1] X1 + [1] >= [1] X1 + [1] = g(X1,X2) a__g(a(),X) = [1] >= [1] = a__f(b(),X) a__h(X) = [1] X + [12] >= [1] X + [12] = h(X) mark(a()) = [0] >= [0] = a__a() mark(b()) = [0] >= [0] = b() mark(f(X1,X2)) = [1] X1 + [8] >= [1] X1 + [1] = a__f(mark(X1),X2) mark(g(X1,X2)) = [1] X1 + [1] >= [1] X1 + [1] = a__g(mark(X1),X2) mark(h(X)) = [1] X + [12] >= [1] X + [12] = a__h(mark(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: WeightGap MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__h(X) -> h(X) mark(g(X1,X2)) -> a__g(mark(X1),X2) - Weak TRS: a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [15] p(a__a) = [0] p(a__f) = [1] x1 + [2] p(a__g) = [1] x1 + [0] p(a__h) = [1] x1 + [0] p(b) = [13] p(f) = [1] x1 + [9] p(g) = [1] x1 + [0] p(h) = [1] x1 + [11] p(mark) = [1] x1 + [0] Following rules are strictly oriented: a__f(X,X) = [1] X + [2] > [0] = a__h(a__a()) Following rules are (at-least) weakly oriented: a__a() = [0] >= [15] = a() a__a() = [0] >= [13] = b() a__f(X1,X2) = [1] X1 + [2] >= [1] X1 + [9] = f(X1,X2) a__g(X1,X2) = [1] X1 + [0] >= [1] X1 + [0] = g(X1,X2) a__g(a(),X) = [15] >= [15] = a__f(b(),X) a__h(X) = [1] X + [0] >= [1] X + [0] = a__g(mark(X),X) a__h(X) = [1] X + [0] >= [1] X + [11] = h(X) mark(a()) = [15] >= [0] = a__a() mark(b()) = [13] >= [13] = b() mark(f(X1,X2)) = [1] X1 + [9] >= [1] X1 + [2] = a__f(mark(X1),X2) mark(g(X1,X2)) = [1] X1 + [0] >= [1] X1 + [0] = a__g(mark(X1),X2) mark(h(X)) = [1] X + [11] >= [1] X + [0] = a__h(mark(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: WeightGap MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__a() -> b() a__f(X1,X2) -> f(X1,X2) a__h(X) -> h(X) mark(g(X1,X2)) -> a__g(mark(X1),X2) - Weak TRS: a__f(X,X) -> a__h(a__a()) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [12] p(a__a) = [1] p(a__f) = [1] x1 + [8] p(a__g) = [1] x1 + [4] p(a__h) = [1] x1 + [4] p(b) = [0] p(f) = [1] x1 + [13] p(g) = [1] x1 + [0] p(h) = [1] x1 + [4] p(mark) = [1] x1 + [0] Following rules are strictly oriented: a__a() = [1] > [0] = b() Following rules are (at-least) weakly oriented: a__a() = [1] >= [12] = a() a__f(X,X) = [1] X + [8] >= [5] = a__h(a__a()) a__f(X1,X2) = [1] X1 + [8] >= [1] X1 + [13] = f(X1,X2) a__g(X1,X2) = [1] X1 + [4] >= [1] X1 + [0] = g(X1,X2) a__g(a(),X) = [16] >= [8] = a__f(b(),X) a__h(X) = [1] X + [4] >= [1] X + [4] = a__g(mark(X),X) a__h(X) = [1] X + [4] >= [1] X + [4] = h(X) mark(a()) = [12] >= [1] = a__a() mark(b()) = [0] >= [0] = b() mark(f(X1,X2)) = [1] X1 + [13] >= [1] X1 + [8] = a__f(mark(X1),X2) mark(g(X1,X2)) = [1] X1 + [0] >= [1] X1 + [4] = a__g(mark(X1),X2) mark(h(X)) = [1] X + [4] >= [1] X + [4] = a__h(mark(X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: NaturalMI MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__f(X1,X2) -> f(X1,X2) a__h(X) -> h(X) mark(g(X1,X2)) -> a__g(mark(X1),X2) - Weak TRS: a__a() -> b() a__f(X,X) -> a__h(a__a()) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: {a__a,a__f,a__g,a__h,mark} TcT has computed the following interpretation: p(a) = [0] [0] p(a__a) = [0] [0] p(a__f) = [1 0] x1 + [0] [0 1] [1] p(a__g) = [1 0] x1 + [0] [0 1] [1] p(a__h) = [1 4] x1 + [0] [0 1] [1] p(b) = [0] [0] p(f) = [1 0] x1 + [0] [0 1] [1] p(g) = [1 0] x1 + [0] [0 1] [1] p(h) = [1 4] x1 + [0] [0 1] [1] p(mark) = [1 4] x1 + [0] [0 1] [0] Following rules are strictly oriented: mark(g(X1,X2)) = [1 4] X1 + [4] [0 1] [1] > [1 4] X1 + [0] [0 1] [1] = a__g(mark(X1),X2) Following rules are (at-least) weakly oriented: a__a() = [0] [0] >= [0] [0] = a() a__a() = [0] [0] >= [0] [0] = b() a__f(X,X) = [1 0] X + [0] [0 1] [1] >= [0] [1] = a__h(a__a()) a__f(X1,X2) = [1 0] X1 + [0] [0 1] [1] >= [1 0] X1 + [0] [0 1] [1] = f(X1,X2) a__g(X1,X2) = [1 0] X1 + [0] [0 1] [1] >= [1 0] X1 + [0] [0 1] [1] = g(X1,X2) a__g(a(),X) = [0] [1] >= [0] [1] = a__f(b(),X) a__h(X) = [1 4] X + [0] [0 1] [1] >= [1 4] X + [0] [0 1] [1] = a__g(mark(X),X) a__h(X) = [1 4] X + [0] [0 1] [1] >= [1 4] X + [0] [0 1] [1] = h(X) mark(a()) = [0] [0] >= [0] [0] = a__a() mark(b()) = [0] [0] >= [0] [0] = b() mark(f(X1,X2)) = [1 4] X1 + [4] [0 1] [1] >= [1 4] X1 + [0] [0 1] [1] = a__f(mark(X1),X2) mark(h(X)) = [1 8] X + [4] [0 1] [1] >= [1 8] X + [0] [0 1] [1] = a__h(mark(X)) * Step 9: NaturalMI MAYBE + Considered Problem: - Strict TRS: a__a() -> a() a__f(X1,X2) -> f(X1,X2) a__h(X) -> h(X) - Weak TRS: a__a() -> b() a__f(X,X) -> a__h(a__a()) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(a__f) = {1}, uargs(a__g) = {1}, uargs(a__h) = {1} Following symbols are considered usable: {a__a,a__f,a__g,a__h,mark} TcT has computed the following interpretation: p(a) = [0] [0] p(a__a) = [0] [0] p(a__f) = [1 0] x1 + [1] [0 1] [2] p(a__g) = [1 0] x1 + [1] [0 1] [2] p(a__h) = [1 4] x1 + [1] [0 1] [2] p(b) = [0] [0] p(f) = [1 0] x1 + [0] [0 1] [2] p(g) = [1 0] x1 + [0] [0 1] [2] p(h) = [1 4] x1 + [0] [0 1] [2] p(mark) = [1 4] x1 + [0] [0 1] [0] Following rules are strictly oriented: a__f(X1,X2) = [1 0] X1 + [1] [0 1] [2] > [1 0] X1 + [0] [0 1] [2] = f(X1,X2) a__h(X) = [1 4] X + [1] [0 1] [2] > [1 4] X + [0] [0 1] [2] = h(X) Following rules are (at-least) weakly oriented: a__a() = [0] [0] >= [0] [0] = a() a__a() = [0] [0] >= [0] [0] = b() a__f(X,X) = [1 0] X + [1] [0 1] [2] >= [1] [2] = a__h(a__a()) a__g(X1,X2) = [1 0] X1 + [1] [0 1] [2] >= [1 0] X1 + [0] [0 1] [2] = g(X1,X2) a__g(a(),X) = [1] [2] >= [1] [2] = a__f(b(),X) a__h(X) = [1 4] X + [1] [0 1] [2] >= [1 4] X + [1] [0 1] [2] = a__g(mark(X),X) mark(a()) = [0] [0] >= [0] [0] = a__a() mark(b()) = [0] [0] >= [0] [0] = b() mark(f(X1,X2)) = [1 4] X1 + [8] [0 1] [2] >= [1 4] X1 + [1] [0 1] [2] = a__f(mark(X1),X2) mark(g(X1,X2)) = [1 4] X1 + [8] [0 1] [2] >= [1 4] X1 + [1] [0 1] [2] = a__g(mark(X1),X2) mark(h(X)) = [1 8] X + [8] [0 1] [2] >= [1 8] X + [1] [0 1] [2] = a__h(mark(X)) * Step 10: Failure MAYBE + Considered Problem: - Strict TRS: a__a() -> a() - Weak TRS: a__a() -> b() a__f(X,X) -> a__h(a__a()) a__f(X1,X2) -> f(X1,X2) a__g(X1,X2) -> g(X1,X2) a__g(a(),X) -> a__f(b(),X) a__h(X) -> a__g(mark(X),X) a__h(X) -> h(X) mark(a()) -> a__a() mark(b()) -> b() mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(g(X1,X2)) -> a__g(mark(X1),X2) mark(h(X)) -> a__h(mark(X)) - Signature: {a__a/0,a__f/2,a__g/2,a__h/1,mark/1} / {a/0,b/0,f/2,g/2,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__a,a__f,a__g,a__h,mark} and constructors {a,b,f,g,h} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE