YES(O(1),O(n^1)) 1182.67/297.11 YES(O(1),O(n^1)) 1182.67/297.11 1182.67/297.11 We are left with following problem, upon which TcT provides the 1182.67/297.11 certificate YES(O(1),O(n^1)). 1182.67/297.11 1182.67/297.11 Strict Trs: 1182.67/297.11 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.11 , a__and(true(), X) -> mark(X) 1182.67/297.11 , a__and(false(), Y) -> false() 1182.67/297.11 , mark(true()) -> true() 1182.67/297.11 , mark(false()) -> false() 1182.67/297.11 , mark(0()) -> 0() 1182.67/297.11 , mark(s(X)) -> s(X) 1182.67/297.11 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.11 , mark(nil()) -> nil() 1182.67/297.11 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.11 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.11 , mark(from(X)) -> a__from(X) 1182.67/297.11 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.11 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.11 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.11 , a__if(true(), X, Y) -> mark(X) 1182.67/297.11 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.11 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.11 , a__add(0(), X) -> mark(X) 1182.67/297.11 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.11 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.11 , a__first(0(), X) -> nil() 1182.67/297.11 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.11 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.11 , a__from(X) -> from(X) } 1182.67/297.11 Obligation: 1182.67/297.11 runtime complexity 1182.67/297.11 Answer: 1182.67/297.11 YES(O(1),O(n^1)) 1182.67/297.11 1182.67/297.11 The weightgap principle applies (using the following nonconstant 1182.67/297.11 growth matrix-interpretation) 1182.67/297.11 1182.67/297.11 The following argument positions are usable: 1182.67/297.11 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.11 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.11 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.11 1182.67/297.11 TcT has computed the following matrix interpretation satisfying 1182.67/297.11 not(EDA) and not(IDA(1)). 1182.67/297.11 1182.67/297.11 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [true] = [0] 1182.67/297.11 1182.67/297.11 [mark](x1) = [0] 1182.67/297.11 1182.67/297.11 [false] = [0] 1182.67/297.11 1182.67/297.11 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [0] = [0] 1182.67/297.11 1182.67/297.11 [s](x1) = [0] 1182.67/297.11 1182.67/297.11 [add](x1, x2) = [1] x1 + [5] 1182.67/297.11 1182.67/297.11 [a__first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.11 1182.67/297.11 [nil] = [7] 1182.67/297.11 1182.67/297.11 [cons](x1, x2) = [0] 1182.67/297.11 1182.67/297.11 [first](x1, x2) = [1] x1 + [1] x2 + [5] 1182.67/297.11 1182.67/297.11 [a__from](x1) = [5] 1182.67/297.11 1182.67/297.11 [from](x1) = [5] 1182.67/297.11 1182.67/297.11 [and](x1, x2) = [1] x1 + [7] 1182.67/297.11 1182.67/297.11 [if](x1, x2, x3) = [1] x1 + [7] 1182.67/297.11 1182.67/297.11 The order satisfies the following ordering constraints: 1182.67/297.11 1182.67/297.11 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.11 ? [1] X1 + [7] 1182.67/297.11 = [and(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__and(true(), X)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__and(false(), Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [false()] 1182.67/297.11 1182.67/297.11 [mark(true())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [true()] 1182.67/297.11 1182.67/297.11 [mark(false())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [false()] 1182.67/297.11 1182.67/297.11 [mark(0())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [0()] 1182.67/297.11 1182.67/297.11 [mark(s(X))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [s(X)] 1182.67/297.11 1182.67/297.11 [mark(add(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__add(mark(X1), X2)] 1182.67/297.11 1182.67/297.11 [mark(nil())] = [0] 1182.67/297.11 ? [7] 1182.67/297.11 = [nil()] 1182.67/297.11 1182.67/297.11 [mark(cons(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [cons(X1, X2)] 1182.67/297.11 1182.67/297.11 [mark(first(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__first(mark(X1), mark(X2))] 1182.67/297.11 1182.67/297.11 [mark(from(X))] = [0] 1182.67/297.11 ? [5] 1182.67/297.11 = [a__from(X)] 1182.67/297.11 1182.67/297.11 [mark(and(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__and(mark(X1), X2)] 1182.67/297.11 1182.67/297.11 [mark(if(X1, X2, X3))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__if(mark(X1), X2, X3)] 1182.67/297.11 1182.67/297.11 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.11 ? [1] X1 + [7] 1182.67/297.11 = [if(X1, X2, X3)] 1182.67/297.11 1182.67/297.11 [a__if(true(), X, Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__if(false(), X, Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(Y)] 1182.67/297.11 1182.67/297.11 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.11 ? [1] X1 + [5] 1182.67/297.11 = [add(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__add(0(), X)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__add(s(X), Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [s(add(X, Y))] 1182.67/297.11 1182.67/297.11 [a__first(X1, X2)] = [1] X1 + [1] X2 + [0] 1182.67/297.11 ? [1] X1 + [1] X2 + [5] 1182.67/297.11 = [first(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__first(0(), X)] = [1] X + [0] 1182.67/297.11 ? [7] 1182.67/297.11 = [nil()] 1182.67/297.11 1182.67/297.11 [a__first(s(X), cons(Y, Z))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [cons(Y, first(X, Z))] 1182.67/297.11 1182.67/297.11 [a__from(X)] = [5] 1182.67/297.11 > [0] 1182.67/297.11 = [cons(X, from(s(X)))] 1182.67/297.11 1182.67/297.11 [a__from(X)] = [5] 1182.67/297.11 >= [5] 1182.67/297.11 = [from(X)] 1182.67/297.11 1182.67/297.11 1182.67/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.11 1182.67/297.11 We are left with following problem, upon which TcT provides the 1182.67/297.11 certificate YES(O(1),O(n^1)). 1182.67/297.11 1182.67/297.11 Strict Trs: 1182.67/297.11 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.11 , a__and(true(), X) -> mark(X) 1182.67/297.11 , a__and(false(), Y) -> false() 1182.67/297.11 , mark(true()) -> true() 1182.67/297.11 , mark(false()) -> false() 1182.67/297.11 , mark(0()) -> 0() 1182.67/297.11 , mark(s(X)) -> s(X) 1182.67/297.11 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.11 , mark(nil()) -> nil() 1182.67/297.11 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.11 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.11 , mark(from(X)) -> a__from(X) 1182.67/297.11 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.11 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.11 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.11 , a__if(true(), X, Y) -> mark(X) 1182.67/297.11 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.11 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.11 , a__add(0(), X) -> mark(X) 1182.67/297.11 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.11 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.11 , a__first(0(), X) -> nil() 1182.67/297.11 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.11 , a__from(X) -> from(X) } 1182.67/297.11 Weak Trs: { a__from(X) -> cons(X, from(s(X))) } 1182.67/297.11 Obligation: 1182.67/297.11 runtime complexity 1182.67/297.11 Answer: 1182.67/297.11 YES(O(1),O(n^1)) 1182.67/297.11 1182.67/297.11 The weightgap principle applies (using the following nonconstant 1182.67/297.11 growth matrix-interpretation) 1182.67/297.11 1182.67/297.11 The following argument positions are usable: 1182.67/297.11 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.11 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.11 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.11 1182.67/297.11 TcT has computed the following matrix interpretation satisfying 1182.67/297.11 not(EDA) and not(IDA(1)). 1182.67/297.11 1182.67/297.11 [a__and](x1, x2) = [1] x1 + [4] 1182.67/297.11 1182.67/297.11 [true] = [0] 1182.67/297.11 1182.67/297.11 [mark](x1) = [0] 1182.67/297.11 1182.67/297.11 [false] = [0] 1182.67/297.11 1182.67/297.11 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [0] = [0] 1182.67/297.11 1182.67/297.11 [s](x1) = [0] 1182.67/297.11 1182.67/297.11 [add](x1, x2) = [1] x1 + [5] 1182.67/297.11 1182.67/297.11 [a__first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.11 1182.67/297.11 [nil] = [7] 1182.67/297.11 1182.67/297.11 [cons](x1, x2) = [0] 1182.67/297.11 1182.67/297.11 [first](x1, x2) = [1] x1 + [1] x2 + [5] 1182.67/297.11 1182.67/297.11 [a__from](x1) = [5] 1182.67/297.11 1182.67/297.11 [from](x1) = [5] 1182.67/297.11 1182.67/297.11 [and](x1, x2) = [1] x1 + [3] 1182.67/297.11 1182.67/297.11 [if](x1, x2, x3) = [1] x1 + [7] 1182.67/297.11 1182.67/297.11 The order satisfies the following ordering constraints: 1182.67/297.11 1182.67/297.11 [a__and(X1, X2)] = [1] X1 + [4] 1182.67/297.11 > [1] X1 + [3] 1182.67/297.11 = [and(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__and(true(), X)] = [4] 1182.67/297.11 > [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__and(false(), Y)] = [4] 1182.67/297.11 > [0] 1182.67/297.11 = [false()] 1182.67/297.11 1182.67/297.11 [mark(true())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [true()] 1182.67/297.11 1182.67/297.11 [mark(false())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [false()] 1182.67/297.11 1182.67/297.11 [mark(0())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [0()] 1182.67/297.11 1182.67/297.11 [mark(s(X))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [s(X)] 1182.67/297.11 1182.67/297.11 [mark(add(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__add(mark(X1), X2)] 1182.67/297.11 1182.67/297.11 [mark(nil())] = [0] 1182.67/297.11 ? [7] 1182.67/297.11 = [nil()] 1182.67/297.11 1182.67/297.11 [mark(cons(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [cons(X1, X2)] 1182.67/297.11 1182.67/297.11 [mark(first(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__first(mark(X1), mark(X2))] 1182.67/297.11 1182.67/297.11 [mark(from(X))] = [0] 1182.67/297.11 ? [5] 1182.67/297.11 = [a__from(X)] 1182.67/297.11 1182.67/297.11 [mark(and(X1, X2))] = [0] 1182.67/297.11 ? [4] 1182.67/297.11 = [a__and(mark(X1), X2)] 1182.67/297.11 1182.67/297.11 [mark(if(X1, X2, X3))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__if(mark(X1), X2, X3)] 1182.67/297.11 1182.67/297.11 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.11 ? [1] X1 + [7] 1182.67/297.11 = [if(X1, X2, X3)] 1182.67/297.11 1182.67/297.11 [a__if(true(), X, Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__if(false(), X, Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(Y)] 1182.67/297.11 1182.67/297.11 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.11 ? [1] X1 + [5] 1182.67/297.11 = [add(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__add(0(), X)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__add(s(X), Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [s(add(X, Y))] 1182.67/297.11 1182.67/297.11 [a__first(X1, X2)] = [1] X1 + [1] X2 + [0] 1182.67/297.11 ? [1] X1 + [1] X2 + [5] 1182.67/297.11 = [first(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__first(0(), X)] = [1] X + [0] 1182.67/297.11 ? [7] 1182.67/297.11 = [nil()] 1182.67/297.11 1182.67/297.11 [a__first(s(X), cons(Y, Z))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [cons(Y, first(X, Z))] 1182.67/297.11 1182.67/297.11 [a__from(X)] = [5] 1182.67/297.11 > [0] 1182.67/297.11 = [cons(X, from(s(X)))] 1182.67/297.11 1182.67/297.11 [a__from(X)] = [5] 1182.67/297.11 >= [5] 1182.67/297.11 = [from(X)] 1182.67/297.11 1182.67/297.11 1182.67/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.11 1182.67/297.11 We are left with following problem, upon which TcT provides the 1182.67/297.11 certificate YES(O(1),O(n^1)). 1182.67/297.11 1182.67/297.11 Strict Trs: 1182.67/297.11 { mark(true()) -> true() 1182.67/297.11 , mark(false()) -> false() 1182.67/297.11 , mark(0()) -> 0() 1182.67/297.11 , mark(s(X)) -> s(X) 1182.67/297.11 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.11 , mark(nil()) -> nil() 1182.67/297.11 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.11 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.11 , mark(from(X)) -> a__from(X) 1182.67/297.11 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.11 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.11 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.11 , a__if(true(), X, Y) -> mark(X) 1182.67/297.11 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.11 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.11 , a__add(0(), X) -> mark(X) 1182.67/297.11 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.11 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.11 , a__first(0(), X) -> nil() 1182.67/297.11 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.11 , a__from(X) -> from(X) } 1182.67/297.11 Weak Trs: 1182.67/297.11 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.11 , a__and(true(), X) -> mark(X) 1182.67/297.11 , a__and(false(), Y) -> false() 1182.67/297.11 , a__from(X) -> cons(X, from(s(X))) } 1182.67/297.11 Obligation: 1182.67/297.11 runtime complexity 1182.67/297.11 Answer: 1182.67/297.11 YES(O(1),O(n^1)) 1182.67/297.11 1182.67/297.11 The weightgap principle applies (using the following nonconstant 1182.67/297.11 growth matrix-interpretation) 1182.67/297.11 1182.67/297.11 The following argument positions are usable: 1182.67/297.11 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.11 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.11 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.11 1182.67/297.11 TcT has computed the following matrix interpretation satisfying 1182.67/297.11 not(EDA) and not(IDA(1)). 1182.67/297.11 1182.67/297.11 [a__and](x1, x2) = [1] x1 + [4] 1182.67/297.11 1182.67/297.11 [true] = [0] 1182.67/297.11 1182.67/297.11 [mark](x1) = [0] 1182.67/297.11 1182.67/297.11 [false] = [0] 1182.67/297.11 1182.67/297.11 [a__if](x1, x2, x3) = [1] x1 + [1] 1182.67/297.11 1182.67/297.11 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [0] = [0] 1182.67/297.11 1182.67/297.11 [s](x1) = [0] 1182.67/297.11 1182.67/297.11 [add](x1, x2) = [1] x1 + [5] 1182.67/297.11 1182.67/297.11 [a__first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.11 1182.67/297.11 [nil] = [7] 1182.67/297.11 1182.67/297.11 [cons](x1, x2) = [0] 1182.67/297.11 1182.67/297.11 [first](x1, x2) = [1] x1 + [1] x2 + [5] 1182.67/297.11 1182.67/297.11 [a__from](x1) = [5] 1182.67/297.11 1182.67/297.11 [from](x1) = [5] 1182.67/297.11 1182.67/297.11 [and](x1, x2) = [1] x1 + [3] 1182.67/297.11 1182.67/297.11 [if](x1, x2, x3) = [1] x1 + [6] 1182.67/297.11 1182.67/297.11 The order satisfies the following ordering constraints: 1182.67/297.11 1182.67/297.11 [a__and(X1, X2)] = [1] X1 + [4] 1182.67/297.11 > [1] X1 + [3] 1182.67/297.11 = [and(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__and(true(), X)] = [4] 1182.67/297.11 > [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__and(false(), Y)] = [4] 1182.67/297.11 > [0] 1182.67/297.11 = [false()] 1182.67/297.11 1182.67/297.11 [mark(true())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [true()] 1182.67/297.11 1182.67/297.11 [mark(false())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [false()] 1182.67/297.11 1182.67/297.11 [mark(0())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [0()] 1182.67/297.11 1182.67/297.11 [mark(s(X))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [s(X)] 1182.67/297.11 1182.67/297.11 [mark(add(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__add(mark(X1), X2)] 1182.67/297.11 1182.67/297.11 [mark(nil())] = [0] 1182.67/297.11 ? [7] 1182.67/297.11 = [nil()] 1182.67/297.11 1182.67/297.11 [mark(cons(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [cons(X1, X2)] 1182.67/297.11 1182.67/297.11 [mark(first(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__first(mark(X1), mark(X2))] 1182.67/297.11 1182.67/297.11 [mark(from(X))] = [0] 1182.67/297.11 ? [5] 1182.67/297.11 = [a__from(X)] 1182.67/297.11 1182.67/297.11 [mark(and(X1, X2))] = [0] 1182.67/297.11 ? [4] 1182.67/297.11 = [a__and(mark(X1), X2)] 1182.67/297.11 1182.67/297.11 [mark(if(X1, X2, X3))] = [0] 1182.67/297.11 ? [1] 1182.67/297.11 = [a__if(mark(X1), X2, X3)] 1182.67/297.11 1182.67/297.11 [a__if(X1, X2, X3)] = [1] X1 + [1] 1182.67/297.11 ? [1] X1 + [6] 1182.67/297.11 = [if(X1, X2, X3)] 1182.67/297.11 1182.67/297.11 [a__if(true(), X, Y)] = [1] 1182.67/297.11 > [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__if(false(), X, Y)] = [1] 1182.67/297.11 > [0] 1182.67/297.11 = [mark(Y)] 1182.67/297.11 1182.67/297.11 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.11 ? [1] X1 + [5] 1182.67/297.11 = [add(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__add(0(), X)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__add(s(X), Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [s(add(X, Y))] 1182.67/297.11 1182.67/297.11 [a__first(X1, X2)] = [1] X1 + [1] X2 + [0] 1182.67/297.11 ? [1] X1 + [1] X2 + [5] 1182.67/297.11 = [first(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__first(0(), X)] = [1] X + [0] 1182.67/297.11 ? [7] 1182.67/297.11 = [nil()] 1182.67/297.11 1182.67/297.11 [a__first(s(X), cons(Y, Z))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [cons(Y, first(X, Z))] 1182.67/297.11 1182.67/297.11 [a__from(X)] = [5] 1182.67/297.11 > [0] 1182.67/297.11 = [cons(X, from(s(X)))] 1182.67/297.11 1182.67/297.11 [a__from(X)] = [5] 1182.67/297.11 >= [5] 1182.67/297.11 = [from(X)] 1182.67/297.11 1182.67/297.11 1182.67/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.11 1182.67/297.11 We are left with following problem, upon which TcT provides the 1182.67/297.11 certificate YES(O(1),O(n^1)). 1182.67/297.11 1182.67/297.11 Strict Trs: 1182.67/297.11 { mark(true()) -> true() 1182.67/297.11 , mark(false()) -> false() 1182.67/297.11 , mark(0()) -> 0() 1182.67/297.11 , mark(s(X)) -> s(X) 1182.67/297.11 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.11 , mark(nil()) -> nil() 1182.67/297.11 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.11 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.11 , mark(from(X)) -> a__from(X) 1182.67/297.11 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.11 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.11 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.11 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.11 , a__add(0(), X) -> mark(X) 1182.67/297.11 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.11 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.11 , a__first(0(), X) -> nil() 1182.67/297.11 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.11 , a__from(X) -> from(X) } 1182.67/297.11 Weak Trs: 1182.67/297.11 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.11 , a__and(true(), X) -> mark(X) 1182.67/297.11 , a__and(false(), Y) -> false() 1182.67/297.11 , a__if(true(), X, Y) -> mark(X) 1182.67/297.11 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.11 , a__from(X) -> cons(X, from(s(X))) } 1182.67/297.11 Obligation: 1182.67/297.11 runtime complexity 1182.67/297.11 Answer: 1182.67/297.11 YES(O(1),O(n^1)) 1182.67/297.11 1182.67/297.11 The weightgap principle applies (using the following nonconstant 1182.67/297.11 growth matrix-interpretation) 1182.67/297.11 1182.67/297.11 The following argument positions are usable: 1182.67/297.11 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.11 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.11 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.11 1182.67/297.11 TcT has computed the following matrix interpretation satisfying 1182.67/297.11 not(EDA) and not(IDA(1)). 1182.67/297.11 1182.67/297.11 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [true] = [4] 1182.67/297.11 1182.67/297.11 [mark](x1) = [0] 1182.67/297.11 1182.67/297.11 [false] = [4] 1182.67/297.11 1182.67/297.11 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [0] = [0] 1182.67/297.11 1182.67/297.11 [s](x1) = [0] 1182.67/297.11 1182.67/297.11 [add](x1, x2) = [1] x1 + [5] 1182.67/297.11 1182.67/297.11 [a__first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.11 1182.67/297.11 [nil] = [7] 1182.67/297.11 1182.67/297.11 [cons](x1, x2) = [0] 1182.67/297.11 1182.67/297.11 [first](x1, x2) = [1] x1 + [1] x2 + [5] 1182.67/297.11 1182.67/297.11 [a__from](x1) = [5] 1182.67/297.11 1182.67/297.11 [from](x1) = [1] 1182.67/297.11 1182.67/297.11 [and](x1, x2) = [1] x1 + [0] 1182.67/297.11 1182.67/297.11 [if](x1, x2, x3) = [1] x1 + [7] 1182.67/297.11 1182.67/297.11 The order satisfies the following ordering constraints: 1182.67/297.11 1182.67/297.11 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.11 >= [1] X1 + [0] 1182.67/297.11 = [and(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__and(true(), X)] = [4] 1182.67/297.11 > [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__and(false(), Y)] = [4] 1182.67/297.11 >= [4] 1182.67/297.11 = [false()] 1182.67/297.11 1182.67/297.11 [mark(true())] = [0] 1182.67/297.11 ? [4] 1182.67/297.11 = [true()] 1182.67/297.11 1182.67/297.11 [mark(false())] = [0] 1182.67/297.11 ? [4] 1182.67/297.11 = [false()] 1182.67/297.11 1182.67/297.11 [mark(0())] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [0()] 1182.67/297.11 1182.67/297.11 [mark(s(X))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [s(X)] 1182.67/297.11 1182.67/297.11 [mark(add(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__add(mark(X1), X2)] 1182.67/297.11 1182.67/297.11 [mark(nil())] = [0] 1182.67/297.11 ? [7] 1182.67/297.11 = [nil()] 1182.67/297.11 1182.67/297.11 [mark(cons(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [cons(X1, X2)] 1182.67/297.11 1182.67/297.11 [mark(first(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__first(mark(X1), mark(X2))] 1182.67/297.11 1182.67/297.11 [mark(from(X))] = [0] 1182.67/297.11 ? [5] 1182.67/297.11 = [a__from(X)] 1182.67/297.11 1182.67/297.11 [mark(and(X1, X2))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__and(mark(X1), X2)] 1182.67/297.11 1182.67/297.11 [mark(if(X1, X2, X3))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [a__if(mark(X1), X2, X3)] 1182.67/297.11 1182.67/297.11 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.11 ? [1] X1 + [7] 1182.67/297.11 = [if(X1, X2, X3)] 1182.67/297.11 1182.67/297.11 [a__if(true(), X, Y)] = [4] 1182.67/297.11 > [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__if(false(), X, Y)] = [4] 1182.67/297.11 > [0] 1182.67/297.11 = [mark(Y)] 1182.67/297.11 1182.67/297.11 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.11 ? [1] X1 + [5] 1182.67/297.11 = [add(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__add(0(), X)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [mark(X)] 1182.67/297.11 1182.67/297.11 [a__add(s(X), Y)] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [s(add(X, Y))] 1182.67/297.11 1182.67/297.11 [a__first(X1, X2)] = [1] X1 + [1] X2 + [0] 1182.67/297.11 ? [1] X1 + [1] X2 + [5] 1182.67/297.11 = [first(X1, X2)] 1182.67/297.11 1182.67/297.11 [a__first(0(), X)] = [1] X + [0] 1182.67/297.11 ? [7] 1182.67/297.11 = [nil()] 1182.67/297.11 1182.67/297.11 [a__first(s(X), cons(Y, Z))] = [0] 1182.67/297.11 >= [0] 1182.67/297.11 = [cons(Y, first(X, Z))] 1182.67/297.11 1182.67/297.11 [a__from(X)] = [5] 1182.67/297.11 > [0] 1182.67/297.11 = [cons(X, from(s(X)))] 1182.67/297.11 1182.67/297.11 [a__from(X)] = [5] 1182.67/297.11 > [1] 1182.67/297.11 = [from(X)] 1182.67/297.11 1182.67/297.11 1182.67/297.11 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.11 1182.67/297.11 We are left with following problem, upon which TcT provides the 1182.67/297.11 certificate YES(O(1),O(n^1)). 1182.67/297.11 1182.67/297.11 Strict Trs: 1182.67/297.11 { mark(true()) -> true() 1182.67/297.11 , mark(false()) -> false() 1182.67/297.11 , mark(0()) -> 0() 1182.67/297.11 , mark(s(X)) -> s(X) 1182.67/297.11 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.11 , mark(nil()) -> nil() 1182.67/297.11 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.11 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.11 , mark(from(X)) -> a__from(X) 1182.67/297.11 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.11 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.11 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.11 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.11 , a__add(0(), X) -> mark(X) 1182.67/297.11 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.11 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.11 , a__first(0(), X) -> nil() 1182.67/297.11 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) } 1182.67/297.11 Weak Trs: 1182.67/297.11 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.11 , a__and(true(), X) -> mark(X) 1182.67/297.11 , a__and(false(), Y) -> false() 1182.67/297.11 , a__if(true(), X, Y) -> mark(X) 1182.67/297.11 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.11 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.11 , a__from(X) -> from(X) } 1182.67/297.11 Obligation: 1182.67/297.11 runtime complexity 1182.67/297.11 Answer: 1182.67/297.11 YES(O(1),O(n^1)) 1182.67/297.11 1182.67/297.11 The weightgap principle applies (using the following nonconstant 1182.67/297.11 growth matrix-interpretation) 1182.67/297.11 1182.67/297.11 The following argument positions are usable: 1182.67/297.11 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.11 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.11 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.11 1182.67/297.11 TcT has computed the following matrix interpretation satisfying 1182.67/297.11 not(EDA) and not(IDA(1)). 1182.67/297.11 1182.67/297.11 [a__and](x1, x2) = [1] x1 + [4] 1182.67/297.11 1182.67/297.11 [true] = [4] 1182.67/297.11 1182.67/297.11 [mark](x1) = [0] 1182.67/297.11 1182.67/297.11 [false] = [4] 1182.67/297.11 1182.67/297.11 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [a__add](x1, x2) = [1] x1 + [1] 1182.67/297.12 1182.67/297.12 [0] = [0] 1182.67/297.12 1182.67/297.12 [s](x1) = [0] 1182.67/297.12 1182.67/297.12 [add](x1, x2) = [1] x1 + [5] 1182.67/297.12 1182.67/297.12 [a__first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.12 1182.67/297.12 [nil] = [7] 1182.67/297.12 1182.67/297.12 [cons](x1, x2) = [0] 1182.67/297.12 1182.67/297.12 [first](x1, x2) = [1] x1 + [1] x2 + [5] 1182.67/297.12 1182.67/297.12 [a__from](x1) = [7] 1182.67/297.12 1182.67/297.12 [from](x1) = [1] 1182.67/297.12 1182.67/297.12 [and](x1, x2) = [1] x1 + [3] 1182.67/297.12 1182.67/297.12 [if](x1, x2, x3) = [1] x1 + [7] 1182.67/297.12 1182.67/297.12 The order satisfies the following ordering constraints: 1182.67/297.12 1182.67/297.12 [a__and(X1, X2)] = [1] X1 + [4] 1182.67/297.12 > [1] X1 + [3] 1182.67/297.12 = [and(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__and(true(), X)] = [8] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__and(false(), Y)] = [8] 1182.67/297.12 > [4] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(true())] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [true()] 1182.67/297.12 1182.67/297.12 [mark(false())] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(0())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [0()] 1182.67/297.12 1182.67/297.12 [mark(s(X))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [s(X)] 1182.67/297.12 1182.67/297.12 [mark(add(X1, X2))] = [0] 1182.67/297.12 ? [1] 1182.67/297.12 = [a__add(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(nil())] = [0] 1182.67/297.12 ? [7] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [mark(cons(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [cons(X1, X2)] 1182.67/297.12 1182.67/297.12 [mark(first(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__first(mark(X1), mark(X2))] 1182.67/297.12 1182.67/297.12 [mark(from(X))] = [0] 1182.67/297.12 ? [7] 1182.67/297.12 = [a__from(X)] 1182.67/297.12 1182.67/297.12 [mark(and(X1, X2))] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [a__and(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(if(X1, X2, X3))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__if(mark(X1), X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.12 ? [1] X1 + [7] 1182.67/297.12 = [if(X1, X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(true(), X, Y)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__if(false(), X, Y)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(Y)] 1182.67/297.12 1182.67/297.12 [a__add(X1, X2)] = [1] X1 + [1] 1182.67/297.12 ? [1] X1 + [5] 1182.67/297.12 = [add(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__add(0(), X)] = [1] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__add(s(X), Y)] = [1] 1182.67/297.12 > [0] 1182.67/297.12 = [s(add(X, Y))] 1182.67/297.12 1182.67/297.12 [a__first(X1, X2)] = [1] X1 + [1] X2 + [0] 1182.67/297.12 ? [1] X1 + [1] X2 + [5] 1182.67/297.12 = [first(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__first(0(), X)] = [1] X + [0] 1182.67/297.12 ? [7] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [a__first(s(X), cons(Y, Z))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [cons(Y, first(X, Z))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [7] 1182.67/297.12 > [0] 1182.67/297.12 = [cons(X, from(s(X)))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [7] 1182.67/297.12 > [1] 1182.67/297.12 = [from(X)] 1182.67/297.12 1182.67/297.12 1182.67/297.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.12 1182.67/297.12 We are left with following problem, upon which TcT provides the 1182.67/297.12 certificate YES(O(1),O(n^1)). 1182.67/297.12 1182.67/297.12 Strict Trs: 1182.67/297.12 { mark(true()) -> true() 1182.67/297.12 , mark(false()) -> false() 1182.67/297.12 , mark(0()) -> 0() 1182.67/297.12 , mark(s(X)) -> s(X) 1182.67/297.12 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.12 , mark(nil()) -> nil() 1182.67/297.12 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.12 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.12 , mark(from(X)) -> a__from(X) 1182.67/297.12 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.12 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.12 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.12 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.12 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.12 , a__first(0(), X) -> nil() 1182.67/297.12 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) } 1182.67/297.12 Weak Trs: 1182.67/297.12 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.12 , a__and(true(), X) -> mark(X) 1182.67/297.12 , a__and(false(), Y) -> false() 1182.67/297.12 , a__if(true(), X, Y) -> mark(X) 1182.67/297.12 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.12 , a__add(0(), X) -> mark(X) 1182.67/297.12 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.12 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.12 , a__from(X) -> from(X) } 1182.67/297.12 Obligation: 1182.67/297.12 runtime complexity 1182.67/297.12 Answer: 1182.67/297.12 YES(O(1),O(n^1)) 1182.67/297.12 1182.67/297.12 The weightgap principle applies (using the following nonconstant 1182.67/297.12 growth matrix-interpretation) 1182.67/297.12 1182.67/297.12 The following argument positions are usable: 1182.67/297.12 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.12 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.12 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.12 1182.67/297.12 TcT has computed the following matrix interpretation satisfying 1182.67/297.12 not(EDA) and not(IDA(1)). 1182.67/297.12 1182.67/297.12 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [true] = [0] 1182.67/297.12 1182.67/297.12 [mark](x1) = [0] 1182.67/297.12 1182.67/297.12 [false] = [0] 1182.67/297.12 1182.67/297.12 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [a__add](x1, x2) = [1] x1 + [4] 1182.67/297.12 1182.67/297.12 [0] = [0] 1182.67/297.12 1182.67/297.12 [s](x1) = [0] 1182.67/297.12 1182.67/297.12 [add](x1, x2) = [1] x1 + [1] 1182.67/297.12 1182.67/297.12 [a__first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.12 1182.67/297.12 [nil] = [7] 1182.67/297.12 1182.67/297.12 [cons](x1, x2) = [0] 1182.67/297.12 1182.67/297.12 [first](x1, x2) = [1] x1 + [1] x2 + [5] 1182.67/297.12 1182.67/297.12 [a__from](x1) = [5] 1182.67/297.12 1182.67/297.12 [from](x1) = [2] 1182.67/297.12 1182.67/297.12 [and](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [if](x1, x2, x3) = [1] x1 + [7] 1182.67/297.12 1182.67/297.12 The order satisfies the following ordering constraints: 1182.67/297.12 1182.67/297.12 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.12 >= [1] X1 + [0] 1182.67/297.12 = [and(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__and(true(), X)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__and(false(), Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(true())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [true()] 1182.67/297.12 1182.67/297.12 [mark(false())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(0())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [0()] 1182.67/297.12 1182.67/297.12 [mark(s(X))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [s(X)] 1182.67/297.12 1182.67/297.12 [mark(add(X1, X2))] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [a__add(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(nil())] = [0] 1182.67/297.12 ? [7] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [mark(cons(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [cons(X1, X2)] 1182.67/297.12 1182.67/297.12 [mark(first(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__first(mark(X1), mark(X2))] 1182.67/297.12 1182.67/297.12 [mark(from(X))] = [0] 1182.67/297.12 ? [5] 1182.67/297.12 = [a__from(X)] 1182.67/297.12 1182.67/297.12 [mark(and(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__and(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(if(X1, X2, X3))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__if(mark(X1), X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.12 ? [1] X1 + [7] 1182.67/297.12 = [if(X1, X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(true(), X, Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__if(false(), X, Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(Y)] 1182.67/297.12 1182.67/297.12 [a__add(X1, X2)] = [1] X1 + [4] 1182.67/297.12 > [1] X1 + [1] 1182.67/297.12 = [add(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__add(0(), X)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__add(s(X), Y)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [s(add(X, Y))] 1182.67/297.12 1182.67/297.12 [a__first(X1, X2)] = [1] X1 + [1] X2 + [0] 1182.67/297.12 ? [1] X1 + [1] X2 + [5] 1182.67/297.12 = [first(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__first(0(), X)] = [1] X + [0] 1182.67/297.12 ? [7] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [a__first(s(X), cons(Y, Z))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [cons(Y, first(X, Z))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [5] 1182.67/297.12 > [0] 1182.67/297.12 = [cons(X, from(s(X)))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [5] 1182.67/297.12 > [2] 1182.67/297.12 = [from(X)] 1182.67/297.12 1182.67/297.12 1182.67/297.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.12 1182.67/297.12 We are left with following problem, upon which TcT provides the 1182.67/297.12 certificate YES(O(1),O(n^1)). 1182.67/297.12 1182.67/297.12 Strict Trs: 1182.67/297.12 { mark(true()) -> true() 1182.67/297.12 , mark(false()) -> false() 1182.67/297.12 , mark(0()) -> 0() 1182.67/297.12 , mark(s(X)) -> s(X) 1182.67/297.12 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.12 , mark(nil()) -> nil() 1182.67/297.12 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.12 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.12 , mark(from(X)) -> a__from(X) 1182.67/297.12 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.12 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.12 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.12 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.12 , a__first(0(), X) -> nil() 1182.67/297.12 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) } 1182.67/297.12 Weak Trs: 1182.67/297.12 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.12 , a__and(true(), X) -> mark(X) 1182.67/297.12 , a__and(false(), Y) -> false() 1182.67/297.12 , a__if(true(), X, Y) -> mark(X) 1182.67/297.12 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.12 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.12 , a__add(0(), X) -> mark(X) 1182.67/297.12 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.12 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.12 , a__from(X) -> from(X) } 1182.67/297.12 Obligation: 1182.67/297.12 runtime complexity 1182.67/297.12 Answer: 1182.67/297.12 YES(O(1),O(n^1)) 1182.67/297.12 1182.67/297.12 The weightgap principle applies (using the following nonconstant 1182.67/297.12 growth matrix-interpretation) 1182.67/297.12 1182.67/297.12 The following argument positions are usable: 1182.67/297.12 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.12 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.12 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.12 1182.67/297.12 TcT has computed the following matrix interpretation satisfying 1182.67/297.12 not(EDA) and not(IDA(1)). 1182.67/297.12 1182.67/297.12 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [true] = [0] 1182.67/297.12 1182.67/297.12 [mark](x1) = [0] 1182.67/297.12 1182.67/297.12 [false] = [0] 1182.67/297.12 1182.67/297.12 [a__if](x1, x2, x3) = [1] x1 + [4] 1182.67/297.12 1182.67/297.12 [a__add](x1, x2) = [1] x1 + [4] 1182.67/297.12 1182.67/297.12 [0] = [0] 1182.67/297.12 1182.67/297.12 [s](x1) = [0] 1182.67/297.12 1182.67/297.12 [add](x1, x2) = [1] x1 + [2] 1182.67/297.12 1182.67/297.12 [a__first](x1, x2) = [1] x1 + [1] x2 + [1] 1182.67/297.12 1182.67/297.12 [nil] = [6] 1182.67/297.12 1182.67/297.12 [cons](x1, x2) = [0] 1182.67/297.12 1182.67/297.12 [first](x1, x2) = [1] x1 + [1] x2 + [5] 1182.67/297.12 1182.67/297.12 [a__from](x1) = [4] 1182.67/297.12 1182.67/297.12 [from](x1) = [2] 1182.67/297.12 1182.67/297.12 [and](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [if](x1, x2, x3) = [1] x1 + [7] 1182.67/297.12 1182.67/297.12 The order satisfies the following ordering constraints: 1182.67/297.12 1182.67/297.12 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.12 >= [1] X1 + [0] 1182.67/297.12 = [and(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__and(true(), X)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__and(false(), Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(true())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [true()] 1182.67/297.12 1182.67/297.12 [mark(false())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(0())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [0()] 1182.67/297.12 1182.67/297.12 [mark(s(X))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [s(X)] 1182.67/297.12 1182.67/297.12 [mark(add(X1, X2))] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [a__add(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(nil())] = [0] 1182.67/297.12 ? [6] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [mark(cons(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [cons(X1, X2)] 1182.67/297.12 1182.67/297.12 [mark(first(X1, X2))] = [0] 1182.67/297.12 ? [1] 1182.67/297.12 = [a__first(mark(X1), mark(X2))] 1182.67/297.12 1182.67/297.12 [mark(from(X))] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [a__from(X)] 1182.67/297.12 1182.67/297.12 [mark(and(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__and(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(if(X1, X2, X3))] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [a__if(mark(X1), X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(X1, X2, X3)] = [1] X1 + [4] 1182.67/297.12 ? [1] X1 + [7] 1182.67/297.12 = [if(X1, X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(true(), X, Y)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__if(false(), X, Y)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(Y)] 1182.67/297.12 1182.67/297.12 [a__add(X1, X2)] = [1] X1 + [4] 1182.67/297.12 > [1] X1 + [2] 1182.67/297.12 = [add(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__add(0(), X)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__add(s(X), Y)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [s(add(X, Y))] 1182.67/297.12 1182.67/297.12 [a__first(X1, X2)] = [1] X1 + [1] X2 + [1] 1182.67/297.12 ? [1] X1 + [1] X2 + [5] 1182.67/297.12 = [first(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__first(0(), X)] = [1] X + [1] 1182.67/297.12 ? [6] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [a__first(s(X), cons(Y, Z))] = [1] 1182.67/297.12 > [0] 1182.67/297.12 = [cons(Y, first(X, Z))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [cons(X, from(s(X)))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [4] 1182.67/297.12 > [2] 1182.67/297.12 = [from(X)] 1182.67/297.12 1182.67/297.12 1182.67/297.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.12 1182.67/297.12 We are left with following problem, upon which TcT provides the 1182.67/297.12 certificate YES(O(1),O(n^1)). 1182.67/297.12 1182.67/297.12 Strict Trs: 1182.67/297.12 { mark(true()) -> true() 1182.67/297.12 , mark(false()) -> false() 1182.67/297.12 , mark(0()) -> 0() 1182.67/297.12 , mark(s(X)) -> s(X) 1182.67/297.12 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.12 , mark(nil()) -> nil() 1182.67/297.12 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.12 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.12 , mark(from(X)) -> a__from(X) 1182.67/297.12 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.12 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.12 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.12 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.12 , a__first(0(), X) -> nil() } 1182.67/297.12 Weak Trs: 1182.67/297.12 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.12 , a__and(true(), X) -> mark(X) 1182.67/297.12 , a__and(false(), Y) -> false() 1182.67/297.12 , a__if(true(), X, Y) -> mark(X) 1182.67/297.12 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.12 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.12 , a__add(0(), X) -> mark(X) 1182.67/297.12 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.12 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.12 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.12 , a__from(X) -> from(X) } 1182.67/297.12 Obligation: 1182.67/297.12 runtime complexity 1182.67/297.12 Answer: 1182.67/297.12 YES(O(1),O(n^1)) 1182.67/297.12 1182.67/297.12 The weightgap principle applies (using the following nonconstant 1182.67/297.12 growth matrix-interpretation) 1182.67/297.12 1182.67/297.12 The following argument positions are usable: 1182.67/297.12 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.12 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.12 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.12 1182.67/297.12 TcT has computed the following matrix interpretation satisfying 1182.67/297.12 not(EDA) and not(IDA(1)). 1182.67/297.12 1182.67/297.12 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [true] = [0] 1182.67/297.12 1182.67/297.12 [mark](x1) = [0] 1182.67/297.12 1182.67/297.12 [false] = [0] 1182.67/297.12 1182.67/297.12 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [0] = [7] 1182.67/297.12 1182.67/297.12 [s](x1) = [0] 1182.67/297.12 1182.67/297.12 [add](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [a__first](x1, x2) = [1] x1 + [1] x2 + [1] 1182.67/297.12 1182.67/297.12 [nil] = [7] 1182.67/297.12 1182.67/297.12 [cons](x1, x2) = [0] 1182.67/297.12 1182.67/297.12 [first](x1, x2) = [1] x1 + [1] x2 + [5] 1182.67/297.12 1182.67/297.12 [a__from](x1) = [4] 1182.67/297.12 1182.67/297.12 [from](x1) = [1] 1182.67/297.12 1182.67/297.12 [and](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [if](x1, x2, x3) = [1] x1 + [7] 1182.67/297.12 1182.67/297.12 The order satisfies the following ordering constraints: 1182.67/297.12 1182.67/297.12 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.12 >= [1] X1 + [0] 1182.67/297.12 = [and(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__and(true(), X)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__and(false(), Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(true())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [true()] 1182.67/297.12 1182.67/297.12 [mark(false())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(0())] = [0] 1182.67/297.12 ? [7] 1182.67/297.12 = [0()] 1182.67/297.12 1182.67/297.12 [mark(s(X))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [s(X)] 1182.67/297.12 1182.67/297.12 [mark(add(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__add(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(nil())] = [0] 1182.67/297.12 ? [7] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [mark(cons(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [cons(X1, X2)] 1182.67/297.12 1182.67/297.12 [mark(first(X1, X2))] = [0] 1182.67/297.12 ? [1] 1182.67/297.12 = [a__first(mark(X1), mark(X2))] 1182.67/297.12 1182.67/297.12 [mark(from(X))] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [a__from(X)] 1182.67/297.12 1182.67/297.12 [mark(and(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__and(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(if(X1, X2, X3))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__if(mark(X1), X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.12 ? [1] X1 + [7] 1182.67/297.12 = [if(X1, X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(true(), X, Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__if(false(), X, Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(Y)] 1182.67/297.12 1182.67/297.12 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.12 >= [1] X1 + [0] 1182.67/297.12 = [add(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__add(0(), X)] = [7] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__add(s(X), Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [s(add(X, Y))] 1182.67/297.12 1182.67/297.12 [a__first(X1, X2)] = [1] X1 + [1] X2 + [1] 1182.67/297.12 ? [1] X1 + [1] X2 + [5] 1182.67/297.12 = [first(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__first(0(), X)] = [1] X + [8] 1182.67/297.12 > [7] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [a__first(s(X), cons(Y, Z))] = [1] 1182.67/297.12 > [0] 1182.67/297.12 = [cons(Y, first(X, Z))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [cons(X, from(s(X)))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [4] 1182.67/297.12 > [1] 1182.67/297.12 = [from(X)] 1182.67/297.12 1182.67/297.12 1182.67/297.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.12 1182.67/297.12 We are left with following problem, upon which TcT provides the 1182.67/297.12 certificate YES(O(1),O(n^1)). 1182.67/297.12 1182.67/297.12 Strict Trs: 1182.67/297.12 { mark(true()) -> true() 1182.67/297.12 , mark(false()) -> false() 1182.67/297.12 , mark(0()) -> 0() 1182.67/297.12 , mark(s(X)) -> s(X) 1182.67/297.12 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.12 , mark(nil()) -> nil() 1182.67/297.12 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.12 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.12 , mark(from(X)) -> a__from(X) 1182.67/297.12 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.12 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.12 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.12 , a__first(X1, X2) -> first(X1, X2) } 1182.67/297.12 Weak Trs: 1182.67/297.12 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.12 , a__and(true(), X) -> mark(X) 1182.67/297.12 , a__and(false(), Y) -> false() 1182.67/297.12 , a__if(true(), X, Y) -> mark(X) 1182.67/297.12 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.12 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.12 , a__add(0(), X) -> mark(X) 1182.67/297.12 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.12 , a__first(0(), X) -> nil() 1182.67/297.12 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.12 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.12 , a__from(X) -> from(X) } 1182.67/297.12 Obligation: 1182.67/297.12 runtime complexity 1182.67/297.12 Answer: 1182.67/297.12 YES(O(1),O(n^1)) 1182.67/297.12 1182.67/297.12 The weightgap principle applies (using the following nonconstant 1182.67/297.12 growth matrix-interpretation) 1182.67/297.12 1182.67/297.12 The following argument positions are usable: 1182.67/297.12 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.12 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.12 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.12 1182.67/297.12 TcT has computed the following matrix interpretation satisfying 1182.67/297.12 not(EDA) and not(IDA(1)). 1182.67/297.12 1182.67/297.12 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [true] = [4] 1182.67/297.12 1182.67/297.12 [mark](x1) = [0] 1182.67/297.12 1182.67/297.12 [false] = [0] 1182.67/297.12 1182.67/297.12 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [0] = [0] 1182.67/297.12 1182.67/297.12 [s](x1) = [0] 1182.67/297.12 1182.67/297.12 [add](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [a__first](x1, x2) = [1] x1 + [1] x2 + [4] 1182.67/297.12 1182.67/297.12 [nil] = [3] 1182.67/297.12 1182.67/297.12 [cons](x1, x2) = [4] 1182.67/297.12 1182.67/297.12 [first](x1, x2) = [1] x1 + [1] x2 + [1] 1182.67/297.12 1182.67/297.12 [a__from](x1) = [7] 1182.67/297.12 1182.67/297.12 [from](x1) = [1] 1182.67/297.12 1182.67/297.12 [and](x1, x2) = [1] x1 + [0] 1182.67/297.12 1182.67/297.12 [if](x1, x2, x3) = [1] x1 + [7] 1182.67/297.12 1182.67/297.12 The order satisfies the following ordering constraints: 1182.67/297.12 1182.67/297.12 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.12 >= [1] X1 + [0] 1182.67/297.12 = [and(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__and(true(), X)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__and(false(), Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(true())] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [true()] 1182.67/297.12 1182.67/297.12 [mark(false())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [false()] 1182.67/297.12 1182.67/297.12 [mark(0())] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [0()] 1182.67/297.12 1182.67/297.12 [mark(s(X))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [s(X)] 1182.67/297.12 1182.67/297.12 [mark(add(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__add(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(nil())] = [0] 1182.67/297.12 ? [3] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [mark(cons(X1, X2))] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [cons(X1, X2)] 1182.67/297.12 1182.67/297.12 [mark(first(X1, X2))] = [0] 1182.67/297.12 ? [4] 1182.67/297.12 = [a__first(mark(X1), mark(X2))] 1182.67/297.12 1182.67/297.12 [mark(from(X))] = [0] 1182.67/297.12 ? [7] 1182.67/297.12 = [a__from(X)] 1182.67/297.12 1182.67/297.12 [mark(and(X1, X2))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__and(mark(X1), X2)] 1182.67/297.12 1182.67/297.12 [mark(if(X1, X2, X3))] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [a__if(mark(X1), X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.12 ? [1] X1 + [7] 1182.67/297.12 = [if(X1, X2, X3)] 1182.67/297.12 1182.67/297.12 [a__if(true(), X, Y)] = [4] 1182.67/297.12 > [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__if(false(), X, Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(Y)] 1182.67/297.12 1182.67/297.12 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.12 >= [1] X1 + [0] 1182.67/297.12 = [add(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__add(0(), X)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [mark(X)] 1182.67/297.12 1182.67/297.12 [a__add(s(X), Y)] = [0] 1182.67/297.12 >= [0] 1182.67/297.12 = [s(add(X, Y))] 1182.67/297.12 1182.67/297.12 [a__first(X1, X2)] = [1] X1 + [1] X2 + [4] 1182.67/297.12 > [1] X1 + [1] X2 + [1] 1182.67/297.12 = [first(X1, X2)] 1182.67/297.12 1182.67/297.12 [a__first(0(), X)] = [1] X + [4] 1182.67/297.12 > [3] 1182.67/297.12 = [nil()] 1182.67/297.12 1182.67/297.12 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.12 > [4] 1182.67/297.12 = [cons(Y, first(X, Z))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [7] 1182.67/297.12 > [4] 1182.67/297.12 = [cons(X, from(s(X)))] 1182.67/297.12 1182.67/297.12 [a__from(X)] = [7] 1182.67/297.12 > [1] 1182.67/297.12 = [from(X)] 1182.67/297.12 1182.67/297.12 1182.67/297.12 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.12 1182.67/297.12 We are left with following problem, upon which TcT provides the 1182.67/297.12 certificate YES(O(1),O(n^1)). 1182.67/297.12 1182.67/297.12 Strict Trs: 1182.67/297.12 { mark(true()) -> true() 1182.67/297.12 , mark(false()) -> false() 1182.67/297.12 , mark(0()) -> 0() 1182.67/297.12 , mark(s(X)) -> s(X) 1182.67/297.12 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.12 , mark(nil()) -> nil() 1182.67/297.12 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.12 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.12 , mark(from(X)) -> a__from(X) 1182.67/297.12 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.12 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.12 , a__if(X1, X2, X3) -> if(X1, X2, X3) } 1182.67/297.12 Weak Trs: 1182.67/297.12 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.12 , a__and(true(), X) -> mark(X) 1182.67/297.12 , a__and(false(), Y) -> false() 1182.67/297.12 , a__if(true(), X, Y) -> mark(X) 1182.67/297.12 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.12 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.12 , a__add(0(), X) -> mark(X) 1182.67/297.12 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.12 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.12 , a__first(0(), X) -> nil() 1182.67/297.12 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.12 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.12 , a__from(X) -> from(X) } 1182.67/297.12 Obligation: 1182.67/297.12 runtime complexity 1182.67/297.12 Answer: 1182.67/297.12 YES(O(1),O(n^1)) 1182.67/297.12 1182.67/297.12 The weightgap principle applies (using the following nonconstant 1182.67/297.12 growth matrix-interpretation) 1182.67/297.12 1182.67/297.12 The following argument positions are usable: 1182.67/297.12 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.12 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.12 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.12 1182.67/297.12 TcT has computed the following matrix interpretation satisfying 1182.67/297.12 not(EDA) and not(IDA(1)). 1182.67/297.12 1182.67/297.12 [a__and](x1, x2) = [1] x1 + [4] 1182.67/297.12 1182.67/297.12 [true] = [4] 1182.67/297.12 1182.67/297.12 [mark](x1) = [0] 1182.67/297.12 1182.67/297.12 [false] = [4] 1182.67/297.12 1182.67/297.12 [a__if](x1, x2, x3) = [1] x1 + [1] 1182.67/297.12 1182.67/297.12 [a__add](x1, x2) = [1] x1 + [4] 1182.67/297.12 1182.67/297.12 [0] = [0] 1182.67/297.12 1182.67/297.12 [s](x1) = [4] 1182.67/297.12 1182.67/297.13 [add](x1, x2) = [1] x1 + [2] 1182.67/297.13 1182.67/297.13 [a__first](x1, x2) = [1] x1 + [1] x2 + [4] 1182.67/297.13 1182.67/297.13 [nil] = [3] 1182.67/297.13 1182.67/297.13 [cons](x1, x2) = [0] 1182.67/297.13 1182.67/297.13 [first](x1, x2) = [1] x1 + [1] x2 + [1] 1182.67/297.13 1182.67/297.13 [a__from](x1) = [4] 1182.67/297.13 1182.67/297.13 [from](x1) = [2] 1182.67/297.13 1182.67/297.13 [and](x1, x2) = [1] x1 + [3] 1182.67/297.13 1182.67/297.13 [if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 The order satisfies the following ordering constraints: 1182.67/297.13 1182.67/297.13 [a__and(X1, X2)] = [1] X1 + [4] 1182.67/297.13 > [1] X1 + [3] 1182.67/297.13 = [and(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__and(true(), X)] = [8] 1182.67/297.13 > [0] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__and(false(), Y)] = [8] 1182.67/297.13 > [4] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(true())] = [0] 1182.67/297.13 ? [4] 1182.67/297.13 = [true()] 1182.67/297.13 1182.67/297.13 [mark(false())] = [0] 1182.67/297.13 ? [4] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(0())] = [0] 1182.67/297.13 >= [0] 1182.67/297.13 = [0()] 1182.67/297.13 1182.67/297.13 [mark(s(X))] = [0] 1182.67/297.13 ? [4] 1182.67/297.13 = [s(X)] 1182.67/297.13 1182.67/297.13 [mark(add(X1, X2))] = [0] 1182.67/297.13 ? [4] 1182.67/297.13 = [a__add(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(nil())] = [0] 1182.67/297.13 ? [3] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [mark(cons(X1, X2))] = [0] 1182.67/297.13 >= [0] 1182.67/297.13 = [cons(X1, X2)] 1182.67/297.13 1182.67/297.13 [mark(first(X1, X2))] = [0] 1182.67/297.13 ? [4] 1182.67/297.13 = [a__first(mark(X1), mark(X2))] 1182.67/297.13 1182.67/297.13 [mark(from(X))] = [0] 1182.67/297.13 ? [4] 1182.67/297.13 = [a__from(X)] 1182.67/297.13 1182.67/297.13 [mark(and(X1, X2))] = [0] 1182.67/297.13 ? [4] 1182.67/297.13 = [a__and(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(if(X1, X2, X3))] = [0] 1182.67/297.13 ? [1] 1182.67/297.13 = [a__if(mark(X1), X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(X1, X2, X3)] = [1] X1 + [1] 1182.67/297.13 > [1] X1 + [0] 1182.67/297.13 = [if(X1, X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(true(), X, Y)] = [5] 1182.67/297.13 > [0] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__if(false(), X, Y)] = [5] 1182.67/297.13 > [0] 1182.67/297.13 = [mark(Y)] 1182.67/297.13 1182.67/297.13 [a__add(X1, X2)] = [1] X1 + [4] 1182.67/297.13 > [1] X1 + [2] 1182.67/297.13 = [add(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__add(0(), X)] = [4] 1182.67/297.13 > [0] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__add(s(X), Y)] = [8] 1182.67/297.13 > [4] 1182.67/297.13 = [s(add(X, Y))] 1182.67/297.13 1182.67/297.13 [a__first(X1, X2)] = [1] X1 + [1] X2 + [4] 1182.67/297.13 > [1] X1 + [1] X2 + [1] 1182.67/297.13 = [first(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__first(0(), X)] = [1] X + [4] 1182.67/297.13 > [3] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.13 > [0] 1182.67/297.13 = [cons(Y, first(X, Z))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [4] 1182.67/297.13 > [0] 1182.67/297.13 = [cons(X, from(s(X)))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [4] 1182.67/297.13 > [2] 1182.67/297.13 = [from(X)] 1182.67/297.13 1182.67/297.13 1182.67/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.13 1182.67/297.13 We are left with following problem, upon which TcT provides the 1182.67/297.13 certificate YES(O(1),O(n^1)). 1182.67/297.13 1182.67/297.13 Strict Trs: 1182.67/297.13 { mark(true()) -> true() 1182.67/297.13 , mark(false()) -> false() 1182.67/297.13 , mark(0()) -> 0() 1182.67/297.13 , mark(s(X)) -> s(X) 1182.67/297.13 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.13 , mark(nil()) -> nil() 1182.67/297.13 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.13 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.13 , mark(from(X)) -> a__from(X) 1182.67/297.13 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.13 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.13 Weak Trs: 1182.67/297.13 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.13 , a__and(true(), X) -> mark(X) 1182.67/297.13 , a__and(false(), Y) -> false() 1182.67/297.13 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.13 , a__if(true(), X, Y) -> mark(X) 1182.67/297.13 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.13 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.13 , a__add(0(), X) -> mark(X) 1182.67/297.13 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.13 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.13 , a__first(0(), X) -> nil() 1182.67/297.13 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.13 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.13 , a__from(X) -> from(X) } 1182.67/297.13 Obligation: 1182.67/297.13 runtime complexity 1182.67/297.13 Answer: 1182.67/297.13 YES(O(1),O(n^1)) 1182.67/297.13 1182.67/297.13 The weightgap principle applies (using the following nonconstant 1182.67/297.13 growth matrix-interpretation) 1182.67/297.13 1182.67/297.13 The following argument positions are usable: 1182.67/297.13 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.13 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.13 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.13 1182.67/297.13 TcT has computed the following matrix interpretation satisfying 1182.67/297.13 not(EDA) and not(IDA(1)). 1182.67/297.13 1182.67/297.13 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [true] = [4] 1182.67/297.13 1182.67/297.13 [mark](x1) = [1] 1182.67/297.13 1182.67/297.13 [false] = [4] 1182.67/297.13 1182.67/297.13 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [a__add](x1, x2) = [1] x1 + [7] 1182.67/297.13 1182.67/297.13 [0] = [2] 1182.67/297.13 1182.67/297.13 [s](x1) = [1] 1182.67/297.13 1182.67/297.13 [add](x1, x2) = [1] x1 + [1] 1182.67/297.13 1182.67/297.13 [a__first](x1, x2) = [1] x1 + [1] x2 + [6] 1182.67/297.13 1182.67/297.13 [nil] = [0] 1182.67/297.13 1182.67/297.13 [cons](x1, x2) = [1] 1182.67/297.13 1182.67/297.13 [first](x1, x2) = [1] x1 + [1] x2 + [2] 1182.67/297.13 1182.67/297.13 [a__from](x1) = [7] 1182.67/297.13 1182.67/297.13 [from](x1) = [1] 1182.67/297.13 1182.67/297.13 [and](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 The order satisfies the following ordering constraints: 1182.67/297.13 1182.67/297.13 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [and(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__and(true(), X)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__and(false(), Y)] = [4] 1182.67/297.13 >= [4] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(true())] = [1] 1182.67/297.13 ? [4] 1182.67/297.13 = [true()] 1182.67/297.13 1182.67/297.13 [mark(false())] = [1] 1182.67/297.13 ? [4] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(0())] = [1] 1182.67/297.13 ? [2] 1182.67/297.13 = [0()] 1182.67/297.13 1182.67/297.13 [mark(s(X))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [s(X)] 1182.67/297.13 1182.67/297.13 [mark(add(X1, X2))] = [1] 1182.67/297.13 ? [8] 1182.67/297.13 = [a__add(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(nil())] = [1] 1182.67/297.13 > [0] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [mark(cons(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [cons(X1, X2)] 1182.67/297.13 1182.67/297.13 [mark(first(X1, X2))] = [1] 1182.67/297.13 ? [8] 1182.67/297.13 = [a__first(mark(X1), mark(X2))] 1182.67/297.13 1182.67/297.13 [mark(from(X))] = [1] 1182.67/297.13 ? [7] 1182.67/297.13 = [a__from(X)] 1182.67/297.13 1182.67/297.13 [mark(and(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__and(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(if(X1, X2, X3))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__if(mark(X1), X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [if(X1, X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(true(), X, Y)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__if(false(), X, Y)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(Y)] 1182.67/297.13 1182.67/297.13 [a__add(X1, X2)] = [1] X1 + [7] 1182.67/297.13 > [1] X1 + [1] 1182.67/297.13 = [add(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__add(0(), X)] = [9] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__add(s(X), Y)] = [8] 1182.67/297.13 > [1] 1182.67/297.13 = [s(add(X, Y))] 1182.67/297.13 1182.67/297.13 [a__first(X1, X2)] = [1] X1 + [1] X2 + [6] 1182.67/297.13 > [1] X1 + [1] X2 + [2] 1182.67/297.13 = [first(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__first(0(), X)] = [1] X + [8] 1182.67/297.13 > [0] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.13 > [1] 1182.67/297.13 = [cons(Y, first(X, Z))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [7] 1182.67/297.13 > [1] 1182.67/297.13 = [cons(X, from(s(X)))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [7] 1182.67/297.13 > [1] 1182.67/297.13 = [from(X)] 1182.67/297.13 1182.67/297.13 1182.67/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.13 1182.67/297.13 We are left with following problem, upon which TcT provides the 1182.67/297.13 certificate YES(O(1),O(n^1)). 1182.67/297.13 1182.67/297.13 Strict Trs: 1182.67/297.13 { mark(true()) -> true() 1182.67/297.13 , mark(false()) -> false() 1182.67/297.13 , mark(0()) -> 0() 1182.67/297.13 , mark(s(X)) -> s(X) 1182.67/297.13 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.13 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.13 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.13 , mark(from(X)) -> a__from(X) 1182.67/297.13 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.13 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.13 Weak Trs: 1182.67/297.13 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.13 , a__and(true(), X) -> mark(X) 1182.67/297.13 , a__and(false(), Y) -> false() 1182.67/297.13 , mark(nil()) -> nil() 1182.67/297.13 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.13 , a__if(true(), X, Y) -> mark(X) 1182.67/297.13 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.13 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.13 , a__add(0(), X) -> mark(X) 1182.67/297.13 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.13 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.13 , a__first(0(), X) -> nil() 1182.67/297.13 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.13 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.13 , a__from(X) -> from(X) } 1182.67/297.13 Obligation: 1182.67/297.13 runtime complexity 1182.67/297.13 Answer: 1182.67/297.13 YES(O(1),O(n^1)) 1182.67/297.13 1182.67/297.13 The weightgap principle applies (using the following nonconstant 1182.67/297.13 growth matrix-interpretation) 1182.67/297.13 1182.67/297.13 The following argument positions are usable: 1182.67/297.13 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.13 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.13 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.13 1182.67/297.13 TcT has computed the following matrix interpretation satisfying 1182.67/297.13 not(EDA) and not(IDA(1)). 1182.67/297.13 1182.67/297.13 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [true] = [4] 1182.67/297.13 1182.67/297.13 [mark](x1) = [1] 1182.67/297.13 1182.67/297.13 [false] = [1] 1182.67/297.13 1182.67/297.13 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [0] = [4] 1182.67/297.13 1182.67/297.13 [s](x1) = [0] 1182.67/297.13 1182.67/297.13 [add](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [a__first](x1, x2) = [1] x1 + [1] x2 + [7] 1182.67/297.13 1182.67/297.13 [nil] = [1] 1182.67/297.13 1182.67/297.13 [cons](x1, x2) = [1] 1182.67/297.13 1182.67/297.13 [first](x1, x2) = [1] x1 + [1] x2 + [2] 1182.67/297.13 1182.67/297.13 [a__from](x1) = [7] 1182.67/297.13 1182.67/297.13 [from](x1) = [1] 1182.67/297.13 1182.67/297.13 [and](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 The order satisfies the following ordering constraints: 1182.67/297.13 1182.67/297.13 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [and(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__and(true(), X)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__and(false(), Y)] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(true())] = [1] 1182.67/297.13 ? [4] 1182.67/297.13 = [true()] 1182.67/297.13 1182.67/297.13 [mark(false())] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(0())] = [1] 1182.67/297.13 ? [4] 1182.67/297.13 = [0()] 1182.67/297.13 1182.67/297.13 [mark(s(X))] = [1] 1182.67/297.13 > [0] 1182.67/297.13 = [s(X)] 1182.67/297.13 1182.67/297.13 [mark(add(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__add(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(nil())] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [mark(cons(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [cons(X1, X2)] 1182.67/297.13 1182.67/297.13 [mark(first(X1, X2))] = [1] 1182.67/297.13 ? [9] 1182.67/297.13 = [a__first(mark(X1), mark(X2))] 1182.67/297.13 1182.67/297.13 [mark(from(X))] = [1] 1182.67/297.13 ? [7] 1182.67/297.13 = [a__from(X)] 1182.67/297.13 1182.67/297.13 [mark(and(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__and(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(if(X1, X2, X3))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__if(mark(X1), X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [if(X1, X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(true(), X, Y)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__if(false(), X, Y)] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [mark(Y)] 1182.67/297.13 1182.67/297.13 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [add(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__add(0(), X)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__add(s(X), Y)] = [0] 1182.67/297.13 >= [0] 1182.67/297.13 = [s(add(X, Y))] 1182.67/297.13 1182.67/297.13 [a__first(X1, X2)] = [1] X1 + [1] X2 + [7] 1182.67/297.13 > [1] X1 + [1] X2 + [2] 1182.67/297.13 = [first(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__first(0(), X)] = [1] X + [11] 1182.67/297.13 > [1] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.13 > [1] 1182.67/297.13 = [cons(Y, first(X, Z))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [7] 1182.67/297.13 > [1] 1182.67/297.13 = [cons(X, from(s(X)))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [7] 1182.67/297.13 > [1] 1182.67/297.13 = [from(X)] 1182.67/297.13 1182.67/297.13 1182.67/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.13 1182.67/297.13 We are left with following problem, upon which TcT provides the 1182.67/297.13 certificate YES(O(1),O(n^1)). 1182.67/297.13 1182.67/297.13 Strict Trs: 1182.67/297.13 { mark(true()) -> true() 1182.67/297.13 , mark(false()) -> false() 1182.67/297.13 , mark(0()) -> 0() 1182.67/297.13 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.13 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.13 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.13 , mark(from(X)) -> a__from(X) 1182.67/297.13 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.13 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.13 Weak Trs: 1182.67/297.13 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.13 , a__and(true(), X) -> mark(X) 1182.67/297.13 , a__and(false(), Y) -> false() 1182.67/297.13 , mark(s(X)) -> s(X) 1182.67/297.13 , mark(nil()) -> nil() 1182.67/297.13 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.13 , a__if(true(), X, Y) -> mark(X) 1182.67/297.13 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.13 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.13 , a__add(0(), X) -> mark(X) 1182.67/297.13 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.13 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.13 , a__first(0(), X) -> nil() 1182.67/297.13 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.13 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.13 , a__from(X) -> from(X) } 1182.67/297.13 Obligation: 1182.67/297.13 runtime complexity 1182.67/297.13 Answer: 1182.67/297.13 YES(O(1),O(n^1)) 1182.67/297.13 1182.67/297.13 The weightgap principle applies (using the following nonconstant 1182.67/297.13 growth matrix-interpretation) 1182.67/297.13 1182.67/297.13 The following argument positions are usable: 1182.67/297.13 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.13 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.13 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.13 1182.67/297.13 TcT has computed the following matrix interpretation satisfying 1182.67/297.13 not(EDA) and not(IDA(1)). 1182.67/297.13 1182.67/297.13 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [true] = [4] 1182.67/297.13 1182.67/297.13 [mark](x1) = [1] 1182.67/297.13 1182.67/297.13 [false] = [4] 1182.67/297.13 1182.67/297.13 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [0] = [4] 1182.67/297.13 1182.67/297.13 [s](x1) = [1] 1182.67/297.13 1182.67/297.13 [add](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [a__first](x1, x2) = [1] x1 + [1] x2 + [7] 1182.67/297.13 1182.67/297.13 [nil] = [1] 1182.67/297.13 1182.67/297.13 [cons](x1, x2) = [0] 1182.67/297.13 1182.67/297.13 [first](x1, x2) = [1] x1 + [1] x2 + [2] 1182.67/297.13 1182.67/297.13 [a__from](x1) = [5] 1182.67/297.13 1182.67/297.13 [from](x1) = [2] 1182.67/297.13 1182.67/297.13 [and](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 The order satisfies the following ordering constraints: 1182.67/297.13 1182.67/297.13 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [and(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__and(true(), X)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__and(false(), Y)] = [4] 1182.67/297.13 >= [4] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(true())] = [1] 1182.67/297.13 ? [4] 1182.67/297.13 = [true()] 1182.67/297.13 1182.67/297.13 [mark(false())] = [1] 1182.67/297.13 ? [4] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(0())] = [1] 1182.67/297.13 ? [4] 1182.67/297.13 = [0()] 1182.67/297.13 1182.67/297.13 [mark(s(X))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [s(X)] 1182.67/297.13 1182.67/297.13 [mark(add(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__add(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(nil())] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [mark(cons(X1, X2))] = [1] 1182.67/297.13 > [0] 1182.67/297.13 = [cons(X1, X2)] 1182.67/297.13 1182.67/297.13 [mark(first(X1, X2))] = [1] 1182.67/297.13 ? [9] 1182.67/297.13 = [a__first(mark(X1), mark(X2))] 1182.67/297.13 1182.67/297.13 [mark(from(X))] = [1] 1182.67/297.13 ? [5] 1182.67/297.13 = [a__from(X)] 1182.67/297.13 1182.67/297.13 [mark(and(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__and(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(if(X1, X2, X3))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__if(mark(X1), X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [if(X1, X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(true(), X, Y)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__if(false(), X, Y)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(Y)] 1182.67/297.13 1182.67/297.13 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [add(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__add(0(), X)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__add(s(X), Y)] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [s(add(X, Y))] 1182.67/297.13 1182.67/297.13 [a__first(X1, X2)] = [1] X1 + [1] X2 + [7] 1182.67/297.13 > [1] X1 + [1] X2 + [2] 1182.67/297.13 = [first(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__first(0(), X)] = [1] X + [11] 1182.67/297.13 > [1] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.13 > [0] 1182.67/297.13 = [cons(Y, first(X, Z))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [5] 1182.67/297.13 > [0] 1182.67/297.13 = [cons(X, from(s(X)))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [5] 1182.67/297.13 > [2] 1182.67/297.13 = [from(X)] 1182.67/297.13 1182.67/297.13 1182.67/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.13 1182.67/297.13 We are left with following problem, upon which TcT provides the 1182.67/297.13 certificate YES(O(1),O(n^1)). 1182.67/297.13 1182.67/297.13 Strict Trs: 1182.67/297.13 { mark(true()) -> true() 1182.67/297.13 , mark(false()) -> false() 1182.67/297.13 , mark(0()) -> 0() 1182.67/297.13 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.13 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.13 , mark(from(X)) -> a__from(X) 1182.67/297.13 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.13 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.13 Weak Trs: 1182.67/297.13 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.13 , a__and(true(), X) -> mark(X) 1182.67/297.13 , a__and(false(), Y) -> false() 1182.67/297.13 , mark(s(X)) -> s(X) 1182.67/297.13 , mark(nil()) -> nil() 1182.67/297.13 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.13 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.13 , a__if(true(), X, Y) -> mark(X) 1182.67/297.13 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.13 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.13 , a__add(0(), X) -> mark(X) 1182.67/297.13 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.13 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.13 , a__first(0(), X) -> nil() 1182.67/297.13 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.13 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.13 , a__from(X) -> from(X) } 1182.67/297.13 Obligation: 1182.67/297.13 runtime complexity 1182.67/297.13 Answer: 1182.67/297.13 YES(O(1),O(n^1)) 1182.67/297.13 1182.67/297.13 The weightgap principle applies (using the following nonconstant 1182.67/297.13 growth matrix-interpretation) 1182.67/297.13 1182.67/297.13 The following argument positions are usable: 1182.67/297.13 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.13 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.13 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.13 1182.67/297.13 TcT has computed the following matrix interpretation satisfying 1182.67/297.13 not(EDA) and not(IDA(1)). 1182.67/297.13 1182.67/297.13 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [true] = [4] 1182.67/297.13 1182.67/297.13 [mark](x1) = [1] 1182.67/297.13 1182.67/297.13 [false] = [0] 1182.67/297.13 1182.67/297.13 [a__if](x1, x2, x3) = [1] x1 + [4] 1182.67/297.13 1182.67/297.13 [a__add](x1, x2) = [1] x1 + [4] 1182.67/297.13 1182.67/297.13 [0] = [0] 1182.67/297.13 1182.67/297.13 [s](x1) = [1] 1182.67/297.13 1182.67/297.13 [add](x1, x2) = [1] x1 + [2] 1182.67/297.13 1182.67/297.13 [a__first](x1, x2) = [1] x1 + [1] x2 + [6] 1182.67/297.13 1182.67/297.13 [nil] = [1] 1182.67/297.13 1182.67/297.13 [cons](x1, x2) = [1] 1182.67/297.13 1182.67/297.13 [first](x1, x2) = [1] x1 + [1] x2 + [1] 1182.67/297.13 1182.67/297.13 [a__from](x1) = [3] 1182.67/297.13 1182.67/297.13 [from](x1) = [1] 1182.67/297.13 1182.67/297.13 [and](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [if](x1, x2, x3) = [1] x1 + [3] 1182.67/297.13 1182.67/297.13 The order satisfies the following ordering constraints: 1182.67/297.13 1182.67/297.13 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.13 >= [1] X1 + [0] 1182.67/297.13 = [and(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__and(true(), X)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__and(false(), Y)] = [0] 1182.67/297.13 >= [0] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(true())] = [1] 1182.67/297.13 ? [4] 1182.67/297.13 = [true()] 1182.67/297.13 1182.67/297.13 [mark(false())] = [1] 1182.67/297.13 > [0] 1182.67/297.13 = [false()] 1182.67/297.13 1182.67/297.13 [mark(0())] = [1] 1182.67/297.13 > [0] 1182.67/297.13 = [0()] 1182.67/297.13 1182.67/297.13 [mark(s(X))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [s(X)] 1182.67/297.13 1182.67/297.13 [mark(add(X1, X2))] = [1] 1182.67/297.13 ? [5] 1182.67/297.13 = [a__add(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(nil())] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [mark(cons(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [cons(X1, X2)] 1182.67/297.13 1182.67/297.13 [mark(first(X1, X2))] = [1] 1182.67/297.13 ? [8] 1182.67/297.13 = [a__first(mark(X1), mark(X2))] 1182.67/297.13 1182.67/297.13 [mark(from(X))] = [1] 1182.67/297.13 ? [3] 1182.67/297.13 = [a__from(X)] 1182.67/297.13 1182.67/297.13 [mark(and(X1, X2))] = [1] 1182.67/297.13 >= [1] 1182.67/297.13 = [a__and(mark(X1), X2)] 1182.67/297.13 1182.67/297.13 [mark(if(X1, X2, X3))] = [1] 1182.67/297.13 ? [5] 1182.67/297.13 = [a__if(mark(X1), X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(X1, X2, X3)] = [1] X1 + [4] 1182.67/297.13 > [1] X1 + [3] 1182.67/297.13 = [if(X1, X2, X3)] 1182.67/297.13 1182.67/297.13 [a__if(true(), X, Y)] = [8] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__if(false(), X, Y)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(Y)] 1182.67/297.13 1182.67/297.13 [a__add(X1, X2)] = [1] X1 + [4] 1182.67/297.13 > [1] X1 + [2] 1182.67/297.13 = [add(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__add(0(), X)] = [4] 1182.67/297.13 > [1] 1182.67/297.13 = [mark(X)] 1182.67/297.13 1182.67/297.13 [a__add(s(X), Y)] = [5] 1182.67/297.13 > [1] 1182.67/297.13 = [s(add(X, Y))] 1182.67/297.13 1182.67/297.13 [a__first(X1, X2)] = [1] X1 + [1] X2 + [6] 1182.67/297.13 > [1] X1 + [1] X2 + [1] 1182.67/297.13 = [first(X1, X2)] 1182.67/297.13 1182.67/297.13 [a__first(0(), X)] = [1] X + [6] 1182.67/297.13 > [1] 1182.67/297.13 = [nil()] 1182.67/297.13 1182.67/297.13 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.13 > [1] 1182.67/297.13 = [cons(Y, first(X, Z))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [3] 1182.67/297.13 > [1] 1182.67/297.13 = [cons(X, from(s(X)))] 1182.67/297.13 1182.67/297.13 [a__from(X)] = [3] 1182.67/297.13 > [1] 1182.67/297.13 = [from(X)] 1182.67/297.13 1182.67/297.13 1182.67/297.13 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.13 1182.67/297.13 We are left with following problem, upon which TcT provides the 1182.67/297.13 certificate YES(O(1),O(n^1)). 1182.67/297.13 1182.67/297.13 Strict Trs: 1182.67/297.13 { mark(true()) -> true() 1182.67/297.13 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.13 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.13 , mark(from(X)) -> a__from(X) 1182.67/297.13 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.13 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.13 Weak Trs: 1182.67/297.13 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.13 , a__and(true(), X) -> mark(X) 1182.67/297.13 , a__and(false(), Y) -> false() 1182.67/297.13 , mark(false()) -> false() 1182.67/297.13 , mark(0()) -> 0() 1182.67/297.13 , mark(s(X)) -> s(X) 1182.67/297.13 , mark(nil()) -> nil() 1182.67/297.13 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.13 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.13 , a__if(true(), X, Y) -> mark(X) 1182.67/297.13 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.13 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.13 , a__add(0(), X) -> mark(X) 1182.67/297.13 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.13 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.13 , a__first(0(), X) -> nil() 1182.67/297.13 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.13 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.13 , a__from(X) -> from(X) } 1182.67/297.13 Obligation: 1182.67/297.13 runtime complexity 1182.67/297.13 Answer: 1182.67/297.13 YES(O(1),O(n^1)) 1182.67/297.13 1182.67/297.13 The weightgap principle applies (using the following nonconstant 1182.67/297.13 growth matrix-interpretation) 1182.67/297.13 1182.67/297.13 The following argument positions are usable: 1182.67/297.13 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.13 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.13 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.13 1182.67/297.13 TcT has computed the following matrix interpretation satisfying 1182.67/297.13 not(EDA) and not(IDA(1)). 1182.67/297.13 1182.67/297.13 [a__and](x1, x2) = [1] x1 + [4] 1182.67/297.13 1182.67/297.13 [true] = [0] 1182.67/297.13 1182.67/297.13 [mark](x1) = [1] 1182.67/297.13 1182.67/297.13 [false] = [0] 1182.67/297.13 1182.67/297.13 [a__if](x1, x2, x3) = [1] x1 + [4] 1182.67/297.13 1182.67/297.13 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [0] = [1] 1182.67/297.13 1182.67/297.13 [s](x1) = [1] 1182.67/297.13 1182.67/297.13 [add](x1, x2) = [1] x1 + [0] 1182.67/297.13 1182.67/297.13 [a__first](x1, x2) = [1] x1 + [1] x2 + [6] 1182.67/297.13 1182.67/297.13 [nil] = [1] 1182.67/297.13 1182.67/297.14 [cons](x1, x2) = [1] 1182.67/297.14 1182.67/297.14 [first](x1, x2) = [1] x1 + [1] x2 + [2] 1182.67/297.14 1182.67/297.14 [a__from](x1) = [4] 1182.67/297.14 1182.67/297.14 [from](x1) = [2] 1182.67/297.14 1182.67/297.14 [and](x1, x2) = [1] x1 + [3] 1182.67/297.14 1182.67/297.14 [if](x1, x2, x3) = [1] x1 + [3] 1182.67/297.14 1182.67/297.14 The order satisfies the following ordering constraints: 1182.67/297.14 1182.67/297.14 [a__and(X1, X2)] = [1] X1 + [4] 1182.67/297.14 > [1] X1 + [3] 1182.67/297.14 = [and(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__and(true(), X)] = [4] 1182.67/297.14 > [1] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__and(false(), Y)] = [4] 1182.67/297.14 > [0] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(true())] = [1] 1182.67/297.14 > [0] 1182.67/297.14 = [true()] 1182.67/297.14 1182.67/297.14 [mark(false())] = [1] 1182.67/297.14 > [0] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(0())] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [0()] 1182.67/297.14 1182.67/297.14 [mark(s(X))] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [s(X)] 1182.67/297.14 1182.67/297.14 [mark(add(X1, X2))] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [a__add(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(nil())] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [mark(cons(X1, X2))] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [cons(X1, X2)] 1182.67/297.14 1182.67/297.14 [mark(first(X1, X2))] = [1] 1182.67/297.14 ? [8] 1182.67/297.14 = [a__first(mark(X1), mark(X2))] 1182.67/297.14 1182.67/297.14 [mark(from(X))] = [1] 1182.67/297.14 ? [4] 1182.67/297.14 = [a__from(X)] 1182.67/297.14 1182.67/297.14 [mark(and(X1, X2))] = [1] 1182.67/297.14 ? [5] 1182.67/297.14 = [a__and(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(if(X1, X2, X3))] = [1] 1182.67/297.14 ? [5] 1182.67/297.14 = [a__if(mark(X1), X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(X1, X2, X3)] = [1] X1 + [4] 1182.67/297.14 > [1] X1 + [3] 1182.67/297.14 = [if(X1, X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(true(), X, Y)] = [4] 1182.67/297.14 > [1] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__if(false(), X, Y)] = [4] 1182.67/297.14 > [1] 1182.67/297.14 = [mark(Y)] 1182.67/297.14 1182.67/297.14 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.14 >= [1] X1 + [0] 1182.67/297.14 = [add(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__add(0(), X)] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__add(s(X), Y)] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [s(add(X, Y))] 1182.67/297.14 1182.67/297.14 [a__first(X1, X2)] = [1] X1 + [1] X2 + [6] 1182.67/297.14 > [1] X1 + [1] X2 + [2] 1182.67/297.14 = [first(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__first(0(), X)] = [1] X + [7] 1182.67/297.14 > [1] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.14 > [1] 1182.67/297.14 = [cons(Y, first(X, Z))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [4] 1182.67/297.14 > [1] 1182.67/297.14 = [cons(X, from(s(X)))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [4] 1182.67/297.14 > [2] 1182.67/297.14 = [from(X)] 1182.67/297.14 1182.67/297.14 1182.67/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.14 1182.67/297.14 We are left with following problem, upon which TcT provides the 1182.67/297.14 certificate YES(O(1),O(n^1)). 1182.67/297.14 1182.67/297.14 Strict Trs: 1182.67/297.14 { mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.14 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.14 , mark(from(X)) -> a__from(X) 1182.67/297.14 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.14 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.14 Weak Trs: 1182.67/297.14 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.14 , a__and(true(), X) -> mark(X) 1182.67/297.14 , a__and(false(), Y) -> false() 1182.67/297.14 , mark(true()) -> true() 1182.67/297.14 , mark(false()) -> false() 1182.67/297.14 , mark(0()) -> 0() 1182.67/297.14 , mark(s(X)) -> s(X) 1182.67/297.14 , mark(nil()) -> nil() 1182.67/297.14 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.14 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.14 , a__if(true(), X, Y) -> mark(X) 1182.67/297.14 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.14 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.14 , a__add(0(), X) -> mark(X) 1182.67/297.14 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.14 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.14 , a__first(0(), X) -> nil() 1182.67/297.14 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.14 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.14 , a__from(X) -> from(X) } 1182.67/297.14 Obligation: 1182.67/297.14 runtime complexity 1182.67/297.14 Answer: 1182.67/297.14 YES(O(1),O(n^1)) 1182.67/297.14 1182.67/297.14 The weightgap principle applies (using the following nonconstant 1182.67/297.14 growth matrix-interpretation) 1182.67/297.14 1182.67/297.14 The following argument positions are usable: 1182.67/297.14 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.14 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.14 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.14 1182.67/297.14 TcT has computed the following matrix interpretation satisfying 1182.67/297.14 not(EDA) and not(IDA(1)). 1182.67/297.14 1182.67/297.14 [a__and](x1, x2) = [1] x1 + [0] 1182.67/297.14 1182.67/297.14 [true] = [1] 1182.67/297.14 1182.67/297.14 [mark](x1) = [1] 1182.67/297.14 1182.67/297.14 [false] = [1] 1182.67/297.14 1182.67/297.14 [a__if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.14 1182.67/297.14 [a__add](x1, x2) = [1] x1 + [0] 1182.67/297.14 1182.67/297.14 [0] = [1] 1182.67/297.14 1182.67/297.14 [s](x1) = [1] 1182.67/297.14 1182.67/297.14 [add](x1, x2) = [1] x1 + [0] 1182.67/297.14 1182.67/297.14 [a__first](x1, x2) = [1] x1 + [1] x2 + [7] 1182.67/297.14 1182.67/297.14 [nil] = [0] 1182.67/297.14 1182.67/297.14 [cons](x1, x2) = [0] 1182.67/297.14 1182.67/297.14 [first](x1, x2) = [1] x1 + [1] x2 + [2] 1182.67/297.14 1182.67/297.14 [a__from](x1) = [0] 1182.67/297.14 1182.67/297.14 [from](x1) = [0] 1182.67/297.14 1182.67/297.14 [and](x1, x2) = [1] x1 + [0] 1182.67/297.14 1182.67/297.14 [if](x1, x2, x3) = [1] x1 + [0] 1182.67/297.14 1182.67/297.14 The order satisfies the following ordering constraints: 1182.67/297.14 1182.67/297.14 [a__and(X1, X2)] = [1] X1 + [0] 1182.67/297.14 >= [1] X1 + [0] 1182.67/297.14 = [and(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__and(true(), X)] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__and(false(), Y)] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(true())] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [true()] 1182.67/297.14 1182.67/297.14 [mark(false())] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(0())] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [0()] 1182.67/297.14 1182.67/297.14 [mark(s(X))] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [s(X)] 1182.67/297.14 1182.67/297.14 [mark(add(X1, X2))] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [a__add(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(nil())] = [1] 1182.67/297.14 > [0] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [mark(cons(X1, X2))] = [1] 1182.67/297.14 > [0] 1182.67/297.14 = [cons(X1, X2)] 1182.67/297.14 1182.67/297.14 [mark(first(X1, X2))] = [1] 1182.67/297.14 ? [9] 1182.67/297.14 = [a__first(mark(X1), mark(X2))] 1182.67/297.14 1182.67/297.14 [mark(from(X))] = [1] 1182.67/297.14 > [0] 1182.67/297.14 = [a__from(X)] 1182.67/297.14 1182.67/297.14 [mark(and(X1, X2))] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [a__and(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(if(X1, X2, X3))] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [a__if(mark(X1), X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(X1, X2, X3)] = [1] X1 + [0] 1182.67/297.14 >= [1] X1 + [0] 1182.67/297.14 = [if(X1, X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(true(), X, Y)] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__if(false(), X, Y)] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [mark(Y)] 1182.67/297.14 1182.67/297.14 [a__add(X1, X2)] = [1] X1 + [0] 1182.67/297.14 >= [1] X1 + [0] 1182.67/297.14 = [add(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__add(0(), X)] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__add(s(X), Y)] = [1] 1182.67/297.14 >= [1] 1182.67/297.14 = [s(add(X, Y))] 1182.67/297.14 1182.67/297.14 [a__first(X1, X2)] = [1] X1 + [1] X2 + [7] 1182.67/297.14 > [1] X1 + [1] X2 + [2] 1182.67/297.14 = [first(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__first(0(), X)] = [1] X + [8] 1182.67/297.14 > [0] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.14 > [0] 1182.67/297.14 = [cons(Y, first(X, Z))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [cons(X, from(s(X)))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [from(X)] 1182.67/297.14 1182.67/297.14 1182.67/297.14 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1182.67/297.14 1182.67/297.14 We are left with following problem, upon which TcT provides the 1182.67/297.14 certificate YES(O(1),O(n^1)). 1182.67/297.14 1182.67/297.14 Strict Trs: 1182.67/297.14 { mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.14 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.14 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.14 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.14 Weak Trs: 1182.67/297.14 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.14 , a__and(true(), X) -> mark(X) 1182.67/297.14 , a__and(false(), Y) -> false() 1182.67/297.14 , mark(true()) -> true() 1182.67/297.14 , mark(false()) -> false() 1182.67/297.14 , mark(0()) -> 0() 1182.67/297.14 , mark(s(X)) -> s(X) 1182.67/297.14 , mark(nil()) -> nil() 1182.67/297.14 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.14 , mark(from(X)) -> a__from(X) 1182.67/297.14 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.14 , a__if(true(), X, Y) -> mark(X) 1182.67/297.14 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.14 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.14 , a__add(0(), X) -> mark(X) 1182.67/297.14 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.14 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.14 , a__first(0(), X) -> nil() 1182.67/297.14 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.14 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.14 , a__from(X) -> from(X) } 1182.67/297.14 Obligation: 1182.67/297.14 runtime complexity 1182.67/297.14 Answer: 1182.67/297.14 YES(O(1),O(n^1)) 1182.67/297.14 1182.67/297.14 We use the processor 'matrix interpretation of dimension 1' to 1182.67/297.14 orient following rules strictly. 1182.67/297.14 1182.67/297.14 Trs: 1182.67/297.14 { mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.14 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) } 1182.67/297.14 1182.67/297.14 The induced complexity on above rules (modulo remaining rules) is 1182.67/297.14 YES(?,O(n^1)) . These rules are moved into the corresponding weak 1182.67/297.14 component(s). 1182.67/297.14 1182.67/297.14 Sub-proof: 1182.67/297.14 ---------- 1182.67/297.14 The following argument positions are usable: 1182.67/297.14 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.14 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.14 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.14 1182.67/297.14 TcT has computed the following constructor-based matrix 1182.67/297.14 interpretation satisfying not(EDA). 1182.67/297.14 1182.67/297.14 [a__and](x1, x2) = [1] x1 + [4] x2 + [0] 1182.67/297.14 1182.67/297.14 [true] = [0] 1182.67/297.14 1182.67/297.14 [mark](x1) = [4] x1 + [0] 1182.67/297.14 1182.67/297.14 [false] = [0] 1182.67/297.14 1182.67/297.14 [a__if](x1, x2, x3) = [1] x1 + [4] x2 + [4] x3 + [0] 1182.67/297.14 1182.67/297.14 [a__add](x1, x2) = [1] x1 + [4] x2 + [1] 1182.67/297.14 1182.67/297.14 [0] = [0] 1182.67/297.14 1182.67/297.14 [s](x1) = [0] 1182.67/297.14 1182.67/297.14 [add](x1, x2) = [1] x1 + [1] x2 + [1] 1182.67/297.14 1182.67/297.14 [a__first](x1, x2) = [1] x1 + [1] x2 + [7] 1182.67/297.14 1182.67/297.14 [nil] = [2] 1182.67/297.14 1182.67/297.14 [cons](x1, x2) = [0] 1182.67/297.14 1182.67/297.14 [first](x1, x2) = [1] x1 + [1] x2 + [3] 1182.67/297.14 1182.67/297.14 [a__from](x1) = [0] 1182.67/297.14 1182.67/297.14 [from](x1) = [0] 1182.67/297.14 1182.67/297.14 [and](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.14 1182.67/297.14 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 1182.67/297.14 1182.67/297.14 The order satisfies the following ordering constraints: 1182.67/297.14 1182.67/297.14 [a__and(X1, X2)] = [1] X1 + [4] X2 + [0] 1182.67/297.14 >= [1] X1 + [1] X2 + [0] 1182.67/297.14 = [and(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__and(true(), X)] = [4] X + [0] 1182.67/297.14 >= [4] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__and(false(), Y)] = [4] Y + [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(true())] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [true()] 1182.67/297.14 1182.67/297.14 [mark(false())] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(0())] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [0()] 1182.67/297.14 1182.67/297.14 [mark(s(X))] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [s(X)] 1182.67/297.14 1182.67/297.14 [mark(add(X1, X2))] = [4] X1 + [4] X2 + [4] 1182.67/297.14 > [4] X1 + [4] X2 + [1] 1182.67/297.14 = [a__add(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(nil())] = [8] 1182.67/297.14 > [2] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [mark(cons(X1, X2))] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [cons(X1, X2)] 1182.67/297.14 1182.67/297.14 [mark(first(X1, X2))] = [4] X1 + [4] X2 + [12] 1182.67/297.14 > [4] X1 + [4] X2 + [7] 1182.67/297.14 = [a__first(mark(X1), mark(X2))] 1182.67/297.14 1182.67/297.14 [mark(from(X))] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [a__from(X)] 1182.67/297.14 1182.67/297.14 [mark(and(X1, X2))] = [4] X1 + [4] X2 + [0] 1182.67/297.14 >= [4] X1 + [4] X2 + [0] 1182.67/297.14 = [a__and(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(if(X1, X2, X3))] = [4] X1 + [4] X2 + [4] X3 + [0] 1182.67/297.14 >= [4] X1 + [4] X2 + [4] X3 + [0] 1182.67/297.14 = [a__if(mark(X1), X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(X1, X2, X3)] = [1] X1 + [4] X2 + [4] X3 + [0] 1182.67/297.14 >= [1] X1 + [1] X2 + [1] X3 + [0] 1182.67/297.14 = [if(X1, X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(true(), X, Y)] = [4] X + [4] Y + [0] 1182.67/297.14 >= [4] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__if(false(), X, Y)] = [4] X + [4] Y + [0] 1182.67/297.14 >= [4] Y + [0] 1182.67/297.14 = [mark(Y)] 1182.67/297.14 1182.67/297.14 [a__add(X1, X2)] = [1] X1 + [4] X2 + [1] 1182.67/297.14 >= [1] X1 + [1] X2 + [1] 1182.67/297.14 = [add(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__add(0(), X)] = [4] X + [1] 1182.67/297.14 > [4] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__add(s(X), Y)] = [4] Y + [1] 1182.67/297.14 > [0] 1182.67/297.14 = [s(add(X, Y))] 1182.67/297.14 1182.67/297.14 [a__first(X1, X2)] = [1] X1 + [1] X2 + [7] 1182.67/297.14 > [1] X1 + [1] X2 + [3] 1182.67/297.14 = [first(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__first(0(), X)] = [1] X + [7] 1182.67/297.14 > [2] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [a__first(s(X), cons(Y, Z))] = [7] 1182.67/297.14 > [0] 1182.67/297.14 = [cons(Y, first(X, Z))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [cons(X, from(s(X)))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [from(X)] 1182.67/297.14 1182.67/297.14 1182.67/297.14 We return to the main proof. 1182.67/297.14 1182.67/297.14 We are left with following problem, upon which TcT provides the 1182.67/297.14 certificate YES(O(1),O(n^1)). 1182.67/297.14 1182.67/297.14 Strict Trs: 1182.67/297.14 { mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.14 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.14 Weak Trs: 1182.67/297.14 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.14 , a__and(true(), X) -> mark(X) 1182.67/297.14 , a__and(false(), Y) -> false() 1182.67/297.14 , mark(true()) -> true() 1182.67/297.14 , mark(false()) -> false() 1182.67/297.14 , mark(0()) -> 0() 1182.67/297.14 , mark(s(X)) -> s(X) 1182.67/297.14 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.14 , mark(nil()) -> nil() 1182.67/297.14 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.14 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.14 , mark(from(X)) -> a__from(X) 1182.67/297.14 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.14 , a__if(true(), X, Y) -> mark(X) 1182.67/297.14 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.14 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.14 , a__add(0(), X) -> mark(X) 1182.67/297.14 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.14 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.14 , a__first(0(), X) -> nil() 1182.67/297.14 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.14 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.14 , a__from(X) -> from(X) } 1182.67/297.14 Obligation: 1182.67/297.14 runtime complexity 1182.67/297.14 Answer: 1182.67/297.14 YES(O(1),O(n^1)) 1182.67/297.14 1182.67/297.14 We use the processor 'matrix interpretation of dimension 1' to 1182.67/297.14 orient following rules strictly. 1182.67/297.14 1182.67/297.14 Trs: { mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) } 1182.67/297.14 1182.67/297.14 The induced complexity on above rules (modulo remaining rules) is 1182.67/297.14 YES(?,O(n^1)) . These rules are moved into the corresponding weak 1182.67/297.14 component(s). 1182.67/297.14 1182.67/297.14 Sub-proof: 1182.67/297.14 ---------- 1182.67/297.14 The following argument positions are usable: 1182.67/297.14 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.14 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.14 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.14 1182.67/297.14 TcT has computed the following constructor-based matrix 1182.67/297.14 interpretation satisfying not(EDA). 1182.67/297.14 1182.67/297.14 [a__and](x1, x2) = [1] x1 + [4] x2 + [0] 1182.67/297.14 1182.67/297.14 [true] = [0] 1182.67/297.14 1182.67/297.14 [mark](x1) = [4] x1 + [0] 1182.67/297.14 1182.67/297.14 [false] = [0] 1182.67/297.14 1182.67/297.14 [a__if](x1, x2, x3) = [1] x1 + [4] x2 + [4] x3 + [2] 1182.67/297.14 1182.67/297.14 [a__add](x1, x2) = [1] x1 + [4] x2 + [4] 1182.67/297.14 1182.67/297.14 [0] = [2] 1182.67/297.14 1182.67/297.14 [s](x1) = [2] 1182.67/297.14 1182.67/297.14 [add](x1, x2) = [1] x1 + [1] x2 + [2] 1182.67/297.14 1182.67/297.14 [a__first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.14 1182.67/297.14 [nil] = [0] 1182.67/297.14 1182.67/297.14 [cons](x1, x2) = [0] 1182.67/297.14 1182.67/297.14 [first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.14 1182.67/297.14 [a__from](x1) = [0] 1182.67/297.14 1182.67/297.14 [from](x1) = [0] 1182.67/297.14 1182.67/297.14 [and](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.14 1182.67/297.14 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] 1182.67/297.14 1182.67/297.14 The order satisfies the following ordering constraints: 1182.67/297.14 1182.67/297.14 [a__and(X1, X2)] = [1] X1 + [4] X2 + [0] 1182.67/297.14 >= [1] X1 + [1] X2 + [0] 1182.67/297.14 = [and(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__and(true(), X)] = [4] X + [0] 1182.67/297.14 >= [4] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__and(false(), Y)] = [4] Y + [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(true())] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [true()] 1182.67/297.14 1182.67/297.14 [mark(false())] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(0())] = [8] 1182.67/297.14 > [2] 1182.67/297.14 = [0()] 1182.67/297.14 1182.67/297.14 [mark(s(X))] = [8] 1182.67/297.14 > [2] 1182.67/297.14 = [s(X)] 1182.67/297.14 1182.67/297.14 [mark(add(X1, X2))] = [4] X1 + [4] X2 + [8] 1182.67/297.14 > [4] X1 + [4] X2 + [4] 1182.67/297.14 = [a__add(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(nil())] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [mark(cons(X1, X2))] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [cons(X1, X2)] 1182.67/297.14 1182.67/297.14 [mark(first(X1, X2))] = [4] X1 + [4] X2 + [0] 1182.67/297.14 >= [4] X1 + [4] X2 + [0] 1182.67/297.14 = [a__first(mark(X1), mark(X2))] 1182.67/297.14 1182.67/297.14 [mark(from(X))] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [a__from(X)] 1182.67/297.14 1182.67/297.14 [mark(and(X1, X2))] = [4] X1 + [4] X2 + [0] 1182.67/297.14 >= [4] X1 + [4] X2 + [0] 1182.67/297.14 = [a__and(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(if(X1, X2, X3))] = [4] X1 + [4] X2 + [4] X3 + [8] 1182.67/297.14 > [4] X1 + [4] X2 + [4] X3 + [2] 1182.67/297.14 = [a__if(mark(X1), X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(X1, X2, X3)] = [1] X1 + [4] X2 + [4] X3 + [2] 1182.67/297.14 >= [1] X1 + [1] X2 + [1] X3 + [2] 1182.67/297.14 = [if(X1, X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(true(), X, Y)] = [4] X + [4] Y + [2] 1182.67/297.14 > [4] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__if(false(), X, Y)] = [4] X + [4] Y + [2] 1182.67/297.14 > [4] Y + [0] 1182.67/297.14 = [mark(Y)] 1182.67/297.14 1182.67/297.14 [a__add(X1, X2)] = [1] X1 + [4] X2 + [4] 1182.67/297.14 > [1] X1 + [1] X2 + [2] 1182.67/297.14 = [add(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__add(0(), X)] = [4] X + [6] 1182.67/297.14 > [4] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__add(s(X), Y)] = [4] Y + [6] 1182.67/297.14 > [2] 1182.67/297.14 = [s(add(X, Y))] 1182.67/297.14 1182.67/297.14 [a__first(X1, X2)] = [1] X1 + [1] X2 + [0] 1182.67/297.14 >= [1] X1 + [1] X2 + [0] 1182.67/297.14 = [first(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__first(0(), X)] = [1] X + [2] 1182.67/297.14 > [0] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [a__first(s(X), cons(Y, Z))] = [2] 1182.67/297.14 > [0] 1182.67/297.14 = [cons(Y, first(X, Z))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [cons(X, from(s(X)))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [from(X)] 1182.67/297.14 1182.67/297.14 1182.67/297.14 We return to the main proof. 1182.67/297.14 1182.67/297.14 We are left with following problem, upon which TcT provides the 1182.67/297.14 certificate YES(O(1),O(n^1)). 1182.67/297.14 1182.67/297.14 Strict Trs: { mark(and(X1, X2)) -> a__and(mark(X1), X2) } 1182.67/297.14 Weak Trs: 1182.67/297.14 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.14 , a__and(true(), X) -> mark(X) 1182.67/297.14 , a__and(false(), Y) -> false() 1182.67/297.14 , mark(true()) -> true() 1182.67/297.14 , mark(false()) -> false() 1182.67/297.14 , mark(0()) -> 0() 1182.67/297.14 , mark(s(X)) -> s(X) 1182.67/297.14 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.14 , mark(nil()) -> nil() 1182.67/297.14 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.14 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.14 , mark(from(X)) -> a__from(X) 1182.67/297.14 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.14 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.14 , a__if(true(), X, Y) -> mark(X) 1182.67/297.14 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.14 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.14 , a__add(0(), X) -> mark(X) 1182.67/297.14 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.14 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.14 , a__first(0(), X) -> nil() 1182.67/297.14 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.14 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.14 , a__from(X) -> from(X) } 1182.67/297.14 Obligation: 1182.67/297.14 runtime complexity 1182.67/297.14 Answer: 1182.67/297.14 YES(O(1),O(n^1)) 1182.67/297.14 1182.67/297.14 We use the processor 'matrix interpretation of dimension 1' to 1182.67/297.14 orient following rules strictly. 1182.67/297.14 1182.67/297.14 Trs: { mark(and(X1, X2)) -> a__and(mark(X1), X2) } 1182.67/297.14 1182.67/297.14 The induced complexity on above rules (modulo remaining rules) is 1182.67/297.14 YES(?,O(n^1)) . These rules are moved into the corresponding weak 1182.67/297.14 component(s). 1182.67/297.14 1182.67/297.14 Sub-proof: 1182.67/297.14 ---------- 1182.67/297.14 The following argument positions are usable: 1182.67/297.14 Uargs(a__and) = {1}, Uargs(a__if) = {1}, Uargs(a__add) = {1}, 1182.67/297.14 Uargs(add) = {1}, Uargs(a__first) = {1, 2}, Uargs(first) = {1, 2}, 1182.67/297.14 Uargs(and) = {1}, Uargs(if) = {1} 1182.67/297.14 1182.67/297.14 TcT has computed the following constructor-based matrix 1182.67/297.14 interpretation satisfying not(EDA). 1182.67/297.14 1182.67/297.14 [a__and](x1, x2) = [1] x1 + [2] x2 + [4] 1182.67/297.14 1182.67/297.14 [true] = [4] 1182.67/297.14 1182.67/297.14 [mark](x1) = [2] x1 + [0] 1182.67/297.14 1182.67/297.14 [false] = [4] 1182.67/297.14 1182.67/297.14 [a__if](x1, x2, x3) = [1] x1 + [2] x2 + [2] x3 + [0] 1182.67/297.14 1182.67/297.14 [a__add](x1, x2) = [1] x1 + [2] x2 + [4] 1182.67/297.14 1182.67/297.14 [0] = [4] 1182.67/297.14 1182.67/297.14 [s](x1) = [4] 1182.67/297.14 1182.67/297.14 [add](x1, x2) = [1] x1 + [1] x2 + [4] 1182.67/297.14 1182.67/297.14 [a__first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.14 1182.67/297.14 [nil] = [0] 1182.67/297.14 1182.67/297.14 [cons](x1, x2) = [4] 1182.67/297.14 1182.67/297.14 [first](x1, x2) = [1] x1 + [1] x2 + [0] 1182.67/297.14 1182.67/297.14 [a__from](x1) = [4] 1182.67/297.14 1182.67/297.14 [from](x1) = [4] 1182.67/297.14 1182.67/297.14 [and](x1, x2) = [1] x1 + [1] x2 + [4] 1182.67/297.14 1182.67/297.14 [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 1182.67/297.14 1182.67/297.14 The order satisfies the following ordering constraints: 1182.67/297.14 1182.67/297.14 [a__and(X1, X2)] = [1] X1 + [2] X2 + [4] 1182.67/297.14 >= [1] X1 + [1] X2 + [4] 1182.67/297.14 = [and(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__and(true(), X)] = [2] X + [8] 1182.67/297.14 > [2] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__and(false(), Y)] = [2] Y + [8] 1182.67/297.14 > [4] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(true())] = [8] 1182.67/297.14 > [4] 1182.67/297.14 = [true()] 1182.67/297.14 1182.67/297.14 [mark(false())] = [8] 1182.67/297.14 > [4] 1182.67/297.14 = [false()] 1182.67/297.14 1182.67/297.14 [mark(0())] = [8] 1182.67/297.14 > [4] 1182.67/297.14 = [0()] 1182.67/297.14 1182.67/297.14 [mark(s(X))] = [8] 1182.67/297.14 > [4] 1182.67/297.14 = [s(X)] 1182.67/297.14 1182.67/297.14 [mark(add(X1, X2))] = [2] X1 + [2] X2 + [8] 1182.67/297.14 > [2] X1 + [2] X2 + [4] 1182.67/297.14 = [a__add(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(nil())] = [0] 1182.67/297.14 >= [0] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [mark(cons(X1, X2))] = [8] 1182.67/297.14 > [4] 1182.67/297.14 = [cons(X1, X2)] 1182.67/297.14 1182.67/297.14 [mark(first(X1, X2))] = [2] X1 + [2] X2 + [0] 1182.67/297.14 >= [2] X1 + [2] X2 + [0] 1182.67/297.14 = [a__first(mark(X1), mark(X2))] 1182.67/297.14 1182.67/297.14 [mark(from(X))] = [8] 1182.67/297.14 > [4] 1182.67/297.14 = [a__from(X)] 1182.67/297.14 1182.67/297.14 [mark(and(X1, X2))] = [2] X1 + [2] X2 + [8] 1182.67/297.14 > [2] X1 + [2] X2 + [4] 1182.67/297.14 = [a__and(mark(X1), X2)] 1182.67/297.14 1182.67/297.14 [mark(if(X1, X2, X3))] = [2] X1 + [2] X2 + [2] X3 + [0] 1182.67/297.14 >= [2] X1 + [2] X2 + [2] X3 + [0] 1182.67/297.14 = [a__if(mark(X1), X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(X1, X2, X3)] = [1] X1 + [2] X2 + [2] X3 + [0] 1182.67/297.14 >= [1] X1 + [1] X2 + [1] X3 + [0] 1182.67/297.14 = [if(X1, X2, X3)] 1182.67/297.14 1182.67/297.14 [a__if(true(), X, Y)] = [2] X + [2] Y + [4] 1182.67/297.14 > [2] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__if(false(), X, Y)] = [2] X + [2] Y + [4] 1182.67/297.14 > [2] Y + [0] 1182.67/297.14 = [mark(Y)] 1182.67/297.14 1182.67/297.14 [a__add(X1, X2)] = [1] X1 + [2] X2 + [4] 1182.67/297.14 >= [1] X1 + [1] X2 + [4] 1182.67/297.14 = [add(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__add(0(), X)] = [2] X + [8] 1182.67/297.14 > [2] X + [0] 1182.67/297.14 = [mark(X)] 1182.67/297.14 1182.67/297.14 [a__add(s(X), Y)] = [2] Y + [8] 1182.67/297.14 > [4] 1182.67/297.14 = [s(add(X, Y))] 1182.67/297.14 1182.67/297.14 [a__first(X1, X2)] = [1] X1 + [1] X2 + [0] 1182.67/297.14 >= [1] X1 + [1] X2 + [0] 1182.67/297.14 = [first(X1, X2)] 1182.67/297.14 1182.67/297.14 [a__first(0(), X)] = [1] X + [4] 1182.67/297.14 > [0] 1182.67/297.14 = [nil()] 1182.67/297.14 1182.67/297.14 [a__first(s(X), cons(Y, Z))] = [8] 1182.67/297.14 > [4] 1182.67/297.14 = [cons(Y, first(X, Z))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [4] 1182.67/297.14 >= [4] 1182.67/297.14 = [cons(X, from(s(X)))] 1182.67/297.14 1182.67/297.14 [a__from(X)] = [4] 1182.67/297.14 >= [4] 1182.67/297.14 = [from(X)] 1182.67/297.14 1182.67/297.14 1182.67/297.14 We return to the main proof. 1182.67/297.14 1182.67/297.14 We are left with following problem, upon which TcT provides the 1182.67/297.14 certificate YES(O(1),O(1)). 1182.67/297.14 1182.67/297.14 Weak Trs: 1182.67/297.14 { a__and(X1, X2) -> and(X1, X2) 1182.67/297.14 , a__and(true(), X) -> mark(X) 1182.67/297.14 , a__and(false(), Y) -> false() 1182.67/297.14 , mark(true()) -> true() 1182.67/297.14 , mark(false()) -> false() 1182.67/297.14 , mark(0()) -> 0() 1182.67/297.14 , mark(s(X)) -> s(X) 1182.67/297.14 , mark(add(X1, X2)) -> a__add(mark(X1), X2) 1182.67/297.14 , mark(nil()) -> nil() 1182.67/297.14 , mark(cons(X1, X2)) -> cons(X1, X2) 1182.67/297.14 , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) 1182.67/297.14 , mark(from(X)) -> a__from(X) 1182.67/297.14 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1182.67/297.14 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1182.67/297.14 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1182.67/297.14 , a__if(true(), X, Y) -> mark(X) 1182.67/297.14 , a__if(false(), X, Y) -> mark(Y) 1182.67/297.14 , a__add(X1, X2) -> add(X1, X2) 1182.67/297.14 , a__add(0(), X) -> mark(X) 1182.67/297.14 , a__add(s(X), Y) -> s(add(X, Y)) 1182.67/297.14 , a__first(X1, X2) -> first(X1, X2) 1182.67/297.14 , a__first(0(), X) -> nil() 1182.67/297.14 , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) 1182.67/297.14 , a__from(X) -> cons(X, from(s(X))) 1182.67/297.14 , a__from(X) -> from(X) } 1182.67/297.14 Obligation: 1182.67/297.14 runtime complexity 1182.67/297.14 Answer: 1182.67/297.14 YES(O(1),O(1)) 1182.67/297.14 1182.67/297.14 Empty rules are trivially bounded 1182.67/297.14 1182.67/297.14 Hurray, we answered YES(O(1),O(n^1)) 1185.64/300.73 EOF