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