YES(O(1),O(n^2)) 441.17/111.36 YES(O(1),O(n^2)) 441.17/111.36 441.17/111.36 We are left with following problem, upon which TcT provides the 441.17/111.36 certificate YES(O(1),O(n^2)). 441.17/111.36 441.17/111.36 Strict Trs: 441.17/111.36 { U11(tt(), V1, V2) -> 441.17/111.36 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.36 , U12(tt(), V1, V2) -> 441.17/111.36 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.36 , isNatKind(n__0()) -> tt() 441.17/111.36 , isNatKind(n__plus(V1, V2)) -> 441.17/111.36 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.36 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.36 , activate(X) -> X 441.17/111.36 , activate(n__0()) -> 0() 441.17/111.36 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.36 , activate(n__s(X)) -> s(X) 441.17/111.36 , U13(tt(), V1, V2) -> 441.17/111.36 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.36 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.36 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.36 , isNat(n__0()) -> tt() 441.17/111.36 , isNat(n__plus(V1, V2)) -> 441.17/111.36 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.36 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.36 , U16(tt()) -> tt() 441.17/111.36 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.36 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.36 , U23(tt()) -> tt() 441.17/111.36 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.36 , U32(tt()) -> tt() 441.17/111.36 , U41(tt()) -> tt() 441.17/111.36 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.36 , U52(tt(), N) -> activate(N) 441.17/111.36 , U61(tt(), M, N) -> 441.17/111.36 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.17/111.36 , U62(tt(), M, N) -> 441.17/111.36 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.36 , U63(tt(), M, N) -> 441.17/111.36 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.36 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) 441.17/111.36 , s(X) -> n__s(X) 441.17/111.36 , plus(X1, X2) -> n__plus(X1, X2) 441.17/111.36 , plus(N, s(M)) -> U61(isNat(M), M, N) 441.17/111.36 , plus(N, 0()) -> U51(isNat(N), N) 441.17/111.36 , 0() -> n__0() } 441.17/111.36 Obligation: 441.17/111.36 innermost runtime complexity 441.17/111.36 Answer: 441.17/111.36 YES(O(1),O(n^2)) 441.17/111.36 441.17/111.36 Arguments of following rules are not normal-forms: 441.17/111.36 441.17/111.36 { plus(N, s(M)) -> U61(isNat(M), M, N) 441.17/111.36 , plus(N, 0()) -> U51(isNat(N), N) } 441.17/111.36 441.17/111.36 All above mentioned rules can be savely removed. 441.17/111.36 441.17/111.36 We are left with following problem, upon which TcT provides the 441.17/111.36 certificate YES(O(1),O(n^2)). 441.17/111.36 441.17/111.36 Strict Trs: 441.17/111.36 { U11(tt(), V1, V2) -> 441.17/111.36 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.36 , U12(tt(), V1, V2) -> 441.17/111.36 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.36 , isNatKind(n__0()) -> tt() 441.17/111.36 , isNatKind(n__plus(V1, V2)) -> 441.17/111.36 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.36 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.36 , activate(X) -> X 441.17/111.36 , activate(n__0()) -> 0() 441.17/111.36 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.36 , activate(n__s(X)) -> s(X) 441.17/111.36 , U13(tt(), V1, V2) -> 441.17/111.36 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.36 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.36 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.36 , isNat(n__0()) -> tt() 441.17/111.36 , isNat(n__plus(V1, V2)) -> 441.17/111.36 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.36 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.36 , U16(tt()) -> tt() 441.17/111.36 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.36 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.36 , U23(tt()) -> tt() 441.17/111.36 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.36 , U32(tt()) -> tt() 441.17/111.36 , U41(tt()) -> tt() 441.17/111.36 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.36 , U52(tt(), N) -> activate(N) 441.17/111.36 , U61(tt(), M, N) -> 441.17/111.36 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.17/111.36 , U62(tt(), M, N) -> 441.17/111.36 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.36 , U63(tt(), M, N) -> 441.17/111.36 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.36 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) 441.17/111.36 , s(X) -> n__s(X) 441.17/111.36 , plus(X1, X2) -> n__plus(X1, X2) 441.17/111.36 , 0() -> n__0() } 441.17/111.36 Obligation: 441.17/111.36 innermost runtime complexity 441.17/111.36 Answer: 441.17/111.36 YES(O(1),O(n^2)) 441.17/111.36 441.17/111.36 We use the processor 'matrix interpretation of dimension 2' to 441.17/111.36 orient following rules strictly. 441.17/111.36 441.17/111.36 Trs: 441.17/111.36 { U11(tt(), V1, V2) -> 441.17/111.36 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.36 , isNat(n__plus(V1, V2)) -> 441.17/111.36 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.36 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.36 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.36 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.36 , U61(tt(), M, N) -> 441.17/111.36 U62(isNatKind(activate(M)), activate(M), activate(N)) } 441.17/111.36 441.17/111.36 The induced complexity on above rules (modulo remaining rules) is 441.17/111.36 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.17/111.36 component(s). 441.17/111.36 441.17/111.36 Sub-proof: 441.17/111.36 ---------- 441.17/111.36 The following argument positions are usable: 441.17/111.36 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.17/111.36 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.17/111.36 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.17/111.36 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.17/111.36 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.17/111.36 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.17/111.36 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.17/111.36 Uargs(plus) = {1, 2} 441.17/111.36 441.17/111.36 TcT has computed the following constructor-based matrix 441.17/111.36 interpretation satisfying not(EDA). 441.17/111.36 441.17/111.36 [U11](x1, x2, x3) = [1 0] x1 + [3 4] x2 + [5 4] x3 + [4] 441.17/111.36 [0 0] [0 0] [4 0] [0] 441.17/111.36 441.17/111.36 [tt] = [0] 441.17/111.36 [0] 441.17/111.36 441.17/111.36 [U12](x1, x2, x3) = [1 0] x1 + [1 4] x2 + [5 4] x3 + [0] 441.17/111.36 [0 0] [0 0] [4 0] [0] 441.17/111.36 441.17/111.36 [isNatKind](x1) = [2 0] x1 + [0] 441.17/111.36 [6 3] [0] 441.17/111.36 441.17/111.36 [activate](x1) = [1 0] x1 + [0] 441.17/111.36 [0 1] [0] 441.17/111.36 441.17/111.36 [U13](x1, x2, x3) = [1 0] x1 + [1 4] x2 + [3 4] x3 + [0] 441.17/111.36 [0 0] [0 0] [0 0] [0] 441.17/111.36 441.17/111.36 [U14](x1, x2, x3) = [1 0] x1 + [1 4] x2 + [1 4] x3 + [0] 441.17/111.36 [0 0] [0 0] [0 0] [0] 441.17/111.36 441.17/111.36 [U15](x1, x2) = [1 0] x1 + [1 4] x2 + [0] 441.17/111.36 [0 0] [0 0] [0] 441.17/111.36 441.17/111.36 [isNat](x1) = [1 4] x1 + [0] 441.17/111.36 [4 0] [4] 441.17/111.36 441.17/111.36 [U16](x1) = [1 0] x1 + [0] 441.17/111.36 [0 0] [0] 441.17/111.36 441.17/111.36 [U21](x1, x2) = [1 0] x1 + [3 4] x2 + [4] 441.17/111.36 [0 0] [0 0] [4] 441.17/111.36 441.17/111.36 [U22](x1, x2) = [1 0] x1 + [1 4] x2 + [0] 441.17/111.36 [0 0] [0 0] [4] 441.17/111.36 441.17/111.36 [U23](x1) = [1 0] x1 + [0] 441.17/111.36 [0 0] [4] 441.17/111.36 441.17/111.36 [U31](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 441.17/111.36 [0 0] [0 0] [0] 441.17/111.36 441.17/111.36 [U32](x1) = [1 0] x1 + [0] 441.17/111.36 [0 0] [0] 441.17/111.36 441.17/111.36 [U41](x1) = [1 0] x1 + [0] 441.17/111.36 [0 0] [0] 441.17/111.36 441.17/111.36 [U51](x1, x2) = [7 4] x1 + [7 7] x2 + [7] 441.17/111.36 [7 7] [7 7] [7] 441.17/111.36 441.17/111.36 [U52](x1, x2) = [1 0] x1 + [4 0] x2 + [0] 441.17/111.36 [0 0] [0 4] [0] 441.17/111.36 441.17/111.36 [U61](x1, x2, x3) = [7 4] x1 + [7 7] x2 + [7 7] x3 + [7] 441.17/111.36 [7 7] [7 7] [7 7] [7] 441.17/111.36 441.17/111.36 [U62](x1, x2, x3) = [1 0] x1 + [4 0] x2 + [4 4] x3 + [0] 441.17/111.36 [0 0] [4 1] [4 4] [6] 441.17/111.36 441.17/111.36 [U63](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [3 0] x3 + [0] 441.17/111.36 [0 0] [2 1] [4 4] [6] 441.17/111.36 441.17/111.36 [U64](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0] 441.17/111.36 [0 0] [2 1] [2 2] [6] 441.17/111.36 441.17/111.36 [s](x1) = [1 0] x1 + [0] 441.17/111.36 [1 1] [3] 441.17/111.36 441.17/111.36 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.36 [1 1] [1 1] [3] 441.17/111.36 441.17/111.36 [n__0] = [0] 441.17/111.36 [0] 441.17/111.36 441.17/111.36 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.36 [1 1] [1 1] [3] 441.17/111.36 441.17/111.36 [n__s](x1) = [1 0] x1 + [0] 441.17/111.36 [1 1] [3] 441.17/111.36 441.17/111.36 [0] = [0] 441.17/111.36 [0] 441.17/111.36 441.17/111.36 The order satisfies the following ordering constraints: 441.17/111.36 441.17/111.36 [U11(tt(), V1, V2)] = [3 4] V1 + [5 4] V2 + [4] 441.17/111.36 [0 0] [4 0] [0] 441.17/111.36 > [3 4] V1 + [5 4] V2 + [0] 441.17/111.36 [0 0] [4 0] [0] 441.17/111.36 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.36 441.17/111.36 [U12(tt(), V1, V2)] = [1 4] V1 + [5 4] V2 + [0] 441.17/111.36 [0 0] [4 0] [0] 441.17/111.36 >= [1 4] V1 + [5 4] V2 + [0] 441.17/111.36 [0 0] [0 0] [0] 441.17/111.36 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.36 441.17/111.36 [isNatKind(n__0())] = [0] 441.17/111.36 [0] 441.17/111.36 >= [0] 441.17/111.36 [0] 441.17/111.36 = [tt()] 441.17/111.36 441.17/111.36 [isNatKind(n__plus(V1, V2))] = [2 0] V1 + [2 0] V2 + [0] 441.17/111.36 [9 3] [9 3] [9] 441.17/111.36 >= [2 0] V1 + [2 0] V2 + [0] 441.17/111.36 [0 0] [0 0] [0] 441.17/111.36 = [U31(isNatKind(activate(V1)), activate(V2))] 441.17/111.36 441.17/111.36 [isNatKind(n__s(V1))] = [2 0] V1 + [0] 441.17/111.36 [9 3] [9] 441.17/111.36 >= [2 0] V1 + [0] 441.17/111.36 [0 0] [0] 441.17/111.36 = [U41(isNatKind(activate(V1)))] 441.17/111.36 441.17/111.36 [activate(X)] = [1 0] X + [0] 441.17/111.36 [0 1] [0] 441.17/111.36 >= [1 0] X + [0] 441.17/111.36 [0 1] [0] 441.17/111.36 = [X] 441.17/111.36 441.17/111.36 [activate(n__0())] = [0] 441.17/111.36 [0] 441.17/111.36 >= [0] 441.17/111.36 [0] 441.17/111.36 = [0()] 441.17/111.36 441.17/111.36 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [0] 441.17/111.36 [1 1] [1 1] [3] 441.17/111.36 >= [1 0] X1 + [1 0] X2 + [0] 441.17/111.36 [1 1] [1 1] [3] 441.17/111.36 = [plus(X1, X2)] 441.17/111.36 441.17/111.36 [activate(n__s(X))] = [1 0] X + [0] 441.17/111.36 [1 1] [3] 441.17/111.36 >= [1 0] X + [0] 441.17/111.36 [1 1] [3] 441.17/111.36 = [s(X)] 441.17/111.36 441.17/111.36 [U13(tt(), V1, V2)] = [1 4] V1 + [3 4] V2 + [0] 441.17/111.36 [0 0] [0 0] [0] 441.17/111.36 >= [1 4] V1 + [3 4] V2 + [0] 441.17/111.36 [0 0] [0 0] [0] 441.17/111.36 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.36 441.17/111.36 [U14(tt(), V1, V2)] = [1 4] V1 + [1 4] V2 + [0] 441.17/111.36 [0 0] [0 0] [0] 441.17/111.36 >= [1 4] V1 + [1 4] V2 + [0] 441.17/111.36 [0 0] [0 0] [0] 441.17/111.36 = [U15(isNat(activate(V1)), activate(V2))] 441.17/111.36 441.17/111.36 [U15(tt(), V2)] = [1 4] V2 + [0] 441.17/111.36 [0 0] [0] 441.17/111.36 >= [1 4] V2 + [0] 441.17/111.36 [0 0] [0] 441.17/111.36 = [U16(isNat(activate(V2)))] 441.17/111.36 441.17/111.36 [isNat(n__0())] = [0] 441.17/111.36 [4] 441.17/111.36 >= [0] 441.17/111.36 [0] 441.17/111.36 = [tt()] 441.17/111.36 441.17/111.36 [isNat(n__plus(V1, V2))] = [5 4] V1 + [5 4] V2 + [12] 441.17/111.36 [4 0] [4 0] [4] 441.17/111.36 > [5 4] V1 + [5 4] V2 + [4] 441.17/111.36 [0 0] [4 0] [0] 441.17/111.36 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.36 441.17/111.36 [isNat(n__s(V1))] = [5 4] V1 + [12] 441.17/111.36 [4 0] [4] 441.17/111.36 > [5 4] V1 + [4] 441.17/111.36 [0 0] [4] 441.17/111.36 = [U21(isNatKind(activate(V1)), activate(V1))] 441.17/111.36 441.17/111.36 [U16(tt())] = [0] 441.17/111.36 [0] 441.17/111.36 >= [0] 441.17/111.36 [0] 441.17/111.36 = [tt()] 441.17/111.36 441.17/111.36 [U21(tt(), V1)] = [3 4] V1 + [4] 441.17/111.36 [0 0] [4] 441.17/111.36 > [3 4] V1 + [0] 441.17/111.36 [0 0] [4] 441.17/111.36 = [U22(isNatKind(activate(V1)), activate(V1))] 441.17/111.36 441.17/111.36 [U22(tt(), V1)] = [1 4] V1 + [0] 441.17/111.36 [0 0] [4] 441.17/111.36 >= [1 4] V1 + [0] 441.17/111.36 [0 0] [4] 441.17/111.36 = [U23(isNat(activate(V1)))] 441.17/111.36 441.17/111.36 [U23(tt())] = [0] 441.17/111.36 [4] 441.17/111.36 >= [0] 441.17/111.36 [0] 441.17/111.36 = [tt()] 441.17/111.36 441.17/111.36 [U31(tt(), V2)] = [2 0] V2 + [0] 441.17/111.36 [0 0] [0] 441.17/111.36 >= [2 0] V2 + [0] 441.17/111.36 [0 0] [0] 441.17/111.36 = [U32(isNatKind(activate(V2)))] 441.17/111.36 441.17/111.36 [U32(tt())] = [0] 441.17/111.36 [0] 441.17/111.36 >= [0] 441.17/111.36 [0] 441.17/111.36 = [tt()] 441.17/111.36 441.17/111.36 [U41(tt())] = [0] 441.17/111.36 [0] 441.17/111.36 >= [0] 441.17/111.36 [0] 441.17/111.36 = [tt()] 441.17/111.36 441.17/111.36 [U51(tt(), N)] = [7 7] N + [7] 441.17/111.36 [7 7] [7] 441.17/111.36 > [6 0] N + [0] 441.17/111.36 [0 4] [0] 441.17/111.36 = [U52(isNatKind(activate(N)), activate(N))] 441.17/111.36 441.17/111.36 [U52(tt(), N)] = [4 0] N + [0] 441.17/111.36 [0 4] [0] 441.17/111.36 >= [1 0] N + [0] 441.17/111.36 [0 1] [0] 441.17/111.36 = [activate(N)] 441.17/111.36 441.17/111.36 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [7] 441.17/111.36 [7 7] [7 7] [7] 441.17/111.36 > [4 4] N + [6 0] M + [0] 441.17/111.36 [4 4] [4 1] [6] 441.17/111.36 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.17/111.37 441.17/111.37 [U62(tt(), M, N)] = [4 4] N + [4 0] M + [0] 441.17/111.37 [4 4] [4 1] [6] 441.17/111.37 >= [4 4] N + [1 0] M + [0] 441.17/111.37 [4 4] [2 1] [6] 441.17/111.37 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.17/111.37 441.17/111.37 [U63(tt(), M, N)] = [3 0] N + [1 0] M + [0] 441.17/111.37 [4 4] [2 1] [6] 441.17/111.37 >= [3 0] N + [1 0] M + [0] 441.17/111.37 [2 2] [2 1] [6] 441.17/111.37 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.17/111.37 441.17/111.37 [U64(tt(), M, N)] = [1 0] N + [1 0] M + [0] 441.17/111.37 [2 2] [2 1] [6] 441.17/111.37 >= [1 0] N + [1 0] M + [0] 441.17/111.37 [2 1] [2 1] [6] 441.17/111.37 = [s(plus(activate(N), activate(M)))] 441.17/111.37 441.17/111.37 [s(X)] = [1 0] X + [0] 441.17/111.37 [1 1] [3] 441.17/111.37 >= [1 0] X + [0] 441.17/111.37 [1 1] [3] 441.17/111.37 = [n__s(X)] 441.17/111.37 441.17/111.37 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] 441.17/111.37 [1 1] [1 1] [3] 441.17/111.37 >= [1 0] X1 + [1 0] X2 + [0] 441.17/111.37 [1 1] [1 1] [3] 441.17/111.37 = [n__plus(X1, X2)] 441.17/111.37 441.17/111.37 [0()] = [0] 441.17/111.37 [0] 441.17/111.37 >= [0] 441.17/111.37 [0] 441.17/111.37 = [n__0()] 441.17/111.37 441.17/111.37 441.17/111.37 We return to the main proof. 441.17/111.37 441.17/111.37 We are left with following problem, upon which TcT provides the 441.17/111.37 certificate YES(O(1),O(n^2)). 441.17/111.37 441.17/111.37 Strict Trs: 441.17/111.37 { U12(tt(), V1, V2) -> 441.17/111.37 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.37 , isNatKind(n__0()) -> tt() 441.17/111.37 , isNatKind(n__plus(V1, V2)) -> 441.17/111.37 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.37 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.37 , activate(X) -> X 441.17/111.37 , activate(n__0()) -> 0() 441.17/111.37 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.37 , activate(n__s(X)) -> s(X) 441.17/111.37 , U13(tt(), V1, V2) -> 441.17/111.37 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.37 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.37 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.37 , isNat(n__0()) -> tt() 441.17/111.37 , U16(tt()) -> tt() 441.17/111.37 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.37 , U23(tt()) -> tt() 441.17/111.37 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.37 , U32(tt()) -> tt() 441.17/111.37 , U41(tt()) -> tt() 441.17/111.37 , U52(tt(), N) -> activate(N) 441.17/111.37 , U62(tt(), M, N) -> 441.17/111.37 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.37 , U63(tt(), M, N) -> 441.17/111.37 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.37 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) 441.17/111.37 , s(X) -> n__s(X) 441.17/111.37 , plus(X1, X2) -> n__plus(X1, X2) 441.17/111.37 , 0() -> n__0() } 441.17/111.37 Weak Trs: 441.17/111.37 { U11(tt(), V1, V2) -> 441.17/111.37 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.37 , isNat(n__plus(V1, V2)) -> 441.17/111.37 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.37 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.37 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.37 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.37 , U61(tt(), M, N) -> 441.17/111.37 U62(isNatKind(activate(M)), activate(M), activate(N)) } 441.17/111.37 Obligation: 441.17/111.37 innermost runtime complexity 441.17/111.37 Answer: 441.17/111.37 YES(O(1),O(n^2)) 441.17/111.37 441.17/111.37 We use the processor 'matrix interpretation of dimension 2' to 441.17/111.37 orient following rules strictly. 441.17/111.37 441.17/111.37 Trs: 441.17/111.37 { U12(tt(), V1, V2) -> 441.17/111.37 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.37 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.37 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.37 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.37 , isNat(n__0()) -> tt() 441.17/111.37 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.37 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.37 , U52(tt(), N) -> activate(N) 441.17/111.37 , U62(tt(), M, N) -> 441.17/111.37 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.37 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) } 441.17/111.37 441.17/111.37 The induced complexity on above rules (modulo remaining rules) is 441.17/111.37 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.17/111.37 component(s). 441.17/111.37 441.17/111.37 Sub-proof: 441.17/111.37 ---------- 441.17/111.37 The following argument positions are usable: 441.17/111.37 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.17/111.37 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.17/111.37 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.17/111.37 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.17/111.37 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.17/111.37 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.17/111.37 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.17/111.37 Uargs(plus) = {1, 2} 441.17/111.37 441.17/111.37 TcT has computed the following constructor-based matrix 441.17/111.37 interpretation satisfying not(EDA). 441.17/111.37 441.17/111.37 [U11](x1, x2, x3) = [1 0] x1 + [5 2] x2 + [6 2] x3 + [0] 441.17/111.37 [0 0] [0 0] [4 0] [0] 441.17/111.37 441.17/111.37 [tt] = [2] 441.17/111.37 [0] 441.17/111.37 441.17/111.37 [U12](x1, x2, x3) = [1 0] x1 + [4 2] x2 + [6 2] x3 + [0] 441.17/111.37 [0 0] [0 0] [4 0] [0] 441.17/111.37 441.17/111.37 [isNatKind](x1) = [1 0] x1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 441.17/111.37 [activate](x1) = [1 0] x1 + [0] 441.17/111.37 [0 1] [0] 441.17/111.37 441.17/111.37 [U13](x1, x2, x3) = [1 0] x1 + [4 2] x2 + [5 2] x3 + [0] 441.17/111.37 [4 0] [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U14](x1, x2, x3) = [1 0] x1 + [4 2] x2 + [4 2] x3 + [2] 441.17/111.37 [0 0] [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U15](x1, x2) = [1 0] x1 + [4 2] x2 + [2] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [isNat](x1) = [4 2] x1 + [0] 441.17/111.37 [4 1] [0] 441.17/111.37 441.17/111.37 [U16](x1) = [1 0] x1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 441.17/111.37 [U21](x1, x2) = [1 0] x1 + [5 2] x2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U22](x1, x2) = [1 0] x1 + [4 2] x2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U23](x1) = [1 0] x1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 441.17/111.37 [U31](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U32](x1) = [1 0] x1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 441.17/111.37 [U41](x1) = [1 0] x1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 441.17/111.37 [U51](x1, x2) = [0 4] x1 + [7 7] x2 + [3] 441.17/111.37 [0 7] [7 7] [7] 441.17/111.37 441.17/111.37 [U52](x1, x2) = [4 0] x1 + [2 0] x2 + [0] 441.17/111.37 [0 0] [0 1] [0] 441.17/111.37 441.17/111.37 [U61](x1, x2, x3) = [0 4] x1 + [7 7] x2 + [7 7] x3 + [7] 441.17/111.37 [0 7] [7 7] [7 7] [7] 441.17/111.37 441.17/111.37 [U62](x1, x2, x3) = [4 0] x1 + [1 0] x2 + [6 4] x3 + [0] 441.17/111.37 [0 0] [4 1] [4 4] [4] 441.17/111.37 441.17/111.37 [U63](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [0] 441.17/111.37 [0 0] [4 1] [2 4] [4] 441.17/111.37 441.17/111.37 [U64](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [2] 441.17/111.37 [0 0] [2 1] [2 4] [4] 441.17/111.37 441.17/111.37 [s](x1) = [1 0] x1 + [1] 441.17/111.37 [1 1] [4] 441.17/111.37 441.17/111.37 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 441.17/111.37 [n__0] = [2] 441.17/111.37 [0] 441.17/111.37 441.17/111.37 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 441.17/111.37 [n__s](x1) = [1 0] x1 + [1] 441.17/111.37 [1 1] [4] 441.17/111.37 441.17/111.37 [0] = [2] 441.17/111.37 [0] 441.17/111.37 441.17/111.37 The order satisfies the following ordering constraints: 441.17/111.37 441.17/111.37 [U11(tt(), V1, V2)] = [5 2] V1 + [6 2] V2 + [2] 441.17/111.37 [0 0] [4 0] [0] 441.17/111.37 > [5 2] V1 + [6 2] V2 + [0] 441.17/111.37 [0 0] [4 0] [0] 441.17/111.37 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.37 441.17/111.37 [U12(tt(), V1, V2)] = [4 2] V1 + [6 2] V2 + [2] 441.17/111.37 [0 0] [4 0] [0] 441.17/111.37 > [4 2] V1 + [6 2] V2 + [0] 441.17/111.37 [0 0] [4 0] [0] 441.17/111.37 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.37 441.17/111.37 [isNatKind(n__0())] = [2] 441.17/111.37 [0] 441.17/111.37 >= [2] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [isNatKind(n__plus(V1, V2))] = [1 0] V1 + [1 0] V2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 >= [1 0] V1 + [1 0] V2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 = [U31(isNatKind(activate(V1)), activate(V2))] 441.17/111.37 441.17/111.37 [isNatKind(n__s(V1))] = [1 0] V1 + [1] 441.17/111.37 [0 0] [0] 441.17/111.37 > [1 0] V1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U41(isNatKind(activate(V1)))] 441.17/111.37 441.17/111.37 [activate(X)] = [1 0] X + [0] 441.17/111.37 [0 1] [0] 441.17/111.37 >= [1 0] X + [0] 441.17/111.37 [0 1] [0] 441.17/111.37 = [X] 441.17/111.37 441.17/111.37 [activate(n__0())] = [2] 441.17/111.37 [0] 441.17/111.37 >= [2] 441.17/111.37 [0] 441.17/111.37 = [0()] 441.17/111.37 441.17/111.37 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 >= [1 0] X1 + [1 0] X2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 = [plus(X1, X2)] 441.17/111.37 441.17/111.37 [activate(n__s(X))] = [1 0] X + [1] 441.17/111.37 [1 1] [4] 441.17/111.37 >= [1 0] X + [1] 441.17/111.37 [1 1] [4] 441.17/111.37 = [s(X)] 441.17/111.37 441.17/111.37 [U13(tt(), V1, V2)] = [4 2] V1 + [5 2] V2 + [2] 441.17/111.37 [0 0] [0 0] [8] 441.17/111.37 >= [4 2] V1 + [5 2] V2 + [2] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.37 441.17/111.37 [U14(tt(), V1, V2)] = [4 2] V1 + [4 2] V2 + [4] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 > [4 2] V1 + [4 2] V2 + [2] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 = [U15(isNat(activate(V1)), activate(V2))] 441.17/111.37 441.17/111.37 [U15(tt(), V2)] = [4 2] V2 + [4] 441.17/111.37 [0 0] [0] 441.17/111.37 > [4 2] V2 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U16(isNat(activate(V2)))] 441.17/111.37 441.17/111.37 [isNat(n__0())] = [8] 441.17/111.37 [8] 441.17/111.37 > [2] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [isNat(n__plus(V1, V2))] = [6 2] V1 + [6 2] V2 + [0] 441.17/111.37 [5 1] [5 1] [0] 441.17/111.37 >= [6 2] V1 + [6 2] V2 + [0] 441.17/111.37 [0 0] [4 0] [0] 441.17/111.37 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.37 441.17/111.37 [isNat(n__s(V1))] = [6 2] V1 + [12] 441.17/111.37 [5 1] [8] 441.17/111.37 > [6 2] V1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U21(isNatKind(activate(V1)), activate(V1))] 441.17/111.37 441.17/111.37 [U16(tt())] = [2] 441.17/111.37 [0] 441.17/111.37 >= [2] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [U21(tt(), V1)] = [5 2] V1 + [2] 441.17/111.37 [0 0] [0] 441.17/111.37 > [5 2] V1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U22(isNatKind(activate(V1)), activate(V1))] 441.17/111.37 441.17/111.37 [U22(tt(), V1)] = [4 2] V1 + [2] 441.17/111.37 [0 0] [0] 441.17/111.37 > [4 2] V1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U23(isNat(activate(V1)))] 441.17/111.37 441.17/111.37 [U23(tt())] = [2] 441.17/111.37 [0] 441.17/111.37 >= [2] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [U31(tt(), V2)] = [1 0] V2 + [2] 441.17/111.37 [0 0] [0] 441.17/111.37 > [1 0] V2 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U32(isNatKind(activate(V2)))] 441.17/111.37 441.17/111.37 [U32(tt())] = [2] 441.17/111.37 [0] 441.17/111.37 >= [2] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [U41(tt())] = [2] 441.17/111.37 [0] 441.17/111.37 >= [2] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [U51(tt(), N)] = [7 7] N + [3] 441.17/111.37 [7 7] [7] 441.17/111.37 > [6 0] N + [0] 441.17/111.37 [0 1] [0] 441.17/111.37 = [U52(isNatKind(activate(N)), activate(N))] 441.17/111.37 441.17/111.37 [U52(tt(), N)] = [2 0] N + [8] 441.17/111.37 [0 1] [0] 441.17/111.37 > [1 0] N + [0] 441.17/111.37 [0 1] [0] 441.17/111.37 = [activate(N)] 441.17/111.37 441.17/111.37 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [7] 441.17/111.37 [7 7] [7 7] [7] 441.17/111.37 > [6 4] N + [5 0] M + [0] 441.17/111.37 [4 4] [4 1] [4] 441.17/111.37 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.17/111.37 441.17/111.37 [U62(tt(), M, N)] = [6 4] N + [1 0] M + [8] 441.17/111.37 [4 4] [4 1] [4] 441.17/111.37 > [6 2] N + [1 0] M + [0] 441.17/111.37 [2 4] [4 1] [4] 441.17/111.37 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.17/111.37 441.17/111.37 [U63(tt(), M, N)] = [2 0] N + [1 0] M + [2] 441.17/111.37 [2 4] [4 1] [4] 441.17/111.37 >= [2 0] N + [1 0] M + [2] 441.17/111.37 [2 4] [2 1] [4] 441.17/111.37 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.17/111.37 441.17/111.37 [U64(tt(), M, N)] = [1 0] N + [1 0] M + [4] 441.17/111.37 [2 4] [2 1] [4] 441.17/111.37 > [1 0] N + [1 0] M + [1] 441.17/111.37 [2 1] [2 1] [4] 441.17/111.37 = [s(plus(activate(N), activate(M)))] 441.17/111.37 441.17/111.37 [s(X)] = [1 0] X + [1] 441.17/111.37 [1 1] [4] 441.17/111.37 >= [1 0] X + [1] 441.17/111.37 [1 1] [4] 441.17/111.37 = [n__s(X)] 441.17/111.37 441.17/111.37 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 >= [1 0] X1 + [1 0] X2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 = [n__plus(X1, X2)] 441.17/111.37 441.17/111.37 [0()] = [2] 441.17/111.37 [0] 441.17/111.37 >= [2] 441.17/111.37 [0] 441.17/111.37 = [n__0()] 441.17/111.37 441.17/111.37 441.17/111.37 We return to the main proof. 441.17/111.37 441.17/111.37 We are left with following problem, upon which TcT provides the 441.17/111.37 certificate YES(O(1),O(n^2)). 441.17/111.37 441.17/111.37 Strict Trs: 441.17/111.37 { isNatKind(n__0()) -> tt() 441.17/111.37 , isNatKind(n__plus(V1, V2)) -> 441.17/111.37 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.37 , activate(X) -> X 441.17/111.37 , activate(n__0()) -> 0() 441.17/111.37 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.37 , activate(n__s(X)) -> s(X) 441.17/111.37 , U13(tt(), V1, V2) -> 441.17/111.37 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.37 , U16(tt()) -> tt() 441.17/111.37 , U23(tt()) -> tt() 441.17/111.37 , U32(tt()) -> tt() 441.17/111.37 , U41(tt()) -> tt() 441.17/111.37 , U63(tt(), M, N) -> 441.17/111.37 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.37 , s(X) -> n__s(X) 441.17/111.37 , plus(X1, X2) -> n__plus(X1, X2) 441.17/111.37 , 0() -> n__0() } 441.17/111.37 Weak Trs: 441.17/111.37 { U11(tt(), V1, V2) -> 441.17/111.37 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.37 , U12(tt(), V1, V2) -> 441.17/111.37 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.37 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.37 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.37 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.37 , isNat(n__0()) -> tt() 441.17/111.37 , isNat(n__plus(V1, V2)) -> 441.17/111.37 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.37 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.37 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.37 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.37 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.37 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.37 , U52(tt(), N) -> activate(N) 441.17/111.37 , U61(tt(), M, N) -> 441.17/111.37 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.17/111.37 , U62(tt(), M, N) -> 441.17/111.37 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.37 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) } 441.17/111.37 Obligation: 441.17/111.37 innermost runtime complexity 441.17/111.37 Answer: 441.17/111.37 YES(O(1),O(n^2)) 441.17/111.37 441.17/111.37 We use the processor 'matrix interpretation of dimension 2' to 441.17/111.37 orient following rules strictly. 441.17/111.37 441.17/111.37 Trs: 441.17/111.37 { U13(tt(), V1, V2) -> 441.17/111.37 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.37 , U41(tt()) -> tt() 441.17/111.37 , U63(tt(), M, N) -> 441.17/111.37 U64(isNatKind(activate(N)), activate(M), activate(N)) } 441.17/111.37 441.17/111.37 The induced complexity on above rules (modulo remaining rules) is 441.17/111.37 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.17/111.37 component(s). 441.17/111.37 441.17/111.37 Sub-proof: 441.17/111.37 ---------- 441.17/111.37 The following argument positions are usable: 441.17/111.37 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.17/111.37 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.17/111.37 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.17/111.37 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.17/111.37 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.17/111.37 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.17/111.37 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.17/111.37 Uargs(plus) = {1, 2} 441.17/111.37 441.17/111.37 TcT has computed the following constructor-based matrix 441.17/111.37 interpretation satisfying not(EDA). 441.17/111.37 441.17/111.37 [U11](x1, x2, x3) = [1 0] x1 + [4 4] x2 + [6 4] x3 + [0] 441.17/111.37 [0 0] [0 0] [0 0] [4] 441.17/111.37 441.17/111.37 [tt] = [4] 441.17/111.37 [0] 441.17/111.37 441.17/111.37 [U12](x1, x2, x3) = [1 0] x1 + [2 4] x2 + [6 4] x3 + [0] 441.17/111.37 [0 0] [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [isNatKind](x1) = [2 0] x1 + [0] 441.17/111.37 [4 4] [0] 441.17/111.37 441.17/111.37 [activate](x1) = [1 0] x1 + [0] 441.17/111.37 [0 1] [0] 441.17/111.37 441.17/111.37 [U13](x1, x2, x3) = [1 0] x1 + [2 4] x2 + [4 4] x3 + [0] 441.17/111.37 [0 0] [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U14](x1, x2, x3) = [1 0] x1 + [2 4] x2 + [2 4] x3 + [0] 441.17/111.37 [0 0] [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U15](x1, x2) = [1 0] x1 + [2 4] x2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [isNat](x1) = [2 4] x1 + [0] 441.17/111.37 [0 0] [4] 441.17/111.37 441.17/111.37 [U16](x1) = [1 0] x1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 441.17/111.37 [U21](x1, x2) = [1 0] x1 + [4 4] x2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U22](x1, x2) = [1 0] x1 + [2 4] x2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U23](x1) = [1 0] x1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 441.17/111.37 [U31](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 441.17/111.37 [U32](x1) = [1 0] x1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 441.17/111.37 [U41](x1) = [1 0] x1 + [4] 441.17/111.37 [0 0] [4] 441.17/111.37 441.17/111.37 [U51](x1, x2) = [0 4] x1 + [7 7] x2 + [3] 441.17/111.37 [0 7] [7 7] [3] 441.17/111.37 441.17/111.37 [U52](x1, x2) = [1 0] x1 + [4 0] x2 + [0] 441.17/111.37 [0 0] [0 1] [0] 441.17/111.37 441.17/111.37 [U61](x1, x2, x3) = [0 4] x1 + [7 7] x2 + [7 7] x3 + [7] 441.17/111.37 [0 7] [7 7] [7 7] [7] 441.17/111.37 441.17/111.37 [U62](x1, x2, x3) = [1 0] x1 + [4 0] x2 + [7 4] x3 + [0] 441.17/111.37 [0 0] [4 4] [6 5] [4] 441.17/111.37 441.17/111.37 [U63](x1, x2, x3) = [1 0] x1 + [4 0] x2 + [5 0] x3 + [0] 441.17/111.37 [1 0] [4 4] [4 1] [0] 441.17/111.37 441.17/111.37 [U64](x1, x2, x3) = [2 0] x1 + [4 0] x2 + [1 0] x3 + [0] 441.17/111.37 [0 0] [2 4] [4 1] [0] 441.17/111.37 441.17/111.37 [s](x1) = [1 0] x1 + [2] 441.17/111.37 [1 1] [0] 441.17/111.37 441.17/111.37 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 441.17/111.37 [n__0] = [2] 441.17/111.37 [0] 441.17/111.37 441.17/111.37 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 441.17/111.37 [n__s](x1) = [1 0] x1 + [2] 441.17/111.37 [1 1] [0] 441.17/111.37 441.17/111.37 [0] = [2] 441.17/111.37 [0] 441.17/111.37 441.17/111.37 The order satisfies the following ordering constraints: 441.17/111.37 441.17/111.37 [U11(tt(), V1, V2)] = [4 4] V1 + [6 4] V2 + [4] 441.17/111.37 [0 0] [0 0] [4] 441.17/111.37 > [4 4] V1 + [6 4] V2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.37 441.17/111.37 [U12(tt(), V1, V2)] = [2 4] V1 + [6 4] V2 + [4] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 > [2 4] V1 + [6 4] V2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.37 441.17/111.37 [isNatKind(n__0())] = [4] 441.17/111.37 [8] 441.17/111.37 >= [4] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [isNatKind(n__plus(V1, V2))] = [2 0] V1 + [2 0] V2 + [0] 441.17/111.37 [8 4] [8 4] [0] 441.17/111.37 >= [2 0] V1 + [2 0] V2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 = [U31(isNatKind(activate(V1)), activate(V2))] 441.17/111.37 441.17/111.37 [isNatKind(n__s(V1))] = [2 0] V1 + [4] 441.17/111.37 [8 4] [8] 441.17/111.37 >= [2 0] V1 + [4] 441.17/111.37 [0 0] [4] 441.17/111.37 = [U41(isNatKind(activate(V1)))] 441.17/111.37 441.17/111.37 [activate(X)] = [1 0] X + [0] 441.17/111.37 [0 1] [0] 441.17/111.37 >= [1 0] X + [0] 441.17/111.37 [0 1] [0] 441.17/111.37 = [X] 441.17/111.37 441.17/111.37 [activate(n__0())] = [2] 441.17/111.37 [0] 441.17/111.37 >= [2] 441.17/111.37 [0] 441.17/111.37 = [0()] 441.17/111.37 441.17/111.37 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 >= [1 0] X1 + [1 0] X2 + [0] 441.17/111.37 [1 1] [1 1] [0] 441.17/111.37 = [plus(X1, X2)] 441.17/111.37 441.17/111.37 [activate(n__s(X))] = [1 0] X + [2] 441.17/111.37 [1 1] [0] 441.17/111.37 >= [1 0] X + [2] 441.17/111.37 [1 1] [0] 441.17/111.37 = [s(X)] 441.17/111.37 441.17/111.37 [U13(tt(), V1, V2)] = [2 4] V1 + [4 4] V2 + [4] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 > [2 4] V1 + [4 4] V2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.37 441.17/111.37 [U14(tt(), V1, V2)] = [2 4] V1 + [2 4] V2 + [4] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 > [2 4] V1 + [2 4] V2 + [0] 441.17/111.37 [0 0] [0 0] [0] 441.17/111.37 = [U15(isNat(activate(V1)), activate(V2))] 441.17/111.37 441.17/111.37 [U15(tt(), V2)] = [2 4] V2 + [4] 441.17/111.37 [0 0] [0] 441.17/111.37 > [2 4] V2 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U16(isNat(activate(V2)))] 441.17/111.37 441.17/111.37 [isNat(n__0())] = [4] 441.17/111.37 [4] 441.17/111.37 >= [4] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [isNat(n__plus(V1, V2))] = [6 4] V1 + [6 4] V2 + [0] 441.17/111.37 [0 0] [0 0] [4] 441.17/111.37 >= [6 4] V1 + [6 4] V2 + [0] 441.17/111.37 [0 0] [0 0] [4] 441.17/111.37 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.37 441.17/111.37 [isNat(n__s(V1))] = [6 4] V1 + [4] 441.17/111.37 [0 0] [4] 441.17/111.37 > [6 4] V1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U21(isNatKind(activate(V1)), activate(V1))] 441.17/111.37 441.17/111.37 [U16(tt())] = [4] 441.17/111.37 [0] 441.17/111.37 >= [4] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [U21(tt(), V1)] = [4 4] V1 + [4] 441.17/111.37 [0 0] [0] 441.17/111.37 > [4 4] V1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U22(isNatKind(activate(V1)), activate(V1))] 441.17/111.37 441.17/111.37 [U22(tt(), V1)] = [2 4] V1 + [4] 441.17/111.37 [0 0] [0] 441.17/111.37 > [2 4] V1 + [0] 441.17/111.37 [0 0] [0] 441.17/111.37 = [U23(isNat(activate(V1)))] 441.17/111.37 441.17/111.37 [U23(tt())] = [4] 441.17/111.37 [0] 441.17/111.37 >= [4] 441.17/111.37 [0] 441.17/111.37 = [tt()] 441.17/111.37 441.17/111.37 [U31(tt(), V2)] = [2 0] V2 + [4] 441.17/111.37 [0 0] [0] 441.17/111.37 > [2 0] V2 + [0] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U32(isNatKind(activate(V2)))] 441.17/111.38 441.17/111.38 [U32(tt())] = [4] 441.17/111.38 [0] 441.17/111.38 >= [4] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U41(tt())] = [8] 441.17/111.38 [4] 441.17/111.38 > [4] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U51(tt(), N)] = [7 7] N + [3] 441.17/111.38 [7 7] [3] 441.17/111.38 > [6 0] N + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 = [U52(isNatKind(activate(N)), activate(N))] 441.17/111.38 441.17/111.38 [U52(tt(), N)] = [4 0] N + [4] 441.17/111.38 [0 1] [0] 441.17/111.38 > [1 0] N + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 = [activate(N)] 441.17/111.38 441.17/111.38 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [7] 441.17/111.38 [7 7] [7 7] [7] 441.17/111.38 > [7 4] N + [6 0] M + [0] 441.17/111.38 [6 5] [4 4] [4] 441.17/111.38 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U62(tt(), M, N)] = [7 4] N + [4 0] M + [4] 441.17/111.38 [6 5] [4 4] [4] 441.17/111.38 > [7 4] N + [4 0] M + [0] 441.17/111.38 [6 5] [4 4] [0] 441.17/111.38 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U63(tt(), M, N)] = [5 0] N + [4 0] M + [4] 441.17/111.38 [4 1] [4 4] [4] 441.17/111.38 > [5 0] N + [4 0] M + [0] 441.17/111.38 [4 1] [2 4] [0] 441.17/111.38 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U64(tt(), M, N)] = [1 0] N + [4 0] M + [8] 441.17/111.38 [4 1] [2 4] [0] 441.17/111.38 > [1 0] N + [1 0] M + [2] 441.17/111.38 [2 1] [2 1] [0] 441.17/111.38 = [s(plus(activate(N), activate(M)))] 441.17/111.38 441.17/111.38 [s(X)] = [1 0] X + [2] 441.17/111.38 [1 1] [0] 441.17/111.38 >= [1 0] X + [2] 441.17/111.38 [1 1] [0] 441.17/111.38 = [n__s(X)] 441.17/111.38 441.17/111.38 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 >= [1 0] X1 + [1 0] X2 + [0] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 = [n__plus(X1, X2)] 441.17/111.38 441.17/111.38 [0()] = [2] 441.17/111.38 [0] 441.17/111.38 >= [2] 441.17/111.38 [0] 441.17/111.38 = [n__0()] 441.17/111.38 441.17/111.38 441.17/111.38 We return to the main proof. 441.17/111.38 441.17/111.38 We are left with following problem, upon which TcT provides the 441.17/111.38 certificate YES(O(1),O(n^2)). 441.17/111.38 441.17/111.38 Strict Trs: 441.17/111.38 { isNatKind(n__0()) -> tt() 441.17/111.38 , isNatKind(n__plus(V1, V2)) -> 441.17/111.38 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.38 , activate(X) -> X 441.17/111.38 , activate(n__0()) -> 0() 441.17/111.38 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.38 , activate(n__s(X)) -> s(X) 441.17/111.38 , U16(tt()) -> tt() 441.17/111.38 , U23(tt()) -> tt() 441.17/111.38 , U32(tt()) -> tt() 441.17/111.38 , s(X) -> n__s(X) 441.17/111.38 , plus(X1, X2) -> n__plus(X1, X2) 441.17/111.38 , 0() -> n__0() } 441.17/111.38 Weak Trs: 441.17/111.38 { U11(tt(), V1, V2) -> 441.17/111.38 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.38 , U12(tt(), V1, V2) -> 441.17/111.38 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.38 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.38 , U13(tt(), V1, V2) -> 441.17/111.38 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.38 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.38 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.38 , isNat(n__0()) -> tt() 441.17/111.38 , isNat(n__plus(V1, V2)) -> 441.17/111.38 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.38 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.38 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.38 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.38 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.38 , U41(tt()) -> tt() 441.17/111.38 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.38 , U52(tt(), N) -> activate(N) 441.17/111.38 , U61(tt(), M, N) -> 441.17/111.38 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.17/111.38 , U62(tt(), M, N) -> 441.17/111.38 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.38 , U63(tt(), M, N) -> 441.17/111.38 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.38 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) } 441.17/111.38 Obligation: 441.17/111.38 innermost runtime complexity 441.17/111.38 Answer: 441.17/111.38 YES(O(1),O(n^2)) 441.17/111.38 441.17/111.38 We use the processor 'matrix interpretation of dimension 2' to 441.17/111.38 orient following rules strictly. 441.17/111.38 441.17/111.38 Trs: 441.17/111.38 { isNatKind(n__0()) -> tt() 441.17/111.38 , U16(tt()) -> tt() 441.17/111.38 , U23(tt()) -> tt() 441.17/111.38 , U32(tt()) -> tt() } 441.17/111.38 441.17/111.38 The induced complexity on above rules (modulo remaining rules) is 441.17/111.38 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.17/111.38 component(s). 441.17/111.38 441.17/111.38 Sub-proof: 441.17/111.38 ---------- 441.17/111.38 The following argument positions are usable: 441.17/111.38 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.17/111.38 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.17/111.38 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.17/111.38 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.17/111.38 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.17/111.38 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.17/111.38 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.17/111.38 Uargs(plus) = {1, 2} 441.17/111.38 441.17/111.38 TcT has computed the following constructor-based matrix 441.17/111.38 interpretation satisfying not(EDA). 441.17/111.38 441.17/111.38 [U11](x1, x2, x3) = [1 0] x1 + [3 5] x2 + [6 5] x3 + [0] 441.17/111.38 [0 0] [4 4] [0 0] [0] 441.17/111.38 441.17/111.38 [tt] = [1] 441.17/111.38 [0] 441.17/111.38 441.17/111.38 [U12](x1, x2, x3) = [1 0] x1 + [1 5] x2 + [6 5] x3 + [0] 441.17/111.38 [0 0] [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [isNatKind](x1) = [2 0] x1 + [0] 441.17/111.38 [1 0] [0] 441.17/111.38 441.17/111.38 [activate](x1) = [1 0] x1 + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 441.17/111.38 [U13](x1, x2, x3) = [1 0] x1 + [1 5] x2 + [4 5] x3 + [0] 441.17/111.38 [0 0] [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U14](x1, x2, x3) = [1 0] x1 + [1 5] x2 + [1 5] x3 + [1] 441.17/111.38 [0 0] [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U15](x1, x2) = [1 0] x1 + [1 5] x2 + [2] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [isNat](x1) = [1 5] x1 + [0] 441.17/111.38 [0 4] [0] 441.17/111.38 441.17/111.38 [U16](x1) = [1 0] x1 + [3] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U21](x1, x2) = [1 1] x1 + [3 5] x2 + [4] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U22](x1, x2) = [1 0] x1 + [1 5] x2 + [4] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U23](x1) = [1 0] x1 + [4] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U31](x1, x2) = [1 0] x1 + [2 0] x2 + [2] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U32](x1) = [1 0] x1 + [2] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U41](x1) = [1 0] x1 + [4] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U51](x1, x2) = [0 4] x1 + [7 7] x2 + [3] 441.17/111.38 [0 7] [7 7] [7] 441.17/111.38 441.17/111.38 [U52](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.38 [0 0] [0 1] [0] 441.17/111.38 441.17/111.38 [U61](x1, x2, x3) = [0 4] x1 + [7 7] x2 + [7 7] x3 + [7] 441.17/111.38 [0 7] [7 7] [7 7] [7] 441.17/111.38 441.17/111.38 [U62](x1, x2, x3) = [2 0] x1 + [1 0] x2 + [5 5] x3 + [4] 441.17/111.38 [0 0] [4 4] [4 4] [4] 441.17/111.38 441.17/111.38 [U63](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [4 0] x3 + [4] 441.17/111.38 [0 0] [4 4] [2 2] [4] 441.17/111.38 441.17/111.38 [U64](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [4] 441.17/111.38 [0 0] [4 4] [2 2] [4] 441.17/111.38 441.17/111.38 [s](x1) = [1 0] x1 + [4] 441.17/111.38 [1 1] [0] 441.17/111.38 441.17/111.38 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 441.17/111.38 [n__0] = [2] 441.17/111.38 [0] 441.17/111.38 441.17/111.38 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 441.17/111.38 [n__s](x1) = [1 0] x1 + [4] 441.17/111.38 [1 1] [0] 441.17/111.38 441.17/111.38 [0] = [2] 441.17/111.38 [0] 441.17/111.38 441.17/111.38 The order satisfies the following ordering constraints: 441.17/111.38 441.17/111.38 [U11(tt(), V1, V2)] = [3 5] V1 + [6 5] V2 + [1] 441.17/111.38 [4 4] [0 0] [0] 441.17/111.38 > [3 5] V1 + [6 5] V2 + [0] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.38 441.17/111.38 [U12(tt(), V1, V2)] = [1 5] V1 + [6 5] V2 + [1] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 > [1 5] V1 + [6 5] V2 + [0] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.38 441.17/111.38 [isNatKind(n__0())] = [4] 441.17/111.38 [2] 441.17/111.38 > [1] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [isNatKind(n__plus(V1, V2))] = [2 0] V1 + [2 0] V2 + [2] 441.17/111.38 [1 0] [1 0] [1] 441.17/111.38 >= [2 0] V1 + [2 0] V2 + [2] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U31(isNatKind(activate(V1)), activate(V2))] 441.17/111.38 441.17/111.38 [isNatKind(n__s(V1))] = [2 0] V1 + [8] 441.17/111.38 [1 0] [4] 441.17/111.38 > [2 0] V1 + [4] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U41(isNatKind(activate(V1)))] 441.17/111.38 441.17/111.38 [activate(X)] = [1 0] X + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 >= [1 0] X + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 = [X] 441.17/111.38 441.17/111.38 [activate(n__0())] = [2] 441.17/111.38 [0] 441.17/111.38 >= [2] 441.17/111.38 [0] 441.17/111.38 = [0()] 441.17/111.38 441.17/111.38 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 >= [1 0] X1 + [1 0] X2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 = [plus(X1, X2)] 441.17/111.38 441.17/111.38 [activate(n__s(X))] = [1 0] X + [4] 441.17/111.38 [1 1] [0] 441.17/111.38 >= [1 0] X + [4] 441.17/111.38 [1 1] [0] 441.17/111.38 = [s(X)] 441.17/111.38 441.17/111.38 [U13(tt(), V1, V2)] = [1 5] V1 + [4 5] V2 + [1] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 >= [1 5] V1 + [3 5] V2 + [1] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.38 441.17/111.38 [U14(tt(), V1, V2)] = [1 5] V1 + [1 5] V2 + [2] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 >= [1 5] V1 + [1 5] V2 + [2] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U15(isNat(activate(V1)), activate(V2))] 441.17/111.38 441.17/111.38 [U15(tt(), V2)] = [1 5] V2 + [3] 441.17/111.38 [0 0] [0] 441.17/111.38 >= [1 5] V2 + [3] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U16(isNat(activate(V2)))] 441.17/111.38 441.17/111.38 [isNat(n__0())] = [2] 441.17/111.38 [0] 441.17/111.38 > [1] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [isNat(n__plus(V1, V2))] = [6 5] V1 + [6 5] V2 + [1] 441.17/111.38 [4 4] [4 4] [0] 441.17/111.38 > [5 5] V1 + [6 5] V2 + [0] 441.17/111.38 [4 4] [0 0] [0] 441.17/111.38 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.38 441.17/111.38 [isNat(n__s(V1))] = [6 5] V1 + [4] 441.17/111.38 [4 4] [0] 441.17/111.38 >= [6 5] V1 + [4] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U21(isNatKind(activate(V1)), activate(V1))] 441.17/111.38 441.17/111.38 [U16(tt())] = [4] 441.17/111.38 [0] 441.17/111.38 > [1] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U21(tt(), V1)] = [3 5] V1 + [5] 441.17/111.38 [0 0] [0] 441.17/111.38 > [3 5] V1 + [4] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U22(isNatKind(activate(V1)), activate(V1))] 441.17/111.38 441.17/111.38 [U22(tt(), V1)] = [1 5] V1 + [5] 441.17/111.38 [0 0] [0] 441.17/111.38 > [1 5] V1 + [4] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U23(isNat(activate(V1)))] 441.17/111.38 441.17/111.38 [U23(tt())] = [5] 441.17/111.38 [0] 441.17/111.38 > [1] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U31(tt(), V2)] = [2 0] V2 + [3] 441.17/111.38 [0 0] [0] 441.17/111.38 > [2 0] V2 + [2] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U32(isNatKind(activate(V2)))] 441.17/111.38 441.17/111.38 [U32(tt())] = [3] 441.17/111.38 [0] 441.17/111.38 > [1] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U41(tt())] = [5] 441.17/111.38 [0] 441.17/111.38 > [1] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U51(tt(), N)] = [7 7] N + [3] 441.17/111.38 [7 7] [7] 441.17/111.38 > [3 0] N + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 = [U52(isNatKind(activate(N)), activate(N))] 441.17/111.38 441.17/111.38 [U52(tt(), N)] = [1 0] N + [1] 441.17/111.38 [0 1] [0] 441.17/111.38 > [1 0] N + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 = [activate(N)] 441.17/111.38 441.17/111.38 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [7] 441.17/111.38 [7 7] [7 7] [7] 441.17/111.38 > [5 5] N + [5 0] M + [4] 441.17/111.38 [4 4] [4 4] [4] 441.17/111.38 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U62(tt(), M, N)] = [5 5] N + [1 0] M + [6] 441.17/111.38 [4 4] [4 4] [4] 441.17/111.38 > [5 5] N + [1 0] M + [4] 441.17/111.38 [2 2] [4 4] [4] 441.17/111.38 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U63(tt(), M, N)] = [4 0] N + [1 0] M + [5] 441.17/111.38 [2 2] [4 4] [4] 441.17/111.38 > [4 0] N + [1 0] M + [4] 441.17/111.38 [2 2] [4 4] [4] 441.17/111.38 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U64(tt(), M, N)] = [2 0] N + [1 0] M + [5] 441.17/111.38 [2 2] [4 4] [4] 441.17/111.38 >= [1 0] N + [1 0] M + [5] 441.17/111.38 [2 1] [2 1] [1] 441.17/111.38 = [s(plus(activate(N), activate(M)))] 441.17/111.38 441.17/111.38 [s(X)] = [1 0] X + [4] 441.17/111.38 [1 1] [0] 441.17/111.38 >= [1 0] X + [4] 441.17/111.38 [1 1] [0] 441.17/111.38 = [n__s(X)] 441.17/111.38 441.17/111.38 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 >= [1 0] X1 + [1 0] X2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 = [n__plus(X1, X2)] 441.17/111.38 441.17/111.38 [0()] = [2] 441.17/111.38 [0] 441.17/111.38 >= [2] 441.17/111.38 [0] 441.17/111.38 = [n__0()] 441.17/111.38 441.17/111.38 441.17/111.38 We return to the main proof. 441.17/111.38 441.17/111.38 We are left with following problem, upon which TcT provides the 441.17/111.38 certificate YES(O(1),O(n^2)). 441.17/111.38 441.17/111.38 Strict Trs: 441.17/111.38 { isNatKind(n__plus(V1, V2)) -> 441.17/111.38 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.38 , activate(X) -> X 441.17/111.38 , activate(n__0()) -> 0() 441.17/111.38 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.38 , activate(n__s(X)) -> s(X) 441.17/111.38 , s(X) -> n__s(X) 441.17/111.38 , plus(X1, X2) -> n__plus(X1, X2) 441.17/111.38 , 0() -> n__0() } 441.17/111.38 Weak Trs: 441.17/111.38 { U11(tt(), V1, V2) -> 441.17/111.38 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.38 , U12(tt(), V1, V2) -> 441.17/111.38 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.38 , isNatKind(n__0()) -> tt() 441.17/111.38 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.38 , U13(tt(), V1, V2) -> 441.17/111.38 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.38 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.38 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.38 , isNat(n__0()) -> tt() 441.17/111.38 , isNat(n__plus(V1, V2)) -> 441.17/111.38 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.38 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.38 , U16(tt()) -> tt() 441.17/111.38 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.38 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.38 , U23(tt()) -> tt() 441.17/111.38 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.38 , U32(tt()) -> tt() 441.17/111.38 , U41(tt()) -> tt() 441.17/111.38 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.38 , U52(tt(), N) -> activate(N) 441.17/111.38 , U61(tt(), M, N) -> 441.17/111.38 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.17/111.38 , U62(tt(), M, N) -> 441.17/111.38 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.38 , U63(tt(), M, N) -> 441.17/111.38 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.38 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) } 441.17/111.38 Obligation: 441.17/111.38 innermost runtime complexity 441.17/111.38 Answer: 441.17/111.38 YES(O(1),O(n^2)) 441.17/111.38 441.17/111.38 We use the processor 'matrix interpretation of dimension 2' to 441.17/111.38 orient following rules strictly. 441.17/111.38 441.17/111.38 Trs: 441.17/111.38 { isNatKind(n__plus(V1, V2)) -> 441.17/111.38 U31(isNatKind(activate(V1)), activate(V2)) } 441.17/111.38 441.17/111.38 The induced complexity on above rules (modulo remaining rules) is 441.17/111.38 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.17/111.38 component(s). 441.17/111.38 441.17/111.38 Sub-proof: 441.17/111.38 ---------- 441.17/111.38 The following argument positions are usable: 441.17/111.38 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.17/111.38 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.17/111.38 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.17/111.38 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.17/111.38 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.17/111.38 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.17/111.38 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.17/111.38 Uargs(plus) = {1, 2} 441.17/111.38 441.17/111.38 TcT has computed the following constructor-based matrix 441.17/111.38 interpretation satisfying not(EDA). 441.17/111.38 441.17/111.38 [U11](x1, x2, x3) = [1 0] x1 + [5 7] x2 + [7 7] x3 + [4] 441.17/111.38 [0 0] [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [tt] = [4] 441.17/111.38 [0] 441.17/111.38 441.17/111.38 [U12](x1, x2, x3) = [2 0] x1 + [1 7] x2 + [7 7] x3 + [0] 441.17/111.38 [0 0] [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [isNatKind](x1) = [2 0] x1 + [0] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [activate](x1) = [1 0] x1 + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 441.17/111.38 [U13](x1, x2, x3) = [1 0] x1 + [1 7] x2 + [5 7] x3 + [0] 441.17/111.38 [0 0] [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U14](x1, x2, x3) = [2 0] x1 + [1 7] x2 + [1 7] x3 + [2] 441.17/111.38 [0 0] [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U15](x1, x2) = [1 0] x1 + [1 7] x2 + [3] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [isNat](x1) = [1 7] x1 + [7] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U16](x1) = [1 0] x1 + [0] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U21](x1, x2) = [1 0] x1 + [3 7] x2 + [3] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U22](x1, x2) = [1 0] x1 + [1 7] x2 + [7] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U23](x1) = [1 0] x1 + [4] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U31](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 441.17/111.38 [U32](x1) = [1 0] x1 + [0] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U41](x1) = [1 0] x1 + [0] 441.17/111.38 [0 0] [0] 441.17/111.38 441.17/111.38 [U51](x1, x2) = [0 4] x1 + [7 7] x2 + [7] 441.17/111.38 [0 7] [7 7] [7] 441.17/111.38 441.17/111.38 [U52](x1, x2) = [1 0] x1 + [4 0] x2 + [0] 441.17/111.38 [0 0] [0 1] [0] 441.17/111.38 441.17/111.38 [U61](x1, x2, x3) = [2 4] x1 + [7 7] x2 + [7 7] x3 + [3] 441.17/111.38 [0 7] [7 7] [7 7] [7] 441.17/111.38 441.17/111.38 [U62](x1, x2, x3) = [3 0] x1 + [1 0] x2 + [4 7] x3 + [0] 441.17/111.38 [0 0] [4 1] [4 4] [4] 441.17/111.38 441.17/111.38 [U63](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [3 0] x3 + [4] 441.17/111.38 [0 0] [4 1] [4 1] [4] 441.17/111.38 441.17/111.38 [U64](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0] 441.17/111.38 [0 0] [4 1] [4 1] [1] 441.17/111.38 441.17/111.38 [s](x1) = [1 0] x1 + [1] 441.17/111.38 [1 1] [0] 441.17/111.38 441.17/111.38 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 441.17/111.38 [n__0] = [4] 441.17/111.38 [0] 441.17/111.38 441.17/111.38 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 441.17/111.38 [n__s](x1) = [1 0] x1 + [1] 441.17/111.38 [1 1] [0] 441.17/111.38 441.17/111.38 [0] = [4] 441.17/111.38 [0] 441.17/111.38 441.17/111.38 The order satisfies the following ordering constraints: 441.17/111.38 441.17/111.38 [U11(tt(), V1, V2)] = [5 7] V1 + [7 7] V2 + [8] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 > [5 7] V1 + [7 7] V2 + [0] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.38 441.17/111.38 [U12(tt(), V1, V2)] = [1 7] V1 + [7 7] V2 + [8] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 > [1 7] V1 + [7 7] V2 + [0] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.38 441.17/111.38 [isNatKind(n__0())] = [8] 441.17/111.38 [0] 441.17/111.38 > [4] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [isNatKind(n__plus(V1, V2))] = [2 0] V1 + [2 0] V2 + [2] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 > [2 0] V1 + [2 0] V2 + [0] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U31(isNatKind(activate(V1)), activate(V2))] 441.17/111.38 441.17/111.38 [isNatKind(n__s(V1))] = [2 0] V1 + [2] 441.17/111.38 [0 0] [0] 441.17/111.38 > [2 0] V1 + [0] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U41(isNatKind(activate(V1)))] 441.17/111.38 441.17/111.38 [activate(X)] = [1 0] X + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 >= [1 0] X + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 = [X] 441.17/111.38 441.17/111.38 [activate(n__0())] = [4] 441.17/111.38 [0] 441.17/111.38 >= [4] 441.17/111.38 [0] 441.17/111.38 = [0()] 441.17/111.38 441.17/111.38 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 >= [1 0] X1 + [1 0] X2 + [1] 441.17/111.38 [1 1] [1 1] [0] 441.17/111.38 = [plus(X1, X2)] 441.17/111.38 441.17/111.38 [activate(n__s(X))] = [1 0] X + [1] 441.17/111.38 [1 1] [0] 441.17/111.38 >= [1 0] X + [1] 441.17/111.38 [1 1] [0] 441.17/111.38 = [s(X)] 441.17/111.38 441.17/111.38 [U13(tt(), V1, V2)] = [1 7] V1 + [5 7] V2 + [4] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 > [1 7] V1 + [5 7] V2 + [2] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.38 441.17/111.38 [U14(tt(), V1, V2)] = [1 7] V1 + [1 7] V2 + [10] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 >= [1 7] V1 + [1 7] V2 + [10] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U15(isNat(activate(V1)), activate(V2))] 441.17/111.38 441.17/111.38 [U15(tt(), V2)] = [1 7] V2 + [7] 441.17/111.38 [0 0] [0] 441.17/111.38 >= [1 7] V2 + [7] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U16(isNat(activate(V2)))] 441.17/111.38 441.17/111.38 [isNat(n__0())] = [11] 441.17/111.38 [0] 441.17/111.38 > [4] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [isNat(n__plus(V1, V2))] = [8 7] V1 + [8 7] V2 + [8] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 > [7 7] V1 + [7 7] V2 + [4] 441.17/111.38 [0 0] [0 0] [0] 441.17/111.38 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.38 441.17/111.38 [isNat(n__s(V1))] = [8 7] V1 + [8] 441.17/111.38 [0 0] [0] 441.17/111.38 > [5 7] V1 + [3] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U21(isNatKind(activate(V1)), activate(V1))] 441.17/111.38 441.17/111.38 [U16(tt())] = [4] 441.17/111.38 [0] 441.17/111.38 >= [4] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U21(tt(), V1)] = [3 7] V1 + [7] 441.17/111.38 [0 0] [0] 441.17/111.38 >= [3 7] V1 + [7] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U22(isNatKind(activate(V1)), activate(V1))] 441.17/111.38 441.17/111.38 [U22(tt(), V1)] = [1 7] V1 + [11] 441.17/111.38 [0 0] [0] 441.17/111.38 >= [1 7] V1 + [11] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U23(isNat(activate(V1)))] 441.17/111.38 441.17/111.38 [U23(tt())] = [8] 441.17/111.38 [0] 441.17/111.38 > [4] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U31(tt(), V2)] = [2 0] V2 + [4] 441.17/111.38 [0 0] [0] 441.17/111.38 > [2 0] V2 + [0] 441.17/111.38 [0 0] [0] 441.17/111.38 = [U32(isNatKind(activate(V2)))] 441.17/111.38 441.17/111.38 [U32(tt())] = [4] 441.17/111.38 [0] 441.17/111.38 >= [4] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U41(tt())] = [4] 441.17/111.38 [0] 441.17/111.38 >= [4] 441.17/111.38 [0] 441.17/111.38 = [tt()] 441.17/111.38 441.17/111.38 [U51(tt(), N)] = [7 7] N + [7] 441.17/111.38 [7 7] [7] 441.17/111.38 > [6 0] N + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 = [U52(isNatKind(activate(N)), activate(N))] 441.17/111.38 441.17/111.38 [U52(tt(), N)] = [4 0] N + [4] 441.17/111.38 [0 1] [0] 441.17/111.38 > [1 0] N + [0] 441.17/111.38 [0 1] [0] 441.17/111.38 = [activate(N)] 441.17/111.38 441.17/111.38 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [11] 441.17/111.38 [7 7] [7 7] [7] 441.17/111.38 > [4 7] N + [7 0] M + [0] 441.17/111.38 [4 4] [4 1] [4] 441.17/111.38 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U62(tt(), M, N)] = [4 7] N + [1 0] M + [12] 441.17/111.38 [4 4] [4 1] [4] 441.17/111.38 > [4 7] N + [1 0] M + [11] 441.17/111.38 [4 1] [4 1] [4] 441.17/111.38 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U63(tt(), M, N)] = [3 0] N + [1 0] M + [8] 441.17/111.38 [4 1] [4 1] [4] 441.17/111.38 > [3 0] N + [1 0] M + [0] 441.17/111.38 [4 1] [4 1] [1] 441.17/111.38 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.17/111.38 441.17/111.38 [U64(tt(), M, N)] = [1 0] N + [1 0] M + [4] 441.17/111.38 [4 1] [4 1] [1] 441.17/111.38 > [1 0] N + [1 0] M + [2] 441.17/111.38 [2 1] [2 1] [1] 441.17/111.38 = [s(plus(activate(N), activate(M)))] 441.17/111.38 441.17/111.38 [s(X)] = [1 0] X + [1] 441.17/111.38 [1 1] [0] 441.17/111.38 >= [1 0] X + [1] 441.17/111.38 [1 1] [0] 441.17/111.38 = [n__s(X)] 441.17/111.38 441.17/111.38 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [1] 441.17/111.39 [1 1] [1 1] [0] 441.17/111.39 >= [1 0] X1 + [1 0] X2 + [1] 441.17/111.39 [1 1] [1 1] [0] 441.17/111.39 = [n__plus(X1, X2)] 441.17/111.39 441.17/111.39 [0()] = [4] 441.17/111.39 [0] 441.17/111.39 >= [4] 441.17/111.39 [0] 441.17/111.39 = [n__0()] 441.17/111.39 441.17/111.39 441.17/111.39 We return to the main proof. 441.17/111.39 441.17/111.39 We are left with following problem, upon which TcT provides the 441.17/111.39 certificate YES(O(1),O(n^2)). 441.17/111.39 441.17/111.39 Strict Trs: 441.17/111.39 { activate(X) -> X 441.17/111.39 , activate(n__0()) -> 0() 441.17/111.39 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.39 , activate(n__s(X)) -> s(X) 441.17/111.39 , s(X) -> n__s(X) 441.17/111.39 , plus(X1, X2) -> n__plus(X1, X2) 441.17/111.39 , 0() -> n__0() } 441.17/111.39 Weak Trs: 441.17/111.39 { U11(tt(), V1, V2) -> 441.17/111.39 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.39 , U12(tt(), V1, V2) -> 441.17/111.39 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.39 , isNatKind(n__0()) -> tt() 441.17/111.39 , isNatKind(n__plus(V1, V2)) -> 441.17/111.39 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.39 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.39 , U13(tt(), V1, V2) -> 441.17/111.39 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.39 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.39 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.39 , isNat(n__0()) -> tt() 441.17/111.39 , isNat(n__plus(V1, V2)) -> 441.17/111.39 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.39 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.39 , U16(tt()) -> tt() 441.17/111.39 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.39 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.39 , U23(tt()) -> tt() 441.17/111.39 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.39 , U32(tt()) -> tt() 441.17/111.39 , U41(tt()) -> tt() 441.17/111.39 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.39 , U52(tt(), N) -> activate(N) 441.17/111.39 , U61(tt(), M, N) -> 441.17/111.39 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.17/111.39 , U62(tt(), M, N) -> 441.17/111.39 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.39 , U63(tt(), M, N) -> 441.17/111.39 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.39 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) } 441.17/111.39 Obligation: 441.17/111.39 innermost runtime complexity 441.17/111.39 Answer: 441.17/111.39 YES(O(1),O(n^2)) 441.17/111.39 441.17/111.39 We use the processor 'matrix interpretation of dimension 2' to 441.17/111.39 orient following rules strictly. 441.17/111.39 441.17/111.39 Trs: 441.17/111.39 { activate(X) -> X 441.17/111.39 , activate(n__0()) -> 0() 441.17/111.39 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.39 , activate(n__s(X)) -> s(X) } 441.17/111.39 441.17/111.39 The induced complexity on above rules (modulo remaining rules) is 441.17/111.39 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.17/111.39 component(s). 441.17/111.39 441.17/111.39 Sub-proof: 441.17/111.39 ---------- 441.17/111.39 The following argument positions are usable: 441.17/111.39 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.17/111.39 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.17/111.39 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.17/111.39 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.17/111.39 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.17/111.39 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.17/111.39 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.17/111.39 Uargs(plus) = {1, 2} 441.17/111.39 441.17/111.39 TcT has computed the following constructor-based matrix 441.17/111.39 interpretation satisfying not(EDA). 441.17/111.39 441.17/111.39 [U11](x1, x2, x3) = [2 0] x1 + [3 6] x2 + [7 6] x3 + [0] 441.17/111.39 [0 0] [0 0] [0 0] [0] 441.17/111.39 441.17/111.39 [tt] = [7] 441.17/111.39 [0] 441.17/111.39 441.17/111.39 [U12](x1, x2, x3) = [1 0] x1 + [1 6] x2 + [7 6] x3 + [2] 441.17/111.39 [0 0] [0 0] [0 0] [0] 441.17/111.39 441.17/111.39 [isNatKind](x1) = [2 0] x1 + [0] 441.17/111.39 [0 0] [0] 441.17/111.39 441.17/111.39 [activate](x1) = [1 0] x1 + [1] 441.17/111.39 [0 1] [0] 441.17/111.39 441.17/111.39 [U13](x1, x2, x3) = [1 0] x1 + [1 6] x2 + [5 6] x3 + [0] 441.17/111.39 [0 0] [0 0] [0 0] [0] 441.17/111.39 441.17/111.39 [U14](x1, x2, x3) = [2 0] x1 + [1 6] x2 + [1 6] x3 + [0] 441.17/111.39 [0 0] [0 0] [0 0] [0] 441.17/111.39 441.17/111.39 [U15](x1, x2) = [1 0] x1 + [1 6] x2 + [0] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 441.17/111.39 [isNat](x1) = [1 6] x1 + [0] 441.17/111.39 [0 0] [1] 441.17/111.39 441.17/111.39 [U16](x1) = [1 0] x1 + [0] 441.17/111.39 [0 0] [0] 441.17/111.39 441.17/111.39 [U21](x1, x2) = [1 0] x1 + [5 6] x2 + [0] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 441.17/111.39 [U22](x1, x2) = [2 0] x1 + [1 6] x2 + [0] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 441.17/111.39 [U23](x1) = [1 0] x1 + [0] 441.17/111.39 [0 0] [0] 441.17/111.39 441.17/111.39 [U31](x1, x2) = [1 0] x1 + [2 0] x2 + [0] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 441.17/111.39 [U32](x1) = [1 0] x1 + [0] 441.17/111.39 [0 0] [0] 441.17/111.39 441.17/111.39 [U41](x1) = [1 0] x1 + [0] 441.17/111.39 [0 0] [0] 441.17/111.39 441.17/111.39 [U51](x1, x2) = [0 4] x1 + [7 7] x2 + [7] 441.17/111.39 [0 7] [7 7] [3] 441.17/111.39 441.17/111.39 [U52](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.39 [0 0] [0 4] [0] 441.17/111.39 441.17/111.39 [U61](x1, x2, x3) = [1 4] x1 + [7 7] x2 + [7 7] x3 + [7] 441.17/111.39 [1 7] [7 7] [7 7] [7] 441.17/111.39 441.17/111.39 [U62](x1, x2, x3) = [1 0] x1 + [1 4] x2 + [7 6] x3 + [3] 441.17/111.39 [2 0] [2 1] [7 7] [0] 441.17/111.39 441.17/111.39 [U63](x1, x2, x3) = [1 1] x1 + [1 4] x2 + [6 0] x3 + [1] 441.17/111.39 [1 0] [2 1] [6 1] [4] 441.17/111.39 441.17/111.39 [U64](x1, x2, x3) = [1 0] x1 + [1 4] x2 + [4 0] x3 + [0] 441.17/111.39 [2 0] [2 1] [2 1] [0] 441.17/111.39 441.17/111.39 [s](x1) = [1 0] x1 + [1] 441.17/111.39 [1 1] [2] 441.17/111.39 441.17/111.39 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 441.17/111.39 [1 1] [1 1] [2] 441.17/111.39 441.17/111.39 [n__0] = [7] 441.17/111.39 [0] 441.17/111.39 441.17/111.39 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [2] 441.17/111.39 [1 1] [1 1] [2] 441.17/111.39 441.17/111.39 [n__s](x1) = [1 0] x1 + [1] 441.17/111.39 [1 1] [2] 441.17/111.39 441.17/111.39 [0] = [7] 441.17/111.39 [0] 441.17/111.39 441.17/111.39 The order satisfies the following ordering constraints: 441.17/111.39 441.17/111.39 [U11(tt(), V1, V2)] = [3 6] V1 + [7 6] V2 + [14] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 > [3 6] V1 + [7 6] V2 + [12] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.39 441.17/111.39 [U12(tt(), V1, V2)] = [1 6] V1 + [7 6] V2 + [9] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 > [1 6] V1 + [7 6] V2 + [8] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.39 441.17/111.39 [isNatKind(n__0())] = [14] 441.17/111.39 [0] 441.17/111.39 > [7] 441.17/111.39 [0] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [isNatKind(n__plus(V1, V2))] = [2 0] V1 + [2 0] V2 + [4] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 >= [2 0] V1 + [2 0] V2 + [4] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 = [U31(isNatKind(activate(V1)), activate(V2))] 441.17/111.39 441.17/111.39 [isNatKind(n__s(V1))] = [2 0] V1 + [2] 441.17/111.39 [0 0] [0] 441.17/111.39 >= [2 0] V1 + [2] 441.17/111.39 [0 0] [0] 441.17/111.39 = [U41(isNatKind(activate(V1)))] 441.17/111.39 441.17/111.39 [activate(X)] = [1 0] X + [1] 441.17/111.39 [0 1] [0] 441.17/111.39 > [1 0] X + [0] 441.17/111.39 [0 1] [0] 441.17/111.39 = [X] 441.17/111.39 441.17/111.39 [activate(n__0())] = [8] 441.17/111.39 [0] 441.17/111.39 > [7] 441.17/111.39 [0] 441.17/111.39 = [0()] 441.17/111.39 441.17/111.39 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [3] 441.17/111.39 [1 1] [1 1] [2] 441.17/111.39 > [1 0] X1 + [1 0] X2 + [2] 441.17/111.39 [1 1] [1 1] [2] 441.17/111.39 = [plus(X1, X2)] 441.17/111.39 441.17/111.39 [activate(n__s(X))] = [1 0] X + [2] 441.17/111.39 [1 1] [2] 441.17/111.39 > [1 0] X + [1] 441.17/111.39 [1 1] [2] 441.17/111.39 = [s(X)] 441.17/111.39 441.17/111.39 [U13(tt(), V1, V2)] = [1 6] V1 + [5 6] V2 + [7] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 > [1 6] V1 + [5 6] V2 + [6] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.39 441.17/111.39 [U14(tt(), V1, V2)] = [1 6] V1 + [1 6] V2 + [14] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 > [1 6] V1 + [1 6] V2 + [2] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 = [U15(isNat(activate(V1)), activate(V2))] 441.17/111.39 441.17/111.39 [U15(tt(), V2)] = [1 6] V2 + [7] 441.17/111.39 [0 0] [0] 441.17/111.39 > [1 6] V2 + [1] 441.17/111.39 [0 0] [0] 441.17/111.39 = [U16(isNat(activate(V2)))] 441.17/111.39 441.17/111.39 [isNat(n__0())] = [7] 441.17/111.39 [1] 441.17/111.39 >= [7] 441.17/111.39 [0] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [isNat(n__plus(V1, V2))] = [7 6] V1 + [7 6] V2 + [14] 441.17/111.39 [0 0] [0 0] [1] 441.17/111.39 >= [7 6] V1 + [7 6] V2 + [14] 441.17/111.39 [0 0] [0 0] [0] 441.17/111.39 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.39 441.17/111.39 [isNat(n__s(V1))] = [7 6] V1 + [13] 441.17/111.39 [0 0] [1] 441.17/111.39 > [7 6] V1 + [7] 441.17/111.39 [0 0] [0] 441.17/111.39 = [U21(isNatKind(activate(V1)), activate(V1))] 441.17/111.39 441.17/111.39 [U16(tt())] = [7] 441.17/111.39 [0] 441.17/111.39 >= [7] 441.17/111.39 [0] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [U21(tt(), V1)] = [5 6] V1 + [7] 441.17/111.39 [0 0] [0] 441.17/111.39 > [5 6] V1 + [5] 441.17/111.39 [0 0] [0] 441.17/111.39 = [U22(isNatKind(activate(V1)), activate(V1))] 441.17/111.39 441.17/111.39 [U22(tt(), V1)] = [1 6] V1 + [14] 441.17/111.39 [0 0] [0] 441.17/111.39 > [1 6] V1 + [1] 441.17/111.39 [0 0] [0] 441.17/111.39 = [U23(isNat(activate(V1)))] 441.17/111.39 441.17/111.39 [U23(tt())] = [7] 441.17/111.39 [0] 441.17/111.39 >= [7] 441.17/111.39 [0] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [U31(tt(), V2)] = [2 0] V2 + [7] 441.17/111.39 [0 0] [0] 441.17/111.39 > [2 0] V2 + [2] 441.17/111.39 [0 0] [0] 441.17/111.39 = [U32(isNatKind(activate(V2)))] 441.17/111.39 441.17/111.39 [U32(tt())] = [7] 441.17/111.39 [0] 441.17/111.39 >= [7] 441.17/111.39 [0] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [U41(tt())] = [7] 441.17/111.39 [0] 441.17/111.39 >= [7] 441.17/111.39 [0] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [U51(tt(), N)] = [7 7] N + [7] 441.17/111.39 [7 7] [3] 441.17/111.39 > [3 0] N + [3] 441.17/111.39 [0 4] [0] 441.17/111.39 = [U52(isNatKind(activate(N)), activate(N))] 441.17/111.39 441.17/111.39 [U52(tt(), N)] = [1 0] N + [7] 441.17/111.39 [0 4] [0] 441.17/111.39 > [1 0] N + [1] 441.17/111.39 [0 1] [0] 441.17/111.39 = [activate(N)] 441.17/111.39 441.17/111.39 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [14] 441.17/111.39 [7 7] [7 7] [14] 441.17/111.39 > [7 6] N + [3 4] M + [13] 441.17/111.39 [7 7] [6 1] [13] 441.17/111.39 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.17/111.39 441.17/111.39 [U62(tt(), M, N)] = [7 6] N + [1 4] M + [10] 441.17/111.39 [7 7] [2 1] [14] 441.17/111.39 >= [7 6] N + [1 4] M + [10] 441.17/111.39 [7 7] [2 1] [13] 441.17/111.39 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.17/111.39 441.17/111.39 [U63(tt(), M, N)] = [6 0] N + [1 4] M + [8] 441.17/111.39 [6 1] [2 1] [11] 441.17/111.39 > [6 0] N + [1 4] M + [7] 441.17/111.39 [6 1] [2 1] [8] 441.17/111.39 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.17/111.39 441.17/111.39 [U64(tt(), M, N)] = [4 0] N + [1 4] M + [7] 441.17/111.39 [2 1] [2 1] [14] 441.17/111.39 > [1 0] N + [1 0] M + [5] 441.17/111.39 [2 1] [2 1] [10] 441.17/111.39 = [s(plus(activate(N), activate(M)))] 441.17/111.39 441.17/111.39 [s(X)] = [1 0] X + [1] 441.17/111.39 [1 1] [2] 441.17/111.39 >= [1 0] X + [1] 441.17/111.39 [1 1] [2] 441.17/111.39 = [n__s(X)] 441.17/111.39 441.17/111.39 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [2] 441.17/111.39 [1 1] [1 1] [2] 441.17/111.39 >= [1 0] X1 + [1 0] X2 + [2] 441.17/111.39 [1 1] [1 1] [2] 441.17/111.39 = [n__plus(X1, X2)] 441.17/111.39 441.17/111.39 [0()] = [7] 441.17/111.39 [0] 441.17/111.39 >= [7] 441.17/111.39 [0] 441.17/111.39 = [n__0()] 441.17/111.39 441.17/111.39 441.17/111.39 We return to the main proof. 441.17/111.39 441.17/111.39 We are left with following problem, upon which TcT provides the 441.17/111.39 certificate YES(O(1),O(n^2)). 441.17/111.39 441.17/111.39 Strict Trs: 441.17/111.39 { s(X) -> n__s(X) 441.17/111.39 , plus(X1, X2) -> n__plus(X1, X2) 441.17/111.39 , 0() -> n__0() } 441.17/111.39 Weak Trs: 441.17/111.39 { U11(tt(), V1, V2) -> 441.17/111.39 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.39 , U12(tt(), V1, V2) -> 441.17/111.39 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.39 , isNatKind(n__0()) -> tt() 441.17/111.39 , isNatKind(n__plus(V1, V2)) -> 441.17/111.39 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.39 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.39 , activate(X) -> X 441.17/111.39 , activate(n__0()) -> 0() 441.17/111.39 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.39 , activate(n__s(X)) -> s(X) 441.17/111.39 , U13(tt(), V1, V2) -> 441.17/111.39 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.39 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.39 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.39 , isNat(n__0()) -> tt() 441.17/111.39 , isNat(n__plus(V1, V2)) -> 441.17/111.39 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.39 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.39 , U16(tt()) -> tt() 441.17/111.39 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.39 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.39 , U23(tt()) -> tt() 441.17/111.39 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.39 , U32(tt()) -> tt() 441.17/111.39 , U41(tt()) -> tt() 441.17/111.39 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.39 , U52(tt(), N) -> activate(N) 441.17/111.39 , U61(tt(), M, N) -> 441.17/111.39 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.17/111.39 , U62(tt(), M, N) -> 441.17/111.39 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.39 , U63(tt(), M, N) -> 441.17/111.39 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.39 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) } 441.17/111.39 Obligation: 441.17/111.39 innermost runtime complexity 441.17/111.39 Answer: 441.17/111.39 YES(O(1),O(n^2)) 441.17/111.39 441.17/111.39 We use the processor 'matrix interpretation of dimension 2' to 441.17/111.39 orient following rules strictly. 441.17/111.39 441.17/111.39 Trs: { 0() -> n__0() } 441.17/111.39 441.17/111.39 The induced complexity on above rules (modulo remaining rules) is 441.17/111.39 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.17/111.39 component(s). 441.17/111.39 441.17/111.39 Sub-proof: 441.17/111.39 ---------- 441.17/111.39 The following argument positions are usable: 441.17/111.39 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.17/111.39 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.17/111.39 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.17/111.39 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.17/111.39 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.17/111.39 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.17/111.39 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.17/111.39 Uargs(plus) = {1, 2} 441.17/111.39 441.17/111.39 TcT has computed the following constructor-based matrix 441.17/111.39 interpretation satisfying not(EDA). 441.17/111.39 441.17/111.39 [U11](x1, x2, x3) = [2 0] x1 + [2 3] x2 + [3 3] x3 + [0] 441.17/111.39 [0 0] [0 1] [0 0] [0] 441.17/111.39 441.17/111.39 [tt] = [6] 441.17/111.39 [2] 441.17/111.39 441.17/111.39 [U12](x1, x2, x3) = [1 0] x1 + [1 3] x2 + [3 3] x3 + [2] 441.17/111.39 [0 0] [0 1] [0 0] [0] 441.17/111.39 441.17/111.39 [isNatKind](x1) = [1 0] x1 + [0] 441.17/111.39 [0 1] [0] 441.17/111.39 441.17/111.39 [activate](x1) = [1 0] x1 + [2] 441.17/111.39 [0 1] [0] 441.17/111.39 441.17/111.39 [U13](x1, x2, x3) = [1 0] x1 + [1 3] x2 + [2 3] x3 + [0] 441.17/111.39 [0 0] [0 1] [0 0] [0] 441.17/111.39 441.17/111.39 [U14](x1, x2, x3) = [1 0] x1 + [1 3] x2 + [1 3] x3 + [0] 441.17/111.39 [0 0] [0 1] [0 0] [0] 441.17/111.39 441.17/111.39 [U15](x1, x2) = [1 0] x1 + [1 3] x2 + [0] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 441.17/111.39 [isNat](x1) = [1 3] x1 + [1] 441.17/111.39 [0 1] [0] 441.17/111.39 441.17/111.39 [U16](x1) = [1 0] x1 + [0] 441.17/111.39 [0 0] [2] 441.17/111.39 441.17/111.39 [U21](x1, x2) = [1 0] x1 + [2 3] x2 + [0] 441.17/111.39 [0 0] [0 1] [0] 441.17/111.39 441.17/111.39 [U22](x1, x2) = [1 0] x1 + [1 3] x2 + [0] 441.17/111.39 [0 0] [0 1] [0] 441.17/111.39 441.17/111.39 [U23](x1) = [1 0] x1 + [0] 441.17/111.39 [0 1] [0] 441.17/111.39 441.17/111.39 [U31](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.17/111.39 [0 0] [0 0] [2] 441.17/111.39 441.17/111.39 [U32](x1) = [1 0] x1 + [1] 441.17/111.39 [0 0] [2] 441.17/111.39 441.17/111.39 [U41](x1) = [1 0] x1 + [0] 441.17/111.39 [0 1] [0] 441.17/111.39 441.17/111.39 [U51](x1, x2) = [0 4] x1 + [7 7] x2 + [7] 441.17/111.39 [0 4] [7 7] [3] 441.17/111.39 441.17/111.39 [U52](x1, x2) = [1 1] x1 + [4 0] x2 + [1] 441.17/111.39 [0 0] [0 1] [4] 441.17/111.39 441.17/111.39 [U61](x1, x2, x3) = [0 4] x1 + [7 7] x2 + [7 7] x3 + [7] 441.17/111.39 [0 4] [7 7] [7 7] [7] 441.17/111.39 441.17/111.39 [U62](x1, x2, x3) = [1 4] x1 + [2 0] x2 + [4 7] x3 + [0] 441.17/111.39 [0 6] [2 1] [4 7] [3] 441.17/111.39 441.17/111.39 [U63](x1, x2, x3) = [1 4] x1 + [2 0] x2 + [2 0] x3 + [1] 441.17/111.39 [0 6] [2 1] [4 1] [3] 441.17/111.39 441.17/111.39 [U64](x1, x2, x3) = [1 0] x1 + [2 0] x2 + [1 0] x3 + [7] 441.17/111.39 [2 0] [2 1] [2 1] [3] 441.17/111.39 441.17/111.39 [s](x1) = [1 0] x1 + [5] 441.17/111.39 [1 1] [0] 441.17/111.39 441.17/111.39 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [4] 441.17/111.39 [1 1] [1 1] [3] 441.17/111.39 441.17/111.39 [n__0] = [6] 441.17/111.39 [2] 441.17/111.39 441.17/111.39 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [4] 441.17/111.39 [1 1] [1 1] [3] 441.17/111.39 441.17/111.39 [n__s](x1) = [1 0] x1 + [5] 441.17/111.39 [1 1] [0] 441.17/111.39 441.17/111.39 [0] = [7] 441.17/111.39 [2] 441.17/111.39 441.17/111.39 The order satisfies the following ordering constraints: 441.17/111.39 441.17/111.39 [U11(tt(), V1, V2)] = [2 3] V1 + [3 3] V2 + [12] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 >= [2 3] V1 + [3 3] V2 + [12] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.39 441.17/111.39 [U12(tt(), V1, V2)] = [1 3] V1 + [3 3] V2 + [8] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 >= [1 3] V1 + [3 3] V2 + [8] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.39 441.17/111.39 [isNatKind(n__0())] = [6] 441.17/111.39 [2] 441.17/111.39 >= [6] 441.17/111.39 [2] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [isNatKind(n__plus(V1, V2))] = [1 0] V1 + [1 0] V2 + [4] 441.17/111.39 [1 1] [1 1] [3] 441.17/111.39 >= [1 0] V1 + [1 0] V2 + [4] 441.17/111.39 [0 0] [0 0] [2] 441.17/111.39 = [U31(isNatKind(activate(V1)), activate(V2))] 441.17/111.39 441.17/111.39 [isNatKind(n__s(V1))] = [1 0] V1 + [5] 441.17/111.39 [1 1] [0] 441.17/111.39 > [1 0] V1 + [2] 441.17/111.39 [0 1] [0] 441.17/111.39 = [U41(isNatKind(activate(V1)))] 441.17/111.39 441.17/111.39 [activate(X)] = [1 0] X + [2] 441.17/111.39 [0 1] [0] 441.17/111.39 > [1 0] X + [0] 441.17/111.39 [0 1] [0] 441.17/111.39 = [X] 441.17/111.39 441.17/111.39 [activate(n__0())] = [8] 441.17/111.39 [2] 441.17/111.39 > [7] 441.17/111.39 [2] 441.17/111.39 = [0()] 441.17/111.39 441.17/111.39 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [6] 441.17/111.39 [1 1] [1 1] [3] 441.17/111.39 > [1 0] X1 + [1 0] X2 + [4] 441.17/111.39 [1 1] [1 1] [3] 441.17/111.39 = [plus(X1, X2)] 441.17/111.39 441.17/111.39 [activate(n__s(X))] = [1 0] X + [7] 441.17/111.39 [1 1] [0] 441.17/111.39 > [1 0] X + [5] 441.17/111.39 [1 1] [0] 441.17/111.39 = [s(X)] 441.17/111.39 441.17/111.39 [U13(tt(), V1, V2)] = [1 3] V1 + [2 3] V2 + [6] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 >= [1 3] V1 + [2 3] V2 + [6] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.17/111.39 441.17/111.39 [U14(tt(), V1, V2)] = [1 3] V1 + [1 3] V2 + [6] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 > [1 3] V1 + [1 3] V2 + [5] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 = [U15(isNat(activate(V1)), activate(V2))] 441.17/111.39 441.17/111.39 [U15(tt(), V2)] = [1 3] V2 + [6] 441.17/111.39 [0 0] [2] 441.17/111.39 > [1 3] V2 + [3] 441.17/111.39 [0 0] [2] 441.17/111.39 = [U16(isNat(activate(V2)))] 441.17/111.39 441.17/111.39 [isNat(n__0())] = [13] 441.17/111.39 [2] 441.17/111.39 > [6] 441.17/111.39 [2] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [isNat(n__plus(V1, V2))] = [4 3] V1 + [4 3] V2 + [14] 441.17/111.39 [1 1] [1 1] [3] 441.17/111.39 >= [4 3] V1 + [3 3] V2 + [14] 441.17/111.39 [0 1] [0 0] [0] 441.17/111.39 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.17/111.39 441.17/111.39 [isNat(n__s(V1))] = [4 3] V1 + [6] 441.17/111.39 [1 1] [0] 441.17/111.39 >= [3 3] V1 + [6] 441.17/111.39 [0 1] [0] 441.17/111.39 = [U21(isNatKind(activate(V1)), activate(V1))] 441.17/111.39 441.17/111.39 [U16(tt())] = [6] 441.17/111.39 [2] 441.17/111.39 >= [6] 441.17/111.39 [2] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [U21(tt(), V1)] = [2 3] V1 + [6] 441.17/111.39 [0 1] [0] 441.17/111.39 > [2 3] V1 + [4] 441.17/111.39 [0 1] [0] 441.17/111.39 = [U22(isNatKind(activate(V1)), activate(V1))] 441.17/111.39 441.17/111.39 [U22(tt(), V1)] = [1 3] V1 + [6] 441.17/111.39 [0 1] [0] 441.17/111.39 > [1 3] V1 + [3] 441.17/111.39 [0 1] [0] 441.17/111.39 = [U23(isNat(activate(V1)))] 441.17/111.39 441.17/111.39 [U23(tt())] = [6] 441.17/111.39 [2] 441.17/111.39 >= [6] 441.17/111.39 [2] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [U31(tt(), V2)] = [1 0] V2 + [6] 441.17/111.39 [0 0] [2] 441.17/111.39 > [1 0] V2 + [3] 441.17/111.39 [0 0] [2] 441.17/111.39 = [U32(isNatKind(activate(V2)))] 441.17/111.39 441.17/111.39 [U32(tt())] = [7] 441.17/111.39 [2] 441.17/111.39 > [6] 441.17/111.39 [2] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [U41(tt())] = [6] 441.17/111.39 [2] 441.17/111.39 >= [6] 441.17/111.39 [2] 441.17/111.39 = [tt()] 441.17/111.39 441.17/111.39 [U51(tt(), N)] = [7 7] N + [15] 441.17/111.39 [7 7] [11] 441.17/111.39 > [5 1] N + [11] 441.17/111.39 [0 1] [4] 441.17/111.39 = [U52(isNatKind(activate(N)), activate(N))] 441.17/111.39 441.17/111.39 [U52(tt(), N)] = [4 0] N + [9] 441.17/111.39 [0 1] [4] 441.17/111.39 > [1 0] N + [2] 441.17/111.39 [0 1] [0] 441.17/111.39 = [activate(N)] 441.17/111.39 441.17/111.39 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [15] 441.17/111.39 [7 7] [7 7] [15] 441.17/111.39 > [4 7] N + [3 4] M + [14] 441.17/111.39 [4 7] [2 7] [15] 441.17/111.39 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.17/111.40 441.17/111.40 [U62(tt(), M, N)] = [4 7] N + [2 0] M + [14] 441.17/111.40 [4 7] [2 1] [15] 441.17/111.40 > [3 7] N + [2 0] M + [12] 441.17/111.40 [4 7] [2 1] [15] 441.17/111.40 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.17/111.40 441.17/111.40 [U63(tt(), M, N)] = [2 0] N + [2 0] M + [15] 441.17/111.40 [4 1] [2 1] [15] 441.17/111.40 >= [2 0] N + [2 0] M + [15] 441.17/111.40 [4 1] [2 1] [15] 441.17/111.40 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.17/111.40 441.17/111.40 [U64(tt(), M, N)] = [1 0] N + [2 0] M + [13] 441.17/111.40 [2 1] [2 1] [15] 441.17/111.40 >= [1 0] N + [1 0] M + [13] 441.17/111.40 [2 1] [2 1] [15] 441.17/111.40 = [s(plus(activate(N), activate(M)))] 441.17/111.40 441.17/111.40 [s(X)] = [1 0] X + [5] 441.17/111.40 [1 1] [0] 441.17/111.40 >= [1 0] X + [5] 441.17/111.40 [1 1] [0] 441.17/111.40 = [n__s(X)] 441.17/111.40 441.17/111.40 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [4] 441.17/111.40 [1 1] [1 1] [3] 441.17/111.40 >= [1 0] X1 + [1 0] X2 + [4] 441.17/111.40 [1 1] [1 1] [3] 441.17/111.40 = [n__plus(X1, X2)] 441.17/111.40 441.17/111.40 [0()] = [7] 441.17/111.40 [2] 441.17/111.40 > [6] 441.17/111.40 [2] 441.17/111.40 = [n__0()] 441.17/111.40 441.17/111.40 441.17/111.40 We return to the main proof. 441.17/111.40 441.17/111.40 We are left with following problem, upon which TcT provides the 441.17/111.40 certificate YES(O(1),O(n^2)). 441.17/111.40 441.17/111.40 Strict Trs: 441.17/111.40 { s(X) -> n__s(X) 441.17/111.40 , plus(X1, X2) -> n__plus(X1, X2) } 441.17/111.40 Weak Trs: 441.17/111.40 { U11(tt(), V1, V2) -> 441.17/111.40 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.40 , U12(tt(), V1, V2) -> 441.17/111.40 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.40 , isNatKind(n__0()) -> tt() 441.17/111.40 , isNatKind(n__plus(V1, V2)) -> 441.17/111.40 U31(isNatKind(activate(V1)), activate(V2)) 441.17/111.40 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.17/111.40 , activate(X) -> X 441.17/111.40 , activate(n__0()) -> 0() 441.17/111.40 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.17/111.40 , activate(n__s(X)) -> s(X) 441.17/111.40 , U13(tt(), V1, V2) -> 441.17/111.40 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.17/111.40 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.17/111.40 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.17/111.40 , isNat(n__0()) -> tt() 441.17/111.40 , isNat(n__plus(V1, V2)) -> 441.17/111.40 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.17/111.40 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.17/111.40 , U16(tt()) -> tt() 441.17/111.40 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.17/111.40 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.17/111.40 , U23(tt()) -> tt() 441.17/111.40 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.17/111.40 , U32(tt()) -> tt() 441.17/111.40 , U41(tt()) -> tt() 441.17/111.40 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.17/111.40 , U52(tt(), N) -> activate(N) 441.17/111.40 , U61(tt(), M, N) -> 441.17/111.40 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.17/111.40 , U62(tt(), M, N) -> 441.17/111.40 U63(isNat(activate(N)), activate(M), activate(N)) 441.17/111.40 , U63(tt(), M, N) -> 441.17/111.40 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.17/111.40 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) 441.17/111.40 , 0() -> n__0() } 441.17/111.40 Obligation: 441.17/111.40 innermost runtime complexity 441.17/111.40 Answer: 441.17/111.40 YES(O(1),O(n^2)) 441.17/111.40 441.17/111.40 We use the processor 'matrix interpretation of dimension 2' to 441.17/111.40 orient following rules strictly. 441.17/111.40 441.17/111.40 Trs: { s(X) -> n__s(X) } 441.17/111.40 441.17/111.40 The induced complexity on above rules (modulo remaining rules) is 441.17/111.40 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.17/111.40 component(s). 441.17/111.40 441.17/111.40 Sub-proof: 441.17/111.40 ---------- 441.17/111.40 The following argument positions are usable: 441.17/111.40 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.17/111.40 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.17/111.40 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.17/111.40 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.17/111.40 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.17/111.40 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.17/111.40 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.17/111.40 Uargs(plus) = {1, 2} 441.17/111.40 441.17/111.40 TcT has computed the following constructor-based matrix 441.17/111.40 interpretation satisfying not(EDA). 441.17/111.40 441.17/111.40 [U11](x1, x2, x3) = [4 2] x1 + [2 7] x2 + [4 7] x3 + [2] 441.17/111.40 [0 2] [0 0] [0 5] [0] 441.17/111.40 441.17/111.40 [tt] = [0] 441.17/111.40 [5] 441.17/111.40 441.17/111.40 [U12](x1, x2, x3) = [1 0] x1 + [1 7] x2 + [4 7] x3 + [6] 441.17/111.40 [0 0] [0 0] [0 5] [0] 441.17/111.40 441.17/111.40 [isNatKind](x1) = [1 0] x1 + [0] 441.17/111.40 [1 0] [0] 441.17/111.40 441.17/111.40 [activate](x1) = [1 0] x1 + [1] 441.17/111.40 [0 1] [0] 441.17/111.40 441.17/111.40 [U13](x1, x2, x3) = [1 1] x1 + [1 7] x2 + [2 7] x3 + [1] 441.17/111.40 [0 0] [0 0] [0 5] [0] 441.17/111.40 441.17/111.40 [U14](x1, x2, x3) = [1 0] x1 + [1 7] x2 + [1 7] x3 + [3] 441.17/111.40 [0 0] [0 0] [0 5] [0] 441.17/111.40 441.17/111.40 [U15](x1, x2) = [1 0] x1 + [1 7] x2 + [1] 441.17/111.40 [0 0] [0 5] [0] 441.17/111.40 441.17/111.40 [isNat](x1) = [1 7] x1 + [0] 441.17/111.40 [0 5] [0] 441.17/111.40 441.17/111.40 [U16](x1) = [1 0] x1 + [0] 441.17/111.40 [0 1] [0] 441.17/111.40 441.17/111.40 [U21](x1, x2) = [1 1] x1 + [6 7] x2 + [6] 441.44/111.40 [0 0] [0 0] [5] 441.44/111.40 441.44/111.40 [U22](x1, x2) = [2 0] x1 + [4 7] x2 + [4] 441.44/111.40 [0 0] [0 0] [5] 441.44/111.40 441.44/111.40 [U23](x1) = [1 0] x1 + [0] 441.44/111.40 [0 0] [5] 441.44/111.40 441.44/111.40 [U31](x1, x2) = [1 0] x1 + [1 0] x2 + [1] 441.44/111.40 [0 1] [1 0] [4] 441.44/111.40 441.44/111.40 [U32](x1) = [1 0] x1 + [0] 441.44/111.40 [0 1] [0] 441.44/111.40 441.44/111.40 [U41](x1) = [1 0] x1 + [0] 441.44/111.40 [0 1] [0] 441.44/111.40 441.44/111.40 [U51](x1, x2) = [7 0] x1 + [7 7] x2 + [7] 441.44/111.40 [7 0] [7 7] [3] 441.44/111.40 441.44/111.40 [U52](x1, x2) = [1 0] x1 + [4 0] x2 + [2] 441.44/111.40 [0 0] [0 4] [0] 441.44/111.40 441.44/111.40 [U61](x1, x2, x3) = [7 2] x1 + [7 7] x2 + [7 7] x3 + [5] 441.44/111.40 [7 2] [7 7] [7 7] [5] 441.44/111.40 441.44/111.40 [U62](x1, x2, x3) = [2 2] x1 + [2 4] x2 + [5 7] x3 + [3] 441.44/111.40 [0 2] [4 4] [6 6] [2] 441.44/111.40 441.44/111.40 [U63](x1, x2, x3) = [1 0] x1 + [1 4] x2 + [4 0] x3 + [7] 441.44/111.40 [0 1] [2 4] [6 1] [2] 441.44/111.40 441.44/111.40 [U64](x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 0] x3 + [2] 441.44/111.40 [0 3] [2 4] [2 1] [0] 441.44/111.40 441.44/111.40 [s](x1) = [1 0] x1 + [2] 441.44/111.40 [1 1] [2] 441.44/111.40 441.44/111.40 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [7] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 441.44/111.40 [n__0] = [5] 441.44/111.40 [1] 441.44/111.40 441.44/111.40 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [7] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 441.44/111.40 [n__s](x1) = [1 0] x1 + [1] 441.44/111.40 [1 1] [2] 441.44/111.40 441.44/111.40 [0] = [5] 441.44/111.40 [1] 441.44/111.40 441.44/111.40 The order satisfies the following ordering constraints: 441.44/111.40 441.44/111.40 [U11(tt(), V1, V2)] = [2 7] V1 + [4 7] V2 + [12] 441.44/111.40 [0 0] [0 5] [10] 441.44/111.40 >= [2 7] V1 + [4 7] V2 + [12] 441.44/111.40 [0 0] [0 5] [0] 441.44/111.40 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.44/111.40 441.44/111.40 [U12(tt(), V1, V2)] = [1 7] V1 + [4 7] V2 + [6] 441.44/111.40 [0 0] [0 5] [0] 441.44/111.40 >= [1 7] V1 + [4 7] V2 + [6] 441.44/111.40 [0 0] [0 5] [0] 441.44/111.40 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.44/111.40 441.44/111.40 [isNatKind(n__0())] = [5] 441.44/111.40 [5] 441.44/111.40 > [0] 441.44/111.40 [5] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [isNatKind(n__plus(V1, V2))] = [1 0] V1 + [1 0] V2 + [7] 441.44/111.40 [1 0] [1 0] [7] 441.44/111.40 > [1 0] V1 + [1 0] V2 + [3] 441.44/111.40 [1 0] [1 0] [6] 441.44/111.40 = [U31(isNatKind(activate(V1)), activate(V2))] 441.44/111.40 441.44/111.40 [isNatKind(n__s(V1))] = [1 0] V1 + [1] 441.44/111.40 [1 0] [1] 441.44/111.40 >= [1 0] V1 + [1] 441.44/111.40 [1 0] [1] 441.44/111.40 = [U41(isNatKind(activate(V1)))] 441.44/111.40 441.44/111.40 [activate(X)] = [1 0] X + [1] 441.44/111.40 [0 1] [0] 441.44/111.40 > [1 0] X + [0] 441.44/111.40 [0 1] [0] 441.44/111.40 = [X] 441.44/111.40 441.44/111.40 [activate(n__0())] = [6] 441.44/111.40 [1] 441.44/111.40 > [5] 441.44/111.40 [1] 441.44/111.40 = [0()] 441.44/111.40 441.44/111.40 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [8] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 > [1 0] X1 + [1 0] X2 + [7] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 = [plus(X1, X2)] 441.44/111.40 441.44/111.40 [activate(n__s(X))] = [1 0] X + [2] 441.44/111.40 [1 1] [2] 441.44/111.40 >= [1 0] X + [2] 441.44/111.40 [1 1] [2] 441.44/111.40 = [s(X)] 441.44/111.40 441.44/111.40 [U13(tt(), V1, V2)] = [1 7] V1 + [2 7] V2 + [6] 441.44/111.40 [0 0] [0 5] [0] 441.44/111.40 >= [1 7] V1 + [2 7] V2 + [6] 441.44/111.40 [0 0] [0 5] [0] 441.44/111.40 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.44/111.40 441.44/111.40 [U14(tt(), V1, V2)] = [1 7] V1 + [1 7] V2 + [3] 441.44/111.40 [0 0] [0 5] [0] 441.44/111.40 >= [1 7] V1 + [1 7] V2 + [3] 441.44/111.40 [0 0] [0 5] [0] 441.44/111.40 = [U15(isNat(activate(V1)), activate(V2))] 441.44/111.40 441.44/111.40 [U15(tt(), V2)] = [1 7] V2 + [1] 441.44/111.40 [0 5] [0] 441.44/111.40 >= [1 7] V2 + [1] 441.44/111.40 [0 5] [0] 441.44/111.40 = [U16(isNat(activate(V2)))] 441.44/111.40 441.44/111.40 [isNat(n__0())] = [12] 441.44/111.40 [5] 441.44/111.40 > [0] 441.44/111.40 [5] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [isNat(n__plus(V1, V2))] = [8 7] V1 + [8 7] V2 + [14] 441.44/111.40 [5 5] [5 5] [5] 441.44/111.40 >= [8 7] V1 + [4 7] V2 + [14] 441.44/111.40 [2 0] [0 5] [2] 441.44/111.40 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.44/111.40 441.44/111.40 [isNat(n__s(V1))] = [8 7] V1 + [15] 441.44/111.40 [5 5] [10] 441.44/111.40 > [8 7] V1 + [14] 441.44/111.40 [0 0] [5] 441.44/111.40 = [U21(isNatKind(activate(V1)), activate(V1))] 441.44/111.40 441.44/111.40 [U16(tt())] = [0] 441.44/111.40 [5] 441.44/111.40 >= [0] 441.44/111.40 [5] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [U21(tt(), V1)] = [6 7] V1 + [11] 441.44/111.40 [0 0] [5] 441.44/111.40 > [6 7] V1 + [10] 441.44/111.40 [0 0] [5] 441.44/111.40 = [U22(isNatKind(activate(V1)), activate(V1))] 441.44/111.40 441.44/111.40 [U22(tt(), V1)] = [4 7] V1 + [4] 441.44/111.40 [0 0] [5] 441.44/111.40 > [1 7] V1 + [1] 441.44/111.40 [0 0] [5] 441.44/111.40 = [U23(isNat(activate(V1)))] 441.44/111.40 441.44/111.40 [U23(tt())] = [0] 441.44/111.40 [5] 441.44/111.40 >= [0] 441.44/111.40 [5] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [U31(tt(), V2)] = [1 0] V2 + [1] 441.44/111.40 [1 0] [9] 441.44/111.40 >= [1 0] V2 + [1] 441.44/111.40 [1 0] [1] 441.44/111.40 = [U32(isNatKind(activate(V2)))] 441.44/111.40 441.44/111.40 [U32(tt())] = [0] 441.44/111.40 [5] 441.44/111.40 >= [0] 441.44/111.40 [5] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [U41(tt())] = [0] 441.44/111.40 [5] 441.44/111.40 >= [0] 441.44/111.40 [5] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [U51(tt(), N)] = [7 7] N + [7] 441.44/111.40 [7 7] [3] 441.44/111.40 >= [5 0] N + [7] 441.44/111.40 [0 4] [0] 441.44/111.40 = [U52(isNatKind(activate(N)), activate(N))] 441.44/111.40 441.44/111.40 [U52(tt(), N)] = [4 0] N + [2] 441.44/111.40 [0 4] [0] 441.44/111.40 > [1 0] N + [1] 441.44/111.40 [0 1] [0] 441.44/111.40 = [activate(N)] 441.44/111.40 441.44/111.40 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [15] 441.44/111.40 [7 7] [7 7] [15] 441.44/111.40 > [5 7] N + [6 4] M + [14] 441.44/111.40 [6 6] [6 4] [14] 441.44/111.40 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.44/111.40 441.44/111.40 [U62(tt(), M, N)] = [5 7] N + [2 4] M + [13] 441.44/111.40 [6 6] [4 4] [12] 441.44/111.40 >= [5 7] N + [1 4] M + [13] 441.44/111.40 [6 6] [2 4] [10] 441.44/111.40 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.44/111.40 441.44/111.40 [U63(tt(), M, N)] = [4 0] N + [1 4] M + [7] 441.44/111.40 [6 1] [2 4] [7] 441.44/111.40 >= [4 0] N + [1 0] M + [7] 441.44/111.40 [5 1] [2 4] [7] 441.44/111.40 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.44/111.40 441.44/111.40 [U64(tt(), M, N)] = [1 0] N + [1 0] M + [12] 441.44/111.40 [2 1] [2 4] [15] 441.44/111.40 > [1 0] N + [1 0] M + [11] 441.44/111.40 [2 1] [2 1] [14] 441.44/111.40 = [s(plus(activate(N), activate(M)))] 441.44/111.40 441.44/111.40 [s(X)] = [1 0] X + [2] 441.44/111.40 [1 1] [2] 441.44/111.40 > [1 0] X + [1] 441.44/111.40 [1 1] [2] 441.44/111.40 = [n__s(X)] 441.44/111.40 441.44/111.40 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [7] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 >= [1 0] X1 + [1 0] X2 + [7] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 = [n__plus(X1, X2)] 441.44/111.40 441.44/111.40 [0()] = [5] 441.44/111.40 [1] 441.44/111.40 >= [5] 441.44/111.40 [1] 441.44/111.40 = [n__0()] 441.44/111.40 441.44/111.40 441.44/111.40 We return to the main proof. 441.44/111.40 441.44/111.40 We are left with following problem, upon which TcT provides the 441.44/111.40 certificate YES(O(1),O(n^2)). 441.44/111.40 441.44/111.40 Strict Trs: { plus(X1, X2) -> n__plus(X1, X2) } 441.44/111.40 Weak Trs: 441.44/111.40 { U11(tt(), V1, V2) -> 441.44/111.40 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.44/111.40 , U12(tt(), V1, V2) -> 441.44/111.40 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.44/111.40 , isNatKind(n__0()) -> tt() 441.44/111.40 , isNatKind(n__plus(V1, V2)) -> 441.44/111.40 U31(isNatKind(activate(V1)), activate(V2)) 441.44/111.40 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.44/111.40 , activate(X) -> X 441.44/111.40 , activate(n__0()) -> 0() 441.44/111.40 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.44/111.40 , activate(n__s(X)) -> s(X) 441.44/111.40 , U13(tt(), V1, V2) -> 441.44/111.40 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.44/111.40 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.44/111.40 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.44/111.40 , isNat(n__0()) -> tt() 441.44/111.40 , isNat(n__plus(V1, V2)) -> 441.44/111.40 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.44/111.40 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.44/111.40 , U16(tt()) -> tt() 441.44/111.40 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.44/111.40 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.44/111.40 , U23(tt()) -> tt() 441.44/111.40 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.44/111.40 , U32(tt()) -> tt() 441.44/111.40 , U41(tt()) -> tt() 441.44/111.40 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.44/111.40 , U52(tt(), N) -> activate(N) 441.44/111.40 , U61(tt(), M, N) -> 441.44/111.40 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.44/111.40 , U62(tt(), M, N) -> 441.44/111.40 U63(isNat(activate(N)), activate(M), activate(N)) 441.44/111.40 , U63(tt(), M, N) -> 441.44/111.40 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.44/111.40 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) 441.44/111.40 , s(X) -> n__s(X) 441.44/111.40 , 0() -> n__0() } 441.44/111.40 Obligation: 441.44/111.40 innermost runtime complexity 441.44/111.40 Answer: 441.44/111.40 YES(O(1),O(n^2)) 441.44/111.40 441.44/111.40 We use the processor 'matrix interpretation of dimension 2' to 441.44/111.40 orient following rules strictly. 441.44/111.40 441.44/111.40 Trs: { plus(X1, X2) -> n__plus(X1, X2) } 441.44/111.40 441.44/111.40 The induced complexity on above rules (modulo remaining rules) is 441.44/111.40 YES(?,O(n^2)) . These rules are moved into the corresponding weak 441.44/111.40 component(s). 441.44/111.40 441.44/111.40 Sub-proof: 441.44/111.40 ---------- 441.44/111.40 The following argument positions are usable: 441.44/111.40 Uargs(U11) = {1, 2, 3}, Uargs(U12) = {1, 2, 3}, 441.44/111.40 Uargs(isNatKind) = {1}, Uargs(U13) = {1, 2, 3}, 441.44/111.40 Uargs(U14) = {1, 2, 3}, Uargs(U15) = {1, 2}, Uargs(isNat) = {1}, 441.44/111.40 Uargs(U16) = {1}, Uargs(U21) = {1, 2}, Uargs(U22) = {1, 2}, 441.44/111.40 Uargs(U23) = {1}, Uargs(U31) = {1, 2}, Uargs(U32) = {1}, 441.44/111.40 Uargs(U41) = {1}, Uargs(U52) = {1, 2}, Uargs(U62) = {1, 2, 3}, 441.44/111.40 Uargs(U63) = {1, 2, 3}, Uargs(U64) = {1, 2, 3}, Uargs(s) = {1}, 441.44/111.40 Uargs(plus) = {1, 2} 441.44/111.40 441.44/111.40 TcT has computed the following constructor-based matrix 441.44/111.40 interpretation satisfying not(EDA). 441.44/111.40 441.44/111.40 [U11](x1, x2, x3) = [1 0] x1 + [3 5] x2 + [3 5] x3 + [2] 441.44/111.40 [0 0] [0 4] [0 4] [4] 441.44/111.40 441.44/111.40 [tt] = [4] 441.44/111.40 [1] 441.44/111.40 441.44/111.40 [U12](x1, x2, x3) = [2 0] x1 + [1 5] x2 + [3 5] x3 + [0] 441.44/111.40 [0 0] [0 0] [0 4] [4] 441.44/111.40 441.44/111.40 [isNatKind](x1) = [1 0] x1 + [0] 441.44/111.40 [2 0] [0] 441.44/111.40 441.44/111.40 [activate](x1) = [1 0] x1 + [1] 441.44/111.40 [0 1] [0] 441.44/111.40 441.44/111.40 [U13](x1, x2, x3) = [1 0] x1 + [1 5] x2 + [2 5] x3 + [0] 441.44/111.40 [0 0] [0 0] [0 0] [1] 441.44/111.40 441.44/111.40 [U14](x1, x2, x3) = [1 0] x1 + [1 5] x2 + [1 5] x3 + [0] 441.44/111.40 [0 0] [0 0] [0 0] [1] 441.44/111.40 441.44/111.40 [U15](x1, x2) = [1 0] x1 + [1 5] x2 + [0] 441.44/111.40 [0 0] [0 0] [1] 441.44/111.40 441.44/111.40 [isNat](x1) = [1 5] x1 + [2] 441.44/111.40 [0 4] [2] 441.44/111.40 441.44/111.40 [U16](x1) = [1 0] x1 + [0] 441.44/111.40 [0 0] [1] 441.44/111.40 441.44/111.40 [U21](x1, x2) = [1 0] x1 + [5 5] x2 + [1] 441.44/111.40 [2 0] [0 0] [0] 441.44/111.40 441.44/111.40 [U22](x1, x2) = [1 1] x1 + [2 5] x2 + [0] 441.44/111.40 [0 0] [0 0] [1] 441.44/111.40 441.44/111.40 [U23](x1) = [1 0] x1 + [0] 441.44/111.40 [0 0] [1] 441.44/111.40 441.44/111.40 [U31](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 441.44/111.40 [1 0] [0 0] [0] 441.44/111.40 441.44/111.40 [U32](x1) = [1 0] x1 + [0] 441.44/111.40 [0 0] [4] 441.44/111.40 441.44/111.40 [U41](x1) = [1 0] x1 + [0] 441.44/111.40 [0 0] [1] 441.44/111.40 441.44/111.40 [U51](x1, x2) = [2 0] x1 + [7 7] x2 + [3] 441.44/111.40 [2 0] [7 7] [3] 441.44/111.40 441.44/111.40 [U52](x1, x2) = [2 0] x1 + [4 0] x2 + [1] 441.44/111.40 [0 0] [0 1] [0] 441.44/111.40 441.44/111.40 [U61](x1, x2, x3) = [2 0] x1 + [7 7] x2 + [7 7] x3 + [7] 441.44/111.40 [2 0] [7 7] [7 7] [7] 441.44/111.40 441.44/111.40 [U62](x1, x2, x3) = [2 1] x1 + [1 4] x2 + [5 5] x3 + [5] 441.44/111.40 [2 0] [2 4] [5 6] [6] 441.44/111.40 441.44/111.40 [U63](x1, x2, x3) = [1 0] x1 + [1 4] x2 + [4 0] x3 + [6] 441.44/111.40 [1 0] [2 4] [4 1] [5] 441.44/111.40 441.44/111.40 [U64](x1, x2, x3) = [2 0] x1 + [1 0] x2 + [2 0] x3 + [4] 441.44/111.40 [2 0] [2 4] [2 1] [3] 441.44/111.40 441.44/111.40 [s](x1) = [1 0] x1 + [1] 441.44/111.40 [1 1] [1] 441.44/111.40 441.44/111.40 [plus](x1, x2) = [1 0] x1 + [1 0] x2 + [5] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 441.44/111.40 [n__0] = [4] 441.44/111.40 [0] 441.44/111.40 441.44/111.40 [n__plus](x1, x2) = [1 0] x1 + [1 0] x2 + [4] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 441.44/111.40 [n__s](x1) = [1 0] x1 + [1] 441.44/111.40 [1 1] [1] 441.44/111.40 441.44/111.40 [0] = [5] 441.44/111.40 [0] 441.44/111.40 441.44/111.40 The order satisfies the following ordering constraints: 441.44/111.40 441.44/111.40 [U11(tt(), V1, V2)] = [3 5] V1 + [3 5] V2 + [6] 441.44/111.40 [0 4] [0 4] [4] 441.44/111.40 >= [3 5] V1 + [3 5] V2 + [6] 441.44/111.40 [0 0] [0 4] [4] 441.44/111.40 = [U12(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.44/111.40 441.44/111.40 [U12(tt(), V1, V2)] = [1 5] V1 + [3 5] V2 + [8] 441.44/111.40 [0 0] [0 4] [4] 441.44/111.40 > [1 5] V1 + [3 5] V2 + [4] 441.44/111.40 [0 0] [0 0] [1] 441.44/111.40 = [U13(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.44/111.40 441.44/111.40 [isNatKind(n__0())] = [4] 441.44/111.40 [8] 441.44/111.40 >= [4] 441.44/111.40 [1] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [isNatKind(n__plus(V1, V2))] = [1 0] V1 + [1 0] V2 + [4] 441.44/111.40 [2 0] [2 0] [8] 441.44/111.40 > [1 0] V1 + [1 0] V2 + [2] 441.44/111.40 [1 0] [0 0] [1] 441.44/111.40 = [U31(isNatKind(activate(V1)), activate(V2))] 441.44/111.40 441.44/111.40 [isNatKind(n__s(V1))] = [1 0] V1 + [1] 441.44/111.40 [2 0] [2] 441.44/111.40 >= [1 0] V1 + [1] 441.44/111.40 [0 0] [1] 441.44/111.40 = [U41(isNatKind(activate(V1)))] 441.44/111.40 441.44/111.40 [activate(X)] = [1 0] X + [1] 441.44/111.40 [0 1] [0] 441.44/111.40 > [1 0] X + [0] 441.44/111.40 [0 1] [0] 441.44/111.40 = [X] 441.44/111.40 441.44/111.40 [activate(n__0())] = [5] 441.44/111.40 [0] 441.44/111.40 >= [5] 441.44/111.40 [0] 441.44/111.40 = [0()] 441.44/111.40 441.44/111.40 [activate(n__plus(X1, X2))] = [1 0] X1 + [1 0] X2 + [5] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 >= [1 0] X1 + [1 0] X2 + [5] 441.44/111.40 [1 1] [1 1] [1] 441.44/111.40 = [plus(X1, X2)] 441.44/111.40 441.44/111.40 [activate(n__s(X))] = [1 0] X + [2] 441.44/111.40 [1 1] [1] 441.44/111.40 > [1 0] X + [1] 441.44/111.40 [1 1] [1] 441.44/111.40 = [s(X)] 441.44/111.40 441.44/111.40 [U13(tt(), V1, V2)] = [1 5] V1 + [2 5] V2 + [4] 441.44/111.40 [0 0] [0 0] [1] 441.44/111.40 > [1 5] V1 + [2 5] V2 + [3] 441.44/111.40 [0 0] [0 0] [1] 441.44/111.40 = [U14(isNatKind(activate(V2)), activate(V1), activate(V2))] 441.44/111.40 441.44/111.40 [U14(tt(), V1, V2)] = [1 5] V1 + [1 5] V2 + [4] 441.44/111.40 [0 0] [0 0] [1] 441.44/111.40 >= [1 5] V1 + [1 5] V2 + [4] 441.44/111.40 [0 0] [0 0] [1] 441.44/111.40 = [U15(isNat(activate(V1)), activate(V2))] 441.44/111.40 441.44/111.40 [U15(tt(), V2)] = [1 5] V2 + [4] 441.44/111.40 [0 0] [1] 441.44/111.40 > [1 5] V2 + [3] 441.44/111.40 [0 0] [1] 441.44/111.40 = [U16(isNat(activate(V2)))] 441.44/111.40 441.44/111.40 [isNat(n__0())] = [6] 441.44/111.40 [2] 441.44/111.40 > [4] 441.44/111.40 [1] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [isNat(n__plus(V1, V2))] = [6 5] V1 + [6 5] V2 + [11] 441.44/111.40 [4 4] [4 4] [6] 441.44/111.40 > [4 5] V1 + [3 5] V2 + [9] 441.44/111.40 [0 4] [0 4] [4] 441.44/111.40 = [U11(isNatKind(activate(V1)), activate(V1), activate(V2))] 441.44/111.40 441.44/111.40 [isNat(n__s(V1))] = [6 5] V1 + [8] 441.44/111.40 [4 4] [6] 441.44/111.40 > [6 5] V1 + [7] 441.44/111.40 [2 0] [2] 441.44/111.40 = [U21(isNatKind(activate(V1)), activate(V1))] 441.44/111.40 441.44/111.40 [U16(tt())] = [4] 441.44/111.40 [1] 441.44/111.40 >= [4] 441.44/111.40 [1] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [U21(tt(), V1)] = [5 5] V1 + [5] 441.44/111.40 [0 0] [8] 441.44/111.40 >= [5 5] V1 + [5] 441.44/111.40 [0 0] [1] 441.44/111.40 = [U22(isNatKind(activate(V1)), activate(V1))] 441.44/111.40 441.44/111.40 [U22(tt(), V1)] = [2 5] V1 + [5] 441.44/111.40 [0 0] [1] 441.44/111.40 > [1 5] V1 + [3] 441.44/111.40 [0 0] [1] 441.44/111.40 = [U23(isNat(activate(V1)))] 441.44/111.40 441.44/111.40 [U23(tt())] = [4] 441.44/111.40 [1] 441.44/111.40 >= [4] 441.44/111.40 [1] 441.44/111.40 = [tt()] 441.44/111.40 441.44/111.40 [U31(tt(), V2)] = [1 0] V2 + [4] 441.44/111.40 [0 0] [4] 441.44/111.40 > [1 0] V2 + [1] 441.44/111.40 [0 0] [4] 441.44/111.40 = [U32(isNatKind(activate(V2)))] 441.44/111.40 441.44/111.40 [U32(tt())] = [4] 441.44/111.40 [4] 441.44/111.40 >= [4] 441.44/111.40 [1] 441.44/111.41 = [tt()] 441.44/111.41 441.44/111.41 [U41(tt())] = [4] 441.44/111.41 [1] 441.44/111.41 >= [4] 441.44/111.41 [1] 441.44/111.41 = [tt()] 441.44/111.41 441.44/111.41 [U51(tt(), N)] = [7 7] N + [11] 441.44/111.41 [7 7] [11] 441.44/111.41 > [6 0] N + [7] 441.44/111.41 [0 1] [0] 441.44/111.41 = [U52(isNatKind(activate(N)), activate(N))] 441.44/111.41 441.44/111.41 [U52(tt(), N)] = [4 0] N + [9] 441.44/111.41 [0 1] [0] 441.44/111.41 > [1 0] N + [1] 441.44/111.41 [0 1] [0] 441.44/111.41 = [activate(N)] 441.44/111.41 441.44/111.41 [U61(tt(), M, N)] = [7 7] N + [7 7] M + [15] 441.44/111.41 [7 7] [7 7] [15] 441.44/111.41 >= [5 5] N + [5 4] M + [15] 441.44/111.41 [5 6] [4 4] [15] 441.44/111.41 = [U62(isNatKind(activate(M)), activate(M), activate(N))] 441.44/111.41 441.44/111.41 [U62(tt(), M, N)] = [5 5] N + [1 4] M + [14] 441.44/111.41 [5 6] [2 4] [14] 441.44/111.41 >= [5 5] N + [1 4] M + [14] 441.44/111.41 [5 6] [2 4] [14] 441.44/111.41 = [U63(isNat(activate(N)), activate(M), activate(N))] 441.44/111.41 441.44/111.41 [U63(tt(), M, N)] = [4 0] N + [1 4] M + [10] 441.44/111.41 [4 1] [2 4] [9] 441.44/111.41 > [4 0] N + [1 0] M + [9] 441.44/111.41 [4 1] [2 4] [9] 441.44/111.41 = [U64(isNatKind(activate(N)), activate(M), activate(N))] 441.44/111.41 441.44/111.41 [U64(tt(), M, N)] = [2 0] N + [1 0] M + [12] 441.44/111.41 [2 1] [2 4] [11] 441.44/111.41 > [1 0] N + [1 0] M + [8] 441.44/111.41 [2 1] [2 1] [11] 441.44/111.41 = [s(plus(activate(N), activate(M)))] 441.44/111.41 441.44/111.41 [s(X)] = [1 0] X + [1] 441.44/111.41 [1 1] [1] 441.44/111.41 >= [1 0] X + [1] 441.44/111.41 [1 1] [1] 441.44/111.41 = [n__s(X)] 441.44/111.41 441.44/111.41 [plus(X1, X2)] = [1 0] X1 + [1 0] X2 + [5] 441.44/111.41 [1 1] [1 1] [1] 441.44/111.41 > [1 0] X1 + [1 0] X2 + [4] 441.44/111.41 [1 1] [1 1] [1] 441.44/111.41 = [n__plus(X1, X2)] 441.44/111.41 441.44/111.41 [0()] = [5] 441.44/111.41 [0] 441.44/111.41 > [4] 441.44/111.41 [0] 441.44/111.41 = [n__0()] 441.44/111.41 441.44/111.41 441.44/111.41 We return to the main proof. 441.44/111.41 441.44/111.41 We are left with following problem, upon which TcT provides the 441.44/111.41 certificate YES(O(1),O(1)). 441.44/111.41 441.44/111.41 Weak Trs: 441.44/111.41 { U11(tt(), V1, V2) -> 441.44/111.41 U12(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.44/111.41 , U12(tt(), V1, V2) -> 441.44/111.41 U13(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.44/111.41 , isNatKind(n__0()) -> tt() 441.44/111.41 , isNatKind(n__plus(V1, V2)) -> 441.44/111.41 U31(isNatKind(activate(V1)), activate(V2)) 441.44/111.41 , isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1))) 441.44/111.41 , activate(X) -> X 441.44/111.41 , activate(n__0()) -> 0() 441.44/111.41 , activate(n__plus(X1, X2)) -> plus(X1, X2) 441.44/111.41 , activate(n__s(X)) -> s(X) 441.44/111.41 , U13(tt(), V1, V2) -> 441.44/111.41 U14(isNatKind(activate(V2)), activate(V1), activate(V2)) 441.44/111.41 , U14(tt(), V1, V2) -> U15(isNat(activate(V1)), activate(V2)) 441.44/111.41 , U15(tt(), V2) -> U16(isNat(activate(V2))) 441.44/111.41 , isNat(n__0()) -> tt() 441.44/111.41 , isNat(n__plus(V1, V2)) -> 441.44/111.41 U11(isNatKind(activate(V1)), activate(V1), activate(V2)) 441.44/111.41 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 441.44/111.41 , U16(tt()) -> tt() 441.44/111.41 , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) 441.44/111.41 , U22(tt(), V1) -> U23(isNat(activate(V1))) 441.44/111.41 , U23(tt()) -> tt() 441.44/111.41 , U31(tt(), V2) -> U32(isNatKind(activate(V2))) 441.44/111.41 , U32(tt()) -> tt() 441.44/111.41 , U41(tt()) -> tt() 441.44/111.41 , U51(tt(), N) -> U52(isNatKind(activate(N)), activate(N)) 441.44/111.41 , U52(tt(), N) -> activate(N) 441.44/111.41 , U61(tt(), M, N) -> 441.44/111.41 U62(isNatKind(activate(M)), activate(M), activate(N)) 441.44/111.41 , U62(tt(), M, N) -> 441.44/111.41 U63(isNat(activate(N)), activate(M), activate(N)) 441.44/111.41 , U63(tt(), M, N) -> 441.44/111.41 U64(isNatKind(activate(N)), activate(M), activate(N)) 441.44/111.41 , U64(tt(), M, N) -> s(plus(activate(N), activate(M))) 441.44/111.41 , s(X) -> n__s(X) 441.44/111.41 , plus(X1, X2) -> n__plus(X1, X2) 441.44/111.41 , 0() -> n__0() } 441.44/111.41 Obligation: 441.44/111.41 innermost runtime complexity 441.44/111.41 Answer: 441.44/111.41 YES(O(1),O(1)) 441.44/111.41 441.44/111.41 Empty rules are trivially bounded 441.44/111.41 441.44/111.41 Hurray, we answered YES(O(1),O(n^2)) 441.56/111.50 EOF