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