YES(O(1),O(n^2))
443.01/211.57 YES(O(1),O(n^2))
443.01/211.57
443.01/211.57 We are left with following problem, upon which TcT provides the
443.01/211.57 certificate YES(O(1),O(n^2)).
443.01/211.57
443.01/211.57 Strict Trs:
443.01/211.57 { eq(0(), 0()) -> true()
443.01/211.57 , eq(0(), s(X)) -> false()
443.01/211.57 , eq(s(X), 0()) -> false()
443.01/211.57 , eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.57 , rm(N, nil()) -> nil()
443.01/211.57 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
443.01/211.57 , ifrm(true(), N, add(M, X)) -> rm(N, X)
443.01/211.57 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
443.01/211.57 , purge(nil()) -> nil()
443.01/211.57 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.57 Obligation:
443.01/211.57 runtime complexity
443.01/211.57 Answer:
443.01/211.57 YES(O(1),O(n^2))
443.01/211.57
443.01/211.57 The weightgap principle applies (using the following nonconstant
443.01/211.57 growth matrix-interpretation)
443.01/211.57
443.01/211.57 The following argument positions are usable:
443.01/211.57 Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
443.01/211.57 Uargs(purge) = {1}
443.01/211.57
443.01/211.57 TcT has computed the following matrix interpretation satisfying
443.01/211.57 not(EDA) and not(IDA(1)).
443.01/211.57
443.01/211.57 [eq](x1, x2) = [4]
443.01/211.57
443.01/211.57 [0] = [7]
443.01/211.57
443.01/211.57 [true] = [0]
443.01/211.57
443.01/211.57 [s](x1) = [1] x1 + [7]
443.01/211.57
443.01/211.57 [false] = [0]
443.01/211.57
443.01/211.57 [rm](x1, x2) = [1] x2 + [0]
443.01/211.57
443.01/211.57 [nil] = [4]
443.01/211.57
443.01/211.57 [add](x1, x2) = [1] x1 + [1] x2 + [0]
443.01/211.57
443.01/211.57 [ifrm](x1, x2, x3) = [1] x1 + [1] x3 + [0]
443.01/211.57
443.01/211.57 [purge](x1) = [1] x1 + [0]
443.01/211.57
443.01/211.57 The order satisfies the following ordering constraints:
443.01/211.57
443.01/211.57 [eq(0(), 0())] = [4]
443.01/211.57 > [0]
443.01/211.57 = [true()]
443.01/211.57
443.01/211.57 [eq(0(), s(X))] = [4]
443.01/211.57 > [0]
443.01/211.57 = [false()]
443.01/211.57
443.01/211.57 [eq(s(X), 0())] = [4]
443.01/211.57 > [0]
443.01/211.57 = [false()]
443.01/211.57
443.01/211.57 [eq(s(X), s(Y))] = [4]
443.01/211.57 >= [4]
443.01/211.57 = [eq(X, Y)]
443.01/211.57
443.01/211.57 [rm(N, nil())] = [4]
443.01/211.57 >= [4]
443.01/211.57 = [nil()]
443.01/211.57
443.01/211.57 [rm(N, add(M, X))] = [1] X + [1] M + [0]
443.01/211.57 ? [1] X + [1] M + [4]
443.01/211.57 = [ifrm(eq(N, M), N, add(M, X))]
443.01/211.57
443.01/211.57 [ifrm(true(), N, add(M, X))] = [1] X + [1] M + [0]
443.01/211.57 >= [1] X + [0]
443.01/211.57 = [rm(N, X)]
443.01/211.57
443.01/211.57 [ifrm(false(), N, add(M, X))] = [1] X + [1] M + [0]
443.01/211.57 >= [1] X + [1] M + [0]
443.01/211.57 = [add(M, rm(N, X))]
443.01/211.57
443.01/211.57 [purge(nil())] = [4]
443.01/211.57 >= [4]
443.01/211.57 = [nil()]
443.01/211.57
443.01/211.57 [purge(add(N, X))] = [1] X + [1] N + [0]
443.01/211.57 >= [1] X + [1] N + [0]
443.01/211.57 = [add(N, purge(rm(N, X)))]
443.01/211.57
443.01/211.57
443.01/211.57 Further, it can be verified that all rules not oriented are covered by the weightgap condition.
443.01/211.57
443.01/211.57 We are left with following problem, upon which TcT provides the
443.01/211.57 certificate YES(O(1),O(n^2)).
443.01/211.57
443.01/211.57 Strict Trs:
443.01/211.57 { eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.57 , rm(N, nil()) -> nil()
443.01/211.57 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
443.01/211.57 , ifrm(true(), N, add(M, X)) -> rm(N, X)
443.01/211.57 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
443.01/211.57 , purge(nil()) -> nil()
443.01/211.57 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.57 Weak Trs:
443.01/211.57 { eq(0(), 0()) -> true()
443.01/211.57 , eq(0(), s(X)) -> false()
443.01/211.57 , eq(s(X), 0()) -> false() }
443.01/211.57 Obligation:
443.01/211.57 runtime complexity
443.01/211.57 Answer:
443.01/211.57 YES(O(1),O(n^2))
443.01/211.57
443.01/211.57 The weightgap principle applies (using the following nonconstant
443.01/211.57 growth matrix-interpretation)
443.01/211.57
443.01/211.57 The following argument positions are usable:
443.01/211.57 Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
443.01/211.57 Uargs(purge) = {1}
443.01/211.57
443.01/211.57 TcT has computed the following matrix interpretation satisfying
443.01/211.57 not(EDA) and not(IDA(1)).
443.01/211.57
443.01/211.57 [eq](x1, x2) = [1]
443.01/211.57
443.01/211.57 [0] = [7]
443.01/211.57
443.01/211.57 [true] = [1]
443.01/211.57
443.01/211.57 [s](x1) = [1] x1 + [7]
443.01/211.57
443.01/211.57 [false] = [0]
443.01/211.57
443.01/211.57 [rm](x1, x2) = [1] x2 + [0]
443.01/211.57
443.01/211.57 [nil] = [4]
443.01/211.57
443.01/211.57 [add](x1, x2) = [1] x1 + [1] x2 + [0]
443.01/211.57
443.01/211.57 [ifrm](x1, x2, x3) = [1] x1 + [1] x3 + [0]
443.01/211.57
443.01/211.57 [purge](x1) = [1] x1 + [0]
443.01/211.57
443.01/211.57 The order satisfies the following ordering constraints:
443.01/211.57
443.01/211.57 [eq(0(), 0())] = [1]
443.01/211.57 >= [1]
443.01/211.57 = [true()]
443.01/211.57
443.01/211.57 [eq(0(), s(X))] = [1]
443.01/211.57 > [0]
443.01/211.57 = [false()]
443.01/211.57
443.01/211.57 [eq(s(X), 0())] = [1]
443.01/211.57 > [0]
443.01/211.57 = [false()]
443.01/211.57
443.01/211.57 [eq(s(X), s(Y))] = [1]
443.01/211.57 >= [1]
443.01/211.57 = [eq(X, Y)]
443.01/211.57
443.01/211.57 [rm(N, nil())] = [4]
443.01/211.57 >= [4]
443.01/211.57 = [nil()]
443.01/211.57
443.01/211.57 [rm(N, add(M, X))] = [1] X + [1] M + [0]
443.01/211.57 ? [1] X + [1] M + [1]
443.01/211.57 = [ifrm(eq(N, M), N, add(M, X))]
443.01/211.57
443.01/211.57 [ifrm(true(), N, add(M, X))] = [1] X + [1] M + [1]
443.01/211.57 > [1] X + [0]
443.01/211.57 = [rm(N, X)]
443.01/211.57
443.01/211.57 [ifrm(false(), N, add(M, X))] = [1] X + [1] M + [0]
443.01/211.57 >= [1] X + [1] M + [0]
443.01/211.57 = [add(M, rm(N, X))]
443.01/211.57
443.01/211.57 [purge(nil())] = [4]
443.01/211.57 >= [4]
443.01/211.57 = [nil()]
443.01/211.57
443.01/211.57 [purge(add(N, X))] = [1] X + [1] N + [0]
443.01/211.57 >= [1] X + [1] N + [0]
443.01/211.57 = [add(N, purge(rm(N, X)))]
443.01/211.57
443.01/211.57
443.01/211.57 Further, it can be verified that all rules not oriented are covered by the weightgap condition.
443.01/211.57
443.01/211.57 We are left with following problem, upon which TcT provides the
443.01/211.57 certificate YES(O(1),O(n^2)).
443.01/211.57
443.01/211.57 Strict Trs:
443.01/211.57 { eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.57 , rm(N, nil()) -> nil()
443.01/211.57 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
443.01/211.57 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
443.01/211.57 , purge(nil()) -> nil()
443.01/211.57 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.57 Weak Trs:
443.01/211.57 { eq(0(), 0()) -> true()
443.01/211.57 , eq(0(), s(X)) -> false()
443.01/211.57 , eq(s(X), 0()) -> false()
443.01/211.57 , ifrm(true(), N, add(M, X)) -> rm(N, X) }
443.01/211.57 Obligation:
443.01/211.57 runtime complexity
443.01/211.57 Answer:
443.01/211.57 YES(O(1),O(n^2))
443.01/211.57
443.01/211.57 The weightgap principle applies (using the following nonconstant
443.01/211.57 growth matrix-interpretation)
443.01/211.57
443.01/211.57 The following argument positions are usable:
443.01/211.57 Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
443.01/211.57 Uargs(purge) = {1}
443.01/211.57
443.01/211.57 TcT has computed the following matrix interpretation satisfying
443.01/211.57 not(EDA) and not(IDA(1)).
443.01/211.57
443.01/211.57 [eq](x1, x2) = [1]
443.01/211.57
443.01/211.57 [0] = [7]
443.01/211.57
443.01/211.57 [true] = [0]
443.01/211.57
443.01/211.57 [s](x1) = [1] x1 + [7]
443.01/211.57
443.01/211.57 [false] = [1]
443.01/211.57
443.01/211.57 [rm](x1, x2) = [1] x2 + [0]
443.01/211.57
443.01/211.57 [nil] = [4]
443.01/211.57
443.01/211.57 [add](x1, x2) = [1] x1 + [1] x2 + [0]
443.01/211.57
443.01/211.57 [ifrm](x1, x2, x3) = [1] x1 + [1] x3 + [0]
443.01/211.57
443.01/211.57 [purge](x1) = [1] x1 + [0]
443.01/211.57
443.01/211.57 The order satisfies the following ordering constraints:
443.01/211.57
443.01/211.57 [eq(0(), 0())] = [1]
443.01/211.57 > [0]
443.01/211.57 = [true()]
443.01/211.57
443.01/211.57 [eq(0(), s(X))] = [1]
443.01/211.57 >= [1]
443.01/211.57 = [false()]
443.01/211.57
443.01/211.57 [eq(s(X), 0())] = [1]
443.01/211.57 >= [1]
443.01/211.57 = [false()]
443.01/211.57
443.01/211.57 [eq(s(X), s(Y))] = [1]
443.01/211.57 >= [1]
443.01/211.57 = [eq(X, Y)]
443.01/211.57
443.01/211.57 [rm(N, nil())] = [4]
443.01/211.57 >= [4]
443.01/211.57 = [nil()]
443.01/211.57
443.01/211.57 [rm(N, add(M, X))] = [1] X + [1] M + [0]
443.01/211.57 ? [1] X + [1] M + [1]
443.01/211.57 = [ifrm(eq(N, M), N, add(M, X))]
443.01/211.57
443.01/211.57 [ifrm(true(), N, add(M, X))] = [1] X + [1] M + [0]
443.01/211.57 >= [1] X + [0]
443.01/211.57 = [rm(N, X)]
443.01/211.57
443.01/211.57 [ifrm(false(), N, add(M, X))] = [1] X + [1] M + [1]
443.01/211.57 > [1] X + [1] M + [0]
443.01/211.57 = [add(M, rm(N, X))]
443.01/211.57
443.01/211.57 [purge(nil())] = [4]
443.01/211.57 >= [4]
443.01/211.57 = [nil()]
443.01/211.57
443.01/211.57 [purge(add(N, X))] = [1] X + [1] N + [0]
443.01/211.57 >= [1] X + [1] N + [0]
443.01/211.57 = [add(N, purge(rm(N, X)))]
443.01/211.57
443.01/211.57
443.01/211.57 Further, it can be verified that all rules not oriented are covered by the weightgap condition.
443.01/211.57
443.01/211.57 We are left with following problem, upon which TcT provides the
443.01/211.57 certificate YES(O(1),O(n^2)).
443.01/211.57
443.01/211.57 Strict Trs:
443.01/211.57 { eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.57 , rm(N, nil()) -> nil()
443.01/211.57 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
443.01/211.57 , purge(nil()) -> nil()
443.01/211.57 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.57 Weak Trs:
443.01/211.57 { eq(0(), 0()) -> true()
443.01/211.57 , eq(0(), s(X)) -> false()
443.01/211.57 , eq(s(X), 0()) -> false()
443.01/211.57 , ifrm(true(), N, add(M, X)) -> rm(N, X)
443.01/211.57 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) }
443.01/211.57 Obligation:
443.01/211.57 runtime complexity
443.01/211.57 Answer:
443.01/211.57 YES(O(1),O(n^2))
443.01/211.57
443.01/211.57 The weightgap principle applies (using the following nonconstant
443.01/211.57 growth matrix-interpretation)
443.01/211.57
443.01/211.57 The following argument positions are usable:
443.01/211.57 Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
443.01/211.57 Uargs(purge) = {1}
443.01/211.57
443.01/211.57 TcT has computed the following matrix interpretation satisfying
443.01/211.57 not(EDA) and not(IDA(1)).
443.01/211.57
443.01/211.57 [eq](x1, x2) = [4]
443.01/211.57
443.01/211.57 [0] = [7]
443.01/211.57
443.01/211.57 [true] = [4]
443.01/211.57
443.01/211.57 [s](x1) = [1] x1 + [7]
443.01/211.57
443.01/211.57 [false] = [0]
443.01/211.57
443.01/211.57 [rm](x1, x2) = [1] x2 + [0]
443.01/211.57
443.01/211.57 [nil] = [4]
443.01/211.57
443.01/211.57 [add](x1, x2) = [1] x2 + [0]
443.01/211.57
443.01/211.57 [ifrm](x1, x2, x3) = [1] x1 + [1] x3 + [0]
443.01/211.57
443.01/211.57 [purge](x1) = [1] x1 + [4]
443.01/211.57
443.01/211.57 The order satisfies the following ordering constraints:
443.01/211.57
443.01/211.57 [eq(0(), 0())] = [4]
443.01/211.57 >= [4]
443.01/211.57 = [true()]
443.01/211.57
443.01/211.57 [eq(0(), s(X))] = [4]
443.01/211.57 > [0]
443.01/211.57 = [false()]
443.01/211.57
443.01/211.57 [eq(s(X), 0())] = [4]
443.01/211.57 > [0]
443.01/211.57 = [false()]
443.01/211.57
443.01/211.57 [eq(s(X), s(Y))] = [4]
443.01/211.57 >= [4]
443.01/211.58 = [eq(X, Y)]
443.01/211.58
443.01/211.58 [rm(N, nil())] = [4]
443.01/211.58 >= [4]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [rm(N, add(M, X))] = [1] X + [0]
443.01/211.58 ? [1] X + [4]
443.01/211.58 = [ifrm(eq(N, M), N, add(M, X))]
443.01/211.58
443.01/211.58 [ifrm(true(), N, add(M, X))] = [1] X + [4]
443.01/211.58 > [1] X + [0]
443.01/211.58 = [rm(N, X)]
443.01/211.58
443.01/211.58 [ifrm(false(), N, add(M, X))] = [1] X + [0]
443.01/211.58 >= [1] X + [0]
443.01/211.58 = [add(M, rm(N, X))]
443.01/211.58
443.01/211.58 [purge(nil())] = [8]
443.01/211.58 > [4]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [purge(add(N, X))] = [1] X + [4]
443.01/211.58 >= [1] X + [4]
443.01/211.58 = [add(N, purge(rm(N, X)))]
443.01/211.58
443.01/211.58
443.01/211.58 Further, it can be verified that all rules not oriented are covered by the weightgap condition.
443.01/211.58
443.01/211.58 We are left with following problem, upon which TcT provides the
443.01/211.58 certificate YES(O(1),O(n^2)).
443.01/211.58
443.01/211.58 Strict Trs:
443.01/211.58 { eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.58 , rm(N, nil()) -> nil()
443.01/211.58 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
443.01/211.58 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.58 Weak Trs:
443.01/211.58 { eq(0(), 0()) -> true()
443.01/211.58 , eq(0(), s(X)) -> false()
443.01/211.58 , eq(s(X), 0()) -> false()
443.01/211.58 , ifrm(true(), N, add(M, X)) -> rm(N, X)
443.01/211.58 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
443.01/211.58 , purge(nil()) -> nil() }
443.01/211.58 Obligation:
443.01/211.58 runtime complexity
443.01/211.58 Answer:
443.01/211.58 YES(O(1),O(n^2))
443.01/211.58
443.01/211.58 The weightgap principle applies (using the following nonconstant
443.01/211.58 growth matrix-interpretation)
443.01/211.58
443.01/211.58 The following argument positions are usable:
443.01/211.58 Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
443.01/211.58 Uargs(purge) = {1}
443.01/211.58
443.01/211.58 TcT has computed the following matrix interpretation satisfying
443.01/211.58 not(EDA) and not(IDA(1)).
443.01/211.58
443.01/211.58 [eq](x1, x2) = [1]
443.01/211.58
443.01/211.58 [0] = [7]
443.01/211.58
443.01/211.58 [true] = [1]
443.01/211.58
443.01/211.58 [s](x1) = [1] x1 + [7]
443.01/211.58
443.01/211.58 [false] = [1]
443.01/211.58
443.01/211.58 [rm](x1, x2) = [1] x2 + [1]
443.01/211.58
443.01/211.58 [nil] = [7]
443.01/211.58
443.01/211.58 [add](x1, x2) = [1] x1 + [1] x2 + [0]
443.01/211.58
443.01/211.58 [ifrm](x1, x2, x3) = [1] x1 + [1] x3 + [0]
443.01/211.58
443.01/211.58 [purge](x1) = [1] x1 + [0]
443.01/211.58
443.01/211.58 The order satisfies the following ordering constraints:
443.01/211.58
443.01/211.58 [eq(0(), 0())] = [1]
443.01/211.58 >= [1]
443.01/211.58 = [true()]
443.01/211.58
443.01/211.58 [eq(0(), s(X))] = [1]
443.01/211.58 >= [1]
443.01/211.58 = [false()]
443.01/211.58
443.01/211.58 [eq(s(X), 0())] = [1]
443.01/211.58 >= [1]
443.01/211.58 = [false()]
443.01/211.58
443.01/211.58 [eq(s(X), s(Y))] = [1]
443.01/211.58 >= [1]
443.01/211.58 = [eq(X, Y)]
443.01/211.58
443.01/211.58 [rm(N, nil())] = [8]
443.01/211.58 > [7]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [rm(N, add(M, X))] = [1] X + [1] M + [1]
443.01/211.58 >= [1] X + [1] M + [1]
443.01/211.58 = [ifrm(eq(N, M), N, add(M, X))]
443.01/211.58
443.01/211.58 [ifrm(true(), N, add(M, X))] = [1] X + [1] M + [1]
443.01/211.58 >= [1] X + [1]
443.01/211.58 = [rm(N, X)]
443.01/211.58
443.01/211.58 [ifrm(false(), N, add(M, X))] = [1] X + [1] M + [1]
443.01/211.58 >= [1] X + [1] M + [1]
443.01/211.58 = [add(M, rm(N, X))]
443.01/211.58
443.01/211.58 [purge(nil())] = [7]
443.01/211.58 >= [7]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [purge(add(N, X))] = [1] X + [1] N + [0]
443.01/211.58 ? [1] X + [1] N + [1]
443.01/211.58 = [add(N, purge(rm(N, X)))]
443.01/211.58
443.01/211.58
443.01/211.58 Further, it can be verified that all rules not oriented are covered by the weightgap condition.
443.01/211.58
443.01/211.58 We are left with following problem, upon which TcT provides the
443.01/211.58 certificate YES(O(1),O(n^2)).
443.01/211.58
443.01/211.58 Strict Trs:
443.01/211.58 { eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.58 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
443.01/211.58 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.58 Weak Trs:
443.01/211.58 { eq(0(), 0()) -> true()
443.01/211.58 , eq(0(), s(X)) -> false()
443.01/211.58 , eq(s(X), 0()) -> false()
443.01/211.58 , rm(N, nil()) -> nil()
443.01/211.58 , ifrm(true(), N, add(M, X)) -> rm(N, X)
443.01/211.58 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
443.01/211.58 , purge(nil()) -> nil() }
443.01/211.58 Obligation:
443.01/211.58 runtime complexity
443.01/211.58 Answer:
443.01/211.58 YES(O(1),O(n^2))
443.01/211.58
443.01/211.58 We use the processor 'matrix interpretation of dimension 1' to
443.01/211.58 orient following rules strictly.
443.01/211.58
443.01/211.58 Trs: { purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.58
443.01/211.58 The induced complexity on above rules (modulo remaining rules) is
443.01/211.58 YES(?,O(n^1)) . These rules are moved into the corresponding weak
443.01/211.58 component(s).
443.01/211.58
443.01/211.58 Sub-proof:
443.01/211.58 ----------
443.01/211.58 The following argument positions are usable:
443.01/211.58 Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
443.01/211.58 Uargs(purge) = {1}
443.01/211.58
443.01/211.58 TcT has computed the following constructor-based matrix
443.01/211.58 interpretation satisfying not(EDA).
443.01/211.58
443.01/211.58 [eq](x1, x2) = [0]
443.01/211.58
443.01/211.58 [0] = [0]
443.01/211.58
443.01/211.58 [true] = [0]
443.01/211.58
443.01/211.58 [s](x1) = [1] x1 + [0]
443.01/211.58
443.01/211.58 [false] = [0]
443.01/211.58
443.01/211.58 [rm](x1, x2) = [1] x2 + [0]
443.01/211.58
443.01/211.58 [nil] = [0]
443.01/211.58
443.01/211.58 [add](x1, x2) = [1] x2 + [1]
443.01/211.58
443.01/211.58 [ifrm](x1, x2, x3) = [4] x1 + [1] x3 + [0]
443.01/211.58
443.01/211.58 [purge](x1) = [4] x1 + [0]
443.01/211.58
443.01/211.58 The order satisfies the following ordering constraints:
443.01/211.58
443.01/211.58 [eq(0(), 0())] = [0]
443.01/211.58 >= [0]
443.01/211.58 = [true()]
443.01/211.58
443.01/211.58 [eq(0(), s(X))] = [0]
443.01/211.58 >= [0]
443.01/211.58 = [false()]
443.01/211.58
443.01/211.58 [eq(s(X), 0())] = [0]
443.01/211.58 >= [0]
443.01/211.58 = [false()]
443.01/211.58
443.01/211.58 [eq(s(X), s(Y))] = [0]
443.01/211.58 >= [0]
443.01/211.58 = [eq(X, Y)]
443.01/211.58
443.01/211.58 [rm(N, nil())] = [0]
443.01/211.58 >= [0]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [rm(N, add(M, X))] = [1] X + [1]
443.01/211.58 >= [1] X + [1]
443.01/211.58 = [ifrm(eq(N, M), N, add(M, X))]
443.01/211.58
443.01/211.58 [ifrm(true(), N, add(M, X))] = [1] X + [1]
443.01/211.58 > [1] X + [0]
443.01/211.58 = [rm(N, X)]
443.01/211.58
443.01/211.58 [ifrm(false(), N, add(M, X))] = [1] X + [1]
443.01/211.58 >= [1] X + [1]
443.01/211.58 = [add(M, rm(N, X))]
443.01/211.58
443.01/211.58 [purge(nil())] = [0]
443.01/211.58 >= [0]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [purge(add(N, X))] = [4] X + [4]
443.01/211.58 > [4] X + [1]
443.01/211.58 = [add(N, purge(rm(N, X)))]
443.01/211.58
443.01/211.58
443.01/211.58 We return to the main proof.
443.01/211.58
443.01/211.58 We are left with following problem, upon which TcT provides the
443.01/211.58 certificate YES(O(1),O(n^2)).
443.01/211.58
443.01/211.58 Strict Trs:
443.01/211.58 { eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.58 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) }
443.01/211.58 Weak Trs:
443.01/211.58 { eq(0(), 0()) -> true()
443.01/211.58 , eq(0(), s(X)) -> false()
443.01/211.58 , eq(s(X), 0()) -> false()
443.01/211.58 , rm(N, nil()) -> nil()
443.01/211.58 , ifrm(true(), N, add(M, X)) -> rm(N, X)
443.01/211.58 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
443.01/211.58 , purge(nil()) -> nil()
443.01/211.58 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.58 Obligation:
443.01/211.58 runtime complexity
443.01/211.58 Answer:
443.01/211.58 YES(O(1),O(n^2))
443.01/211.58
443.01/211.58 The weightgap principle applies (using the following nonconstant
443.01/211.58 growth matrix-interpretation)
443.01/211.58
443.01/211.58 The following argument positions are usable:
443.01/211.58 Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
443.01/211.58 Uargs(purge) = {1}
443.01/211.58
443.01/211.58 TcT has computed the following matrix interpretation satisfying
443.01/211.58 not(EDA) and not(IDA(1)).
443.01/211.58
443.01/211.58 [eq](x1, x2) = [0 1] x2 + [0]
443.01/211.58 [0 0] [4]
443.01/211.58
443.01/211.58 [0] = [0]
443.01/211.58 [4]
443.01/211.58
443.01/211.58 [true] = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [s](x1) = [0 0] x1 + [0]
443.01/211.58 [0 1] [4]
443.01/211.58
443.01/211.58 [false] = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [rm](x1, x2) = [1 4] x2 + [0]
443.01/211.58 [0 0] [0]
443.01/211.58
443.01/211.58 [nil] = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [add](x1, x2) = [0 0] x1 + [1 4] x2 + [0]
443.01/211.58 [0 1] [0 0] [0]
443.01/211.58
443.01/211.58 [ifrm](x1, x2, x3) = [1 0] x1 + [1 0] x3 + [0]
443.01/211.58 [0 0] [0 1] [4]
443.01/211.58
443.01/211.58 [purge](x1) = [1 0] x1 + [0]
443.01/211.58 [0 1] [0]
443.01/211.58
443.01/211.58 The order satisfies the following ordering constraints:
443.01/211.58
443.01/211.58 [eq(0(), 0())] = [4]
443.01/211.58 [4]
443.01/211.58 > [0]
443.01/211.58 [0]
443.01/211.58 = [true()]
443.01/211.58
443.01/211.58 [eq(0(), s(X))] = [0 1] X + [4]
443.01/211.58 [0 0] [4]
443.01/211.58 > [0]
443.01/211.58 [0]
443.01/211.58 = [false()]
443.01/211.58
443.01/211.58 [eq(s(X), 0())] = [4]
443.01/211.58 [4]
443.01/211.58 > [0]
443.01/211.58 [0]
443.01/211.58 = [false()]
443.01/211.58
443.01/211.58 [eq(s(X), s(Y))] = [0 1] Y + [4]
443.01/211.58 [0 0] [4]
443.01/211.58 > [0 1] Y + [0]
443.01/211.58 [0 0] [4]
443.01/211.58 = [eq(X, Y)]
443.01/211.58
443.01/211.58 [rm(N, nil())] = [0]
443.01/211.58 [0]
443.01/211.58 >= [0]
443.01/211.58 [0]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [rm(N, add(M, X))] = [1 4] X + [0 4] M + [0]
443.01/211.58 [0 0] [0 0] [0]
443.01/211.58 ? [1 4] X + [0 1] M + [0]
443.01/211.58 [0 0] [0 1] [4]
443.01/211.58 = [ifrm(eq(N, M), N, add(M, X))]
443.01/211.58
443.01/211.58 [ifrm(true(), N, add(M, X))] = [1 4] X + [0 0] M + [0]
443.01/211.58 [0 0] [0 1] [4]
443.01/211.58 >= [1 4] X + [0]
443.01/211.58 [0 0] [0]
443.01/211.58 = [rm(N, X)]
443.01/211.58
443.01/211.58 [ifrm(false(), N, add(M, X))] = [1 4] X + [0 0] M + [0]
443.01/211.58 [0 0] [0 1] [4]
443.01/211.58 >= [1 4] X + [0 0] M + [0]
443.01/211.58 [0 0] [0 1] [0]
443.01/211.58 = [add(M, rm(N, X))]
443.01/211.58
443.01/211.58 [purge(nil())] = [0]
443.01/211.58 [0]
443.01/211.58 >= [0]
443.01/211.58 [0]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [purge(add(N, X))] = [1 4] X + [0 0] N + [0]
443.01/211.58 [0 0] [0 1] [0]
443.01/211.58 >= [1 4] X + [0 0] N + [0]
443.01/211.58 [0 0] [0 1] [0]
443.01/211.58 = [add(N, purge(rm(N, X)))]
443.01/211.58
443.01/211.58
443.01/211.58 Further, it can be verified that all rules not oriented are covered by the weightgap condition.
443.01/211.58
443.01/211.58 We are left with following problem, upon which TcT provides the
443.01/211.58 certificate YES(O(1),O(n^2)).
443.01/211.58
443.01/211.58 Strict Trs: { rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) }
443.01/211.58 Weak Trs:
443.01/211.58 { eq(0(), 0()) -> true()
443.01/211.58 , eq(0(), s(X)) -> false()
443.01/211.58 , eq(s(X), 0()) -> false()
443.01/211.58 , eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.58 , rm(N, nil()) -> nil()
443.01/211.58 , ifrm(true(), N, add(M, X)) -> rm(N, X)
443.01/211.58 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
443.01/211.58 , purge(nil()) -> nil()
443.01/211.58 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.58 Obligation:
443.01/211.58 runtime complexity
443.01/211.58 Answer:
443.01/211.58 YES(O(1),O(n^2))
443.01/211.58
443.01/211.58 We use the processor 'matrix interpretation of dimension 2' to
443.01/211.58 orient following rules strictly.
443.01/211.58
443.01/211.58 Trs: { rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) }
443.01/211.58
443.01/211.58 The induced complexity on above rules (modulo remaining rules) is
443.01/211.58 YES(?,O(n^2)) . These rules are moved into the corresponding weak
443.01/211.58 component(s).
443.01/211.58
443.01/211.58 Sub-proof:
443.01/211.58 ----------
443.01/211.58 The following argument positions are usable:
443.01/211.58 Uargs(rm) = {2}, Uargs(add) = {2}, Uargs(ifrm) = {1, 3},
443.01/211.58 Uargs(purge) = {1}
443.01/211.58
443.01/211.58 TcT has computed the following constructor-based matrix
443.01/211.58 interpretation satisfying not(EDA).
443.01/211.58
443.01/211.58 [eq](x1, x2) = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [0] = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [true] = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [s](x1) = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [false] = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [rm](x1, x2) = [1 2] x2 + [1]
443.01/211.58 [0 1] [0]
443.01/211.58
443.01/211.58 [nil] = [0]
443.01/211.58 [0]
443.01/211.58
443.01/211.58 [add](x1, x2) = [1 4] x2 + [0]
443.01/211.58 [0 1] [2]
443.01/211.58
443.01/211.58 [ifrm](x1, x2, x3) = [1 0] x1 + [1 2] x3 + [0]
443.01/211.58 [0 0] [0 1] [0]
443.01/211.58
443.01/211.58 [purge](x1) = [2 2] x1 + [4]
443.01/211.58 [0 1] [0]
443.01/211.58
443.01/211.58 The order satisfies the following ordering constraints:
443.01/211.58
443.01/211.58 [eq(0(), 0())] = [0]
443.01/211.58 [0]
443.01/211.58 >= [0]
443.01/211.58 [0]
443.01/211.58 = [true()]
443.01/211.58
443.01/211.58 [eq(0(), s(X))] = [0]
443.01/211.58 [0]
443.01/211.58 >= [0]
443.01/211.58 [0]
443.01/211.58 = [false()]
443.01/211.58
443.01/211.58 [eq(s(X), 0())] = [0]
443.01/211.58 [0]
443.01/211.58 >= [0]
443.01/211.58 [0]
443.01/211.58 = [false()]
443.01/211.58
443.01/211.58 [eq(s(X), s(Y))] = [0]
443.01/211.58 [0]
443.01/211.58 >= [0]
443.01/211.58 [0]
443.01/211.58 = [eq(X, Y)]
443.01/211.58
443.01/211.58 [rm(N, nil())] = [1]
443.01/211.58 [0]
443.01/211.58 > [0]
443.01/211.58 [0]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [rm(N, add(M, X))] = [1 6] X + [5]
443.01/211.58 [0 1] [2]
443.01/211.58 > [1 6] X + [4]
443.01/211.58 [0 1] [2]
443.01/211.58 = [ifrm(eq(N, M), N, add(M, X))]
443.01/211.58
443.01/211.58 [ifrm(true(), N, add(M, X))] = [1 6] X + [4]
443.01/211.58 [0 1] [2]
443.01/211.58 > [1 2] X + [1]
443.01/211.58 [0 1] [0]
443.01/211.58 = [rm(N, X)]
443.01/211.58
443.01/211.58 [ifrm(false(), N, add(M, X))] = [1 6] X + [4]
443.01/211.58 [0 1] [2]
443.01/211.58 > [1 6] X + [1]
443.01/211.58 [0 1] [2]
443.01/211.58 = [add(M, rm(N, X))]
443.01/211.58
443.01/211.58 [purge(nil())] = [4]
443.01/211.58 [0]
443.01/211.58 > [0]
443.01/211.58 [0]
443.01/211.58 = [nil()]
443.01/211.58
443.01/211.58 [purge(add(N, X))] = [2 10] X + [8]
443.01/211.58 [0 1] [2]
443.01/211.58 > [2 10] X + [6]
443.01/211.58 [0 1] [2]
443.01/211.58 = [add(N, purge(rm(N, X)))]
443.01/211.58
443.01/211.58
443.01/211.58 We return to the main proof.
443.01/211.58
443.01/211.58 We are left with following problem, upon which TcT provides the
443.01/211.58 certificate YES(O(1),O(1)).
443.01/211.58
443.01/211.58 Weak Trs:
443.01/211.58 { eq(0(), 0()) -> true()
443.01/211.58 , eq(0(), s(X)) -> false()
443.01/211.58 , eq(s(X), 0()) -> false()
443.01/211.58 , eq(s(X), s(Y)) -> eq(X, Y)
443.01/211.58 , rm(N, nil()) -> nil()
443.01/211.58 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
443.01/211.58 , ifrm(true(), N, add(M, X)) -> rm(N, X)
443.01/211.58 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
443.01/211.58 , purge(nil()) -> nil()
443.01/211.58 , purge(add(N, X)) -> add(N, purge(rm(N, X))) }
443.01/211.58 Obligation:
443.01/211.58 runtime complexity
443.01/211.58 Answer:
443.01/211.58 YES(O(1),O(1))
443.01/211.58
443.01/211.58 Empty rules are trivially bounded
443.01/211.58
443.01/211.58 Hurray, we answered YES(O(1),O(n^2))
443.37/211.81 EOF