YES(O(1),O(n^1)) 40.14/11.35 YES(O(1),O(n^1)) 40.14/11.35 40.14/11.35 We are left with following problem, upon which TcT provides the 40.14/11.35 certificate YES(O(1),O(n^1)). 40.14/11.35 40.14/11.35 Strict Trs: 40.14/11.35 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.35 , fst(0(), Z) -> nil() 40.14/11.35 , fst(s(X), cons(Y, Z)) -> 40.14/11.35 cons(Y, n__fst(activate(X), activate(Z))) 40.14/11.35 , s(X) -> n__s(X) 40.14/11.35 , activate(X) -> X 40.14/11.35 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.35 , activate(n__from(X)) -> from(activate(X)) 40.14/11.35 , activate(n__s(X)) -> s(X) 40.14/11.35 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.35 , activate(n__len(X)) -> len(activate(X)) 40.14/11.35 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.35 , from(X) -> n__from(X) 40.14/11.35 , add(X1, X2) -> n__add(X1, X2) 40.14/11.35 , add(0(), X) -> X 40.14/11.35 , add(s(X), Y) -> s(n__add(activate(X), Y)) 40.14/11.35 , len(X) -> n__len(X) 40.14/11.35 , len(nil()) -> 0() 40.14/11.35 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.35 Obligation: 40.14/11.35 innermost runtime complexity 40.14/11.35 Answer: 40.14/11.35 YES(O(1),O(n^1)) 40.14/11.35 40.14/11.35 Arguments of following rules are not normal-forms: 40.14/11.35 40.14/11.35 { fst(s(X), cons(Y, Z)) -> 40.14/11.35 cons(Y, n__fst(activate(X), activate(Z))) 40.14/11.35 , add(s(X), Y) -> s(n__add(activate(X), Y)) } 40.14/11.35 40.14/11.35 All above mentioned rules can be savely removed. 40.14/11.35 40.14/11.35 We are left with following problem, upon which TcT provides the 40.14/11.35 certificate YES(O(1),O(n^1)). 40.14/11.35 40.14/11.35 Strict Trs: 40.14/11.35 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.35 , fst(0(), Z) -> nil() 40.14/11.35 , s(X) -> n__s(X) 40.14/11.35 , activate(X) -> X 40.14/11.35 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.35 , activate(n__from(X)) -> from(activate(X)) 40.14/11.35 , activate(n__s(X)) -> s(X) 40.14/11.35 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.35 , activate(n__len(X)) -> len(activate(X)) 40.14/11.35 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.35 , from(X) -> n__from(X) 40.14/11.35 , add(X1, X2) -> n__add(X1, X2) 40.14/11.35 , add(0(), X) -> X 40.14/11.35 , len(X) -> n__len(X) 40.14/11.35 , len(nil()) -> 0() 40.14/11.35 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.35 Obligation: 40.14/11.35 innermost runtime complexity 40.14/11.35 Answer: 40.14/11.35 YES(O(1),O(n^1)) 40.14/11.35 40.14/11.35 The weightgap principle applies (using the following nonconstant 40.14/11.35 growth matrix-interpretation) 40.14/11.35 40.14/11.35 The following argument positions are usable: 40.14/11.35 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.35 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.35 40.14/11.35 TcT has computed the following matrix interpretation satisfying 40.14/11.35 not(EDA) and not(IDA(1)). 40.14/11.35 40.14/11.35 [fst](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.35 40.14/11.35 [0] = [4] 40.14/11.35 40.14/11.35 [nil] = [1] 40.14/11.35 40.14/11.35 [s](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [cons](x1, x2) = [1] x2 + [0] 40.14/11.35 40.14/11.35 [n__fst](x1, x2) = [1] x1 + [1] x2 + [1] 40.14/11.35 40.14/11.35 [activate](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [from](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [n__from](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [n__s](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [add](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.35 40.14/11.35 [n__add](x1, x2) = [1] x1 + [1] x2 + [1] 40.14/11.35 40.14/11.35 [len](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [n__len](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 The order satisfies the following ordering constraints: 40.14/11.35 40.14/11.35 [fst(X1, X2)] = [1] X1 + [1] X2 + [0] 40.14/11.35 ? [1] X1 + [1] X2 + [1] 40.14/11.35 = [n__fst(X1, X2)] 40.14/11.35 40.14/11.35 [fst(0(), Z)] = [1] Z + [4] 40.14/11.35 > [1] 40.14/11.35 = [nil()] 40.14/11.35 40.14/11.35 [s(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [n__s(X)] 40.14/11.35 40.14/11.35 [activate(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [X] 40.14/11.35 40.14/11.35 [activate(n__fst(X1, X2))] = [1] X1 + [1] X2 + [1] 40.14/11.35 > [1] X1 + [1] X2 + [0] 40.14/11.35 = [fst(activate(X1), activate(X2))] 40.14/11.35 40.14/11.35 [activate(n__from(X))] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [from(activate(X))] 40.14/11.35 40.14/11.35 [activate(n__s(X))] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [s(X)] 40.14/11.35 40.14/11.35 [activate(n__add(X1, X2))] = [1] X1 + [1] X2 + [1] 40.14/11.35 > [1] X1 + [1] X2 + [0] 40.14/11.35 = [add(activate(X1), activate(X2))] 40.14/11.35 40.14/11.35 [activate(n__len(X))] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [len(activate(X))] 40.14/11.35 40.14/11.35 [from(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [cons(X, n__from(n__s(X)))] 40.14/11.35 40.14/11.35 [from(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [n__from(X)] 40.14/11.35 40.14/11.35 [add(X1, X2)] = [1] X1 + [1] X2 + [0] 40.14/11.35 ? [1] X1 + [1] X2 + [1] 40.14/11.35 = [n__add(X1, X2)] 40.14/11.35 40.14/11.35 [add(0(), X)] = [1] X + [4] 40.14/11.35 > [1] X + [0] 40.14/11.35 = [X] 40.14/11.35 40.14/11.35 [len(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [n__len(X)] 40.14/11.35 40.14/11.35 [len(nil())] = [1] 40.14/11.35 ? [4] 40.14/11.35 = [0()] 40.14/11.35 40.14/11.35 [len(cons(X, Z))] = [1] Z + [0] 40.14/11.35 >= [1] Z + [0] 40.14/11.35 = [s(n__len(activate(Z)))] 40.14/11.35 40.14/11.35 40.14/11.35 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 40.14/11.35 40.14/11.35 We are left with following problem, upon which TcT provides the 40.14/11.35 certificate YES(O(1),O(n^1)). 40.14/11.35 40.14/11.35 Strict Trs: 40.14/11.35 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.35 , s(X) -> n__s(X) 40.14/11.35 , activate(X) -> X 40.14/11.35 , activate(n__from(X)) -> from(activate(X)) 40.14/11.35 , activate(n__s(X)) -> s(X) 40.14/11.35 , activate(n__len(X)) -> len(activate(X)) 40.14/11.35 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.35 , from(X) -> n__from(X) 40.14/11.35 , add(X1, X2) -> n__add(X1, X2) 40.14/11.35 , len(X) -> n__len(X) 40.14/11.35 , len(nil()) -> 0() 40.14/11.35 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.35 Weak Trs: 40.14/11.35 { fst(0(), Z) -> nil() 40.14/11.35 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.35 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.35 , add(0(), X) -> X } 40.14/11.35 Obligation: 40.14/11.35 innermost runtime complexity 40.14/11.35 Answer: 40.14/11.35 YES(O(1),O(n^1)) 40.14/11.35 40.14/11.35 The weightgap principle applies (using the following nonconstant 40.14/11.35 growth matrix-interpretation) 40.14/11.35 40.14/11.35 The following argument positions are usable: 40.14/11.35 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.35 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.35 40.14/11.35 TcT has computed the following matrix interpretation satisfying 40.14/11.35 not(EDA) and not(IDA(1)). 40.14/11.35 40.14/11.35 [fst](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.35 40.14/11.35 [0] = [1] 40.14/11.35 40.14/11.35 [nil] = [0] 40.14/11.35 40.14/11.35 [s](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [cons](x1, x2) = [1] x2 + [0] 40.14/11.35 40.14/11.35 [n__fst](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.35 40.14/11.35 [activate](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [from](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [n__from](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [n__s](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 [add](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.35 40.14/11.35 [n__add](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.35 40.14/11.35 [len](x1) = [1] x1 + [1] 40.14/11.35 40.14/11.35 [n__len](x1) = [1] x1 + [0] 40.14/11.35 40.14/11.35 The order satisfies the following ordering constraints: 40.14/11.35 40.14/11.35 [fst(X1, X2)] = [1] X1 + [1] X2 + [0] 40.14/11.35 >= [1] X1 + [1] X2 + [0] 40.14/11.35 = [n__fst(X1, X2)] 40.14/11.35 40.14/11.35 [fst(0(), Z)] = [1] Z + [1] 40.14/11.35 > [0] 40.14/11.35 = [nil()] 40.14/11.35 40.14/11.35 [s(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [n__s(X)] 40.14/11.35 40.14/11.35 [activate(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [X] 40.14/11.35 40.14/11.35 [activate(n__fst(X1, X2))] = [1] X1 + [1] X2 + [0] 40.14/11.35 >= [1] X1 + [1] X2 + [0] 40.14/11.35 = [fst(activate(X1), activate(X2))] 40.14/11.35 40.14/11.35 [activate(n__from(X))] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [from(activate(X))] 40.14/11.35 40.14/11.35 [activate(n__s(X))] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [s(X)] 40.14/11.35 40.14/11.35 [activate(n__add(X1, X2))] = [1] X1 + [1] X2 + [0] 40.14/11.35 >= [1] X1 + [1] X2 + [0] 40.14/11.35 = [add(activate(X1), activate(X2))] 40.14/11.35 40.14/11.35 [activate(n__len(X))] = [1] X + [0] 40.14/11.35 ? [1] X + [1] 40.14/11.35 = [len(activate(X))] 40.14/11.35 40.14/11.35 [from(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [cons(X, n__from(n__s(X)))] 40.14/11.35 40.14/11.35 [from(X)] = [1] X + [0] 40.14/11.35 >= [1] X + [0] 40.14/11.35 = [n__from(X)] 40.14/11.35 40.14/11.35 [add(X1, X2)] = [1] X1 + [1] X2 + [0] 40.14/11.35 >= [1] X1 + [1] X2 + [0] 40.14/11.35 = [n__add(X1, X2)] 40.14/11.35 40.14/11.36 [add(0(), X)] = [1] X + [1] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [len(X)] = [1] X + [1] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [n__len(X)] 40.14/11.36 40.14/11.36 [len(nil())] = [1] 40.14/11.36 >= [1] 40.14/11.36 = [0()] 40.14/11.36 40.14/11.36 [len(cons(X, Z))] = [1] Z + [1] 40.14/11.36 > [1] Z + [0] 40.14/11.36 = [s(n__len(activate(Z)))] 40.14/11.36 40.14/11.36 40.14/11.36 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 40.14/11.36 40.14/11.36 We are left with following problem, upon which TcT provides the 40.14/11.36 certificate YES(O(1),O(n^1)). 40.14/11.36 40.14/11.36 Strict Trs: 40.14/11.36 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.36 , s(X) -> n__s(X) 40.14/11.36 , activate(X) -> X 40.14/11.36 , activate(n__from(X)) -> from(activate(X)) 40.14/11.36 , activate(n__s(X)) -> s(X) 40.14/11.36 , activate(n__len(X)) -> len(activate(X)) 40.14/11.36 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.36 , from(X) -> n__from(X) 40.14/11.36 , add(X1, X2) -> n__add(X1, X2) 40.14/11.36 , len(nil()) -> 0() } 40.14/11.36 Weak Trs: 40.14/11.36 { fst(0(), Z) -> nil() 40.14/11.36 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.36 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.36 , add(0(), X) -> X 40.14/11.36 , len(X) -> n__len(X) 40.14/11.36 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.36 Obligation: 40.14/11.36 innermost runtime complexity 40.14/11.36 Answer: 40.14/11.36 YES(O(1),O(n^1)) 40.14/11.36 40.14/11.36 The weightgap principle applies (using the following nonconstant 40.14/11.36 growth matrix-interpretation) 40.14/11.36 40.14/11.36 The following argument positions are usable: 40.14/11.36 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.36 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.36 40.14/11.36 TcT has computed the following matrix interpretation satisfying 40.14/11.36 not(EDA) and not(IDA(1)). 40.14/11.36 40.14/11.36 [fst](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.36 40.14/11.36 [0] = [1] 40.14/11.36 40.14/11.36 [nil] = [0] 40.14/11.36 40.14/11.36 [s](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [cons](x1, x2) = [1] x2 + [4] 40.14/11.36 40.14/11.36 [n__fst](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.36 40.14/11.36 [activate](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [from](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [n__from](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [n__s](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [add](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.36 40.14/11.36 [n__add](x1, x2) = [1] x1 + [1] x2 + [4] 40.14/11.36 40.14/11.36 [len](x1) = [1] x1 + [4] 40.14/11.36 40.14/11.36 [n__len](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 The order satisfies the following ordering constraints: 40.14/11.36 40.14/11.36 [fst(X1, X2)] = [1] X1 + [1] X2 + [0] 40.14/11.36 >= [1] X1 + [1] X2 + [0] 40.14/11.36 = [n__fst(X1, X2)] 40.14/11.36 40.14/11.36 [fst(0(), Z)] = [1] Z + [1] 40.14/11.36 > [0] 40.14/11.36 = [nil()] 40.14/11.36 40.14/11.36 [s(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [n__s(X)] 40.14/11.36 40.14/11.36 [activate(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [activate(n__fst(X1, X2))] = [1] X1 + [1] X2 + [0] 40.14/11.36 >= [1] X1 + [1] X2 + [0] 40.14/11.36 = [fst(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__from(X))] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [from(activate(X))] 40.14/11.36 40.14/11.36 [activate(n__s(X))] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [s(X)] 40.14/11.36 40.14/11.36 [activate(n__add(X1, X2))] = [1] X1 + [1] X2 + [4] 40.14/11.36 > [1] X1 + [1] X2 + [0] 40.14/11.36 = [add(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__len(X))] = [1] X + [0] 40.14/11.36 ? [1] X + [4] 40.14/11.36 = [len(activate(X))] 40.14/11.36 40.14/11.36 [from(X)] = [1] X + [0] 40.14/11.36 ? [1] X + [4] 40.14/11.36 = [cons(X, n__from(n__s(X)))] 40.14/11.36 40.14/11.36 [from(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [n__from(X)] 40.14/11.36 40.14/11.36 [add(X1, X2)] = [1] X1 + [1] X2 + [0] 40.14/11.36 ? [1] X1 + [1] X2 + [4] 40.14/11.36 = [n__add(X1, X2)] 40.14/11.36 40.14/11.36 [add(0(), X)] = [1] X + [1] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [len(X)] = [1] X + [4] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [n__len(X)] 40.14/11.36 40.14/11.36 [len(nil())] = [4] 40.14/11.36 > [1] 40.14/11.36 = [0()] 40.14/11.36 40.14/11.36 [len(cons(X, Z))] = [1] Z + [8] 40.14/11.36 > [1] Z + [0] 40.14/11.36 = [s(n__len(activate(Z)))] 40.14/11.36 40.14/11.36 40.14/11.36 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 40.14/11.36 40.14/11.36 We are left with following problem, upon which TcT provides the 40.14/11.36 certificate YES(O(1),O(n^1)). 40.14/11.36 40.14/11.36 Strict Trs: 40.14/11.36 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.36 , s(X) -> n__s(X) 40.14/11.36 , activate(X) -> X 40.14/11.36 , activate(n__from(X)) -> from(activate(X)) 40.14/11.36 , activate(n__s(X)) -> s(X) 40.14/11.36 , activate(n__len(X)) -> len(activate(X)) 40.14/11.36 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.36 , from(X) -> n__from(X) 40.14/11.36 , add(X1, X2) -> n__add(X1, X2) } 40.14/11.36 Weak Trs: 40.14/11.36 { fst(0(), Z) -> nil() 40.14/11.36 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.36 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.36 , add(0(), X) -> X 40.14/11.36 , len(X) -> n__len(X) 40.14/11.36 , len(nil()) -> 0() 40.14/11.36 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.36 Obligation: 40.14/11.36 innermost runtime complexity 40.14/11.36 Answer: 40.14/11.36 YES(O(1),O(n^1)) 40.14/11.36 40.14/11.36 The weightgap principle applies (using the following nonconstant 40.14/11.36 growth matrix-interpretation) 40.14/11.36 40.14/11.36 The following argument positions are usable: 40.14/11.36 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.36 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.36 40.14/11.36 TcT has computed the following matrix interpretation satisfying 40.14/11.36 not(EDA) and not(IDA(1)). 40.14/11.36 40.14/11.36 [fst](x1, x2) = [1] x1 + [1] x2 + [1] 40.14/11.36 40.14/11.36 [0] = [3] 40.14/11.36 40.14/11.36 [nil] = [4] 40.14/11.36 40.14/11.36 [s](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [cons](x1, x2) = [1] x2 + [4] 40.14/11.36 40.14/11.36 [n__fst](x1, x2) = [1] x1 + [1] x2 + [1] 40.14/11.36 40.14/11.36 [activate](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [from](x1) = [1] x1 + [1] 40.14/11.36 40.14/11.36 [n__from](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [n__s](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [add](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.36 40.14/11.36 [n__add](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.36 40.14/11.36 [len](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [n__len](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 The order satisfies the following ordering constraints: 40.14/11.36 40.14/11.36 [fst(X1, X2)] = [1] X1 + [1] X2 + [1] 40.14/11.36 >= [1] X1 + [1] X2 + [1] 40.14/11.36 = [n__fst(X1, X2)] 40.14/11.36 40.14/11.36 [fst(0(), Z)] = [1] Z + [4] 40.14/11.36 >= [4] 40.14/11.36 = [nil()] 40.14/11.36 40.14/11.36 [s(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [n__s(X)] 40.14/11.36 40.14/11.36 [activate(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [activate(n__fst(X1, X2))] = [1] X1 + [1] X2 + [1] 40.14/11.36 >= [1] X1 + [1] X2 + [1] 40.14/11.36 = [fst(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__from(X))] = [1] X + [0] 40.14/11.36 ? [1] X + [1] 40.14/11.36 = [from(activate(X))] 40.14/11.36 40.14/11.36 [activate(n__s(X))] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [s(X)] 40.14/11.36 40.14/11.36 [activate(n__add(X1, X2))] = [1] X1 + [1] X2 + [0] 40.14/11.36 >= [1] X1 + [1] X2 + [0] 40.14/11.36 = [add(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__len(X))] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [len(activate(X))] 40.14/11.36 40.14/11.36 [from(X)] = [1] X + [1] 40.14/11.36 ? [1] X + [4] 40.14/11.36 = [cons(X, n__from(n__s(X)))] 40.14/11.36 40.14/11.36 [from(X)] = [1] X + [1] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [n__from(X)] 40.14/11.36 40.14/11.36 [add(X1, X2)] = [1] X1 + [1] X2 + [0] 40.14/11.36 >= [1] X1 + [1] X2 + [0] 40.14/11.36 = [n__add(X1, X2)] 40.14/11.36 40.14/11.36 [add(0(), X)] = [1] X + [3] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [len(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [n__len(X)] 40.14/11.36 40.14/11.36 [len(nil())] = [4] 40.14/11.36 > [3] 40.14/11.36 = [0()] 40.14/11.36 40.14/11.36 [len(cons(X, Z))] = [1] Z + [4] 40.14/11.36 > [1] Z + [0] 40.14/11.36 = [s(n__len(activate(Z)))] 40.14/11.36 40.14/11.36 40.14/11.36 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 40.14/11.36 40.14/11.36 We are left with following problem, upon which TcT provides the 40.14/11.36 certificate YES(O(1),O(n^1)). 40.14/11.36 40.14/11.36 Strict Trs: 40.14/11.36 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.36 , s(X) -> n__s(X) 40.14/11.36 , activate(X) -> X 40.14/11.36 , activate(n__from(X)) -> from(activate(X)) 40.14/11.36 , activate(n__s(X)) -> s(X) 40.14/11.36 , activate(n__len(X)) -> len(activate(X)) 40.14/11.36 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.36 , add(X1, X2) -> n__add(X1, X2) } 40.14/11.36 Weak Trs: 40.14/11.36 { fst(0(), Z) -> nil() 40.14/11.36 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.36 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.36 , from(X) -> n__from(X) 40.14/11.36 , add(0(), X) -> X 40.14/11.36 , len(X) -> n__len(X) 40.14/11.36 , len(nil()) -> 0() 40.14/11.36 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.36 Obligation: 40.14/11.36 innermost runtime complexity 40.14/11.36 Answer: 40.14/11.36 YES(O(1),O(n^1)) 40.14/11.36 40.14/11.36 The weightgap principle applies (using the following nonconstant 40.14/11.36 growth matrix-interpretation) 40.14/11.36 40.14/11.36 The following argument positions are usable: 40.14/11.36 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.36 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.36 40.14/11.36 TcT has computed the following matrix interpretation satisfying 40.14/11.36 not(EDA) and not(IDA(1)). 40.14/11.36 40.14/11.36 [fst](x1, x2) = [1] x1 + [1] x2 + [2] 40.14/11.36 40.14/11.36 [0] = [7] 40.14/11.36 40.14/11.36 [nil] = [5] 40.14/11.36 40.14/11.36 [s](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [cons](x1, x2) = [1] x2 + [0] 40.14/11.36 40.14/11.36 [n__fst](x1, x2) = [1] x1 + [1] x2 + [7] 40.14/11.36 40.14/11.36 [activate](x1) = [1] x1 + [1] 40.14/11.36 40.14/11.36 [from](x1) = [1] x1 + [7] 40.14/11.36 40.14/11.36 [n__from](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [n__s](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [add](x1, x2) = [1] x1 + [1] x2 + [6] 40.14/11.36 40.14/11.36 [n__add](x1, x2) = [1] x1 + [1] x2 + [7] 40.14/11.36 40.14/11.36 [len](x1) = [1] x1 + [4] 40.14/11.36 40.14/11.36 [n__len](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 The order satisfies the following ordering constraints: 40.14/11.36 40.14/11.36 [fst(X1, X2)] = [1] X1 + [1] X2 + [2] 40.14/11.36 ? [1] X1 + [1] X2 + [7] 40.14/11.36 = [n__fst(X1, X2)] 40.14/11.36 40.14/11.36 [fst(0(), Z)] = [1] Z + [9] 40.14/11.36 > [5] 40.14/11.36 = [nil()] 40.14/11.36 40.14/11.36 [s(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [n__s(X)] 40.14/11.36 40.14/11.36 [activate(X)] = [1] X + [1] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [activate(n__fst(X1, X2))] = [1] X1 + [1] X2 + [8] 40.14/11.36 > [1] X1 + [1] X2 + [4] 40.14/11.36 = [fst(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__from(X))] = [1] X + [1] 40.14/11.36 ? [1] X + [8] 40.14/11.36 = [from(activate(X))] 40.14/11.36 40.14/11.36 [activate(n__s(X))] = [1] X + [1] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [s(X)] 40.14/11.36 40.14/11.36 [activate(n__add(X1, X2))] = [1] X1 + [1] X2 + [8] 40.14/11.36 >= [1] X1 + [1] X2 + [8] 40.14/11.36 = [add(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__len(X))] = [1] X + [1] 40.14/11.36 ? [1] X + [5] 40.14/11.36 = [len(activate(X))] 40.14/11.36 40.14/11.36 [from(X)] = [1] X + [7] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [cons(X, n__from(n__s(X)))] 40.14/11.36 40.14/11.36 [from(X)] = [1] X + [7] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [n__from(X)] 40.14/11.36 40.14/11.36 [add(X1, X2)] = [1] X1 + [1] X2 + [6] 40.14/11.36 ? [1] X1 + [1] X2 + [7] 40.14/11.36 = [n__add(X1, X2)] 40.14/11.36 40.14/11.36 [add(0(), X)] = [1] X + [13] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [len(X)] = [1] X + [4] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [n__len(X)] 40.14/11.36 40.14/11.36 [len(nil())] = [9] 40.14/11.36 > [7] 40.14/11.36 = [0()] 40.14/11.36 40.14/11.36 [len(cons(X, Z))] = [1] Z + [4] 40.14/11.36 > [1] Z + [1] 40.14/11.36 = [s(n__len(activate(Z)))] 40.14/11.36 40.14/11.36 40.14/11.36 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 40.14/11.36 40.14/11.36 We are left with following problem, upon which TcT provides the 40.14/11.36 certificate YES(O(1),O(n^1)). 40.14/11.36 40.14/11.36 Strict Trs: 40.14/11.36 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.36 , s(X) -> n__s(X) 40.14/11.36 , activate(n__from(X)) -> from(activate(X)) 40.14/11.36 , activate(n__len(X)) -> len(activate(X)) 40.14/11.36 , add(X1, X2) -> n__add(X1, X2) } 40.14/11.36 Weak Trs: 40.14/11.36 { fst(0(), Z) -> nil() 40.14/11.36 , activate(X) -> X 40.14/11.36 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.36 , activate(n__s(X)) -> s(X) 40.14/11.36 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.36 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.36 , from(X) -> n__from(X) 40.14/11.36 , add(0(), X) -> X 40.14/11.36 , len(X) -> n__len(X) 40.14/11.36 , len(nil()) -> 0() 40.14/11.36 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.36 Obligation: 40.14/11.36 innermost runtime complexity 40.14/11.36 Answer: 40.14/11.36 YES(O(1),O(n^1)) 40.14/11.36 40.14/11.36 The weightgap principle applies (using the following nonconstant 40.14/11.36 growth matrix-interpretation) 40.14/11.36 40.14/11.36 The following argument positions are usable: 40.14/11.36 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.36 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.36 40.14/11.36 TcT has computed the following matrix interpretation satisfying 40.14/11.36 not(EDA) and not(IDA(1)). 40.14/11.36 40.14/11.36 [fst](x1, x2) = [1] x1 + [1] x2 + [6] 40.14/11.36 40.14/11.36 [0] = [7] 40.14/11.36 40.14/11.36 [nil] = [5] 40.14/11.36 40.14/11.36 [s](x1) = [1] x1 + [1] 40.14/11.36 40.14/11.36 [cons](x1, x2) = [1] x2 + [0] 40.14/11.36 40.14/11.36 [n__fst](x1, x2) = [1] x1 + [1] x2 + [7] 40.14/11.36 40.14/11.36 [activate](x1) = [1] x1 + [1] 40.14/11.36 40.14/11.36 [from](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [n__from](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [n__s](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 [add](x1, x2) = [1] x1 + [1] x2 + [0] 40.14/11.36 40.14/11.36 [n__add](x1, x2) = [1] x1 + [1] x2 + [4] 40.14/11.36 40.14/11.36 [len](x1) = [1] x1 + [4] 40.14/11.36 40.14/11.36 [n__len](x1) = [1] x1 + [0] 40.14/11.36 40.14/11.36 The order satisfies the following ordering constraints: 40.14/11.36 40.14/11.36 [fst(X1, X2)] = [1] X1 + [1] X2 + [6] 40.14/11.36 ? [1] X1 + [1] X2 + [7] 40.14/11.36 = [n__fst(X1, X2)] 40.14/11.36 40.14/11.36 [fst(0(), Z)] = [1] Z + [13] 40.14/11.36 > [5] 40.14/11.36 = [nil()] 40.14/11.36 40.14/11.36 [s(X)] = [1] X + [1] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [n__s(X)] 40.14/11.36 40.14/11.36 [activate(X)] = [1] X + [1] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [activate(n__fst(X1, X2))] = [1] X1 + [1] X2 + [8] 40.14/11.36 >= [1] X1 + [1] X2 + [8] 40.14/11.36 = [fst(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__from(X))] = [1] X + [1] 40.14/11.36 >= [1] X + [1] 40.14/11.36 = [from(activate(X))] 40.14/11.36 40.14/11.36 [activate(n__s(X))] = [1] X + [1] 40.14/11.36 >= [1] X + [1] 40.14/11.36 = [s(X)] 40.14/11.36 40.14/11.36 [activate(n__add(X1, X2))] = [1] X1 + [1] X2 + [5] 40.14/11.36 > [1] X1 + [1] X2 + [2] 40.14/11.36 = [add(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__len(X))] = [1] X + [1] 40.14/11.36 ? [1] X + [5] 40.14/11.36 = [len(activate(X))] 40.14/11.36 40.14/11.36 [from(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [cons(X, n__from(n__s(X)))] 40.14/11.36 40.14/11.36 [from(X)] = [1] X + [0] 40.14/11.36 >= [1] X + [0] 40.14/11.36 = [n__from(X)] 40.14/11.36 40.14/11.36 [add(X1, X2)] = [1] X1 + [1] X2 + [0] 40.14/11.36 ? [1] X1 + [1] X2 + [4] 40.14/11.36 = [n__add(X1, X2)] 40.14/11.36 40.14/11.36 [add(0(), X)] = [1] X + [7] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [len(X)] = [1] X + [4] 40.14/11.36 > [1] X + [0] 40.14/11.36 = [n__len(X)] 40.14/11.36 40.14/11.36 [len(nil())] = [9] 40.14/11.36 > [7] 40.14/11.36 = [0()] 40.14/11.36 40.14/11.36 [len(cons(X, Z))] = [1] Z + [4] 40.14/11.36 > [1] Z + [2] 40.14/11.36 = [s(n__len(activate(Z)))] 40.14/11.36 40.14/11.36 40.14/11.36 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 40.14/11.36 40.14/11.36 We are left with following problem, upon which TcT provides the 40.14/11.36 certificate YES(O(1),O(n^1)). 40.14/11.36 40.14/11.36 Strict Trs: 40.14/11.36 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.36 , activate(n__from(X)) -> from(activate(X)) 40.14/11.36 , activate(n__len(X)) -> len(activate(X)) 40.14/11.36 , add(X1, X2) -> n__add(X1, X2) } 40.14/11.36 Weak Trs: 40.14/11.36 { fst(0(), Z) -> nil() 40.14/11.36 , s(X) -> n__s(X) 40.14/11.36 , activate(X) -> X 40.14/11.36 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.36 , activate(n__s(X)) -> s(X) 40.14/11.36 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.36 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.36 , from(X) -> n__from(X) 40.14/11.36 , add(0(), X) -> X 40.14/11.36 , len(X) -> n__len(X) 40.14/11.36 , len(nil()) -> 0() 40.14/11.36 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.36 Obligation: 40.14/11.36 innermost runtime complexity 40.14/11.36 Answer: 40.14/11.36 YES(O(1),O(n^1)) 40.14/11.36 40.14/11.36 We use the processor 'matrix interpretation of dimension 2' to 40.14/11.36 orient following rules strictly. 40.14/11.36 40.14/11.36 Trs: { activate(n__len(X)) -> len(activate(X)) } 40.14/11.36 40.14/11.36 The induced complexity on above rules (modulo remaining rules) is 40.14/11.36 YES(?,O(n^1)) . These rules are moved into the corresponding weak 40.14/11.36 component(s). 40.14/11.36 40.14/11.36 Sub-proof: 40.14/11.36 ---------- 40.14/11.36 The following argument positions are usable: 40.14/11.36 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.36 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.36 40.14/11.36 TcT has computed the following constructor-based matrix 40.14/11.36 interpretation satisfying not(EDA) and not(IDA(1)). 40.14/11.36 40.14/11.36 [fst](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 40.14/11.36 [0] = [0] 40.14/11.36 [0] 40.14/11.36 40.14/11.36 [nil] = [0] 40.14/11.36 [0] 40.14/11.36 40.14/11.36 [s](x1) = [1 0] x1 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [cons](x1, x2) = [1 1] x2 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [n__fst](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 40.14/11.36 [activate](x1) = [1 1] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 [from](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 [n__from](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 [n__s](x1) = [1 0] x1 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [add](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 40.14/11.36 [n__add](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 40.14/11.36 [len](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [1] 40.14/11.36 40.14/11.36 [n__len](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [1] 40.14/11.36 40.14/11.36 The order satisfies the following ordering constraints: 40.14/11.36 40.14/11.36 [fst(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 >= [1 0] X1 + [1 0] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 = [n__fst(X1, X2)] 40.14/11.36 40.14/11.36 [fst(0(), Z)] = [1 0] Z + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [0] 40.14/11.36 [0] 40.14/11.36 = [nil()] 40.14/11.36 40.14/11.36 [s(X)] = [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 = [n__s(X)] 40.14/11.36 40.14/11.36 [activate(X)] = [1 1] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [activate(n__fst(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 >= [1 1] X1 + [1 1] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 = [fst(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__from(X))] = [1 1] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [1 1] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 = [from(activate(X))] 40.14/11.36 40.14/11.36 [activate(n__s(X))] = [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 = [s(X)] 40.14/11.36 40.14/11.36 [activate(n__add(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 >= [1 1] X1 + [1 1] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 = [add(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__len(X))] = [1 1] X + [1] 40.14/11.36 [0 1] [1] 40.14/11.36 > [1 1] X + [0] 40.14/11.36 [0 1] [1] 40.14/11.36 = [len(activate(X))] 40.14/11.36 40.14/11.36 [from(X)] = [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 = [cons(X, n__from(n__s(X)))] 40.14/11.36 40.14/11.36 [from(X)] = [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 = [n__from(X)] 40.14/11.36 40.14/11.36 [add(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 >= [1 0] X1 + [1 0] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 = [n__add(X1, X2)] 40.14/11.36 40.14/11.36 [add(0(), X)] = [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [len(X)] = [1 0] X + [0] 40.14/11.36 [0 1] [1] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 1] [1] 40.14/11.36 = [n__len(X)] 40.14/11.36 40.14/11.36 [len(nil())] = [0] 40.14/11.36 [1] 40.14/11.36 >= [0] 40.14/11.36 [0] 40.14/11.36 = [0()] 40.14/11.36 40.14/11.36 [len(cons(X, Z))] = [1 1] Z + [0] 40.14/11.36 [0 0] [1] 40.14/11.36 >= [1 1] Z + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 = [s(n__len(activate(Z)))] 40.14/11.36 40.14/11.36 40.14/11.36 We return to the main proof. 40.14/11.36 40.14/11.36 We are left with following problem, upon which TcT provides the 40.14/11.36 certificate YES(O(1),O(n^1)). 40.14/11.36 40.14/11.36 Strict Trs: 40.14/11.36 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.36 , activate(n__from(X)) -> from(activate(X)) 40.14/11.36 , add(X1, X2) -> n__add(X1, X2) } 40.14/11.36 Weak Trs: 40.14/11.36 { fst(0(), Z) -> nil() 40.14/11.36 , s(X) -> n__s(X) 40.14/11.36 , activate(X) -> X 40.14/11.36 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.36 , activate(n__s(X)) -> s(X) 40.14/11.36 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.36 , activate(n__len(X)) -> len(activate(X)) 40.14/11.36 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.36 , from(X) -> n__from(X) 40.14/11.36 , add(0(), X) -> X 40.14/11.36 , len(X) -> n__len(X) 40.14/11.36 , len(nil()) -> 0() 40.14/11.36 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.36 Obligation: 40.14/11.36 innermost runtime complexity 40.14/11.36 Answer: 40.14/11.36 YES(O(1),O(n^1)) 40.14/11.36 40.14/11.36 We use the processor 'matrix interpretation of dimension 2' to 40.14/11.36 orient following rules strictly. 40.14/11.36 40.14/11.36 Trs: { add(X1, X2) -> n__add(X1, X2) } 40.14/11.36 40.14/11.36 The induced complexity on above rules (modulo remaining rules) is 40.14/11.36 YES(?,O(n^1)) . These rules are moved into the corresponding weak 40.14/11.36 component(s). 40.14/11.36 40.14/11.36 Sub-proof: 40.14/11.36 ---------- 40.14/11.36 The following argument positions are usable: 40.14/11.36 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.36 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.36 40.14/11.36 TcT has computed the following constructor-based matrix 40.14/11.36 interpretation satisfying not(EDA) and not(IDA(1)). 40.14/11.36 40.14/11.36 [fst](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 40.14/11.36 [0] = [0] 40.14/11.36 [0] 40.14/11.36 40.14/11.36 [nil] = [0] 40.14/11.36 [0] 40.14/11.36 40.14/11.36 [s](x1) = [1 0] x1 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [cons](x1, x2) = [1 1] x2 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [n__fst](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 40.14/11.36 [activate](x1) = [1 1] x1 + [0] 40.14/11.36 [0 2] [0] 40.14/11.36 40.14/11.36 [from](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 [n__from](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 [n__s](x1) = [1 0] x1 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [add](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 40.14/11.36 [0 1] [0 1] [1] 40.14/11.36 40.14/11.36 [n__add](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [1] 40.14/11.36 40.14/11.36 [len](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 [n__len](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 The order satisfies the following ordering constraints: 40.14/11.36 40.14/11.36 [fst(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 >= [1 0] X1 + [1 0] X2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.36 = [n__fst(X1, X2)] 40.14/11.36 40.14/11.36 [fst(0(), Z)] = [1 0] Z + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [0] 40.14/11.36 [0] 40.14/11.36 = [nil()] 40.14/11.36 40.14/11.36 [s(X)] = [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 = [n__s(X)] 40.14/11.36 40.14/11.36 [activate(X)] = [1 1] X + [0] 40.14/11.36 [0 2] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [activate(n__fst(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 40.14/11.36 [0 2] [0 2] [0] 40.14/11.36 >= [1 1] X1 + [1 1] X2 + [0] 40.14/11.36 [0 2] [0 2] [0] 40.14/11.36 = [fst(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__from(X))] = [1 1] X + [0] 40.14/11.36 [0 2] [0] 40.14/11.36 >= [1 1] X + [0] 40.14/11.36 [0 2] [0] 40.14/11.36 = [from(activate(X))] 40.14/11.36 40.14/11.36 [activate(n__s(X))] = [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 = [s(X)] 40.14/11.36 40.14/11.36 [activate(n__add(X1, X2))] = [1 1] X1 + [1 1] X2 + [1] 40.14/11.36 [0 2] [0 2] [2] 40.14/11.36 >= [1 1] X1 + [1 1] X2 + [1] 40.14/11.36 [0 2] [0 2] [1] 40.14/11.36 = [add(activate(X1), activate(X2))] 40.14/11.36 40.14/11.36 [activate(n__len(X))] = [1 1] X + [0] 40.14/11.36 [0 2] [0] 40.14/11.36 >= [1 1] X + [0] 40.14/11.36 [0 2] [0] 40.14/11.36 = [len(activate(X))] 40.14/11.36 40.14/11.36 [from(X)] = [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 = [cons(X, n__from(n__s(X)))] 40.14/11.36 40.14/11.36 [from(X)] = [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 = [n__from(X)] 40.14/11.36 40.14/11.36 [add(X1, X2)] = [1 0] X1 + [1 0] X2 + [1] 40.14/11.36 [0 1] [0 1] [1] 40.14/11.36 > [1 0] X1 + [1 0] X2 + [0] 40.14/11.36 [0 1] [0 1] [1] 40.14/11.36 = [n__add(X1, X2)] 40.14/11.36 40.14/11.36 [add(0(), X)] = [1 0] X + [1] 40.14/11.36 [0 1] [1] 40.14/11.36 > [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 = [X] 40.14/11.36 40.14/11.36 [len(X)] = [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 >= [1 0] X + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 = [n__len(X)] 40.14/11.36 40.14/11.36 [len(nil())] = [0] 40.14/11.36 [0] 40.14/11.36 >= [0] 40.14/11.36 [0] 40.14/11.36 = [0()] 40.14/11.36 40.14/11.36 [len(cons(X, Z))] = [1 1] Z + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 >= [1 1] Z + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 = [s(n__len(activate(Z)))] 40.14/11.36 40.14/11.36 40.14/11.36 We return to the main proof. 40.14/11.36 40.14/11.36 We are left with following problem, upon which TcT provides the 40.14/11.36 certificate YES(O(1),O(n^1)). 40.14/11.36 40.14/11.36 Strict Trs: 40.14/11.36 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.36 , activate(n__from(X)) -> from(activate(X)) } 40.14/11.36 Weak Trs: 40.14/11.36 { fst(0(), Z) -> nil() 40.14/11.36 , s(X) -> n__s(X) 40.14/11.36 , activate(X) -> X 40.14/11.36 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.36 , activate(n__s(X)) -> s(X) 40.14/11.36 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.36 , activate(n__len(X)) -> len(activate(X)) 40.14/11.36 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.36 , from(X) -> n__from(X) 40.14/11.36 , add(X1, X2) -> n__add(X1, X2) 40.14/11.36 , add(0(), X) -> X 40.14/11.36 , len(X) -> n__len(X) 40.14/11.36 , len(nil()) -> 0() 40.14/11.36 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.36 Obligation: 40.14/11.36 innermost runtime complexity 40.14/11.36 Answer: 40.14/11.36 YES(O(1),O(n^1)) 40.14/11.36 40.14/11.36 We use the processor 'matrix interpretation of dimension 2' to 40.14/11.36 orient following rules strictly. 40.14/11.36 40.14/11.36 Trs: { fst(X1, X2) -> n__fst(X1, X2) } 40.14/11.36 40.14/11.36 The induced complexity on above rules (modulo remaining rules) is 40.14/11.36 YES(?,O(n^1)) . These rules are moved into the corresponding weak 40.14/11.36 component(s). 40.14/11.36 40.14/11.36 Sub-proof: 40.14/11.36 ---------- 40.14/11.36 The following argument positions are usable: 40.14/11.36 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.36 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.36 40.14/11.36 TcT has computed the following constructor-based matrix 40.14/11.36 interpretation satisfying not(EDA) and not(IDA(1)). 40.14/11.36 40.14/11.36 [fst](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 40.14/11.36 [0 1] [0 1] [4] 40.14/11.36 40.14/11.36 [0] = [0] 40.14/11.36 [0] 40.14/11.36 40.14/11.36 [nil] = [0] 40.14/11.36 [0] 40.14/11.36 40.14/11.36 [s](x1) = [1 0] x1 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [cons](x1, x2) = [1 1] x2 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [n__fst](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [2] 40.14/11.36 40.14/11.36 [activate](x1) = [1 1] x1 + [0] 40.14/11.36 [0 4] [0] 40.14/11.36 40.14/11.36 [from](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 [n__from](x1) = [1 0] x1 + [0] 40.14/11.36 [0 1] [0] 40.14/11.36 40.14/11.36 [n__s](x1) = [1 0] x1 + [0] 40.14/11.36 [0 0] [0] 40.14/11.36 40.14/11.36 [add](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.36 [0 1] [0 1] [0] 40.14/11.37 40.14/11.37 [n__add](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 40.14/11.37 [0 1] [0 1] [0] 40.14/11.37 40.14/11.37 [len](x1) = [1 0] x1 + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 40.14/11.37 [n__len](x1) = [1 0] x1 + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 40.14/11.37 The order satisfies the following ordering constraints: 40.14/11.37 40.14/11.37 [fst(X1, X2)] = [1 0] X1 + [1 0] X2 + [1] 40.14/11.37 [0 1] [0 1] [4] 40.14/11.37 > [1 0] X1 + [1 0] X2 + [0] 40.14/11.37 [0 1] [0 1] [2] 40.14/11.37 = [n__fst(X1, X2)] 40.14/11.37 40.14/11.37 [fst(0(), Z)] = [1 0] Z + [1] 40.14/11.37 [0 1] [4] 40.14/11.37 > [0] 40.14/11.37 [0] 40.14/11.37 = [nil()] 40.14/11.37 40.14/11.37 [s(X)] = [1 0] X + [0] 40.14/11.37 [0 0] [0] 40.14/11.37 >= [1 0] X + [0] 40.14/11.37 [0 0] [0] 40.14/11.37 = [n__s(X)] 40.14/11.37 40.14/11.37 [activate(X)] = [1 1] X + [0] 40.14/11.37 [0 4] [0] 40.14/11.37 >= [1 0] X + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 = [X] 40.14/11.37 40.14/11.37 [activate(n__fst(X1, X2))] = [1 1] X1 + [1 1] X2 + [2] 40.14/11.37 [0 4] [0 4] [8] 40.14/11.37 > [1 1] X1 + [1 1] X2 + [1] 40.14/11.37 [0 4] [0 4] [4] 40.14/11.37 = [fst(activate(X1), activate(X2))] 40.14/11.37 40.14/11.37 [activate(n__from(X))] = [1 1] X + [0] 40.14/11.37 [0 4] [0] 40.14/11.37 >= [1 1] X + [0] 40.14/11.37 [0 4] [0] 40.14/11.37 = [from(activate(X))] 40.14/11.37 40.14/11.37 [activate(n__s(X))] = [1 0] X + [0] 40.14/11.37 [0 0] [0] 40.14/11.37 >= [1 0] X + [0] 40.14/11.37 [0 0] [0] 40.14/11.37 = [s(X)] 40.14/11.37 40.14/11.37 [activate(n__add(X1, X2))] = [1 1] X1 + [1 1] X2 + [0] 40.14/11.37 [0 4] [0 4] [0] 40.14/11.37 >= [1 1] X1 + [1 1] X2 + [0] 40.14/11.37 [0 4] [0 4] [0] 40.14/11.37 = [add(activate(X1), activate(X2))] 40.14/11.37 40.14/11.37 [activate(n__len(X))] = [1 1] X + [0] 40.14/11.37 [0 4] [0] 40.14/11.37 >= [1 1] X + [0] 40.14/11.37 [0 4] [0] 40.14/11.37 = [len(activate(X))] 40.14/11.37 40.14/11.37 [from(X)] = [1 0] X + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 >= [1 0] X + [0] 40.14/11.37 [0 0] [0] 40.14/11.37 = [cons(X, n__from(n__s(X)))] 40.14/11.37 40.14/11.37 [from(X)] = [1 0] X + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 >= [1 0] X + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 = [n__from(X)] 40.14/11.37 40.14/11.37 [add(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] 40.14/11.37 [0 1] [0 1] [0] 40.14/11.37 >= [1 0] X1 + [1 0] X2 + [0] 40.14/11.37 [0 1] [0 1] [0] 40.14/11.37 = [n__add(X1, X2)] 40.14/11.37 40.14/11.37 [add(0(), X)] = [1 0] X + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 >= [1 0] X + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 = [X] 40.14/11.37 40.14/11.37 [len(X)] = [1 0] X + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 >= [1 0] X + [0] 40.14/11.37 [0 1] [0] 40.14/11.37 = [n__len(X)] 40.14/11.37 40.14/11.37 [len(nil())] = [0] 40.14/11.37 [0] 40.14/11.37 >= [0] 40.14/11.37 [0] 40.14/11.37 = [0()] 40.14/11.37 40.14/11.37 [len(cons(X, Z))] = [1 1] Z + [0] 40.14/11.37 [0 0] [0] 40.14/11.37 >= [1 1] Z + [0] 40.14/11.37 [0 0] [0] 40.14/11.37 = [s(n__len(activate(Z)))] 40.14/11.37 40.14/11.37 40.14/11.37 We return to the main proof. 40.14/11.37 40.14/11.37 We are left with following problem, upon which TcT provides the 40.14/11.37 certificate YES(O(1),O(n^1)). 40.14/11.37 40.14/11.37 Strict Trs: { activate(n__from(X)) -> from(activate(X)) } 40.14/11.37 Weak Trs: 40.14/11.37 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.37 , fst(0(), Z) -> nil() 40.14/11.37 , s(X) -> n__s(X) 40.14/11.37 , activate(X) -> X 40.14/11.37 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.37 , activate(n__s(X)) -> s(X) 40.14/11.37 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.37 , activate(n__len(X)) -> len(activate(X)) 40.14/11.37 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.37 , from(X) -> n__from(X) 40.14/11.37 , add(X1, X2) -> n__add(X1, X2) 40.14/11.37 , add(0(), X) -> X 40.14/11.37 , len(X) -> n__len(X) 40.14/11.37 , len(nil()) -> 0() 40.14/11.37 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.37 Obligation: 40.14/11.37 innermost runtime complexity 40.14/11.37 Answer: 40.14/11.37 YES(O(1),O(n^1)) 40.14/11.37 40.14/11.37 We use the processor 'matrix interpretation of dimension 3' to 40.14/11.37 orient following rules strictly. 40.14/11.37 40.14/11.37 Trs: { activate(n__from(X)) -> from(activate(X)) } 40.14/11.37 40.14/11.37 The induced complexity on above rules (modulo remaining rules) is 40.14/11.37 YES(?,O(n^1)) . These rules are moved into the corresponding weak 40.14/11.37 component(s). 40.14/11.37 40.14/11.37 Sub-proof: 40.14/11.37 ---------- 40.14/11.37 The following argument positions are usable: 40.14/11.37 Uargs(fst) = {1, 2}, Uargs(s) = {1}, Uargs(from) = {1}, 40.14/11.37 Uargs(add) = {1, 2}, Uargs(len) = {1}, Uargs(n__len) = {1} 40.14/11.37 40.14/11.37 TcT has computed the following constructor-based matrix 40.14/11.37 interpretation satisfying not(EDA) and not(IDA(1)). 40.14/11.37 40.14/11.37 [1 0 0] [1 0 0] [0] 40.14/11.37 [fst](x1, x2) = [0 1 0] x1 + [0 1 4] x2 + [4] 40.14/11.37 [0 0 1] [0 0 0] [0] 40.14/11.37 40.14/11.37 [0] 40.14/11.37 [0] = [0] 40.14/11.37 [0] 40.14/11.37 40.14/11.37 [0] 40.14/11.37 [nil] = [0] 40.14/11.37 [0] 40.14/11.37 40.14/11.37 [1 0 0] [0] 40.14/11.37 [s](x1) = [0 0 0] x1 + [0] 40.14/11.37 [0 0 0] [0] 40.14/11.37 40.14/11.37 [1 4 0] [0] 40.14/11.37 [cons](x1, x2) = [0 0 0] x2 + [0] 40.14/11.37 [0 0 1] [0] 40.14/11.37 40.14/11.37 [1 0 0] [1 0 0] [0] 40.14/11.37 [n__fst](x1, x2) = [0 1 0] x1 + [0 1 4] x2 + [4] 40.14/11.37 [0 0 1] [0 0 0] [0] 40.14/11.37 40.14/11.37 [1 2 1] [0] 40.14/11.37 [activate](x1) = [0 2 0] x1 + [0] 40.14/11.37 [0 0 2] [0] 40.14/11.37 40.14/11.37 [1 0 0] [0] 40.14/11.37 [from](x1) = [0 1 2] x1 + [0] 40.14/11.37 [0 0 0] [1] 40.14/11.37 40.14/11.37 [1 0 0] [0] 40.14/11.37 [n__from](x1) = [0 1 2] x1 + [0] 40.14/11.37 [0 0 0] [1] 40.14/11.37 40.14/11.37 [1 0 0] [0] 40.14/11.37 [n__s](x1) = [0 0 0] x1 + [0] 40.14/11.37 [0 0 0] [0] 40.14/11.37 40.14/11.37 [1 0 0] [1 0 0] [0] 40.14/11.37 [add](x1, x2) = [0 1 4] x1 + [0 1 0] x2 + [2] 40.14/11.37 [0 0 0] [0 0 1] [4] 40.14/11.37 40.14/11.37 [1 0 0] [1 0 0] [0] 40.14/11.37 [n__add](x1, x2) = [0 1 4] x1 + [0 1 0] x2 + [2] 40.14/11.37 [0 0 0] [0 0 1] [4] 40.14/11.37 40.14/11.37 [1 0 1] [0] 40.14/11.37 [len](x1) = [0 1 4] x1 + [4] 40.14/11.37 [0 0 0] [0] 40.14/11.37 40.14/11.37 [1 0 0] [0] 40.14/11.37 [n__len](x1) = [0 1 4] x1 + [4] 40.14/11.37 [0 0 0] [0] 40.14/11.37 40.14/11.37 The order satisfies the following ordering constraints: 40.14/11.37 40.14/11.37 [fst(X1, X2)] = [1 0 0] [1 0 0] [0] 40.14/11.37 [0 1 0] X1 + [0 1 4] X2 + [4] 40.14/11.37 [0 0 1] [0 0 0] [0] 40.14/11.37 >= [1 0 0] [1 0 0] [0] 40.14/11.37 [0 1 0] X1 + [0 1 4] X2 + [4] 40.14/11.37 [0 0 1] [0 0 0] [0] 40.14/11.37 = [n__fst(X1, X2)] 40.14/11.37 40.14/11.37 [fst(0(), Z)] = [1 0 0] [0] 40.14/11.37 [0 1 4] Z + [4] 40.14/11.37 [0 0 0] [0] 40.14/11.37 >= [0] 40.14/11.37 [0] 40.14/11.37 [0] 40.14/11.37 = [nil()] 40.14/11.37 40.14/11.37 [s(X)] = [1 0 0] [0] 40.14/11.37 [0 0 0] X + [0] 40.14/11.37 [0 0 0] [0] 40.14/11.37 >= [1 0 0] [0] 40.14/11.37 [0 0 0] X + [0] 40.14/11.37 [0 0 0] [0] 40.14/11.37 = [n__s(X)] 40.14/11.37 40.14/11.37 [activate(X)] = [1 2 1] [0] 40.14/11.37 [0 2 0] X + [0] 40.14/11.37 [0 0 2] [0] 40.14/11.37 >= [1 0 0] [0] 40.14/11.37 [0 1 0] X + [0] 40.14/11.37 [0 0 1] [0] 40.14/11.37 = [X] 40.14/11.37 40.14/11.37 [activate(n__fst(X1, X2))] = [1 2 1] [1 2 8] [8] 40.14/11.37 [0 2 0] X1 + [0 2 8] X2 + [8] 40.14/11.37 [0 0 2] [0 0 0] [0] 40.14/11.37 > [1 2 1] [1 2 1] [0] 40.14/11.37 [0 2 0] X1 + [0 2 8] X2 + [4] 40.14/11.37 [0 0 2] [0 0 0] [0] 40.14/11.37 = [fst(activate(X1), activate(X2))] 40.14/11.37 40.14/11.37 [activate(n__from(X))] = [1 2 4] [1] 40.14/11.37 [0 2 4] X + [0] 40.14/11.37 [0 0 0] [2] 40.14/11.37 > [1 2 1] [0] 40.14/11.37 [0 2 4] X + [0] 40.14/11.37 [0 0 0] [1] 40.14/11.37 = [from(activate(X))] 40.14/11.37 40.14/11.37 [activate(n__s(X))] = [1 0 0] [0] 40.14/11.37 [0 0 0] X + [0] 40.14/11.37 [0 0 0] [0] 40.14/11.37 >= [1 0 0] [0] 40.14/11.37 [0 0 0] X + [0] 40.14/11.37 [0 0 0] [0] 40.14/11.37 = [s(X)] 40.14/11.37 40.14/11.37 [activate(n__add(X1, X2))] = [1 2 8] [1 2 1] [8] 40.14/11.37 [0 2 8] X1 + [0 2 0] X2 + [4] 40.14/11.37 [0 0 0] [0 0 2] [8] 40.14/11.37 > [1 2 1] [1 2 1] [0] 40.14/11.37 [0 2 8] X1 + [0 2 0] X2 + [2] 40.14/11.37 [0 0 0] [0 0 2] [4] 40.14/11.37 = [add(activate(X1), activate(X2))] 40.14/11.37 40.14/11.37 [activate(n__len(X))] = [1 2 8] [8] 40.14/11.37 [0 2 8] X + [8] 40.14/11.37 [0 0 0] [0] 40.14/11.37 > [1 2 3] [0] 40.14/11.37 [0 2 8] X + [4] 40.14/11.37 [0 0 0] [0] 40.14/11.37 = [len(activate(X))] 40.14/11.37 40.14/11.37 [from(X)] = [1 0 0] [0] 40.14/11.37 [0 1 2] X + [0] 40.14/11.37 [0 0 0] [1] 40.14/11.37 >= [1 0 0] [0] 40.14/11.37 [0 0 0] X + [0] 40.14/11.37 [0 0 0] [1] 40.14/11.37 = [cons(X, n__from(n__s(X)))] 40.14/11.37 40.14/11.37 [from(X)] = [1 0 0] [0] 40.14/11.37 [0 1 2] X + [0] 40.14/11.37 [0 0 0] [1] 40.14/11.37 >= [1 0 0] [0] 40.14/11.37 [0 1 2] X + [0] 40.14/11.37 [0 0 0] [1] 40.14/11.37 = [n__from(X)] 40.14/11.37 40.14/11.37 [add(X1, X2)] = [1 0 0] [1 0 0] [0] 40.14/11.37 [0 1 4] X1 + [0 1 0] X2 + [2] 40.14/11.37 [0 0 0] [0 0 1] [4] 40.14/11.37 >= [1 0 0] [1 0 0] [0] 40.14/11.37 [0 1 4] X1 + [0 1 0] X2 + [2] 40.14/11.37 [0 0 0] [0 0 1] [4] 40.14/11.37 = [n__add(X1, X2)] 40.14/11.37 40.14/11.37 [add(0(), X)] = [1 0 0] [0] 40.14/11.37 [0 1 0] X + [2] 40.14/11.37 [0 0 1] [4] 40.14/11.37 >= [1 0 0] [0] 40.14/11.37 [0 1 0] X + [0] 40.14/11.37 [0 0 1] [0] 40.14/11.37 = [X] 40.14/11.37 40.14/11.37 [len(X)] = [1 0 1] [0] 40.14/11.37 [0 1 4] X + [4] 40.14/11.37 [0 0 0] [0] 40.14/11.37 >= [1 0 0] [0] 40.14/11.37 [0 1 4] X + [4] 40.14/11.37 [0 0 0] [0] 40.14/11.37 = [n__len(X)] 40.14/11.37 40.14/11.37 [len(nil())] = [0] 40.14/11.37 [4] 40.14/11.37 [0] 40.14/11.37 >= [0] 40.14/11.37 [0] 40.14/11.37 [0] 40.14/11.37 = [0()] 40.14/11.37 40.14/11.37 [len(cons(X, Z))] = [1 4 1] [0] 40.14/11.37 [0 0 4] Z + [4] 40.14/11.37 [0 0 0] [0] 40.14/11.37 >= [1 2 1] [0] 40.14/11.37 [0 0 0] Z + [0] 40.14/11.37 [0 0 0] [0] 40.14/11.37 = [s(n__len(activate(Z)))] 40.14/11.37 40.14/11.37 40.14/11.37 We return to the main proof. 40.14/11.37 40.14/11.37 We are left with following problem, upon which TcT provides the 40.14/11.37 certificate YES(O(1),O(1)). 40.14/11.37 40.14/11.37 Weak Trs: 40.14/11.37 { fst(X1, X2) -> n__fst(X1, X2) 40.14/11.37 , fst(0(), Z) -> nil() 40.14/11.37 , s(X) -> n__s(X) 40.14/11.37 , activate(X) -> X 40.14/11.37 , activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)) 40.14/11.37 , activate(n__from(X)) -> from(activate(X)) 40.14/11.37 , activate(n__s(X)) -> s(X) 40.14/11.37 , activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)) 40.14/11.37 , activate(n__len(X)) -> len(activate(X)) 40.14/11.37 , from(X) -> cons(X, n__from(n__s(X))) 40.14/11.37 , from(X) -> n__from(X) 40.14/11.37 , add(X1, X2) -> n__add(X1, X2) 40.14/11.37 , add(0(), X) -> X 40.14/11.37 , len(X) -> n__len(X) 40.14/11.37 , len(nil()) -> 0() 40.14/11.37 , len(cons(X, Z)) -> s(n__len(activate(Z))) } 40.14/11.37 Obligation: 40.14/11.37 innermost runtime complexity 40.14/11.37 Answer: 40.14/11.37 YES(O(1),O(1)) 40.14/11.37 40.14/11.37 Empty rules are trivially bounded 40.14/11.37 40.14/11.37 Hurray, we answered YES(O(1),O(n^1)) 40.14/11.39 EOF