MAYBE * Step 1: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__adx(X)) -> adx(X) activate(n__incr(X)) -> incr(X) activate(n__s(X)) -> s(X) activate(n__zeros()) -> zeros() adx(X) -> n__adx(X) adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) -> activate(X) incr(X) -> n__incr(X) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) nats() -> adx(zeros()) s(X) -> n__s(X) tl(cons(X,Y)) -> activate(Y) zeros() -> cons(n__0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,adx/1,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0} / {cons/2,n__0/0,n__adx/1,n__incr/1,n__s/1 ,n__zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,adx,hd,incr,nats,s,tl ,zeros} and constructors {cons,n__0,n__adx,n__incr,n__s,n__zeros} + 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(adx) = {1}, uargs(cons) = {1,2}, uargs(incr) = {1}, uargs(n__adx) = {1}, uargs(n__incr) = {1}, uargs(n__s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [3] p(adx) = [1] x1 + [0] p(cons) = [1] x1 + [1] x2 + [14] p(hd) = [1] x1 + [2] p(incr) = [1] x1 + [0] p(n__0) = [0] p(n__adx) = [1] x1 + [0] p(n__incr) = [1] x1 + [0] p(n__s) = [1] x1 + [0] p(n__zeros) = [0] p(nats) = [0] p(s) = [1] x1 + [0] p(tl) = [1] x1 + [0] p(zeros) = [0] Following rules are strictly oriented: activate(X) = [1] X + [3] > [1] X + [0] = X activate(n__0()) = [3] > [0] = 0() activate(n__adx(X)) = [1] X + [3] > [1] X + [0] = adx(X) activate(n__incr(X)) = [1] X + [3] > [1] X + [0] = incr(X) activate(n__s(X)) = [1] X + [3] > [1] X + [0] = s(X) activate(n__zeros()) = [3] > [0] = zeros() hd(cons(X,Y)) = [1] X + [1] Y + [16] > [1] X + [3] = activate(X) tl(cons(X,Y)) = [1] X + [1] Y + [14] > [1] Y + [3] = activate(Y) Following rules are (at-least) weakly oriented: 0() = [0] >= [0] = n__0() adx(X) = [1] X + [0] >= [1] X + [0] = n__adx(X) adx(cons(X,Y)) = [1] X + [1] Y + [14] >= [1] X + [1] Y + [20] = incr(cons(activate(X),n__adx(activate(Y)))) incr(X) = [1] X + [0] >= [1] X + [0] = n__incr(X) incr(cons(X,Y)) = [1] X + [1] Y + [14] >= [1] X + [1] Y + [20] = cons(n__s(activate(X)),n__incr(activate(Y))) nats() = [0] >= [0] = adx(zeros()) s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) zeros() = [0] >= [14] = cons(n__0(),n__zeros()) zeros() = [0] >= [0] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() adx(X) -> n__adx(X) adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) incr(X) -> n__incr(X) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) nats() -> adx(zeros()) s(X) -> n__s(X) zeros() -> cons(n__0(),n__zeros()) zeros() -> n__zeros() - Weak TRS: activate(X) -> X activate(n__0()) -> 0() activate(n__adx(X)) -> adx(X) activate(n__incr(X)) -> incr(X) activate(n__s(X)) -> s(X) activate(n__zeros()) -> zeros() hd(cons(X,Y)) -> activate(X) tl(cons(X,Y)) -> activate(Y) - Signature: {0/0,activate/1,adx/1,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0} / {cons/2,n__0/0,n__adx/1,n__incr/1,n__s/1 ,n__zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,adx,hd,incr,nats,s,tl ,zeros} and constructors {cons,n__0,n__adx,n__incr,n__s,n__zeros} + 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(adx) = {1}, uargs(cons) = {1,2}, uargs(incr) = {1}, uargs(n__adx) = {1}, uargs(n__incr) = {1}, uargs(n__s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [6] p(activate) = [1] x1 + [3] p(adx) = [1] x1 + [8] p(cons) = [1] x1 + [1] x2 + [0] p(hd) = [2] x1 + [3] p(incr) = [1] x1 + [9] p(n__0) = [3] p(n__adx) = [1] x1 + [5] p(n__incr) = [1] x1 + [6] p(n__s) = [1] x1 + [2] p(n__zeros) = [2] p(nats) = [0] p(s) = [1] x1 + [5] p(tl) = [1] x1 + [3] p(zeros) = [5] Following rules are strictly oriented: 0() = [6] > [3] = n__0() adx(X) = [1] X + [8] > [1] X + [5] = n__adx(X) incr(X) = [1] X + [9] > [1] X + [6] = n__incr(X) s(X) = [1] X + [5] > [1] X + [2] = n__s(X) zeros() = [5] > [2] = n__zeros() Following rules are (at-least) weakly oriented: activate(X) = [1] X + [3] >= [1] X + [0] = X activate(n__0()) = [6] >= [6] = 0() activate(n__adx(X)) = [1] X + [8] >= [1] X + [8] = adx(X) activate(n__incr(X)) = [1] X + [9] >= [1] X + [9] = incr(X) activate(n__s(X)) = [1] X + [5] >= [1] X + [5] = s(X) activate(n__zeros()) = [5] >= [5] = zeros() adx(cons(X,Y)) = [1] X + [1] Y + [8] >= [1] X + [1] Y + [20] = incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) = [2] X + [2] Y + [3] >= [1] X + [3] = activate(X) incr(cons(X,Y)) = [1] X + [1] Y + [9] >= [1] X + [1] Y + [14] = cons(n__s(activate(X)),n__incr(activate(Y))) nats() = [0] >= [13] = adx(zeros()) tl(cons(X,Y)) = [1] X + [1] Y + [3] >= [1] Y + [3] = activate(Y) zeros() = [5] >= [5] = cons(n__0(),n__zeros()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap MAYBE + Considered Problem: - Strict TRS: adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) nats() -> adx(zeros()) zeros() -> cons(n__0(),n__zeros()) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__adx(X)) -> adx(X) activate(n__incr(X)) -> incr(X) activate(n__s(X)) -> s(X) activate(n__zeros()) -> zeros() adx(X) -> n__adx(X) hd(cons(X,Y)) -> activate(X) incr(X) -> n__incr(X) s(X) -> n__s(X) tl(cons(X,Y)) -> activate(Y) zeros() -> n__zeros() - Signature: {0/0,activate/1,adx/1,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0} / {cons/2,n__0/0,n__adx/1,n__incr/1,n__s/1 ,n__zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,adx,hd,incr,nats,s,tl ,zeros} and constructors {cons,n__0,n__adx,n__incr,n__s,n__zeros} + 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(adx) = {1}, uargs(cons) = {1,2}, uargs(incr) = {1}, uargs(n__adx) = {1}, uargs(n__incr) = {1}, uargs(n__s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [1] p(activate) = [1] x1 + [5] p(adx) = [1] x1 + [12] p(cons) = [1] x1 + [1] x2 + [1] p(hd) = [8] x1 + [8] p(incr) = [1] x1 + [5] p(n__0) = [1] p(n__adx) = [1] x1 + [12] p(n__incr) = [1] x1 + [0] p(n__s) = [1] x1 + [4] p(n__zeros) = [8] p(nats) = [0] p(s) = [1] x1 + [6] p(tl) = [8] x1 + [8] p(zeros) = [12] Following rules are strictly oriented: zeros() = [12] > [10] = cons(n__0(),n__zeros()) Following rules are (at-least) weakly oriented: 0() = [1] >= [1] = n__0() activate(X) = [1] X + [5] >= [1] X + [0] = X activate(n__0()) = [6] >= [1] = 0() activate(n__adx(X)) = [1] X + [17] >= [1] X + [12] = adx(X) activate(n__incr(X)) = [1] X + [5] >= [1] X + [5] = incr(X) activate(n__s(X)) = [1] X + [9] >= [1] X + [6] = s(X) activate(n__zeros()) = [13] >= [12] = zeros() adx(X) = [1] X + [12] >= [1] X + [12] = n__adx(X) adx(cons(X,Y)) = [1] X + [1] Y + [13] >= [1] X + [1] Y + [28] = incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) = [8] X + [8] Y + [16] >= [1] X + [5] = activate(X) incr(X) = [1] X + [5] >= [1] X + [0] = n__incr(X) incr(cons(X,Y)) = [1] X + [1] Y + [6] >= [1] X + [1] Y + [15] = cons(n__s(activate(X)),n__incr(activate(Y))) nats() = [0] >= [24] = adx(zeros()) s(X) = [1] X + [6] >= [1] X + [4] = n__s(X) tl(cons(X,Y)) = [8] X + [8] Y + [16] >= [1] Y + [5] = activate(Y) zeros() = [12] >= [8] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap MAYBE + Considered Problem: - Strict TRS: adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) nats() -> adx(zeros()) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__adx(X)) -> adx(X) activate(n__incr(X)) -> incr(X) activate(n__s(X)) -> s(X) activate(n__zeros()) -> zeros() adx(X) -> n__adx(X) hd(cons(X,Y)) -> activate(X) incr(X) -> n__incr(X) s(X) -> n__s(X) tl(cons(X,Y)) -> activate(Y) zeros() -> cons(n__0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,adx/1,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0} / {cons/2,n__0/0,n__adx/1,n__incr/1,n__s/1 ,n__zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,adx,hd,incr,nats,s,tl ,zeros} and constructors {cons,n__0,n__adx,n__incr,n__s,n__zeros} + 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(adx) = {1}, uargs(cons) = {1,2}, uargs(incr) = {1}, uargs(n__adx) = {1}, uargs(n__incr) = {1}, uargs(n__s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [3] p(activate) = [1] x1 + [3] p(adx) = [1] x1 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(hd) = [8] x1 + [3] p(incr) = [1] x1 + [4] p(n__0) = [3] p(n__adx) = [1] x1 + [0] p(n__incr) = [1] x1 + [2] p(n__s) = [1] x1 + [5] p(n__zeros) = [4] p(nats) = [9] p(s) = [1] x1 + [6] p(tl) = [9] x1 + [9] p(zeros) = [7] Following rules are strictly oriented: nats() = [9] > [7] = adx(zeros()) Following rules are (at-least) weakly oriented: 0() = [3] >= [3] = n__0() activate(X) = [1] X + [3] >= [1] X + [0] = X activate(n__0()) = [6] >= [3] = 0() activate(n__adx(X)) = [1] X + [3] >= [1] X + [0] = adx(X) activate(n__incr(X)) = [1] X + [5] >= [1] X + [4] = incr(X) activate(n__s(X)) = [1] X + [8] >= [1] X + [6] = s(X) activate(n__zeros()) = [7] >= [7] = zeros() adx(X) = [1] X + [0] >= [1] X + [0] = n__adx(X) adx(cons(X,Y)) = [1] X + [1] Y + [0] >= [1] X + [1] Y + [10] = incr(cons(activate(X),n__adx(activate(Y)))) hd(cons(X,Y)) = [8] X + [8] Y + [3] >= [1] X + [3] = activate(X) incr(X) = [1] X + [4] >= [1] X + [2] = n__incr(X) incr(cons(X,Y)) = [1] X + [1] Y + [4] >= [1] X + [1] Y + [13] = cons(n__s(activate(X)),n__incr(activate(Y))) s(X) = [1] X + [6] >= [1] X + [5] = n__s(X) tl(cons(X,Y)) = [9] X + [9] Y + [9] >= [1] Y + [3] = activate(Y) zeros() = [7] >= [7] = cons(n__0(),n__zeros()) zeros() = [7] >= [4] = n__zeros() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: Failure MAYBE + Considered Problem: - Strict TRS: adx(cons(X,Y)) -> incr(cons(activate(X),n__adx(activate(Y)))) incr(cons(X,Y)) -> cons(n__s(activate(X)),n__incr(activate(Y))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__adx(X)) -> adx(X) activate(n__incr(X)) -> incr(X) activate(n__s(X)) -> s(X) activate(n__zeros()) -> zeros() adx(X) -> n__adx(X) hd(cons(X,Y)) -> activate(X) incr(X) -> n__incr(X) nats() -> adx(zeros()) s(X) -> n__s(X) tl(cons(X,Y)) -> activate(Y) zeros() -> cons(n__0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,adx/1,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0} / {cons/2,n__0/0,n__adx/1,n__incr/1,n__s/1 ,n__zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,adx,hd,incr,nats,s,tl ,zeros} and constructors {cons,n__0,n__adx,n__incr,n__s,n__zeros} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE