YES(O(1),O(n^2)) 816.51/297.03 YES(O(1),O(n^2)) 816.51/297.03 816.51/297.03 We are left with following problem, upon which TcT provides the 816.51/297.03 certificate YES(O(1),O(n^2)). 816.51/297.03 816.51/297.03 Strict Trs: 816.51/297.03 { U11(tt(), N) -> activate(N) 816.51/297.03 , activate(X) -> X 816.51/297.03 , activate(n__0()) -> 0() 816.51/297.03 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.03 , activate(n__isNat(X)) -> isNat(X) 816.51/297.03 , activate(n__s(X)) -> s(activate(X)) 816.51/297.03 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.03 , s(X) -> n__s(X) 816.51/297.03 , plus(X1, X2) -> n__plus(X1, X2) 816.51/297.03 , plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N) 816.51/297.03 , plus(N, 0()) -> U11(isNat(N), N) 816.51/297.03 , and(tt(), X) -> activate(X) 816.51/297.03 , isNat(X) -> n__isNat(X) 816.51/297.03 , isNat(n__0()) -> tt() 816.51/297.03 , isNat(n__plus(V1, V2)) -> 816.51/297.03 and(isNat(activate(V1)), n__isNat(activate(V2))) 816.51/297.03 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.03 , 0() -> n__0() } 816.51/297.03 Obligation: 816.51/297.03 innermost runtime complexity 816.51/297.03 Answer: 816.51/297.03 YES(O(1),O(n^2)) 816.51/297.03 816.51/297.03 Arguments of following rules are not normal-forms: 816.51/297.03 816.51/297.03 { plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N) 816.51/297.03 , plus(N, 0()) -> U11(isNat(N), N) } 816.51/297.03 816.51/297.03 All above mentioned rules can be savely removed. 816.51/297.03 816.51/297.03 We are left with following problem, upon which TcT provides the 816.51/297.03 certificate YES(O(1),O(n^2)). 816.51/297.03 816.51/297.03 Strict Trs: 816.51/297.03 { U11(tt(), N) -> activate(N) 816.51/297.03 , activate(X) -> X 816.51/297.03 , activate(n__0()) -> 0() 816.51/297.03 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.03 , activate(n__isNat(X)) -> isNat(X) 816.51/297.03 , activate(n__s(X)) -> s(activate(X)) 816.51/297.03 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.03 , s(X) -> n__s(X) 816.51/297.03 , plus(X1, X2) -> n__plus(X1, X2) 816.51/297.03 , and(tt(), X) -> activate(X) 816.51/297.03 , isNat(X) -> n__isNat(X) 816.51/297.03 , isNat(n__0()) -> tt() 816.51/297.03 , isNat(n__plus(V1, V2)) -> 816.51/297.03 and(isNat(activate(V1)), n__isNat(activate(V2))) 816.51/297.03 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.03 , 0() -> n__0() } 816.51/297.03 Obligation: 816.51/297.03 innermost runtime complexity 816.51/297.03 Answer: 816.51/297.03 YES(O(1),O(n^2)) 816.51/297.03 816.51/297.03 The weightgap principle applies (using the following nonconstant 816.51/297.03 growth matrix-interpretation) 816.51/297.03 816.51/297.03 The following argument positions are usable: 816.51/297.03 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2}, 816.51/297.03 Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 816.51/297.03 816.51/297.03 TcT has computed the following matrix interpretation satisfying 816.51/297.03 not(EDA) and not(IDA(1)). 816.51/297.03 816.51/297.03 [U11](x1, x2) = [1] x1 + [1] x2 + [7] 816.51/297.03 816.51/297.03 [tt] = [7] 816.51/297.03 816.51/297.03 [activate](x1) = [1] x1 + [3] 816.51/297.03 816.51/297.03 [U21](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 816.51/297.03 816.51/297.03 [s](x1) = [1] x1 + [1] 816.51/297.03 816.51/297.03 [plus](x1, x2) = [1] x1 + [1] x2 + [7] 816.51/297.03 816.51/297.03 [and](x1, x2) = [1] x1 + [1] x2 + [3] 816.51/297.03 816.51/297.03 [isNat](x1) = [1] x1 + [3] 816.51/297.03 816.51/297.03 [n__0] = [3] 816.51/297.03 816.51/297.03 [n__plus](x1, x2) = [1] x1 + [1] x2 + [7] 816.51/297.03 816.51/297.03 [n__isNat](x1) = [1] x1 + [3] 816.51/297.03 816.51/297.03 [n__s](x1) = [1] x1 + [7] 816.51/297.03 816.51/297.03 [0] = [5] 816.51/297.03 816.51/297.03 The order satisfies the following ordering constraints: 816.51/297.03 816.51/297.03 [U11(tt(), N)] = [1] N + [14] 816.51/297.03 > [1] N + [3] 816.51/297.03 = [activate(N)] 816.51/297.03 816.51/297.03 [activate(X)] = [1] X + [3] 816.51/297.03 > [1] X + [0] 816.51/297.03 = [X] 816.51/297.03 816.51/297.03 [activate(n__0())] = [6] 816.51/297.03 > [5] 816.51/297.03 = [0()] 816.51/297.03 816.51/297.03 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [10] 816.51/297.03 ? [1] X1 + [1] X2 + [13] 816.51/297.03 = [plus(activate(X1), activate(X2))] 816.51/297.03 816.51/297.03 [activate(n__isNat(X))] = [1] X + [6] 816.51/297.03 > [1] X + [3] 816.51/297.03 = [isNat(X)] 816.51/297.03 816.51/297.03 [activate(n__s(X))] = [1] X + [10] 816.51/297.03 > [1] X + [4] 816.51/297.03 = [s(activate(X))] 816.51/297.03 816.51/297.03 [U21(tt(), M, N)] = [1] N + [1] M + [14] 816.51/297.03 >= [1] N + [1] M + [14] 816.51/297.03 = [s(plus(activate(N), activate(M)))] 816.51/297.03 816.51/297.03 [s(X)] = [1] X + [1] 816.51/297.03 ? [1] X + [7] 816.51/297.03 = [n__s(X)] 816.51/297.03 816.51/297.03 [plus(X1, X2)] = [1] X1 + [1] X2 + [7] 816.51/297.03 >= [1] X1 + [1] X2 + [7] 816.51/297.03 = [n__plus(X1, X2)] 816.51/297.03 816.51/297.03 [and(tt(), X)] = [1] X + [10] 816.51/297.03 > [1] X + [3] 816.51/297.03 = [activate(X)] 816.51/297.03 816.51/297.03 [isNat(X)] = [1] X + [3] 816.51/297.03 >= [1] X + [3] 816.51/297.03 = [n__isNat(X)] 816.51/297.03 816.51/297.03 [isNat(n__0())] = [6] 816.51/297.03 ? [7] 816.51/297.03 = [tt()] 816.51/297.03 816.51/297.03 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [10] 816.51/297.03 ? [1] V1 + [1] V2 + [15] 816.51/297.03 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 816.51/297.03 816.51/297.03 [isNat(n__s(V1))] = [1] V1 + [10] 816.51/297.03 > [1] V1 + [6] 816.51/297.03 = [isNat(activate(V1))] 816.51/297.03 816.51/297.03 [0()] = [5] 816.51/297.03 > [3] 816.51/297.03 = [n__0()] 816.51/297.03 816.51/297.03 816.51/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 816.51/297.03 816.51/297.03 We are left with following problem, upon which TcT provides the 816.51/297.03 certificate YES(O(1),O(n^2)). 816.51/297.03 816.51/297.03 Strict Trs: 816.51/297.03 { activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.03 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.03 , s(X) -> n__s(X) 816.51/297.03 , plus(X1, X2) -> n__plus(X1, X2) 816.51/297.03 , isNat(X) -> n__isNat(X) 816.51/297.03 , isNat(n__0()) -> tt() 816.51/297.03 , isNat(n__plus(V1, V2)) -> 816.51/297.03 and(isNat(activate(V1)), n__isNat(activate(V2))) } 816.51/297.03 Weak Trs: 816.51/297.03 { U11(tt(), N) -> activate(N) 816.51/297.03 , activate(X) -> X 816.51/297.03 , activate(n__0()) -> 0() 816.51/297.03 , activate(n__isNat(X)) -> isNat(X) 816.51/297.03 , activate(n__s(X)) -> s(activate(X)) 816.51/297.03 , and(tt(), X) -> activate(X) 816.51/297.03 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.03 , 0() -> n__0() } 816.51/297.03 Obligation: 816.51/297.03 innermost runtime complexity 816.51/297.03 Answer: 816.51/297.03 YES(O(1),O(n^2)) 816.51/297.03 816.51/297.03 The weightgap principle applies (using the following nonconstant 816.51/297.03 growth matrix-interpretation) 816.51/297.03 816.51/297.03 The following argument positions are usable: 816.51/297.03 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2}, 816.51/297.03 Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 816.51/297.03 816.51/297.03 TcT has computed the following matrix interpretation satisfying 816.51/297.03 not(EDA) and not(IDA(1)). 816.51/297.03 816.51/297.03 [U11](x1, x2) = [1] x1 + [1] x2 + [7] 816.51/297.03 816.51/297.03 [tt] = [0] 816.51/297.03 816.51/297.03 [activate](x1) = [1] x1 + [0] 816.51/297.03 816.51/297.03 [U21](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [7] 816.51/297.03 816.51/297.03 [s](x1) = [1] x1 + [0] 816.51/297.03 816.51/297.03 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 816.51/297.03 816.51/297.03 [and](x1, x2) = [1] x1 + [1] x2 + [0] 816.51/297.03 816.51/297.03 [isNat](x1) = [1] x1 + [1] 816.51/297.03 816.51/297.03 [n__0] = [0] 816.51/297.03 816.51/297.03 [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] 816.51/297.03 816.51/297.03 [n__isNat](x1) = [1] x1 + [7] 816.51/297.03 816.51/297.03 [n__s](x1) = [1] x1 + [3] 816.51/297.03 816.51/297.03 [0] = [0] 816.51/297.03 816.51/297.03 The order satisfies the following ordering constraints: 816.51/297.03 816.51/297.03 [U11(tt(), N)] = [1] N + [7] 816.51/297.03 > [1] N + [0] 816.51/297.03 = [activate(N)] 816.51/297.03 816.51/297.03 [activate(X)] = [1] X + [0] 816.51/297.03 >= [1] X + [0] 816.51/297.03 = [X] 816.51/297.03 816.51/297.03 [activate(n__0())] = [0] 816.51/297.03 >= [0] 816.51/297.03 = [0()] 816.51/297.03 816.51/297.03 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] 816.51/297.03 >= [1] X1 + [1] X2 + [0] 816.51/297.03 = [plus(activate(X1), activate(X2))] 816.51/297.03 816.51/297.03 [activate(n__isNat(X))] = [1] X + [7] 816.51/297.03 > [1] X + [1] 816.51/297.03 = [isNat(X)] 816.51/297.03 816.51/297.03 [activate(n__s(X))] = [1] X + [3] 816.51/297.03 > [1] X + [0] 816.51/297.03 = [s(activate(X))] 816.51/297.03 816.51/297.03 [U21(tt(), M, N)] = [1] N + [1] M + [7] 816.51/297.03 > [1] N + [1] M + [0] 816.51/297.03 = [s(plus(activate(N), activate(M)))] 816.51/297.03 816.51/297.03 [s(X)] = [1] X + [0] 816.51/297.03 ? [1] X + [3] 816.51/297.03 = [n__s(X)] 816.51/297.03 816.51/297.03 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 816.51/297.03 >= [1] X1 + [1] X2 + [0] 816.51/297.03 = [n__plus(X1, X2)] 816.51/297.03 816.51/297.03 [and(tt(), X)] = [1] X + [0] 816.51/297.03 >= [1] X + [0] 816.51/297.03 = [activate(X)] 816.51/297.03 816.51/297.03 [isNat(X)] = [1] X + [1] 816.51/297.03 ? [1] X + [7] 816.51/297.03 = [n__isNat(X)] 816.51/297.03 816.51/297.03 [isNat(n__0())] = [1] 816.51/297.03 > [0] 816.51/297.03 = [tt()] 816.51/297.03 816.51/297.03 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [1] 816.51/297.03 ? [1] V1 + [1] V2 + [8] 816.51/297.03 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 816.51/297.03 816.51/297.03 [isNat(n__s(V1))] = [1] V1 + [4] 816.51/297.03 > [1] V1 + [1] 816.51/297.03 = [isNat(activate(V1))] 816.51/297.03 816.51/297.03 [0()] = [0] 816.51/297.03 >= [0] 816.51/297.03 = [n__0()] 816.51/297.03 816.51/297.03 816.51/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 816.51/297.03 816.51/297.03 We are left with following problem, upon which TcT provides the 816.51/297.03 certificate YES(O(1),O(n^2)). 816.51/297.03 816.51/297.03 Strict Trs: 816.51/297.03 { activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.03 , s(X) -> n__s(X) 816.51/297.03 , plus(X1, X2) -> n__plus(X1, X2) 816.51/297.03 , isNat(X) -> n__isNat(X) 816.51/297.03 , isNat(n__plus(V1, V2)) -> 816.51/297.03 and(isNat(activate(V1)), n__isNat(activate(V2))) } 816.51/297.03 Weak Trs: 816.51/297.03 { U11(tt(), N) -> activate(N) 816.51/297.03 , activate(X) -> X 816.51/297.03 , activate(n__0()) -> 0() 816.51/297.03 , activate(n__isNat(X)) -> isNat(X) 816.51/297.03 , activate(n__s(X)) -> s(activate(X)) 816.51/297.03 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.03 , and(tt(), X) -> activate(X) 816.51/297.03 , isNat(n__0()) -> tt() 816.51/297.03 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.03 , 0() -> n__0() } 816.51/297.03 Obligation: 816.51/297.03 innermost runtime complexity 816.51/297.03 Answer: 816.51/297.03 YES(O(1),O(n^2)) 816.51/297.03 816.51/297.03 The weightgap principle applies (using the following nonconstant 816.51/297.03 growth matrix-interpretation) 816.51/297.03 816.51/297.03 The following argument positions are usable: 816.51/297.03 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2}, 816.51/297.03 Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 816.51/297.03 816.51/297.03 TcT has computed the following matrix interpretation satisfying 816.51/297.03 not(EDA) and not(IDA(1)). 816.51/297.03 816.51/297.03 [U11](x1, x2) = [1] x1 + [1] x2 + [7] 816.51/297.03 816.51/297.03 [tt] = [4] 816.51/297.03 816.51/297.03 [activate](x1) = [1] x1 + [0] 816.51/297.03 816.51/297.03 [U21](x1, x2, x3) = [1] x2 + [1] x3 + [7] 816.51/297.03 816.51/297.03 [s](x1) = [1] x1 + [0] 816.51/297.03 816.51/297.03 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 816.51/297.03 816.51/297.03 [and](x1, x2) = [1] x1 + [1] x2 + [0] 816.51/297.03 816.51/297.03 [isNat](x1) = [1] x1 + [4] 816.51/297.03 816.51/297.03 [n__0] = [0] 816.51/297.03 816.51/297.03 [n__plus](x1, x2) = [1] x1 + [1] x2 + [4] 816.51/297.03 816.51/297.03 [n__isNat](x1) = [1] x1 + [4] 816.51/297.03 816.51/297.03 [n__s](x1) = [1] x1 + [0] 816.51/297.03 816.51/297.03 [0] = [0] 816.51/297.03 816.51/297.03 The order satisfies the following ordering constraints: 816.51/297.03 816.51/297.03 [U11(tt(), N)] = [1] N + [11] 816.51/297.03 > [1] N + [0] 816.51/297.03 = [activate(N)] 816.51/297.03 816.51/297.03 [activate(X)] = [1] X + [0] 816.51/297.03 >= [1] X + [0] 816.51/297.03 = [X] 816.51/297.03 816.51/297.03 [activate(n__0())] = [0] 816.51/297.03 >= [0] 816.51/297.03 = [0()] 816.51/297.03 816.51/297.03 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [4] 816.51/297.03 > [1] X1 + [1] X2 + [0] 816.51/297.03 = [plus(activate(X1), activate(X2))] 816.51/297.03 816.51/297.03 [activate(n__isNat(X))] = [1] X + [4] 816.51/297.03 >= [1] X + [4] 816.51/297.03 = [isNat(X)] 816.51/297.03 816.51/297.03 [activate(n__s(X))] = [1] X + [0] 816.51/297.03 >= [1] X + [0] 816.51/297.03 = [s(activate(X))] 816.51/297.03 816.51/297.03 [U21(tt(), M, N)] = [1] N + [1] M + [7] 816.51/297.03 > [1] N + [1] M + [0] 816.51/297.03 = [s(plus(activate(N), activate(M)))] 816.51/297.03 816.51/297.03 [s(X)] = [1] X + [0] 816.51/297.03 >= [1] X + [0] 816.51/297.03 = [n__s(X)] 816.51/297.03 816.51/297.03 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 816.51/297.03 ? [1] X1 + [1] X2 + [4] 816.51/297.03 = [n__plus(X1, X2)] 816.51/297.03 816.51/297.03 [and(tt(), X)] = [1] X + [4] 816.51/297.03 > [1] X + [0] 816.51/297.03 = [activate(X)] 816.51/297.03 816.51/297.03 [isNat(X)] = [1] X + [4] 816.51/297.03 >= [1] X + [4] 816.51/297.03 = [n__isNat(X)] 816.51/297.03 816.51/297.03 [isNat(n__0())] = [4] 816.51/297.03 >= [4] 816.51/297.03 = [tt()] 816.51/297.03 816.51/297.03 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [8] 816.51/297.03 >= [1] V1 + [1] V2 + [8] 816.51/297.03 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 816.51/297.03 816.51/297.03 [isNat(n__s(V1))] = [1] V1 + [4] 816.51/297.03 >= [1] V1 + [4] 816.51/297.03 = [isNat(activate(V1))] 816.51/297.03 816.51/297.03 [0()] = [0] 816.51/297.03 >= [0] 816.51/297.03 = [n__0()] 816.51/297.03 816.51/297.03 816.51/297.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 816.51/297.03 816.51/297.03 We are left with following problem, upon which TcT provides the 816.51/297.03 certificate YES(O(1),O(n^2)). 816.51/297.03 816.51/297.03 Strict Trs: 816.51/297.03 { s(X) -> n__s(X) 816.51/297.03 , plus(X1, X2) -> n__plus(X1, X2) 816.51/297.03 , isNat(X) -> n__isNat(X) 816.51/297.03 , isNat(n__plus(V1, V2)) -> 816.51/297.03 and(isNat(activate(V1)), n__isNat(activate(V2))) } 816.51/297.03 Weak Trs: 816.51/297.03 { U11(tt(), N) -> activate(N) 816.51/297.03 , activate(X) -> X 816.51/297.03 , activate(n__0()) -> 0() 816.51/297.03 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.03 , activate(n__isNat(X)) -> isNat(X) 816.51/297.03 , activate(n__s(X)) -> s(activate(X)) 816.51/297.03 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.03 , and(tt(), X) -> activate(X) 816.51/297.03 , isNat(n__0()) -> tt() 816.51/297.04 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.04 , 0() -> n__0() } 816.51/297.04 Obligation: 816.51/297.04 innermost runtime complexity 816.51/297.04 Answer: 816.51/297.04 YES(O(1),O(n^2)) 816.51/297.04 816.51/297.04 The weightgap principle applies (using the following nonconstant 816.51/297.04 growth matrix-interpretation) 816.51/297.04 816.51/297.04 The following argument positions are usable: 816.51/297.04 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2}, 816.51/297.04 Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 816.51/297.04 816.51/297.04 TcT has computed the following matrix interpretation satisfying 816.51/297.04 not(EDA) and not(IDA(1)). 816.51/297.04 816.51/297.04 [U11](x1, x2) = [1] x1 + [1] x2 + [7] 816.51/297.04 816.51/297.04 [tt] = [1] 816.51/297.04 816.51/297.04 [activate](x1) = [1] x1 + [1] 816.51/297.04 816.51/297.04 [U21](x1, x2, x3) = [1] x2 + [1] x3 + [7] 816.51/297.04 816.51/297.04 [s](x1) = [1] x1 + [0] 816.51/297.04 816.51/297.04 [plus](x1, x2) = [1] x1 + [1] x2 + [2] 816.51/297.04 816.51/297.04 [and](x1, x2) = [1] x1 + [1] x2 + [0] 816.51/297.04 816.51/297.04 [isNat](x1) = [1] x1 + [4] 816.51/297.04 816.51/297.04 [n__0] = [0] 816.51/297.04 816.51/297.04 [n__plus](x1, x2) = [1] x1 + [1] x2 + [4] 816.51/297.04 816.51/297.04 [n__isNat](x1) = [1] x1 + [3] 816.51/297.04 816.51/297.04 [n__s](x1) = [1] x1 + [4] 816.51/297.04 816.51/297.04 [0] = [1] 816.51/297.04 816.51/297.04 The order satisfies the following ordering constraints: 816.51/297.04 816.51/297.04 [U11(tt(), N)] = [1] N + [8] 816.51/297.04 > [1] N + [1] 816.51/297.04 = [activate(N)] 816.51/297.04 816.51/297.04 [activate(X)] = [1] X + [1] 816.51/297.04 > [1] X + [0] 816.51/297.04 = [X] 816.51/297.04 816.51/297.04 [activate(n__0())] = [1] 816.51/297.04 >= [1] 816.51/297.04 = [0()] 816.51/297.04 816.51/297.04 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [5] 816.51/297.04 > [1] X1 + [1] X2 + [4] 816.51/297.04 = [plus(activate(X1), activate(X2))] 816.51/297.04 816.51/297.04 [activate(n__isNat(X))] = [1] X + [4] 816.51/297.04 >= [1] X + [4] 816.51/297.04 = [isNat(X)] 816.51/297.04 816.51/297.04 [activate(n__s(X))] = [1] X + [5] 816.51/297.04 > [1] X + [1] 816.51/297.04 = [s(activate(X))] 816.51/297.04 816.51/297.04 [U21(tt(), M, N)] = [1] N + [1] M + [7] 816.51/297.04 > [1] N + [1] M + [4] 816.51/297.04 = [s(plus(activate(N), activate(M)))] 816.51/297.04 816.51/297.04 [s(X)] = [1] X + [0] 816.51/297.04 ? [1] X + [4] 816.51/297.04 = [n__s(X)] 816.51/297.04 816.51/297.04 [plus(X1, X2)] = [1] X1 + [1] X2 + [2] 816.51/297.04 ? [1] X1 + [1] X2 + [4] 816.51/297.04 = [n__plus(X1, X2)] 816.51/297.04 816.51/297.04 [and(tt(), X)] = [1] X + [1] 816.51/297.04 >= [1] X + [1] 816.51/297.04 = [activate(X)] 816.51/297.04 816.51/297.04 [isNat(X)] = [1] X + [4] 816.51/297.04 > [1] X + [3] 816.51/297.04 = [n__isNat(X)] 816.51/297.04 816.51/297.04 [isNat(n__0())] = [4] 816.51/297.04 > [1] 816.51/297.04 = [tt()] 816.51/297.04 816.51/297.04 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [8] 816.51/297.04 ? [1] V1 + [1] V2 + [9] 816.51/297.04 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 816.51/297.04 816.51/297.04 [isNat(n__s(V1))] = [1] V1 + [8] 816.51/297.04 > [1] V1 + [5] 816.51/297.04 = [isNat(activate(V1))] 816.51/297.04 816.51/297.04 [0()] = [1] 816.51/297.04 > [0] 816.51/297.04 = [n__0()] 816.51/297.04 816.51/297.04 816.51/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 816.51/297.04 816.51/297.04 We are left with following problem, upon which TcT provides the 816.51/297.04 certificate YES(O(1),O(n^2)). 816.51/297.04 816.51/297.04 Strict Trs: 816.51/297.04 { s(X) -> n__s(X) 816.51/297.04 , plus(X1, X2) -> n__plus(X1, X2) 816.51/297.04 , isNat(n__plus(V1, V2)) -> 816.51/297.04 and(isNat(activate(V1)), n__isNat(activate(V2))) } 816.51/297.04 Weak Trs: 816.51/297.04 { U11(tt(), N) -> activate(N) 816.51/297.04 , activate(X) -> X 816.51/297.04 , activate(n__0()) -> 0() 816.51/297.04 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.04 , activate(n__isNat(X)) -> isNat(X) 816.51/297.04 , activate(n__s(X)) -> s(activate(X)) 816.51/297.04 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.04 , and(tt(), X) -> activate(X) 816.51/297.04 , isNat(X) -> n__isNat(X) 816.51/297.04 , isNat(n__0()) -> tt() 816.51/297.04 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.04 , 0() -> n__0() } 816.51/297.04 Obligation: 816.51/297.04 innermost runtime complexity 816.51/297.04 Answer: 816.51/297.04 YES(O(1),O(n^2)) 816.51/297.04 816.51/297.04 The weightgap principle applies (using the following nonconstant 816.51/297.04 growth matrix-interpretation) 816.51/297.04 816.51/297.04 The following argument positions are usable: 816.51/297.04 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2}, 816.51/297.04 Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 816.51/297.04 816.51/297.04 TcT has computed the following matrix interpretation satisfying 816.51/297.04 not(EDA) and not(IDA(1)). 816.51/297.04 816.51/297.04 [U11](x1, x2) = [1] x1 + [1] x2 + [7] 816.51/297.04 816.51/297.04 [tt] = [0] 816.51/297.04 816.51/297.04 [activate](x1) = [1] x1 + [0] 816.51/297.04 816.51/297.04 [U21](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3] 816.51/297.04 816.51/297.04 [s](x1) = [1] x1 + [0] 816.51/297.04 816.51/297.04 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 816.51/297.04 816.51/297.04 [and](x1, x2) = [1] x1 + [1] x2 + [0] 816.51/297.04 816.51/297.04 [isNat](x1) = [1] x1 + [0] 816.51/297.04 816.51/297.04 [n__0] = [0] 816.51/297.04 816.51/297.04 [n__plus](x1, x2) = [1] x1 + [1] x2 + [4] 816.51/297.04 816.51/297.04 [n__isNat](x1) = [1] x1 + [0] 816.51/297.04 816.51/297.04 [n__s](x1) = [1] x1 + [0] 816.51/297.04 816.51/297.04 [0] = [0] 816.51/297.04 816.51/297.04 The order satisfies the following ordering constraints: 816.51/297.04 816.51/297.04 [U11(tt(), N)] = [1] N + [7] 816.51/297.04 > [1] N + [0] 816.51/297.04 = [activate(N)] 816.51/297.04 816.51/297.04 [activate(X)] = [1] X + [0] 816.51/297.04 >= [1] X + [0] 816.51/297.04 = [X] 816.51/297.04 816.51/297.04 [activate(n__0())] = [0] 816.51/297.04 >= [0] 816.51/297.04 = [0()] 816.51/297.04 816.51/297.04 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [4] 816.51/297.04 > [1] X1 + [1] X2 + [0] 816.51/297.04 = [plus(activate(X1), activate(X2))] 816.51/297.04 816.51/297.04 [activate(n__isNat(X))] = [1] X + [0] 816.51/297.04 >= [1] X + [0] 816.51/297.04 = [isNat(X)] 816.51/297.04 816.51/297.04 [activate(n__s(X))] = [1] X + [0] 816.51/297.04 >= [1] X + [0] 816.51/297.04 = [s(activate(X))] 816.51/297.04 816.51/297.04 [U21(tt(), M, N)] = [1] N + [1] M + [3] 816.51/297.04 > [1] N + [1] M + [0] 816.51/297.04 = [s(plus(activate(N), activate(M)))] 816.51/297.04 816.51/297.04 [s(X)] = [1] X + [0] 816.51/297.04 >= [1] X + [0] 816.51/297.04 = [n__s(X)] 816.51/297.04 816.51/297.04 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 816.51/297.04 ? [1] X1 + [1] X2 + [4] 816.51/297.04 = [n__plus(X1, X2)] 816.51/297.04 816.51/297.04 [and(tt(), X)] = [1] X + [0] 816.51/297.04 >= [1] X + [0] 816.51/297.04 = [activate(X)] 816.51/297.04 816.51/297.04 [isNat(X)] = [1] X + [0] 816.51/297.04 >= [1] X + [0] 816.51/297.04 = [n__isNat(X)] 816.51/297.04 816.51/297.04 [isNat(n__0())] = [0] 816.51/297.04 >= [0] 816.51/297.04 = [tt()] 816.51/297.04 816.51/297.04 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [4] 816.51/297.04 > [1] V1 + [1] V2 + [0] 816.51/297.04 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 816.51/297.04 816.51/297.04 [isNat(n__s(V1))] = [1] V1 + [0] 816.51/297.04 >= [1] V1 + [0] 816.51/297.04 = [isNat(activate(V1))] 816.51/297.04 816.51/297.04 [0()] = [0] 816.51/297.04 >= [0] 816.51/297.04 = [n__0()] 816.51/297.04 816.51/297.04 816.51/297.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 816.51/297.04 816.51/297.04 We are left with following problem, upon which TcT provides the 816.51/297.04 certificate YES(O(1),O(n^2)). 816.51/297.04 816.51/297.04 Strict Trs: 816.51/297.04 { s(X) -> n__s(X) 816.51/297.04 , plus(X1, X2) -> n__plus(X1, X2) } 816.51/297.04 Weak Trs: 816.51/297.04 { U11(tt(), N) -> activate(N) 816.51/297.04 , activate(X) -> X 816.51/297.04 , activate(n__0()) -> 0() 816.51/297.04 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.04 , activate(n__isNat(X)) -> isNat(X) 816.51/297.04 , activate(n__s(X)) -> s(activate(X)) 816.51/297.04 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.04 , and(tt(), X) -> activate(X) 816.51/297.04 , isNat(X) -> n__isNat(X) 816.51/297.04 , isNat(n__0()) -> tt() 816.51/297.04 , isNat(n__plus(V1, V2)) -> 816.51/297.04 and(isNat(activate(V1)), n__isNat(activate(V2))) 816.51/297.04 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.04 , 0() -> n__0() } 816.51/297.04 Obligation: 816.51/297.04 innermost runtime complexity 816.51/297.04 Answer: 816.51/297.04 YES(O(1),O(n^2)) 816.51/297.04 816.51/297.04 We use the processor 'matrix interpretation of dimension 2' to 816.51/297.04 orient following rules strictly. 816.51/297.04 816.51/297.04 Trs: { s(X) -> n__s(X) } 816.51/297.04 816.51/297.04 The induced complexity on above rules (modulo remaining rules) is 816.51/297.04 YES(?,O(n^2)) . These rules are moved into the corresponding weak 816.51/297.04 component(s). 816.51/297.04 816.51/297.04 Sub-proof: 816.51/297.04 ---------- 816.51/297.04 The following argument positions are usable: 816.51/297.04 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2}, 816.51/297.04 Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 816.51/297.04 816.51/297.04 TcT has computed the following constructor-based matrix 816.51/297.04 interpretation satisfying not(EDA). 816.51/297.04 816.51/297.04 [U11](x1, x2) = [7 4] x1 + [7 7] x2 + [7] 816.51/297.04 [7 7] [7 7] [7] 816.51/297.04 816.51/297.04 [tt] = [0] 816.51/297.04 [0] 816.51/297.04 816.51/297.04 [activate](x1) = [1 1] x1 + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 816.51/297.04 [U21](x1, x2, x3) = [7 4] x1 + [7 7] x2 + [7 7] x3 + [7] 816.51/297.04 [7 7] [7 7] [7 7] [7] 816.51/297.04 816.51/297.04 [s](x1) = [1 1] x1 + [4] 816.51/297.04 [0 1] [4] 816.51/297.04 816.51/297.04 [plus](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 816.51/297.04 [0 1] [0 1] [0] 816.51/297.04 816.51/297.04 [and](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 816.51/297.04 [0 0] [0 2] [0] 816.51/297.04 816.51/297.04 [isNat](x1) = [1 0] x1 + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 816.51/297.04 [n__0] = [0] 816.51/297.04 [0] 816.51/297.04 816.51/297.04 [n__plus](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 816.51/297.04 [0 1] [0 1] [0] 816.51/297.04 816.51/297.04 [n__isNat](x1) = [1 0] x1 + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 816.51/297.04 [n__s](x1) = [1 1] x1 + [0] 816.51/297.04 [0 1] [4] 816.51/297.04 816.51/297.04 [0] = [0] 816.51/297.04 [0] 816.51/297.04 816.51/297.04 The order satisfies the following ordering constraints: 816.51/297.04 816.51/297.04 [U11(tt(), N)] = [7 7] N + [7] 816.51/297.04 [7 7] [7] 816.51/297.04 > [1 1] N + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 = [activate(N)] 816.51/297.04 816.51/297.04 [activate(X)] = [1 1] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 >= [1 0] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 = [X] 816.51/297.04 816.51/297.04 [activate(n__0())] = [0] 816.51/297.04 [0] 816.51/297.04 >= [0] 816.51/297.04 [0] 816.51/297.04 = [0()] 816.51/297.04 816.51/297.04 [activate(n__plus(X1, X2))] = [1 2] X1 + [1 2] X2 + [0] 816.51/297.04 [0 1] [0 1] [0] 816.51/297.04 >= [1 2] X1 + [1 2] X2 + [0] 816.51/297.04 [0 1] [0 1] [0] 816.51/297.04 = [plus(activate(X1), activate(X2))] 816.51/297.04 816.51/297.04 [activate(n__isNat(X))] = [1 0] X + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 >= [1 0] X + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 = [isNat(X)] 816.51/297.04 816.51/297.04 [activate(n__s(X))] = [1 2] X + [4] 816.51/297.04 [0 1] [4] 816.51/297.04 >= [1 2] X + [4] 816.51/297.04 [0 1] [4] 816.51/297.04 = [s(activate(X))] 816.51/297.04 816.51/297.04 [U21(tt(), M, N)] = [7 7] N + [7 7] M + [7] 816.51/297.04 [7 7] [7 7] [7] 816.51/297.04 > [1 3] N + [1 3] M + [4] 816.51/297.04 [0 1] [0 1] [4] 816.51/297.04 = [s(plus(activate(N), activate(M)))] 816.51/297.04 816.51/297.04 [s(X)] = [1 1] X + [4] 816.51/297.04 [0 1] [4] 816.51/297.04 > [1 1] X + [0] 816.51/297.04 [0 1] [4] 816.51/297.04 = [n__s(X)] 816.51/297.04 816.51/297.04 [plus(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 816.51/297.04 [0 1] [0 1] [0] 816.51/297.04 >= [1 1] X1 + [1 1] X2 + [0] 816.51/297.04 [0 1] [0 1] [0] 816.51/297.04 = [n__plus(X1, X2)] 816.51/297.04 816.51/297.04 [and(tt(), X)] = [1 1] X + [0] 816.51/297.04 [0 2] [0] 816.51/297.04 >= [1 1] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 = [activate(X)] 816.51/297.04 816.51/297.04 [isNat(X)] = [1 0] X + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 >= [1 0] X + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 = [n__isNat(X)] 816.51/297.04 816.51/297.04 [isNat(n__0())] = [0] 816.51/297.04 [0] 816.51/297.04 >= [0] 816.51/297.04 [0] 816.51/297.04 = [tt()] 816.51/297.04 816.51/297.04 [isNat(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [0] 816.51/297.04 [0 0] [0 0] [0] 816.51/297.04 >= [1 1] V1 + [1 1] V2 + [0] 816.51/297.04 [0 0] [0 0] [0] 816.51/297.04 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 816.51/297.04 816.51/297.04 [isNat(n__s(V1))] = [1 1] V1 + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 >= [1 1] V1 + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 = [isNat(activate(V1))] 816.51/297.04 816.51/297.04 [0()] = [0] 816.51/297.04 [0] 816.51/297.04 >= [0] 816.51/297.04 [0] 816.51/297.04 = [n__0()] 816.51/297.04 816.51/297.04 816.51/297.04 We return to the main proof. 816.51/297.04 816.51/297.04 We are left with following problem, upon which TcT provides the 816.51/297.04 certificate YES(O(1),O(n^2)). 816.51/297.04 816.51/297.04 Strict Trs: { plus(X1, X2) -> n__plus(X1, X2) } 816.51/297.04 Weak Trs: 816.51/297.04 { U11(tt(), N) -> activate(N) 816.51/297.04 , activate(X) -> X 816.51/297.04 , activate(n__0()) -> 0() 816.51/297.04 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.04 , activate(n__isNat(X)) -> isNat(X) 816.51/297.04 , activate(n__s(X)) -> s(activate(X)) 816.51/297.04 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.04 , s(X) -> n__s(X) 816.51/297.04 , and(tt(), X) -> activate(X) 816.51/297.04 , isNat(X) -> n__isNat(X) 816.51/297.04 , isNat(n__0()) -> tt() 816.51/297.04 , isNat(n__plus(V1, V2)) -> 816.51/297.04 and(isNat(activate(V1)), n__isNat(activate(V2))) 816.51/297.04 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.04 , 0() -> n__0() } 816.51/297.04 Obligation: 816.51/297.04 innermost runtime complexity 816.51/297.04 Answer: 816.51/297.04 YES(O(1),O(n^2)) 816.51/297.04 816.51/297.04 We use the processor 'matrix interpretation of dimension 2' to 816.51/297.04 orient following rules strictly. 816.51/297.04 816.51/297.04 Trs: { plus(X1, X2) -> n__plus(X1, X2) } 816.51/297.04 816.51/297.04 The induced complexity on above rules (modulo remaining rules) is 816.51/297.04 YES(?,O(n^2)) . These rules are moved into the corresponding weak 816.51/297.04 component(s). 816.51/297.04 816.51/297.04 Sub-proof: 816.51/297.04 ---------- 816.51/297.04 The following argument positions are usable: 816.51/297.04 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2}, 816.51/297.04 Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 816.51/297.04 816.51/297.04 TcT has computed the following constructor-based matrix 816.51/297.04 interpretation satisfying not(EDA). 816.51/297.04 816.51/297.04 [U11](x1, x2) = [0 4] x1 + [7 7] x2 + [7] 816.51/297.04 [0 7] [7 7] [7] 816.51/297.04 816.51/297.04 [tt] = [4] 816.51/297.04 [0] 816.51/297.04 816.51/297.04 [activate](x1) = [1 1] x1 + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 816.51/297.04 [U21](x1, x2, x3) = [2 4] x1 + [7 7] x2 + [7 7] x3 + [7] 816.51/297.04 [0 7] [7 7] [7 7] [7] 816.51/297.04 816.51/297.04 [s](x1) = [1 4] x1 + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 816.51/297.04 [plus](x1, x2) = [1 1] x1 + [1 1] x2 + [1] 816.51/297.04 [0 1] [0 1] [2] 816.51/297.04 816.51/297.04 [and](x1, x2) = [1 0] x1 + [1 2] x2 + [0] 816.51/297.04 [0 0] [0 4] [0] 816.51/297.04 816.51/297.04 [isNat](x1) = [1 0] x1 + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 816.51/297.04 [n__0] = [7] 816.51/297.04 [1] 816.51/297.04 816.51/297.04 [n__plus](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 816.51/297.04 [0 1] [0 1] [2] 816.51/297.04 816.51/297.04 [n__isNat](x1) = [1 0] x1 + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 816.51/297.04 [n__s](x1) = [1 4] x1 + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 816.51/297.04 [0] = [7] 816.51/297.04 [1] 816.51/297.04 816.51/297.04 The order satisfies the following ordering constraints: 816.51/297.04 816.51/297.04 [U11(tt(), N)] = [7 7] N + [7] 816.51/297.04 [7 7] [7] 816.51/297.04 > [1 1] N + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 = [activate(N)] 816.51/297.04 816.51/297.04 [activate(X)] = [1 1] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 >= [1 0] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 = [X] 816.51/297.04 816.51/297.04 [activate(n__0())] = [8] 816.51/297.04 [1] 816.51/297.04 > [7] 816.51/297.04 [1] 816.51/297.04 = [0()] 816.51/297.04 816.51/297.04 [activate(n__plus(X1, X2))] = [1 2] X1 + [1 2] X2 + [2] 816.51/297.04 [0 1] [0 1] [2] 816.51/297.04 > [1 2] X1 + [1 2] X2 + [1] 816.51/297.04 [0 1] [0 1] [2] 816.51/297.04 = [plus(activate(X1), activate(X2))] 816.51/297.04 816.51/297.04 [activate(n__isNat(X))] = [1 0] X + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 >= [1 0] X + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 = [isNat(X)] 816.51/297.04 816.51/297.04 [activate(n__s(X))] = [1 5] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 >= [1 5] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 = [s(activate(X))] 816.51/297.04 816.51/297.04 [U21(tt(), M, N)] = [7 7] N + [7 7] M + [15] 816.51/297.04 [7 7] [7 7] [7] 816.51/297.04 > [1 6] N + [1 6] M + [9] 816.51/297.04 [0 1] [0 1] [2] 816.51/297.04 = [s(plus(activate(N), activate(M)))] 816.51/297.04 816.51/297.04 [s(X)] = [1 4] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 >= [1 4] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 = [n__s(X)] 816.51/297.04 816.51/297.04 [plus(X1, X2)] = [1 1] X1 + [1 1] X2 + [1] 816.51/297.04 [0 1] [0 1] [2] 816.51/297.04 > [1 1] X1 + [1 1] X2 + [0] 816.51/297.04 [0 1] [0 1] [2] 816.51/297.04 = [n__plus(X1, X2)] 816.51/297.04 816.51/297.04 [and(tt(), X)] = [1 2] X + [4] 816.51/297.04 [0 4] [0] 816.51/297.04 > [1 1] X + [0] 816.51/297.04 [0 1] [0] 816.51/297.04 = [activate(X)] 816.51/297.04 816.51/297.04 [isNat(X)] = [1 0] X + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 >= [1 0] X + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 = [n__isNat(X)] 816.51/297.04 816.51/297.04 [isNat(n__0())] = [7] 816.51/297.04 [0] 816.51/297.04 > [4] 816.51/297.04 [0] 816.51/297.04 = [tt()] 816.51/297.04 816.51/297.04 [isNat(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [0] 816.51/297.04 [0 0] [0 0] [0] 816.51/297.04 >= [1 1] V1 + [1 1] V2 + [0] 816.51/297.04 [0 0] [0 0] [0] 816.51/297.04 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 816.51/297.04 816.51/297.04 [isNat(n__s(V1))] = [1 4] V1 + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 >= [1 1] V1 + [0] 816.51/297.04 [0 0] [0] 816.51/297.04 = [isNat(activate(V1))] 816.51/297.04 816.51/297.04 [0()] = [7] 816.51/297.04 [1] 816.51/297.04 >= [7] 816.51/297.04 [1] 816.51/297.04 = [n__0()] 816.51/297.04 816.51/297.04 816.51/297.04 We return to the main proof. 816.51/297.04 816.51/297.04 We are left with following problem, upon which TcT provides the 816.51/297.04 certificate YES(O(1),O(1)). 816.51/297.04 816.51/297.04 Weak Trs: 816.51/297.04 { U11(tt(), N) -> activate(N) 816.51/297.04 , activate(X) -> X 816.51/297.04 , activate(n__0()) -> 0() 816.51/297.04 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 816.51/297.04 , activate(n__isNat(X)) -> isNat(X) 816.51/297.04 , activate(n__s(X)) -> s(activate(X)) 816.51/297.04 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 816.51/297.04 , s(X) -> n__s(X) 816.51/297.04 , plus(X1, X2) -> n__plus(X1, X2) 816.51/297.04 , and(tt(), X) -> activate(X) 816.51/297.04 , isNat(X) -> n__isNat(X) 816.51/297.04 , isNat(n__0()) -> tt() 816.51/297.04 , isNat(n__plus(V1, V2)) -> 816.51/297.04 and(isNat(activate(V1)), n__isNat(activate(V2))) 816.51/297.04 , isNat(n__s(V1)) -> isNat(activate(V1)) 816.51/297.04 , 0() -> n__0() } 816.51/297.04 Obligation: 816.51/297.04 innermost runtime complexity 816.51/297.04 Answer: 816.51/297.04 YES(O(1),O(1)) 816.51/297.04 816.51/297.04 Empty rules are trivially bounded 816.51/297.04 816.51/297.04 Hurray, we answered YES(O(1),O(n^2)) 816.66/297.14 EOF