MAYBE * Step 1: WeightGap MAYBE + Considered Problem: - Strict TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c)) f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c) foldf(x,cons(y,z)) -> f(foldf(x,z),y) foldf(x,nil()) -> x g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,foldf/2,g/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3} - Obligation: innermost runtime complexity wrt. defined symbols {f,f',f'',foldf,g} and constructors {A,B,C,cons,nil ,triple} + 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(f) = {1}, uargs(f') = {2}, uargs(f'') = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(A) = [0] p(B) = [0] p(C) = [0] p(cons) = [11] p(f) = [1] x1 + [12] p(f') = [1] x2 + [0] p(f'') = [1] x1 + [2] p(foldf) = [4] x1 + [2] p(g) = [8] p(nil) = [1] p(triple) = [5] Following rules are strictly oriented: f(t,x) = [1] t + [12] > [8] = f'(t,g(x)) foldf(x,nil()) = [4] x + [2] > [1] x + [0] = x g(A()) = [8] > [0] = A() g(B()) = [8] > [0] = A() g(B()) = [8] > [0] = B() g(C()) = [8] > [0] = A() g(C()) = [8] > [0] = B() g(C()) = [8] > [0] = C() Following rules are (at-least) weakly oriented: f'(triple(a,b,c),A()) = [0] >= [24] = f''(foldf(triple(cons(A(),a),nil(),c),b)) f'(triple(a,b,c),B()) = [0] >= [17] = f(triple(a,b,c),A()) f'(triple(a,b,c),C()) = [0] >= [5] = triple(a,b,cons(C(),c)) f''(triple(a,b,c)) = [7] >= [22] = foldf(triple(a,b,nil()),c) foldf(x,cons(y,z)) = [4] x + [2] >= [4] x + [14] = f(foldf(x,z),y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap MAYBE + Considered Problem: - Strict TRS: f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c)) f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c) foldf(x,cons(y,z)) -> f(foldf(x,z),y) - Weak TRS: f(t,x) -> f'(t,g(x)) foldf(x,nil()) -> x g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,foldf/2,g/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3} - Obligation: innermost runtime complexity wrt. defined symbols {f,f',f'',foldf,g} and constructors {A,B,C,cons,nil ,triple} + 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(f) = {1}, uargs(f') = {2}, uargs(f'') = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(A) = [0] p(B) = [2] p(C) = [0] p(cons) = [1] x1 + [1] x2 + [0] p(f) = [1] x1 + [4] p(f') = [1] x1 + [1] x2 + [2] p(f'') = [1] x1 + [4] p(foldf) = [1] x1 + [2] p(g) = [2] p(nil) = [0] p(triple) = [0] Following rules are strictly oriented: f'(triple(a,b,c),C()) = [2] > [0] = triple(a,b,cons(C(),c)) f''(triple(a,b,c)) = [4] > [2] = foldf(triple(a,b,nil()),c) Following rules are (at-least) weakly oriented: f(t,x) = [1] t + [4] >= [1] t + [4] = f'(t,g(x)) f'(triple(a,b,c),A()) = [2] >= [6] = f''(foldf(triple(cons(A(),a),nil(),c),b)) f'(triple(a,b,c),B()) = [4] >= [4] = f(triple(a,b,c),A()) foldf(x,cons(y,z)) = [1] x + [2] >= [1] x + [6] = f(foldf(x,z),y) foldf(x,nil()) = [1] x + [2] >= [1] x + [0] = x g(A()) = [2] >= [0] = A() g(B()) = [2] >= [0] = A() g(B()) = [2] >= [2] = B() g(C()) = [2] >= [0] = A() g(C()) = [2] >= [2] = B() g(C()) = [2] >= [0] = C() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap MAYBE + Considered Problem: - Strict TRS: f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) foldf(x,cons(y,z)) -> f(foldf(x,z),y) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c)) f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c) foldf(x,nil()) -> x g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,foldf/2,g/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3} - Obligation: innermost runtime complexity wrt. defined symbols {f,f',f'',foldf,g} and constructors {A,B,C,cons,nil ,triple} + 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(f) = {1}, uargs(f') = {2}, uargs(f'') = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(A) = [1] p(B) = [1] p(C) = [1] p(cons) = [1] x2 + [0] p(f) = [1] x1 + [3] p(f') = [1] x2 + [0] p(f'') = [1] x1 + [0] p(foldf) = [2] x1 + [0] p(g) = [1] p(nil) = [1] p(triple) = [0] Following rules are strictly oriented: f'(triple(a,b,c),A()) = [1] > [0] = f''(foldf(triple(cons(A(),a),nil(),c),b)) Following rules are (at-least) weakly oriented: f(t,x) = [1] t + [3] >= [1] = f'(t,g(x)) f'(triple(a,b,c),B()) = [1] >= [3] = f(triple(a,b,c),A()) f'(triple(a,b,c),C()) = [1] >= [0] = triple(a,b,cons(C(),c)) f''(triple(a,b,c)) = [0] >= [0] = foldf(triple(a,b,nil()),c) foldf(x,cons(y,z)) = [2] x + [0] >= [2] x + [3] = f(foldf(x,z),y) foldf(x,nil()) = [2] x + [0] >= [1] x + [0] = x g(A()) = [1] >= [1] = A() g(B()) = [1] >= [1] = A() g(B()) = [1] >= [1] = B() g(C()) = [1] >= [1] = A() g(C()) = [1] >= [1] = B() g(C()) = [1] >= [1] = C() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap MAYBE + Considered Problem: - Strict TRS: f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) foldf(x,cons(y,z)) -> f(foldf(x,z),y) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b)) f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c)) f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c) foldf(x,nil()) -> x g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,foldf/2,g/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3} - Obligation: innermost runtime complexity wrt. defined symbols {f,f',f'',foldf,g} and constructors {A,B,C,cons,nil ,triple} + 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(f) = {1}, uargs(f') = {2}, uargs(f'') = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(A) = [0] p(B) = [1] p(C) = [1] p(cons) = [1] x1 + [1] x2 + [0] p(f) = [1] x1 + [1] x2 + [0] p(f') = [1] x1 + [1] x2 + [0] p(f'') = [1] x1 + [0] p(foldf) = [1] x1 + [1] x2 + [0] p(g) = [1] x1 + [0] p(nil) = [0] p(triple) = [1] x2 + [1] x3 + [0] Following rules are strictly oriented: f'(triple(a,b,c),B()) = [1] b + [1] c + [1] > [1] b + [1] c + [0] = f(triple(a,b,c),A()) Following rules are (at-least) weakly oriented: f(t,x) = [1] t + [1] x + [0] >= [1] t + [1] x + [0] = f'(t,g(x)) f'(triple(a,b,c),A()) = [1] b + [1] c + [0] >= [1] b + [1] c + [0] = f''(foldf(triple(cons(A(),a),nil(),c),b)) f'(triple(a,b,c),C()) = [1] b + [1] c + [1] >= [1] b + [1] c + [1] = triple(a,b,cons(C(),c)) f''(triple(a,b,c)) = [1] b + [1] c + [0] >= [1] b + [1] c + [0] = foldf(triple(a,b,nil()),c) foldf(x,cons(y,z)) = [1] x + [1] y + [1] z + [0] >= [1] x + [1] y + [1] z + [0] = f(foldf(x,z),y) foldf(x,nil()) = [1] x + [0] >= [1] x + [0] = x g(A()) = [0] >= [0] = A() g(B()) = [1] >= [0] = A() g(B()) = [1] >= [1] = B() g(C()) = [1] >= [0] = A() g(C()) = [1] >= [1] = B() g(C()) = [1] >= [1] = C() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: Failure MAYBE + Considered Problem: - Strict TRS: foldf(x,cons(y,z)) -> f(foldf(x,z),y) - Weak TRS: f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b)) f'(triple(a,b,c),B()) -> f(triple(a,b,c),A()) f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c)) f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c) foldf(x,nil()) -> x g(A()) -> A() g(B()) -> A() g(B()) -> B() g(C()) -> A() g(C()) -> B() g(C()) -> C() - Signature: {f/2,f'/2,f''/1,foldf/2,g/1} / {A/0,B/0,C/0,cons/2,nil/0,triple/3} - Obligation: innermost runtime complexity wrt. defined symbols {f,f',f'',foldf,g} and constructors {A,B,C,cons,nil ,triple} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE