YES(O(1),O(n^2)) 744.65/297.05 YES(O(1),O(n^2)) 744.65/297.05 744.65/297.05 We are left with following problem, upon which TcT provides the 744.65/297.05 certificate YES(O(1),O(n^2)). 744.65/297.05 744.65/297.05 Strict Trs: 744.65/297.05 { U11(tt(), N) -> activate(N) 744.65/297.05 , activate(X) -> X 744.65/297.05 , activate(n__0()) -> 0() 744.65/297.05 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.05 , activate(n__isNat(X)) -> isNat(X) 744.65/297.05 , activate(n__s(X)) -> s(activate(X)) 744.65/297.05 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.05 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.05 , s(X) -> n__s(X) 744.65/297.05 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.05 , plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N) 744.65/297.05 , plus(N, 0()) -> U11(isNat(N), N) 744.65/297.05 , U31(tt()) -> 0() 744.65/297.05 , 0() -> n__0() 744.65/297.05 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.05 , x(X1, X2) -> n__x(X1, X2) 744.65/297.05 , x(N, s(M)) -> U41(and(isNat(M), n__isNat(N)), M, N) 744.65/297.05 , x(N, 0()) -> U31(isNat(N)) 744.65/297.05 , and(tt(), X) -> activate(X) 744.65/297.05 , isNat(X) -> n__isNat(X) 744.65/297.05 , isNat(n__0()) -> tt() 744.65/297.05 , isNat(n__plus(V1, V2)) -> 744.65/297.05 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.05 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.05 , isNat(n__x(V1, V2)) -> 744.65/297.05 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.05 Obligation: 744.65/297.05 innermost runtime complexity 744.65/297.05 Answer: 744.65/297.05 YES(O(1),O(n^2)) 744.65/297.05 744.65/297.05 Arguments of following rules are not normal-forms: 744.65/297.05 744.65/297.05 { plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N) 744.65/297.05 , plus(N, 0()) -> U11(isNat(N), N) 744.65/297.05 , x(N, s(M)) -> U41(and(isNat(M), n__isNat(N)), M, N) 744.65/297.05 , x(N, 0()) -> U31(isNat(N)) } 744.65/297.05 744.65/297.05 All above mentioned rules can be savely removed. 744.65/297.05 744.65/297.05 We are left with following problem, upon which TcT provides the 744.65/297.05 certificate YES(O(1),O(n^2)). 744.65/297.05 744.65/297.05 Strict Trs: 744.65/297.05 { U11(tt(), N) -> activate(N) 744.65/297.05 , activate(X) -> X 744.65/297.05 , activate(n__0()) -> 0() 744.65/297.05 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.05 , activate(n__isNat(X)) -> isNat(X) 744.65/297.05 , activate(n__s(X)) -> s(activate(X)) 744.65/297.05 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.05 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.05 , s(X) -> n__s(X) 744.65/297.05 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.05 , U31(tt()) -> 0() 744.65/297.05 , 0() -> n__0() 744.65/297.05 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.05 , x(X1, X2) -> n__x(X1, X2) 744.65/297.05 , and(tt(), X) -> activate(X) 744.65/297.05 , isNat(X) -> n__isNat(X) 744.65/297.05 , isNat(n__0()) -> tt() 744.65/297.05 , isNat(n__plus(V1, V2)) -> 744.65/297.05 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.05 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.05 , isNat(n__x(V1, V2)) -> 744.65/297.05 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.05 Obligation: 744.65/297.05 innermost runtime complexity 744.65/297.05 Answer: 744.65/297.05 YES(O(1),O(n^2)) 744.65/297.05 744.65/297.05 We use the processor 'matrix interpretation of dimension 1' to 744.65/297.05 orient following rules strictly. 744.65/297.05 744.65/297.05 Trs: 744.65/297.05 { U11(tt(), N) -> activate(N) 744.65/297.05 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.05 , U31(tt()) -> 0() 744.65/297.05 , U41(tt(), M, N) -> 744.65/297.05 plus(x(activate(N), activate(M)), activate(N)) } 744.65/297.05 744.65/297.05 The induced complexity on above rules (modulo remaining rules) is 744.65/297.05 YES(?,O(n^1)) . These rules are moved into the corresponding weak 744.65/297.05 component(s). 744.65/297.05 744.65/297.05 Sub-proof: 744.65/297.05 ---------- 744.65/297.05 The following argument positions are usable: 744.65/297.05 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.05 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.05 744.65/297.05 TcT has computed the following constructor-based matrix 744.65/297.05 interpretation satisfying not(EDA). 744.65/297.05 744.65/297.05 [U11](x1, x2) = [7] x1 + [7] x2 + [7] 744.65/297.05 744.65/297.05 [tt] = [0] 744.65/297.05 744.65/297.05 [activate](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [U21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.05 744.65/297.05 [s](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.05 744.65/297.05 [U31](x1) = [7] x1 + [7] 744.65/297.05 744.65/297.05 [0] = [0] 744.65/297.05 744.65/297.05 [U41](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.05 744.65/297.05 [x](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.05 744.65/297.05 [and](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.05 744.65/297.05 [isNat](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [n__0] = [0] 744.65/297.05 744.65/297.05 [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.05 744.65/297.05 [n__isNat](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [n__s](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [n__x](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.05 744.65/297.05 The order satisfies the following ordering constraints: 744.65/297.05 744.65/297.05 [U11(tt(), N)] = [7] N + [7] 744.65/297.05 > [1] N + [0] 744.65/297.05 = [activate(N)] 744.65/297.05 744.65/297.05 [activate(X)] = [1] X + [0] 744.65/297.05 >= [1] X + [0] 744.65/297.05 = [X] 744.65/297.05 744.65/297.05 [activate(n__0())] = [0] 744.65/297.05 >= [0] 744.65/297.05 = [0()] 744.65/297.05 744.65/297.05 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] 744.65/297.05 >= [1] X1 + [1] X2 + [0] 744.65/297.05 = [plus(activate(X1), activate(X2))] 744.65/297.05 744.65/297.05 [activate(n__isNat(X))] = [1] X + [0] 744.65/297.05 >= [1] X + [0] 744.65/297.05 = [isNat(X)] 744.65/297.05 744.65/297.05 [activate(n__s(X))] = [1] X + [0] 744.65/297.05 >= [1] X + [0] 744.65/297.05 = [s(activate(X))] 744.65/297.05 744.65/297.05 [activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [0] 744.65/297.05 >= [1] X1 + [1] X2 + [0] 744.65/297.05 = [x(activate(X1), activate(X2))] 744.65/297.05 744.65/297.05 [U21(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.05 > [1] N + [1] M + [0] 744.65/297.05 = [s(plus(activate(N), activate(M)))] 744.65/297.05 744.65/297.05 [s(X)] = [1] X + [0] 744.65/297.05 >= [1] X + [0] 744.65/297.05 = [n__s(X)] 744.65/297.05 744.65/297.05 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 744.65/297.05 >= [1] X1 + [1] X2 + [0] 744.65/297.05 = [n__plus(X1, X2)] 744.65/297.05 744.65/297.05 [U31(tt())] = [7] 744.65/297.05 > [0] 744.65/297.05 = [0()] 744.65/297.05 744.65/297.05 [0()] = [0] 744.65/297.05 >= [0] 744.65/297.05 = [n__0()] 744.65/297.05 744.65/297.05 [U41(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.05 > [2] N + [1] M + [0] 744.65/297.05 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.05 744.65/297.05 [x(X1, X2)] = [1] X1 + [1] X2 + [0] 744.65/297.05 >= [1] X1 + [1] X2 + [0] 744.65/297.05 = [n__x(X1, X2)] 744.65/297.05 744.65/297.05 [and(tt(), X)] = [1] X + [0] 744.65/297.05 >= [1] X + [0] 744.65/297.05 = [activate(X)] 744.65/297.05 744.65/297.05 [isNat(X)] = [1] X + [0] 744.65/297.05 >= [1] X + [0] 744.65/297.05 = [n__isNat(X)] 744.65/297.05 744.65/297.05 [isNat(n__0())] = [0] 744.65/297.05 >= [0] 744.65/297.05 = [tt()] 744.65/297.05 744.65/297.05 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [0] 744.65/297.05 >= [1] V1 + [1] V2 + [0] 744.65/297.05 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.05 744.65/297.05 [isNat(n__s(V1))] = [1] V1 + [0] 744.65/297.05 >= [1] V1 + [0] 744.65/297.05 = [isNat(activate(V1))] 744.65/297.05 744.65/297.05 [isNat(n__x(V1, V2))] = [1] V1 + [1] V2 + [0] 744.65/297.05 >= [1] V1 + [1] V2 + [0] 744.65/297.05 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.05 744.65/297.05 744.65/297.05 We return to the main proof. 744.65/297.05 744.65/297.05 We are left with following problem, upon which TcT provides the 744.65/297.05 certificate YES(O(1),O(n^2)). 744.65/297.05 744.65/297.05 Strict Trs: 744.65/297.05 { activate(X) -> X 744.65/297.05 , activate(n__0()) -> 0() 744.65/297.05 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.05 , activate(n__isNat(X)) -> isNat(X) 744.65/297.05 , activate(n__s(X)) -> s(activate(X)) 744.65/297.05 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.05 , s(X) -> n__s(X) 744.65/297.05 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.05 , 0() -> n__0() 744.65/297.05 , x(X1, X2) -> n__x(X1, X2) 744.65/297.05 , and(tt(), X) -> activate(X) 744.65/297.05 , isNat(X) -> n__isNat(X) 744.65/297.05 , isNat(n__0()) -> tt() 744.65/297.05 , isNat(n__plus(V1, V2)) -> 744.65/297.05 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.05 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.05 , isNat(n__x(V1, V2)) -> 744.65/297.05 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.05 Weak Trs: 744.65/297.05 { U11(tt(), N) -> activate(N) 744.65/297.05 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.05 , U31(tt()) -> 0() 744.65/297.05 , U41(tt(), M, N) -> 744.65/297.05 plus(x(activate(N), activate(M)), activate(N)) } 744.65/297.05 Obligation: 744.65/297.05 innermost runtime complexity 744.65/297.05 Answer: 744.65/297.05 YES(O(1),O(n^2)) 744.65/297.05 744.65/297.05 We use the processor 'matrix interpretation of dimension 1' to 744.65/297.05 orient following rules strictly. 744.65/297.05 744.65/297.05 Trs: 744.65/297.05 { isNat(n__x(V1, V2)) -> 744.65/297.05 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.05 744.65/297.05 The induced complexity on above rules (modulo remaining rules) is 744.65/297.05 YES(?,O(n^1)) . These rules are moved into the corresponding weak 744.65/297.05 component(s). 744.65/297.05 744.65/297.05 Sub-proof: 744.65/297.05 ---------- 744.65/297.05 The following argument positions are usable: 744.65/297.05 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.05 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.05 744.65/297.05 TcT has computed the following constructor-based matrix 744.65/297.05 interpretation satisfying not(EDA). 744.65/297.05 744.65/297.05 [U11](x1, x2) = [7] x1 + [7] x2 + [7] 744.65/297.05 744.65/297.05 [tt] = [0] 744.65/297.05 744.65/297.05 [activate](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [U21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [3] 744.65/297.05 744.65/297.05 [s](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.05 744.65/297.05 [U31](x1) = [7] x1 + [7] 744.65/297.05 744.65/297.05 [0] = [0] 744.65/297.05 744.65/297.05 [U41](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.05 744.65/297.05 [x](x1, x2) = [1] x1 + [1] x2 + [1] 744.65/297.05 744.65/297.05 [and](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.05 744.65/297.05 [isNat](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [n__0] = [0] 744.65/297.05 744.65/297.05 [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.05 744.65/297.05 [n__isNat](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [n__s](x1) = [1] x1 + [0] 744.65/297.05 744.65/297.05 [n__x](x1, x2) = [1] x1 + [1] x2 + [1] 744.65/297.05 744.65/297.05 The order satisfies the following ordering constraints: 744.65/297.05 744.65/297.05 [U11(tt(), N)] = [7] N + [7] 744.65/297.05 > [1] N + [0] 744.65/297.05 = [activate(N)] 744.65/297.05 744.65/297.05 [activate(X)] = [1] X + [0] 744.65/297.05 >= [1] X + [0] 744.65/297.05 = [X] 744.65/297.05 744.65/297.06 [activate(n__0())] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [plus(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [activate(n__isNat(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [isNat(X)] 744.65/297.06 744.65/297.06 [activate(n__s(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [s(activate(X))] 744.65/297.06 744.65/297.06 [activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [1] 744.65/297.06 >= [1] X1 + [1] X2 + [1] 744.65/297.06 = [x(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [U21(tt(), M, N)] = [7] N + [7] M + [3] 744.65/297.06 > [1] N + [1] M + [0] 744.65/297.06 = [s(plus(activate(N), activate(M)))] 744.65/297.06 744.65/297.06 [s(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__s(X)] 744.65/297.06 744.65/297.06 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [n__plus(X1, X2)] 744.65/297.06 744.65/297.06 [U31(tt())] = [7] 744.65/297.06 > [0] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [0()] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [n__0()] 744.65/297.06 744.65/297.06 [U41(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.06 > [2] N + [1] M + [1] 744.65/297.06 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.06 744.65/297.06 [x(X1, X2)] = [1] X1 + [1] X2 + [1] 744.65/297.06 >= [1] X1 + [1] X2 + [1] 744.65/297.06 = [n__x(X1, X2)] 744.65/297.06 744.65/297.06 [and(tt(), X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [activate(X)] 744.65/297.06 744.65/297.06 [isNat(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__isNat(X)] 744.65/297.06 744.65/297.06 [isNat(n__0())] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [tt()] 744.65/297.06 744.65/297.06 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [0] 744.65/297.06 >= [1] V1 + [1] V2 + [0] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 [isNat(n__s(V1))] = [1] V1 + [0] 744.65/297.06 >= [1] V1 + [0] 744.65/297.06 = [isNat(activate(V1))] 744.65/297.06 744.65/297.06 [isNat(n__x(V1, V2))] = [1] V1 + [1] V2 + [1] 744.65/297.06 > [1] V1 + [1] V2 + [0] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 744.65/297.06 We return to the main proof. 744.65/297.06 744.65/297.06 We are left with following problem, upon which TcT provides the 744.65/297.06 certificate YES(O(1),O(n^2)). 744.65/297.06 744.65/297.06 Strict Trs: 744.65/297.06 { activate(X) -> X 744.65/297.06 , activate(n__0()) -> 0() 744.65/297.06 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.06 , activate(n__isNat(X)) -> isNat(X) 744.65/297.06 , activate(n__s(X)) -> s(activate(X)) 744.65/297.06 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.06 , s(X) -> n__s(X) 744.65/297.06 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.06 , 0() -> n__0() 744.65/297.06 , x(X1, X2) -> n__x(X1, X2) 744.65/297.06 , and(tt(), X) -> activate(X) 744.65/297.06 , isNat(X) -> n__isNat(X) 744.65/297.06 , isNat(n__0()) -> tt() 744.65/297.06 , isNat(n__plus(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.06 , isNat(n__s(V1)) -> isNat(activate(V1)) } 744.65/297.06 Weak Trs: 744.65/297.06 { U11(tt(), N) -> activate(N) 744.65/297.06 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.06 , U31(tt()) -> 0() 744.65/297.06 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.06 , isNat(n__x(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.06 Obligation: 744.65/297.06 innermost runtime complexity 744.65/297.06 Answer: 744.65/297.06 YES(O(1),O(n^2)) 744.65/297.06 744.65/297.06 We use the processor 'matrix interpretation of dimension 1' to 744.65/297.06 orient following rules strictly. 744.65/297.06 744.65/297.06 Trs: { and(tt(), X) -> activate(X) } 744.65/297.06 744.65/297.06 The induced complexity on above rules (modulo remaining rules) is 744.65/297.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 744.65/297.06 component(s). 744.65/297.06 744.65/297.06 Sub-proof: 744.65/297.06 ---------- 744.65/297.06 The following argument positions are usable: 744.65/297.06 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.06 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.06 744.65/297.06 TcT has computed the following constructor-based matrix 744.65/297.06 interpretation satisfying not(EDA). 744.65/297.06 744.65/297.06 [U11](x1, x2) = [7] x1 + [7] x2 + [7] 744.65/297.06 744.65/297.06 [tt] = [0] 744.65/297.06 744.65/297.06 [activate](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [U21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [3] 744.65/297.06 744.65/297.06 [s](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [plus](x1, x2) = [1] x1 + [1] x2 + [1] 744.65/297.06 744.65/297.06 [U31](x1) = [7] x1 + [7] 744.65/297.06 744.65/297.06 [0] = [0] 744.65/297.06 744.65/297.06 [U41](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.06 744.65/297.06 [x](x1, x2) = [1] x1 + [1] x2 + [1] 744.65/297.06 744.65/297.06 [and](x1, x2) = [1] x1 + [1] x2 + [1] 744.65/297.06 744.65/297.06 [isNat](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__0] = [0] 744.65/297.06 744.65/297.06 [n__plus](x1, x2) = [1] x1 + [1] x2 + [1] 744.65/297.06 744.65/297.06 [n__isNat](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__s](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__x](x1, x2) = [1] x1 + [1] x2 + [1] 744.65/297.06 744.65/297.06 The order satisfies the following ordering constraints: 744.65/297.06 744.65/297.06 [U11(tt(), N)] = [7] N + [7] 744.65/297.06 > [1] N + [0] 744.65/297.06 = [activate(N)] 744.65/297.06 744.65/297.06 [activate(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [X] 744.65/297.06 744.65/297.06 [activate(n__0())] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [1] 744.65/297.06 >= [1] X1 + [1] X2 + [1] 744.65/297.06 = [plus(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [activate(n__isNat(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [isNat(X)] 744.65/297.06 744.65/297.06 [activate(n__s(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [s(activate(X))] 744.65/297.06 744.65/297.06 [activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [1] 744.65/297.06 >= [1] X1 + [1] X2 + [1] 744.65/297.06 = [x(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [U21(tt(), M, N)] = [7] N + [7] M + [3] 744.65/297.06 > [1] N + [1] M + [1] 744.65/297.06 = [s(plus(activate(N), activate(M)))] 744.65/297.06 744.65/297.06 [s(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__s(X)] 744.65/297.06 744.65/297.06 [plus(X1, X2)] = [1] X1 + [1] X2 + [1] 744.65/297.06 >= [1] X1 + [1] X2 + [1] 744.65/297.06 = [n__plus(X1, X2)] 744.65/297.06 744.65/297.06 [U31(tt())] = [7] 744.65/297.06 > [0] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [0()] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [n__0()] 744.65/297.06 744.65/297.06 [U41(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.06 > [2] N + [1] M + [2] 744.65/297.06 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.06 744.65/297.06 [x(X1, X2)] = [1] X1 + [1] X2 + [1] 744.65/297.06 >= [1] X1 + [1] X2 + [1] 744.65/297.06 = [n__x(X1, X2)] 744.65/297.06 744.65/297.06 [and(tt(), X)] = [1] X + [1] 744.65/297.06 > [1] X + [0] 744.65/297.06 = [activate(X)] 744.65/297.06 744.65/297.06 [isNat(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__isNat(X)] 744.65/297.06 744.65/297.06 [isNat(n__0())] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [tt()] 744.65/297.06 744.65/297.06 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [1] 744.65/297.06 >= [1] V1 + [1] V2 + [1] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 [isNat(n__s(V1))] = [1] V1 + [0] 744.65/297.06 >= [1] V1 + [0] 744.65/297.06 = [isNat(activate(V1))] 744.65/297.06 744.65/297.06 [isNat(n__x(V1, V2))] = [1] V1 + [1] V2 + [1] 744.65/297.06 >= [1] V1 + [1] V2 + [1] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 744.65/297.06 We return to the main proof. 744.65/297.06 744.65/297.06 We are left with following problem, upon which TcT provides the 744.65/297.06 certificate YES(O(1),O(n^2)). 744.65/297.06 744.65/297.06 Strict Trs: 744.65/297.06 { activate(X) -> X 744.65/297.06 , activate(n__0()) -> 0() 744.65/297.06 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.06 , activate(n__isNat(X)) -> isNat(X) 744.65/297.06 , activate(n__s(X)) -> s(activate(X)) 744.65/297.06 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.06 , s(X) -> n__s(X) 744.65/297.06 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.06 , 0() -> n__0() 744.65/297.06 , x(X1, X2) -> n__x(X1, X2) 744.65/297.06 , isNat(X) -> n__isNat(X) 744.65/297.06 , isNat(n__0()) -> tt() 744.65/297.06 , isNat(n__plus(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.06 , isNat(n__s(V1)) -> isNat(activate(V1)) } 744.65/297.06 Weak Trs: 744.65/297.06 { U11(tt(), N) -> activate(N) 744.65/297.06 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.06 , U31(tt()) -> 0() 744.65/297.06 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.06 , and(tt(), X) -> activate(X) 744.65/297.06 , isNat(n__x(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.06 Obligation: 744.65/297.06 innermost runtime complexity 744.65/297.06 Answer: 744.65/297.06 YES(O(1),O(n^2)) 744.65/297.06 744.65/297.06 We use the processor 'matrix interpretation of dimension 1' to 744.65/297.06 orient following rules strictly. 744.65/297.06 744.65/297.06 Trs: { isNat(n__s(V1)) -> isNat(activate(V1)) } 744.65/297.06 744.65/297.06 The induced complexity on above rules (modulo remaining rules) is 744.65/297.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 744.65/297.06 component(s). 744.65/297.06 744.65/297.06 Sub-proof: 744.65/297.06 ---------- 744.65/297.06 The following argument positions are usable: 744.65/297.06 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.06 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.06 744.65/297.06 TcT has computed the following constructor-based matrix 744.65/297.06 interpretation satisfying not(EDA). 744.65/297.06 744.65/297.06 [U11](x1, x2) = [7] x1 + [7] x2 + [7] 744.65/297.06 744.65/297.06 [tt] = [0] 744.65/297.06 744.65/297.06 [activate](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [U21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.06 744.65/297.06 [s](x1) = [1] x1 + [1] 744.65/297.06 744.65/297.06 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [U31](x1) = [7] x1 + [7] 744.65/297.06 744.65/297.06 [0] = [0] 744.65/297.06 744.65/297.06 [U41](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [3] 744.65/297.06 744.65/297.06 [x](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [and](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [isNat](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__0] = [0] 744.65/297.06 744.65/297.06 [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [n__isNat](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__s](x1) = [1] x1 + [1] 744.65/297.06 744.65/297.06 [n__x](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 The order satisfies the following ordering constraints: 744.65/297.06 744.65/297.06 [U11(tt(), N)] = [7] N + [7] 744.65/297.06 > [1] N + [0] 744.65/297.06 = [activate(N)] 744.65/297.06 744.65/297.06 [activate(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [X] 744.65/297.06 744.65/297.06 [activate(n__0())] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [plus(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [activate(n__isNat(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [isNat(X)] 744.65/297.06 744.65/297.06 [activate(n__s(X))] = [1] X + [1] 744.65/297.06 >= [1] X + [1] 744.65/297.06 = [s(activate(X))] 744.65/297.06 744.65/297.06 [activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [x(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [U21(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.06 > [1] N + [1] M + [1] 744.65/297.06 = [s(plus(activate(N), activate(M)))] 744.65/297.06 744.65/297.06 [s(X)] = [1] X + [1] 744.65/297.06 >= [1] X + [1] 744.65/297.06 = [n__s(X)] 744.65/297.06 744.65/297.06 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [n__plus(X1, X2)] 744.65/297.06 744.65/297.06 [U31(tt())] = [7] 744.65/297.06 > [0] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [0()] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [n__0()] 744.65/297.06 744.65/297.06 [U41(tt(), M, N)] = [7] N + [7] M + [3] 744.65/297.06 > [2] N + [1] M + [0] 744.65/297.06 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.06 744.65/297.06 [x(X1, X2)] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [n__x(X1, X2)] 744.65/297.06 744.65/297.06 [and(tt(), X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [activate(X)] 744.65/297.06 744.65/297.06 [isNat(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__isNat(X)] 744.65/297.06 744.65/297.06 [isNat(n__0())] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [tt()] 744.65/297.06 744.65/297.06 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [0] 744.65/297.06 >= [1] V1 + [1] V2 + [0] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 [isNat(n__s(V1))] = [1] V1 + [1] 744.65/297.06 > [1] V1 + [0] 744.65/297.06 = [isNat(activate(V1))] 744.65/297.06 744.65/297.06 [isNat(n__x(V1, V2))] = [1] V1 + [1] V2 + [0] 744.65/297.06 >= [1] V1 + [1] V2 + [0] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 744.65/297.06 We return to the main proof. 744.65/297.06 744.65/297.06 We are left with following problem, upon which TcT provides the 744.65/297.06 certificate YES(O(1),O(n^2)). 744.65/297.06 744.65/297.06 Strict Trs: 744.65/297.06 { activate(X) -> X 744.65/297.06 , activate(n__0()) -> 0() 744.65/297.06 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.06 , activate(n__isNat(X)) -> isNat(X) 744.65/297.06 , activate(n__s(X)) -> s(activate(X)) 744.65/297.06 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.06 , s(X) -> n__s(X) 744.65/297.06 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.06 , 0() -> n__0() 744.65/297.06 , x(X1, X2) -> n__x(X1, X2) 744.65/297.06 , isNat(X) -> n__isNat(X) 744.65/297.06 , isNat(n__0()) -> tt() 744.65/297.06 , isNat(n__plus(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.06 Weak Trs: 744.65/297.06 { U11(tt(), N) -> activate(N) 744.65/297.06 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.06 , U31(tt()) -> 0() 744.65/297.06 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.06 , and(tt(), X) -> activate(X) 744.65/297.06 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.06 , isNat(n__x(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.06 Obligation: 744.65/297.06 innermost runtime complexity 744.65/297.06 Answer: 744.65/297.06 YES(O(1),O(n^2)) 744.65/297.06 744.65/297.06 We use the processor 'matrix interpretation of dimension 1' to 744.65/297.06 orient following rules strictly. 744.65/297.06 744.65/297.06 Trs: 744.65/297.06 { isNat(n__plus(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.06 744.65/297.06 The induced complexity on above rules (modulo remaining rules) is 744.65/297.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 744.65/297.06 component(s). 744.65/297.06 744.65/297.06 Sub-proof: 744.65/297.06 ---------- 744.65/297.06 The following argument positions are usable: 744.65/297.06 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.06 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.06 744.65/297.06 TcT has computed the following constructor-based matrix 744.65/297.06 interpretation satisfying not(EDA). 744.65/297.06 744.65/297.06 [U11](x1, x2) = [7] x1 + [7] x2 + [7] 744.65/297.06 744.65/297.06 [tt] = [0] 744.65/297.06 744.65/297.06 [activate](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [U21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.06 744.65/297.06 [s](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [plus](x1, x2) = [1] x1 + [1] x2 + [4] 744.65/297.06 744.65/297.06 [U31](x1) = [7] x1 + [7] 744.65/297.06 744.65/297.06 [0] = [0] 744.65/297.06 744.65/297.06 [U41](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.06 744.65/297.06 [x](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [and](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [isNat](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__0] = [0] 744.65/297.06 744.65/297.06 [n__plus](x1, x2) = [1] x1 + [1] x2 + [4] 744.65/297.06 744.65/297.06 [n__isNat](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__s](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__x](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 The order satisfies the following ordering constraints: 744.65/297.06 744.65/297.06 [U11(tt(), N)] = [7] N + [7] 744.65/297.06 > [1] N + [0] 744.65/297.06 = [activate(N)] 744.65/297.06 744.65/297.06 [activate(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [X] 744.65/297.06 744.65/297.06 [activate(n__0())] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [4] 744.65/297.06 >= [1] X1 + [1] X2 + [4] 744.65/297.06 = [plus(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [activate(n__isNat(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [isNat(X)] 744.65/297.06 744.65/297.06 [activate(n__s(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [s(activate(X))] 744.65/297.06 744.65/297.06 [activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [x(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [U21(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.06 > [1] N + [1] M + [4] 744.65/297.06 = [s(plus(activate(N), activate(M)))] 744.65/297.06 744.65/297.06 [s(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__s(X)] 744.65/297.06 744.65/297.06 [plus(X1, X2)] = [1] X1 + [1] X2 + [4] 744.65/297.06 >= [1] X1 + [1] X2 + [4] 744.65/297.06 = [n__plus(X1, X2)] 744.65/297.06 744.65/297.06 [U31(tt())] = [7] 744.65/297.06 > [0] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [0()] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [n__0()] 744.65/297.06 744.65/297.06 [U41(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.06 > [2] N + [1] M + [4] 744.65/297.06 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.06 744.65/297.06 [x(X1, X2)] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [n__x(X1, X2)] 744.65/297.06 744.65/297.06 [and(tt(), X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [activate(X)] 744.65/297.06 744.65/297.06 [isNat(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__isNat(X)] 744.65/297.06 744.65/297.06 [isNat(n__0())] = [0] 744.65/297.06 >= [0] 744.65/297.06 = [tt()] 744.65/297.06 744.65/297.06 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [4] 744.65/297.06 > [1] V1 + [1] V2 + [0] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 [isNat(n__s(V1))] = [1] V1 + [0] 744.65/297.06 >= [1] V1 + [0] 744.65/297.06 = [isNat(activate(V1))] 744.65/297.06 744.65/297.06 [isNat(n__x(V1, V2))] = [1] V1 + [1] V2 + [0] 744.65/297.06 >= [1] V1 + [1] V2 + [0] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 744.65/297.06 We return to the main proof. 744.65/297.06 744.65/297.06 We are left with following problem, upon which TcT provides the 744.65/297.06 certificate YES(O(1),O(n^2)). 744.65/297.06 744.65/297.06 Strict Trs: 744.65/297.06 { activate(X) -> X 744.65/297.06 , activate(n__0()) -> 0() 744.65/297.06 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.06 , activate(n__isNat(X)) -> isNat(X) 744.65/297.06 , activate(n__s(X)) -> s(activate(X)) 744.65/297.06 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.06 , s(X) -> n__s(X) 744.65/297.06 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.06 , 0() -> n__0() 744.65/297.06 , x(X1, X2) -> n__x(X1, X2) 744.65/297.06 , isNat(X) -> n__isNat(X) 744.65/297.06 , isNat(n__0()) -> tt() } 744.65/297.06 Weak Trs: 744.65/297.06 { U11(tt(), N) -> activate(N) 744.65/297.06 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.06 , U31(tt()) -> 0() 744.65/297.06 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.06 , and(tt(), X) -> activate(X) 744.65/297.06 , isNat(n__plus(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.06 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.06 , isNat(n__x(V1, V2)) -> 744.65/297.06 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.06 Obligation: 744.65/297.06 innermost runtime complexity 744.65/297.06 Answer: 744.65/297.06 YES(O(1),O(n^2)) 744.65/297.06 744.65/297.06 We use the processor 'matrix interpretation of dimension 1' to 744.65/297.06 orient following rules strictly. 744.65/297.06 744.65/297.06 Trs: { isNat(n__0()) -> tt() } 744.65/297.06 744.65/297.06 The induced complexity on above rules (modulo remaining rules) is 744.65/297.06 YES(?,O(n^1)) . These rules are moved into the corresponding weak 744.65/297.06 component(s). 744.65/297.06 744.65/297.06 Sub-proof: 744.65/297.06 ---------- 744.65/297.06 The following argument positions are usable: 744.65/297.06 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.06 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.06 744.65/297.06 TcT has computed the following constructor-based matrix 744.65/297.06 interpretation satisfying not(EDA). 744.65/297.06 744.65/297.06 [U11](x1, x2) = [7] x1 + [7] x2 + [7] 744.65/297.06 744.65/297.06 [tt] = [0] 744.65/297.06 744.65/297.06 [activate](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [U21](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.06 744.65/297.06 [s](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [U31](x1) = [7] x1 + [7] 744.65/297.06 744.65/297.06 [0] = [1] 744.65/297.06 744.65/297.06 [U41](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [7] 744.65/297.06 744.65/297.06 [x](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [and](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [isNat](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__0] = [1] 744.65/297.06 744.65/297.06 [n__plus](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 [n__isNat](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__s](x1) = [1] x1 + [0] 744.65/297.06 744.65/297.06 [n__x](x1, x2) = [1] x1 + [1] x2 + [0] 744.65/297.06 744.65/297.06 The order satisfies the following ordering constraints: 744.65/297.06 744.65/297.06 [U11(tt(), N)] = [7] N + [7] 744.65/297.06 > [1] N + [0] 744.65/297.06 = [activate(N)] 744.65/297.06 744.65/297.06 [activate(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [X] 744.65/297.06 744.65/297.06 [activate(n__0())] = [1] 744.65/297.06 >= [1] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [activate(n__plus(X1, X2))] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [plus(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [activate(n__isNat(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [isNat(X)] 744.65/297.06 744.65/297.06 [activate(n__s(X))] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [s(activate(X))] 744.65/297.06 744.65/297.06 [activate(n__x(X1, X2))] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [x(activate(X1), activate(X2))] 744.65/297.06 744.65/297.06 [U21(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.06 > [1] N + [1] M + [0] 744.65/297.06 = [s(plus(activate(N), activate(M)))] 744.65/297.06 744.65/297.06 [s(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__s(X)] 744.65/297.06 744.65/297.06 [plus(X1, X2)] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [n__plus(X1, X2)] 744.65/297.06 744.65/297.06 [U31(tt())] = [7] 744.65/297.06 > [1] 744.65/297.06 = [0()] 744.65/297.06 744.65/297.06 [0()] = [1] 744.65/297.06 >= [1] 744.65/297.06 = [n__0()] 744.65/297.06 744.65/297.06 [U41(tt(), M, N)] = [7] N + [7] M + [7] 744.65/297.06 > [2] N + [1] M + [0] 744.65/297.06 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.06 744.65/297.06 [x(X1, X2)] = [1] X1 + [1] X2 + [0] 744.65/297.06 >= [1] X1 + [1] X2 + [0] 744.65/297.06 = [n__x(X1, X2)] 744.65/297.06 744.65/297.06 [and(tt(), X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [activate(X)] 744.65/297.06 744.65/297.06 [isNat(X)] = [1] X + [0] 744.65/297.06 >= [1] X + [0] 744.65/297.06 = [n__isNat(X)] 744.65/297.06 744.65/297.06 [isNat(n__0())] = [1] 744.65/297.06 > [0] 744.65/297.06 = [tt()] 744.65/297.06 744.65/297.06 [isNat(n__plus(V1, V2))] = [1] V1 + [1] V2 + [0] 744.65/297.06 >= [1] V1 + [1] V2 + [0] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 [isNat(n__s(V1))] = [1] V1 + [0] 744.65/297.06 >= [1] V1 + [0] 744.65/297.06 = [isNat(activate(V1))] 744.65/297.06 744.65/297.06 [isNat(n__x(V1, V2))] = [1] V1 + [1] V2 + [0] 744.65/297.06 >= [1] V1 + [1] V2 + [0] 744.65/297.06 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.06 744.65/297.06 744.65/297.06 We return to the main proof. 744.65/297.06 744.65/297.06 We are left with following problem, upon which TcT provides the 744.65/297.06 certificate YES(O(1),O(n^2)). 744.65/297.06 744.65/297.06 Strict Trs: 744.65/297.06 { activate(X) -> X 744.65/297.06 , activate(n__0()) -> 0() 744.65/297.06 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.06 , activate(n__isNat(X)) -> isNat(X) 744.65/297.06 , activate(n__s(X)) -> s(activate(X)) 744.65/297.06 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.06 , s(X) -> n__s(X) 744.65/297.06 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.06 , 0() -> n__0() 744.65/297.06 , x(X1, X2) -> n__x(X1, X2) 744.65/297.06 , isNat(X) -> n__isNat(X) } 744.65/297.06 Weak Trs: 744.65/297.06 { U11(tt(), N) -> activate(N) 744.65/297.06 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.06 , U31(tt()) -> 0() 744.65/297.06 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.07 , and(tt(), X) -> activate(X) 744.65/297.07 , isNat(n__0()) -> tt() 744.65/297.07 , isNat(n__plus(V1, V2)) -> 744.65/297.07 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.07 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.07 , isNat(n__x(V1, V2)) -> 744.65/297.07 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.07 Obligation: 744.65/297.07 innermost runtime complexity 744.65/297.07 Answer: 744.65/297.07 YES(O(1),O(n^2)) 744.65/297.07 744.65/297.07 We use the processor 'matrix interpretation of dimension 2' to 744.65/297.07 orient following rules strictly. 744.65/297.07 744.65/297.07 Trs: 744.65/297.07 { activate(n__0()) -> 0() 744.65/297.07 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.07 , activate(n__s(X)) -> s(activate(X)) 744.65/297.07 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.07 , s(X) -> n__s(X) 744.65/297.07 , 0() -> n__0() 744.65/297.07 , x(X1, X2) -> n__x(X1, X2) } 744.65/297.07 744.65/297.07 The induced complexity on above rules (modulo remaining rules) is 744.65/297.07 YES(?,O(n^2)) . These rules are moved into the corresponding weak 744.65/297.07 component(s). 744.65/297.07 744.65/297.07 Sub-proof: 744.65/297.07 ---------- 744.65/297.07 The following argument positions are usable: 744.65/297.07 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.07 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.07 744.65/297.07 TcT has computed the following constructor-based matrix 744.65/297.07 interpretation satisfying not(EDA). 744.65/297.07 744.65/297.07 [U11](x1, x2) = [1 4] x1 + [7 7] x2 + [7] 744.65/297.07 [1 7] [7 7] [7] 744.65/297.07 744.65/297.07 [tt] = [1] 744.65/297.07 [0] 744.65/297.07 744.65/297.07 [activate](x1) = [1 1] x1 + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [U21](x1, x2, x3) = [6 4] x1 + [7 7] x2 + [7 7] x3 + [7] 744.65/297.07 [4 7] [7 7] [7 7] [7] 744.65/297.07 744.65/297.07 [s](x1) = [1 1] x1 + [4] 744.65/297.07 [0 1] [6] 744.65/297.07 744.65/297.07 [plus](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 744.65/297.07 [0 1] [0 1] [4] 744.65/297.07 744.65/297.07 [U31](x1) = [1 4] x1 + [7] 744.65/297.07 [1 7] [7] 744.65/297.07 744.65/297.07 [0] = [4] 744.65/297.07 [6] 744.65/297.07 744.65/297.07 [U41](x1, x2, x3) = [5 4] x1 + [7 7] x2 + [7 7] x3 + [7] 744.65/297.07 [4 7] [7 7] [7 7] [7] 744.65/297.07 744.65/297.07 [x](x1, x2) = [1 1] x1 + [1 1] x2 + [4] 744.65/297.07 [0 1] [0 1] [6] 744.65/297.07 744.65/297.07 [and](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 744.65/297.07 [0 0] [0 1] [0] 744.65/297.07 744.65/297.07 [isNat](x1) = [1 0] x1 + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 744.65/297.07 [n__0] = [2] 744.65/297.07 [6] 744.65/297.07 744.65/297.07 [n__plus](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 744.65/297.07 [0 1] [0 1] [4] 744.65/297.07 744.65/297.07 [n__isNat](x1) = [1 0] x1 + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 744.65/297.07 [n__s](x1) = [1 1] x1 + [2] 744.65/297.07 [0 1] [6] 744.65/297.07 744.65/297.07 [n__x](x1, x2) = [1 1] x1 + [1 1] x2 + [2] 744.65/297.07 [0 1] [0 1] [6] 744.65/297.07 744.65/297.07 The order satisfies the following ordering constraints: 744.65/297.07 744.65/297.07 [U11(tt(), N)] = [7 7] N + [8] 744.65/297.07 [7 7] [8] 744.65/297.07 > [1 1] N + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [activate(N)] 744.65/297.07 744.65/297.07 [activate(X)] = [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 >= [1 0] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [X] 744.65/297.07 744.65/297.07 [activate(n__0())] = [8] 744.65/297.07 [6] 744.65/297.07 > [4] 744.65/297.07 [6] 744.65/297.07 = [0()] 744.65/297.07 744.65/297.07 [activate(n__plus(X1, X2))] = [1 2] X1 + [1 2] X2 + [4] 744.65/297.07 [0 1] [0 1] [4] 744.65/297.07 > [1 2] X1 + [1 2] X2 + [0] 744.65/297.07 [0 1] [0 1] [4] 744.65/297.07 = [plus(activate(X1), activate(X2))] 744.65/297.07 744.65/297.07 [activate(n__isNat(X))] = [1 0] X + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 >= [1 0] X + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 = [isNat(X)] 744.65/297.07 744.65/297.07 [activate(n__s(X))] = [1 2] X + [8] 744.65/297.07 [0 1] [6] 744.65/297.07 > [1 2] X + [4] 744.65/297.07 [0 1] [6] 744.65/297.07 = [s(activate(X))] 744.65/297.07 744.65/297.07 [activate(n__x(X1, X2))] = [1 2] X1 + [1 2] X2 + [8] 744.65/297.07 [0 1] [0 1] [6] 744.65/297.07 > [1 2] X1 + [1 2] X2 + [4] 744.65/297.07 [0 1] [0 1] [6] 744.65/297.07 = [x(activate(X1), activate(X2))] 744.65/297.07 744.65/297.07 [U21(tt(), M, N)] = [7 7] N + [7 7] M + [13] 744.65/297.07 [7 7] [7 7] [11] 744.65/297.07 > [1 3] N + [1 3] M + [8] 744.65/297.07 [0 1] [0 1] [10] 744.65/297.07 = [s(plus(activate(N), activate(M)))] 744.65/297.07 744.65/297.07 [s(X)] = [1 1] X + [4] 744.65/297.07 [0 1] [6] 744.65/297.07 > [1 1] X + [2] 744.65/297.07 [0 1] [6] 744.65/297.07 = [n__s(X)] 744.65/297.07 744.65/297.07 [plus(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 744.65/297.07 [0 1] [0 1] [4] 744.65/297.07 >= [1 1] X1 + [1 1] X2 + [0] 744.65/297.07 [0 1] [0 1] [4] 744.65/297.07 = [n__plus(X1, X2)] 744.65/297.07 744.65/297.07 [U31(tt())] = [8] 744.65/297.07 [8] 744.65/297.07 > [4] 744.65/297.07 [6] 744.65/297.07 = [0()] 744.65/297.07 744.65/297.07 [0()] = [4] 744.65/297.07 [6] 744.65/297.07 > [2] 744.65/297.07 [6] 744.65/297.07 = [n__0()] 744.65/297.07 744.65/297.07 [U41(tt(), M, N)] = [7 7] N + [7 7] M + [12] 744.65/297.07 [7 7] [7 7] [11] 744.65/297.07 > [2 5] N + [1 3] M + [10] 744.65/297.07 [0 2] [0 1] [10] 744.65/297.07 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.07 744.65/297.07 [x(X1, X2)] = [1 1] X1 + [1 1] X2 + [4] 744.65/297.07 [0 1] [0 1] [6] 744.65/297.07 > [1 1] X1 + [1 1] X2 + [2] 744.65/297.07 [0 1] [0 1] [6] 744.65/297.07 = [n__x(X1, X2)] 744.65/297.07 744.65/297.07 [and(tt(), X)] = [1 1] X + [1] 744.65/297.07 [0 1] [0] 744.65/297.07 > [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [activate(X)] 744.65/297.07 744.65/297.07 [isNat(X)] = [1 0] X + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 >= [1 0] X + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 = [n__isNat(X)] 744.65/297.07 744.65/297.07 [isNat(n__0())] = [2] 744.65/297.07 [0] 744.65/297.07 > [1] 744.65/297.07 [0] 744.65/297.07 = [tt()] 744.65/297.07 744.65/297.07 [isNat(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [0] 744.65/297.07 [0 0] [0 0] [0] 744.65/297.07 >= [1 1] V1 + [1 1] V2 + [0] 744.65/297.07 [0 0] [0 0] [0] 744.65/297.07 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.07 744.65/297.07 [isNat(n__s(V1))] = [1 1] V1 + [2] 744.65/297.07 [0 0] [0] 744.65/297.07 > [1 1] V1 + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 = [isNat(activate(V1))] 744.65/297.07 744.65/297.07 [isNat(n__x(V1, V2))] = [1 1] V1 + [1 1] V2 + [2] 744.65/297.07 [0 0] [0 0] [0] 744.65/297.07 > [1 1] V1 + [1 1] V2 + [0] 744.65/297.07 [0 0] [0 0] [0] 744.65/297.07 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.07 744.65/297.07 744.65/297.07 We return to the main proof. 744.65/297.07 744.65/297.07 We are left with following problem, upon which TcT provides the 744.65/297.07 certificate YES(O(1),O(n^2)). 744.65/297.07 744.65/297.07 Strict Trs: 744.65/297.07 { activate(X) -> X 744.65/297.07 , activate(n__isNat(X)) -> isNat(X) 744.65/297.07 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.07 , isNat(X) -> n__isNat(X) } 744.65/297.07 Weak Trs: 744.65/297.07 { U11(tt(), N) -> activate(N) 744.65/297.07 , activate(n__0()) -> 0() 744.65/297.07 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.07 , activate(n__s(X)) -> s(activate(X)) 744.65/297.07 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.07 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.07 , s(X) -> n__s(X) 744.65/297.07 , U31(tt()) -> 0() 744.65/297.07 , 0() -> n__0() 744.65/297.07 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.07 , x(X1, X2) -> n__x(X1, X2) 744.65/297.07 , and(tt(), X) -> activate(X) 744.65/297.07 , isNat(n__0()) -> tt() 744.65/297.07 , isNat(n__plus(V1, V2)) -> 744.65/297.07 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.07 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.07 , isNat(n__x(V1, V2)) -> 744.65/297.07 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.07 Obligation: 744.65/297.07 innermost runtime complexity 744.65/297.07 Answer: 744.65/297.07 YES(O(1),O(n^2)) 744.65/297.07 744.65/297.07 We use the processor 'matrix interpretation of dimension 2' to 744.65/297.07 orient following rules strictly. 744.65/297.07 744.65/297.07 Trs: { plus(X1, X2) -> n__plus(X1, X2) } 744.65/297.07 744.65/297.07 The induced complexity on above rules (modulo remaining rules) is 744.65/297.07 YES(?,O(n^2)) . These rules are moved into the corresponding weak 744.65/297.07 component(s). 744.65/297.07 744.65/297.07 Sub-proof: 744.65/297.07 ---------- 744.65/297.07 The following argument positions are usable: 744.65/297.07 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.07 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.07 744.65/297.07 TcT has computed the following constructor-based matrix 744.65/297.07 interpretation satisfying not(EDA). 744.65/297.07 744.65/297.07 [U11](x1, x2) = [7 4] x1 + [7 7] x2 + [7] 744.65/297.07 [7 7] [7 7] [7] 744.65/297.07 744.65/297.07 [tt] = [0] 744.65/297.07 [0] 744.65/297.07 744.65/297.07 [activate](x1) = [1 1] x1 + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [U21](x1, x2, x3) = [7 4] x1 + [7 7] x2 + [7 7] x3 + [3] 744.65/297.07 [7 7] [7 7] [7 7] [3] 744.65/297.07 744.65/297.07 [s](x1) = [1 1] x1 + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [plus](x1, x2) = [1 1] x1 + [1 3] x2 + [1] 744.65/297.07 [0 1] [0 1] [1] 744.65/297.07 744.65/297.07 [U31](x1) = [7 4] x1 + [7] 744.65/297.07 [7 7] [7] 744.65/297.07 744.65/297.07 [0] = [0] 744.65/297.07 [0] 744.65/297.07 744.65/297.07 [U41](x1, x2, x3) = [7 4] x1 + [7 7] x2 + [7 7] x3 + [7] 744.65/297.07 [7 7] [7 7] [7 7] [7] 744.65/297.07 744.65/297.07 [x](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 744.65/297.07 [and](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 744.65/297.07 [0 0] [0 4] [0] 744.65/297.07 744.65/297.07 [isNat](x1) = [1 0] x1 + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 744.65/297.07 [n__0] = [0] 744.65/297.07 [0] 744.65/297.07 744.65/297.07 [n__plus](x1, x2) = [1 1] x1 + [1 3] x2 + [0] 744.65/297.07 [0 1] [0 1] [1] 744.65/297.07 744.65/297.07 [n__isNat](x1) = [1 0] x1 + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 744.65/297.07 [n__s](x1) = [1 1] x1 + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [n__x](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 744.65/297.07 The order satisfies the following ordering constraints: 744.65/297.07 744.65/297.07 [U11(tt(), N)] = [7 7] N + [7] 744.65/297.07 [7 7] [7] 744.65/297.07 > [1 1] N + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [activate(N)] 744.65/297.07 744.65/297.07 [activate(X)] = [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 >= [1 0] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [X] 744.65/297.07 744.65/297.07 [activate(n__0())] = [0] 744.65/297.07 [0] 744.65/297.07 >= [0] 744.65/297.07 [0] 744.65/297.07 = [0()] 744.65/297.07 744.65/297.07 [activate(n__plus(X1, X2))] = [1 2] X1 + [1 4] X2 + [1] 744.65/297.07 [0 1] [0 1] [1] 744.65/297.07 >= [1 2] X1 + [1 4] X2 + [1] 744.65/297.07 [0 1] [0 1] [1] 744.65/297.07 = [plus(activate(X1), activate(X2))] 744.65/297.07 744.65/297.07 [activate(n__isNat(X))] = [1 0] X + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 >= [1 0] X + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 = [isNat(X)] 744.65/297.07 744.65/297.07 [activate(n__s(X))] = [1 2] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 >= [1 2] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [s(activate(X))] 744.65/297.07 744.65/297.07 [activate(n__x(X1, X2))] = [1 2] X1 + [1 2] X2 + [0] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 >= [1 2] X1 + [1 2] X2 + [0] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 = [x(activate(X1), activate(X2))] 744.65/297.07 744.65/297.07 [U21(tt(), M, N)] = [7 7] N + [7 7] M + [3] 744.65/297.07 [7 7] [7 7] [3] 744.65/297.07 > [1 3] N + [1 5] M + [2] 744.65/297.07 [0 1] [0 1] [1] 744.65/297.07 = [s(plus(activate(N), activate(M)))] 744.65/297.07 744.65/297.07 [s(X)] = [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 >= [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [n__s(X)] 744.65/297.07 744.65/297.07 [plus(X1, X2)] = [1 1] X1 + [1 3] X2 + [1] 744.65/297.07 [0 1] [0 1] [1] 744.65/297.07 > [1 1] X1 + [1 3] X2 + [0] 744.65/297.07 [0 1] [0 1] [1] 744.65/297.07 = [n__plus(X1, X2)] 744.65/297.07 744.65/297.07 [U31(tt())] = [7] 744.65/297.07 [7] 744.65/297.07 > [0] 744.65/297.07 [0] 744.65/297.07 = [0()] 744.65/297.07 744.65/297.07 [0()] = [0] 744.65/297.07 [0] 744.65/297.07 >= [0] 744.65/297.07 [0] 744.65/297.07 = [n__0()] 744.65/297.07 744.65/297.07 [U41(tt(), M, N)] = [7 7] N + [7 7] M + [7] 744.65/297.07 [7 7] [7 7] [7] 744.65/297.07 > [2 7] N + [1 3] M + [1] 744.65/297.07 [0 2] [0 1] [1] 744.65/297.07 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.07 744.65/297.07 [x(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 >= [1 1] X1 + [1 1] X2 + [0] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 = [n__x(X1, X2)] 744.65/297.07 744.65/297.07 [and(tt(), X)] = [1 1] X + [0] 744.65/297.07 [0 4] [0] 744.65/297.07 >= [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [activate(X)] 744.65/297.07 744.65/297.07 [isNat(X)] = [1 0] X + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 >= [1 0] X + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 = [n__isNat(X)] 744.65/297.07 744.65/297.07 [isNat(n__0())] = [0] 744.65/297.07 [0] 744.65/297.07 >= [0] 744.65/297.07 [0] 744.65/297.07 = [tt()] 744.65/297.07 744.65/297.07 [isNat(n__plus(V1, V2))] = [1 1] V1 + [1 3] V2 + [0] 744.65/297.07 [0 0] [0 0] [0] 744.65/297.07 >= [1 1] V1 + [1 1] V2 + [0] 744.65/297.07 [0 0] [0 0] [0] 744.65/297.07 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.07 744.65/297.07 [isNat(n__s(V1))] = [1 1] V1 + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 >= [1 1] V1 + [0] 744.65/297.07 [0 0] [0] 744.65/297.07 = [isNat(activate(V1))] 744.65/297.07 744.65/297.07 [isNat(n__x(V1, V2))] = [1 1] V1 + [1 1] V2 + [0] 744.65/297.07 [0 0] [0 0] [0] 744.65/297.07 >= [1 1] V1 + [1 1] V2 + [0] 744.65/297.07 [0 0] [0 0] [0] 744.65/297.07 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.07 744.65/297.07 744.65/297.07 We return to the main proof. 744.65/297.07 744.65/297.07 We are left with following problem, upon which TcT provides the 744.65/297.07 certificate YES(O(1),O(n^2)). 744.65/297.07 744.65/297.07 Strict Trs: 744.65/297.07 { activate(X) -> X 744.65/297.07 , activate(n__isNat(X)) -> isNat(X) 744.65/297.07 , isNat(X) -> n__isNat(X) } 744.65/297.07 Weak Trs: 744.65/297.07 { U11(tt(), N) -> activate(N) 744.65/297.07 , activate(n__0()) -> 0() 744.65/297.07 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.07 , activate(n__s(X)) -> s(activate(X)) 744.65/297.07 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.07 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.07 , s(X) -> n__s(X) 744.65/297.07 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.07 , U31(tt()) -> 0() 744.65/297.07 , 0() -> n__0() 744.65/297.07 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.07 , x(X1, X2) -> n__x(X1, X2) 744.65/297.07 , and(tt(), X) -> activate(X) 744.65/297.07 , isNat(n__0()) -> tt() 744.65/297.07 , isNat(n__plus(V1, V2)) -> 744.65/297.07 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.07 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.07 , isNat(n__x(V1, V2)) -> 744.65/297.07 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.07 Obligation: 744.65/297.07 innermost runtime complexity 744.65/297.07 Answer: 744.65/297.07 YES(O(1),O(n^2)) 744.65/297.07 744.65/297.07 We use the processor 'matrix interpretation of dimension 2' to 744.65/297.07 orient following rules strictly. 744.65/297.07 744.65/297.07 Trs: { activate(n__isNat(X)) -> isNat(X) } 744.65/297.07 744.65/297.07 The induced complexity on above rules (modulo remaining rules) is 744.65/297.07 YES(?,O(n^2)) . These rules are moved into the corresponding weak 744.65/297.07 component(s). 744.65/297.07 744.65/297.07 Sub-proof: 744.65/297.07 ---------- 744.65/297.07 The following argument positions are usable: 744.65/297.07 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.07 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.07 744.65/297.07 TcT has computed the following constructor-based matrix 744.65/297.07 interpretation satisfying not(EDA). 744.65/297.07 744.65/297.07 [U11](x1, x2) = [7 0] x1 + [7 7] x2 + [7] 744.65/297.07 [7 0] [7 7] [7] 744.65/297.07 744.65/297.07 [tt] = [0] 744.65/297.07 [1] 744.65/297.07 744.65/297.07 [activate](x1) = [1 1] x1 + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [U21](x1, x2, x3) = [7 5] x1 + [7 7] x2 + [7 7] x3 + [7] 744.65/297.07 [7 0] [7 7] [7 7] [3] 744.65/297.07 744.65/297.07 [s](x1) = [1 1] x1 + [4] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [plus](x1, x2) = [1 1] x1 + [1 1] x2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 744.65/297.07 [U31](x1) = [7 0] x1 + [7] 744.65/297.07 [7 0] [7] 744.65/297.07 744.65/297.07 [0] = [0] 744.65/297.07 [0] 744.65/297.07 744.65/297.07 [U41](x1, x2, x3) = [7 4] x1 + [7 7] x2 + [7 7] x3 + [7] 744.65/297.07 [7 0] [7 7] [7 7] [7] 744.65/297.07 744.65/297.07 [x](x1, x2) = [1 1] x1 + [1 1] x2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 744.65/297.07 [and](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 744.65/297.07 [0 0] [0 1] [0] 744.65/297.07 744.65/297.07 [isNat](x1) = [1 0] x1 + [0] 744.65/297.07 [0 0] [1] 744.65/297.07 744.65/297.07 [n__0] = [0] 744.65/297.07 [0] 744.65/297.07 744.65/297.07 [n__plus](x1, x2) = [1 1] x1 + [1 1] x2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 744.65/297.07 [n__isNat](x1) = [1 0] x1 + [0] 744.65/297.07 [0 0] [1] 744.65/297.07 744.65/297.07 [n__s](x1) = [1 1] x1 + [4] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [n__x](x1, x2) = [1 1] x1 + [1 1] x2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 744.65/297.07 The order satisfies the following ordering constraints: 744.65/297.07 744.65/297.07 [U11(tt(), N)] = [7 7] N + [7] 744.65/297.07 [7 7] [7] 744.65/297.07 > [1 1] N + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [activate(N)] 744.65/297.07 744.65/297.07 [activate(X)] = [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 >= [1 0] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [X] 744.65/297.07 744.65/297.07 [activate(n__0())] = [0] 744.65/297.07 [0] 744.65/297.07 >= [0] 744.65/297.07 [0] 744.65/297.07 = [0()] 744.65/297.07 744.65/297.07 [activate(n__plus(X1, X2))] = [1 2] X1 + [1 2] X2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 >= [1 2] X1 + [1 2] X2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 = [plus(activate(X1), activate(X2))] 744.65/297.07 744.65/297.07 [activate(n__isNat(X))] = [1 0] X + [1] 744.65/297.07 [0 0] [1] 744.65/297.07 > [1 0] X + [0] 744.65/297.07 [0 0] [1] 744.65/297.07 = [isNat(X)] 744.65/297.07 744.65/297.07 [activate(n__s(X))] = [1 2] X + [4] 744.65/297.07 [0 1] [0] 744.65/297.07 >= [1 2] X + [4] 744.65/297.07 [0 1] [0] 744.65/297.07 = [s(activate(X))] 744.65/297.07 744.65/297.07 [activate(n__x(X1, X2))] = [1 2] X1 + [1 2] X2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 >= [1 2] X1 + [1 2] X2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 = [x(activate(X1), activate(X2))] 744.65/297.07 744.65/297.07 [U21(tt(), M, N)] = [7 7] N + [7 7] M + [12] 744.65/297.07 [7 7] [7 7] [3] 744.65/297.07 > [1 3] N + [1 3] M + [8] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 = [s(plus(activate(N), activate(M)))] 744.65/297.07 744.65/297.07 [s(X)] = [1 1] X + [4] 744.65/297.07 [0 1] [0] 744.65/297.07 >= [1 1] X + [4] 744.65/297.07 [0 1] [0] 744.65/297.07 = [n__s(X)] 744.65/297.07 744.65/297.07 [plus(X1, X2)] = [1 1] X1 + [1 1] X2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 >= [1 1] X1 + [1 1] X2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 = [n__plus(X1, X2)] 744.65/297.07 744.65/297.07 [U31(tt())] = [7] 744.65/297.07 [7] 744.65/297.07 > [0] 744.65/297.07 [0] 744.65/297.07 = [0()] 744.65/297.07 744.65/297.07 [0()] = [0] 744.65/297.07 [0] 744.65/297.07 >= [0] 744.65/297.07 [0] 744.65/297.07 = [n__0()] 744.65/297.07 744.65/297.07 [U41(tt(), M, N)] = [7 7] N + [7 7] M + [11] 744.65/297.07 [7 7] [7 7] [7] 744.65/297.07 > [2 5] N + [1 3] M + [8] 744.65/297.07 [0 2] [0 1] [0] 744.65/297.07 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.07 744.65/297.07 [x(X1, X2)] = [1 1] X1 + [1 1] X2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 >= [1 1] X1 + [1 1] X2 + [4] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 = [n__x(X1, X2)] 744.65/297.07 744.65/297.07 [and(tt(), X)] = [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 >= [1 1] X + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 = [activate(X)] 744.65/297.07 744.65/297.07 [isNat(X)] = [1 0] X + [0] 744.65/297.07 [0 0] [1] 744.65/297.07 >= [1 0] X + [0] 744.65/297.07 [0 0] [1] 744.65/297.07 = [n__isNat(X)] 744.65/297.07 744.65/297.07 [isNat(n__0())] = [0] 744.65/297.07 [1] 744.65/297.07 >= [0] 744.65/297.07 [1] 744.65/297.07 = [tt()] 744.65/297.07 744.65/297.07 [isNat(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [4] 744.65/297.07 [0 0] [0 0] [1] 744.65/297.07 > [1 1] V1 + [1 1] V2 + [1] 744.65/297.07 [0 0] [0 0] [1] 744.65/297.07 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.07 744.65/297.07 [isNat(n__s(V1))] = [1 1] V1 + [4] 744.65/297.07 [0 0] [1] 744.65/297.07 > [1 1] V1 + [0] 744.65/297.07 [0 0] [1] 744.65/297.07 = [isNat(activate(V1))] 744.65/297.07 744.65/297.07 [isNat(n__x(V1, V2))] = [1 1] V1 + [1 1] V2 + [4] 744.65/297.07 [0 0] [0 0] [1] 744.65/297.07 > [1 1] V1 + [1 1] V2 + [1] 744.65/297.07 [0 0] [0 0] [1] 744.65/297.07 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.07 744.65/297.07 744.65/297.07 We return to the main proof. 744.65/297.07 744.65/297.07 We are left with following problem, upon which TcT provides the 744.65/297.07 certificate YES(O(1),O(n^2)). 744.65/297.07 744.65/297.07 Strict Trs: 744.65/297.07 { activate(X) -> X 744.65/297.07 , isNat(X) -> n__isNat(X) } 744.65/297.07 Weak Trs: 744.65/297.07 { U11(tt(), N) -> activate(N) 744.65/297.07 , activate(n__0()) -> 0() 744.65/297.07 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.07 , activate(n__isNat(X)) -> isNat(X) 744.65/297.07 , activate(n__s(X)) -> s(activate(X)) 744.65/297.07 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.07 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.07 , s(X) -> n__s(X) 744.65/297.07 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.07 , U31(tt()) -> 0() 744.65/297.07 , 0() -> n__0() 744.65/297.07 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.07 , x(X1, X2) -> n__x(X1, X2) 744.65/297.07 , and(tt(), X) -> activate(X) 744.65/297.07 , isNat(n__0()) -> tt() 744.65/297.07 , isNat(n__plus(V1, V2)) -> 744.65/297.07 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.07 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.07 , isNat(n__x(V1, V2)) -> 744.65/297.07 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.07 Obligation: 744.65/297.07 innermost runtime complexity 744.65/297.07 Answer: 744.65/297.07 YES(O(1),O(n^2)) 744.65/297.07 744.65/297.07 We use the processor 'matrix interpretation of dimension 2' to 744.65/297.07 orient following rules strictly. 744.65/297.07 744.65/297.07 Trs: { isNat(X) -> n__isNat(X) } 744.65/297.07 744.65/297.07 The induced complexity on above rules (modulo remaining rules) is 744.65/297.07 YES(?,O(n^2)) . These rules are moved into the corresponding weak 744.65/297.07 component(s). 744.65/297.07 744.65/297.07 Sub-proof: 744.65/297.07 ---------- 744.65/297.07 The following argument positions are usable: 744.65/297.07 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.07 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.07 744.65/297.07 TcT has computed the following constructor-based matrix 744.65/297.07 interpretation satisfying not(EDA). 744.65/297.07 744.65/297.07 [U11](x1, x2) = [7 0] x1 + [7 7] x2 + [7] 744.65/297.07 [7 0] [7 7] [7] 744.65/297.07 744.65/297.07 [tt] = [0] 744.65/297.07 [1] 744.65/297.07 744.65/297.07 [activate](x1) = [1 1] x1 + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [U21](x1, x2, x3) = [7 4] x1 + [7 7] x2 + [7 7] x3 + [7] 744.65/297.07 [7 0] [7 7] [7 7] [7] 744.65/297.07 744.65/297.07 [s](x1) = [1 1] x1 + [0] 744.65/297.07 [0 1] [0] 744.65/297.07 744.65/297.07 [plus](x1, x2) = [1 1] x1 + [1 1] x2 + [2] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 744.65/297.07 [U31](x1) = [7 0] x1 + [7] 744.65/297.07 [7 0] [7] 744.65/297.07 744.65/297.07 [0] = [0] 744.65/297.07 [0] 744.65/297.07 744.65/297.07 [U41](x1, x2, x3) = [7 0] x1 + [7 7] x2 + [7 7] x3 + [7] 744.65/297.07 [7 0] [7 7] [7 7] [7] 744.65/297.07 744.65/297.07 [x](x1, x2) = [1 1] x1 + [1 1] x2 + [2] 744.65/297.07 [0 1] [0 1] [0] 744.65/297.07 744.65/297.07 [and](x1, x2) = [1 0] x1 + [1 2] x2 + [0] 744.65/297.07 [0 0] [0 1] [0] 744.65/297.07 744.65/297.07 [isNat](x1) = [1 0] x1 + [1] 744.65/297.07 [0 0] [1] 744.65/297.07 744.65/297.07 [n__0] = [0] 744.65/297.08 [0] 744.65/297.08 744.65/297.08 [n__plus](x1, x2) = [1 1] x1 + [1 1] x2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 744.65/297.08 [n__isNat](x1) = [1 0] x1 + [0] 744.65/297.08 [0 0] [1] 744.65/297.08 744.65/297.08 [n__s](x1) = [1 1] x1 + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 744.65/297.08 [n__x](x1, x2) = [1 1] x1 + [1 1] x2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 744.65/297.08 The order satisfies the following ordering constraints: 744.65/297.08 744.65/297.08 [U11(tt(), N)] = [7 7] N + [7] 744.65/297.08 [7 7] [7] 744.65/297.08 > [1 1] N + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 = [activate(N)] 744.65/297.08 744.65/297.08 [activate(X)] = [1 1] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 >= [1 0] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 = [X] 744.65/297.08 744.65/297.08 [activate(n__0())] = [0] 744.65/297.08 [0] 744.65/297.08 >= [0] 744.65/297.08 [0] 744.65/297.08 = [0()] 744.65/297.08 744.65/297.08 [activate(n__plus(X1, X2))] = [1 2] X1 + [1 2] X2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 >= [1 2] X1 + [1 2] X2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 = [plus(activate(X1), activate(X2))] 744.65/297.08 744.65/297.08 [activate(n__isNat(X))] = [1 0] X + [1] 744.65/297.08 [0 0] [1] 744.65/297.08 >= [1 0] X + [1] 744.65/297.08 [0 0] [1] 744.65/297.08 = [isNat(X)] 744.65/297.08 744.65/297.08 [activate(n__s(X))] = [1 2] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 >= [1 2] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 = [s(activate(X))] 744.65/297.08 744.65/297.08 [activate(n__x(X1, X2))] = [1 2] X1 + [1 2] X2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 >= [1 2] X1 + [1 2] X2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 = [x(activate(X1), activate(X2))] 744.65/297.08 744.65/297.08 [U21(tt(), M, N)] = [7 7] N + [7 7] M + [11] 744.65/297.08 [7 7] [7 7] [7] 744.65/297.08 > [1 3] N + [1 3] M + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 = [s(plus(activate(N), activate(M)))] 744.65/297.08 744.65/297.08 [s(X)] = [1 1] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 >= [1 1] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 = [n__s(X)] 744.65/297.08 744.65/297.08 [plus(X1, X2)] = [1 1] X1 + [1 1] X2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 >= [1 1] X1 + [1 1] X2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 = [n__plus(X1, X2)] 744.65/297.08 744.65/297.08 [U31(tt())] = [7] 744.65/297.08 [7] 744.65/297.08 > [0] 744.65/297.08 [0] 744.65/297.08 = [0()] 744.65/297.08 744.65/297.08 [0()] = [0] 744.65/297.08 [0] 744.65/297.08 >= [0] 744.65/297.08 [0] 744.65/297.08 = [n__0()] 744.65/297.08 744.65/297.08 [U41(tt(), M, N)] = [7 7] N + [7 7] M + [7] 744.65/297.08 [7 7] [7 7] [7] 744.65/297.08 > [2 5] N + [1 3] M + [4] 744.65/297.08 [0 2] [0 1] [0] 744.65/297.08 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.08 744.65/297.08 [x(X1, X2)] = [1 1] X1 + [1 1] X2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 >= [1 1] X1 + [1 1] X2 + [2] 744.65/297.08 [0 1] [0 1] [0] 744.65/297.08 = [n__x(X1, X2)] 744.65/297.08 744.65/297.08 [and(tt(), X)] = [1 2] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 >= [1 1] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 = [activate(X)] 744.65/297.08 744.65/297.08 [isNat(X)] = [1 0] X + [1] 744.65/297.08 [0 0] [1] 744.65/297.08 > [1 0] X + [0] 744.65/297.08 [0 0] [1] 744.65/297.08 = [n__isNat(X)] 744.65/297.08 744.65/297.08 [isNat(n__0())] = [1] 744.65/297.08 [1] 744.65/297.08 > [0] 744.65/297.08 [1] 744.65/297.08 = [tt()] 744.65/297.08 744.65/297.08 [isNat(n__plus(V1, V2))] = [1 1] V1 + [1 1] V2 + [3] 744.65/297.08 [0 0] [0 0] [1] 744.65/297.08 >= [1 1] V1 + [1 1] V2 + [3] 744.65/297.08 [0 0] [0 0] [1] 744.65/297.08 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.08 744.65/297.08 [isNat(n__s(V1))] = [1 1] V1 + [1] 744.65/297.08 [0 0] [1] 744.65/297.08 >= [1 1] V1 + [1] 744.65/297.08 [0 0] [1] 744.65/297.08 = [isNat(activate(V1))] 744.65/297.08 744.65/297.08 [isNat(n__x(V1, V2))] = [1 1] V1 + [1 1] V2 + [3] 744.65/297.08 [0 0] [0 0] [1] 744.65/297.08 >= [1 1] V1 + [1 1] V2 + [3] 744.65/297.08 [0 0] [0 0] [1] 744.65/297.08 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.08 744.65/297.08 744.65/297.08 We return to the main proof. 744.65/297.08 744.65/297.08 We are left with following problem, upon which TcT provides the 744.65/297.08 certificate YES(O(1),O(n^2)). 744.65/297.08 744.65/297.08 Strict Trs: { activate(X) -> X } 744.65/297.08 Weak Trs: 744.65/297.08 { U11(tt(), N) -> activate(N) 744.65/297.08 , activate(n__0()) -> 0() 744.65/297.08 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.08 , activate(n__isNat(X)) -> isNat(X) 744.65/297.08 , activate(n__s(X)) -> s(activate(X)) 744.65/297.08 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.08 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.08 , s(X) -> n__s(X) 744.65/297.08 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.08 , U31(tt()) -> 0() 744.65/297.08 , 0() -> n__0() 744.65/297.08 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.08 , x(X1, X2) -> n__x(X1, X2) 744.65/297.08 , and(tt(), X) -> activate(X) 744.65/297.08 , isNat(X) -> n__isNat(X) 744.65/297.08 , isNat(n__0()) -> tt() 744.65/297.08 , isNat(n__plus(V1, V2)) -> 744.65/297.08 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.08 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.08 , isNat(n__x(V1, V2)) -> 744.65/297.08 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.08 Obligation: 744.65/297.08 innermost runtime complexity 744.65/297.08 Answer: 744.65/297.08 YES(O(1),O(n^2)) 744.65/297.08 744.65/297.08 We use the processor 'matrix interpretation of dimension 2' to 744.65/297.08 orient following rules strictly. 744.65/297.08 744.65/297.08 Trs: { activate(X) -> X } 744.65/297.08 744.65/297.08 The induced complexity on above rules (modulo remaining rules) is 744.65/297.08 YES(?,O(n^2)) . These rules are moved into the corresponding weak 744.65/297.08 component(s). 744.65/297.08 744.65/297.08 Sub-proof: 744.65/297.08 ---------- 744.65/297.08 The following argument positions are usable: 744.65/297.08 Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(x) = {1, 2}, 744.65/297.08 Uargs(and) = {1, 2}, Uargs(isNat) = {1}, Uargs(n__isNat) = {1} 744.65/297.08 744.65/297.08 TcT has computed the following constructor-based matrix 744.65/297.08 interpretation satisfying not(EDA). 744.65/297.08 744.65/297.08 [U11](x1, x2) = [0 4] x1 + [7 7] x2 + [7] 744.65/297.08 [0 7] [7 7] [7] 744.65/297.08 744.65/297.08 [tt] = [4] 744.65/297.08 [0] 744.65/297.08 744.65/297.08 [activate](x1) = [1 1] x1 + [1] 744.65/297.08 [0 1] [0] 744.65/297.08 744.65/297.08 [U21](x1, x2, x3) = [0 4] x1 + [7 7] x2 + [7 7] x3 + [7] 744.65/297.08 [0 7] [7 7] [7 7] [7] 744.65/297.08 744.65/297.08 [s](x1) = [1 1] x1 + [0] 744.65/297.08 [0 1] [2] 744.65/297.08 744.65/297.08 [plus](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 744.65/297.08 [0 1] [0 1] [1] 744.65/297.08 744.65/297.08 [U31](x1) = [0 4] x1 + [7] 744.65/297.08 [0 7] [7] 744.65/297.08 744.65/297.08 [0] = [5] 744.65/297.08 [4] 744.65/297.08 744.65/297.08 [U41](x1, x2, x3) = [2 4] x1 + [7 7] x2 + [7 7] x3 + [3] 744.65/297.08 [0 7] [7 7] [7 7] [7] 744.65/297.08 744.65/297.08 [x](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 744.65/297.08 [0 1] [0 1] [4] 744.65/297.08 744.65/297.08 [and](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 744.65/297.08 [0 0] [0 1] [0] 744.65/297.08 744.65/297.08 [isNat](x1) = [1 2] x1 + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 744.65/297.08 [n__0] = [0] 744.65/297.08 [4] 744.65/297.08 744.65/297.08 [n__plus](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 744.65/297.08 [0 1] [0 1] [1] 744.65/297.08 744.65/297.08 [n__isNat](x1) = [1 1] x1 + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 744.65/297.08 [n__s](x1) = [1 1] x1 + [0] 744.65/297.08 [0 1] [2] 744.65/297.08 744.65/297.08 [n__x](x1, x2) = [1 1] x1 + [1 1] x2 + [0] 744.65/297.08 [0 1] [0 1] [4] 744.65/297.08 744.65/297.08 The order satisfies the following ordering constraints: 744.65/297.08 744.65/297.08 [U11(tt(), N)] = [7 7] N + [7] 744.65/297.08 [7 7] [7] 744.65/297.08 > [1 1] N + [1] 744.65/297.08 [0 1] [0] 744.65/297.08 = [activate(N)] 744.65/297.08 744.65/297.08 [activate(X)] = [1 1] X + [1] 744.65/297.08 [0 1] [0] 744.65/297.08 > [1 0] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 = [X] 744.65/297.08 744.65/297.08 [activate(n__0())] = [5] 744.65/297.08 [4] 744.65/297.08 >= [5] 744.65/297.08 [4] 744.65/297.08 = [0()] 744.65/297.08 744.65/297.08 [activate(n__plus(X1, X2))] = [1 2] X1 + [1 2] X2 + [2] 744.65/297.08 [0 1] [0 1] [1] 744.65/297.08 >= [1 2] X1 + [1 2] X2 + [2] 744.65/297.08 [0 1] [0 1] [1] 744.65/297.08 = [plus(activate(X1), activate(X2))] 744.65/297.08 744.65/297.08 [activate(n__isNat(X))] = [1 2] X + [1] 744.65/297.08 [0 1] [0] 744.65/297.08 > [1 2] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 = [isNat(X)] 744.65/297.08 744.65/297.08 [activate(n__s(X))] = [1 2] X + [3] 744.65/297.08 [0 1] [2] 744.65/297.08 > [1 2] X + [1] 744.65/297.08 [0 1] [2] 744.65/297.08 = [s(activate(X))] 744.65/297.08 744.65/297.08 [activate(n__x(X1, X2))] = [1 2] X1 + [1 2] X2 + [5] 744.65/297.08 [0 1] [0 1] [4] 744.65/297.08 > [1 2] X1 + [1 2] X2 + [2] 744.65/297.08 [0 1] [0 1] [4] 744.65/297.08 = [x(activate(X1), activate(X2))] 744.65/297.08 744.65/297.08 [U21(tt(), M, N)] = [7 7] N + [7 7] M + [7] 744.65/297.08 [7 7] [7 7] [7] 744.65/297.08 > [1 3] N + [1 3] M + [3] 744.65/297.08 [0 1] [0 1] [3] 744.65/297.08 = [s(plus(activate(N), activate(M)))] 744.65/297.08 744.65/297.08 [s(X)] = [1 1] X + [0] 744.65/297.08 [0 1] [2] 744.65/297.08 >= [1 1] X + [0] 744.65/297.08 [0 1] [2] 744.65/297.08 = [n__s(X)] 744.65/297.08 744.65/297.08 [plus(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 744.65/297.08 [0 1] [0 1] [1] 744.65/297.08 >= [1 1] X1 + [1 1] X2 + [0] 744.65/297.08 [0 1] [0 1] [1] 744.65/297.08 = [n__plus(X1, X2)] 744.65/297.08 744.65/297.08 [U31(tt())] = [7] 744.65/297.08 [7] 744.65/297.08 > [5] 744.65/297.08 [4] 744.65/297.08 = [0()] 744.65/297.08 744.65/297.08 [0()] = [5] 744.65/297.08 [4] 744.65/297.08 > [0] 744.65/297.08 [4] 744.65/297.08 = [n__0()] 744.65/297.08 744.65/297.08 [U41(tt(), M, N)] = [7 7] N + [7 7] M + [11] 744.65/297.08 [7 7] [7 7] [7] 744.65/297.08 > [2 5] N + [1 3] M + [7] 744.65/297.08 [0 2] [0 1] [5] 744.65/297.08 = [plus(x(activate(N), activate(M)), activate(N))] 744.65/297.08 744.65/297.08 [x(X1, X2)] = [1 1] X1 + [1 1] X2 + [0] 744.65/297.08 [0 1] [0 1] [4] 744.65/297.08 >= [1 1] X1 + [1 1] X2 + [0] 744.65/297.08 [0 1] [0 1] [4] 744.65/297.08 = [n__x(X1, X2)] 744.65/297.08 744.65/297.08 [and(tt(), X)] = [1 1] X + [4] 744.65/297.08 [0 1] [0] 744.65/297.08 > [1 1] X + [1] 744.65/297.08 [0 1] [0] 744.65/297.08 = [activate(X)] 744.65/297.08 744.65/297.08 [isNat(X)] = [1 2] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 >= [1 1] X + [0] 744.65/297.08 [0 1] [0] 744.65/297.08 = [n__isNat(X)] 744.65/297.08 744.65/297.08 [isNat(n__0())] = [8] 744.65/297.08 [4] 744.65/297.08 > [4] 744.65/297.08 [0] 744.65/297.08 = [tt()] 744.65/297.08 744.65/297.08 [isNat(n__plus(V1, V2))] = [1 3] V1 + [1 3] V2 + [2] 744.65/297.08 [0 1] [0 1] [1] 744.65/297.08 >= [1 3] V1 + [1 3] V2 + [2] 744.65/297.08 [0 0] [0 1] [0] 744.65/297.08 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.08 744.65/297.08 [isNat(n__s(V1))] = [1 3] V1 + [4] 744.65/297.08 [0 1] [2] 744.65/297.08 > [1 3] V1 + [1] 744.65/297.08 [0 1] [0] 744.65/297.08 = [isNat(activate(V1))] 744.65/297.08 744.65/297.08 [isNat(n__x(V1, V2))] = [1 3] V1 + [1 3] V2 + [8] 744.65/297.08 [0 1] [0 1] [4] 744.65/297.08 > [1 3] V1 + [1 3] V2 + [2] 744.65/297.08 [0 0] [0 1] [0] 744.65/297.08 = [and(isNat(activate(V1)), n__isNat(activate(V2)))] 744.65/297.08 744.65/297.08 744.65/297.08 We return to the main proof. 744.65/297.08 744.65/297.08 We are left with following problem, upon which TcT provides the 744.65/297.08 certificate YES(O(1),O(1)). 744.65/297.08 744.65/297.08 Weak Trs: 744.65/297.08 { U11(tt(), N) -> activate(N) 744.65/297.08 , activate(X) -> X 744.65/297.08 , activate(n__0()) -> 0() 744.65/297.08 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 744.65/297.08 , activate(n__isNat(X)) -> isNat(X) 744.65/297.08 , activate(n__s(X)) -> s(activate(X)) 744.65/297.08 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 744.65/297.08 , U21(tt(), M, N) -> s(plus(activate(N), activate(M))) 744.65/297.08 , s(X) -> n__s(X) 744.65/297.08 , plus(X1, X2) -> n__plus(X1, X2) 744.65/297.08 , U31(tt()) -> 0() 744.65/297.08 , 0() -> n__0() 744.65/297.08 , U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 744.65/297.08 , x(X1, X2) -> n__x(X1, X2) 744.65/297.08 , and(tt(), X) -> activate(X) 744.65/297.08 , isNat(X) -> n__isNat(X) 744.65/297.08 , isNat(n__0()) -> tt() 744.65/297.08 , isNat(n__plus(V1, V2)) -> 744.65/297.08 and(isNat(activate(V1)), n__isNat(activate(V2))) 744.65/297.08 , isNat(n__s(V1)) -> isNat(activate(V1)) 744.65/297.08 , isNat(n__x(V1, V2)) -> 744.65/297.08 and(isNat(activate(V1)), n__isNat(activate(V2))) } 744.65/297.08 Obligation: 744.65/297.08 innermost runtime complexity 744.65/297.08 Answer: 744.65/297.08 YES(O(1),O(1)) 744.65/297.08 744.65/297.08 Empty rules are trivially bounded 744.65/297.08 744.65/297.08 Hurray, we answered YES(O(1),O(n^2)) 744.91/297.25 EOF