YES(O(1),O(n^2)) 218.62/77.60 YES(O(1),O(n^2)) 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(n^2)). 218.62/77.60 218.62/77.60 Strict Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) 218.62/77.60 , purge(nil()) -> nil() 218.62/77.60 , purge(add(N, X)) -> add(N, purge(rm(N, X))) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(n^2)) 218.62/77.60 218.62/77.60 We add the following dependency tuples: 218.62/77.60 218.62/77.60 Strict DPs: 218.62/77.60 { eq^#(0(), 0()) -> c_1() 218.62/77.60 , eq^#(0(), s(X)) -> c_2() 218.62/77.60 , eq^#(s(X), 0()) -> c_3() 218.62/77.60 , eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , rm^#(N, nil()) -> c_5() 218.62/77.60 , rm^#(N, add(M, X)) -> 218.62/77.60 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.60 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.60 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) 218.62/77.60 , purge^#(nil()) -> c_9() 218.62/77.60 , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 218.62/77.60 and mark the set of starting terms. 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(n^2)). 218.62/77.60 218.62/77.60 Strict DPs: 218.62/77.60 { eq^#(0(), 0()) -> c_1() 218.62/77.60 , eq^#(0(), s(X)) -> c_2() 218.62/77.60 , eq^#(s(X), 0()) -> c_3() 218.62/77.60 , eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , rm^#(N, nil()) -> c_5() 218.62/77.60 , rm^#(N, add(M, X)) -> 218.62/77.60 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.60 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.60 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) 218.62/77.60 , purge^#(nil()) -> c_9() 218.62/77.60 , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 Weak Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) 218.62/77.60 , purge(nil()) -> nil() 218.62/77.60 , purge(add(N, X)) -> add(N, purge(rm(N, X))) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(n^2)) 218.62/77.60 218.62/77.60 We estimate the number of application of {1,2,3,5,9} by 218.62/77.60 applications of Pre({1,2,3,5,9}) = {4,6,7,8,10}. Here rules are 218.62/77.60 labeled as follows: 218.62/77.60 218.62/77.60 DPs: 218.62/77.60 { 1: eq^#(0(), 0()) -> c_1() 218.62/77.60 , 2: eq^#(0(), s(X)) -> c_2() 218.62/77.60 , 3: eq^#(s(X), 0()) -> c_3() 218.62/77.60 , 4: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , 5: rm^#(N, nil()) -> c_5() 218.62/77.60 , 6: rm^#(N, add(M, X)) -> 218.62/77.60 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.60 , 7: ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.60 , 8: ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) 218.62/77.60 , 9: purge^#(nil()) -> c_9() 218.62/77.60 , 10: purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(n^2)). 218.62/77.60 218.62/77.60 Strict DPs: 218.62/77.60 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , rm^#(N, add(M, X)) -> 218.62/77.60 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.60 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.60 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) 218.62/77.60 , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 Weak DPs: 218.62/77.60 { eq^#(0(), 0()) -> c_1() 218.62/77.60 , eq^#(0(), s(X)) -> c_2() 218.62/77.60 , eq^#(s(X), 0()) -> c_3() 218.62/77.60 , rm^#(N, nil()) -> c_5() 218.62/77.60 , purge^#(nil()) -> c_9() } 218.62/77.60 Weak Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) 218.62/77.60 , purge(nil()) -> nil() 218.62/77.60 , purge(add(N, X)) -> add(N, purge(rm(N, X))) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(n^2)) 218.62/77.60 218.62/77.60 The following weak DPs constitute a sub-graph of the DG that is 218.62/77.60 closed under successors. The DPs are removed. 218.62/77.60 218.62/77.60 { eq^#(0(), 0()) -> c_1() 218.62/77.60 , eq^#(0(), s(X)) -> c_2() 218.62/77.60 , eq^#(s(X), 0()) -> c_3() 218.62/77.60 , rm^#(N, nil()) -> c_5() 218.62/77.60 , purge^#(nil()) -> c_9() } 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(n^2)). 218.62/77.60 218.62/77.60 Strict DPs: 218.62/77.60 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , rm^#(N, add(M, X)) -> 218.62/77.60 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.60 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.60 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) 218.62/77.60 , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 Weak Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) 218.62/77.60 , purge(nil()) -> nil() 218.62/77.60 , purge(add(N, X)) -> add(N, purge(rm(N, X))) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(n^2)) 218.62/77.60 218.62/77.60 We replace rewrite rules by usable rules: 218.62/77.60 218.62/77.60 Weak Usable Rules: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(n^2)). 218.62/77.60 218.62/77.60 Strict DPs: 218.62/77.60 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , rm^#(N, add(M, X)) -> 218.62/77.60 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.60 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.60 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) 218.62/77.60 , purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 Weak Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(n^2)) 218.62/77.60 218.62/77.60 We decompose the input problem according to the dependency graph 218.62/77.60 into the upper component 218.62/77.60 218.62/77.60 { purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 218.62/77.60 and lower component 218.62/77.60 218.62/77.60 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , rm^#(N, add(M, X)) -> 218.62/77.60 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.60 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.60 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) } 218.62/77.60 218.62/77.60 Further, following extension rules are added to the lower 218.62/77.60 component. 218.62/77.60 218.62/77.60 { purge^#(add(N, X)) -> rm^#(N, X) 218.62/77.60 , purge^#(add(N, X)) -> purge^#(rm(N, X)) } 218.62/77.60 218.62/77.60 TcT solves the upper component with certificate YES(O(1),O(n^1)). 218.62/77.60 218.62/77.60 Sub-proof: 218.62/77.60 ---------- 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(n^1)). 218.62/77.60 218.62/77.60 Strict DPs: 218.62/77.60 { purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 Weak Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(n^1)) 218.62/77.60 218.62/77.60 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 218.62/77.60 to orient following rules strictly. 218.62/77.60 218.62/77.60 DPs: 218.62/77.60 { 1: purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) } 218.62/77.60 218.62/77.60 Sub-proof: 218.62/77.60 ---------- 218.62/77.60 The input was oriented with the instance of 'Small Polynomial Path 218.62/77.60 Order (PS,1-bounded)' as induced by the safe mapping 218.62/77.60 218.62/77.60 safe(eq) = {2}, safe(0) = {}, safe(true) = {}, safe(s) = {1}, 218.62/77.60 safe(false) = {}, safe(rm) = {}, safe(nil) = {}, 218.62/77.60 safe(add) = {1, 2}, safe(ifrm) = {}, safe(rm^#) = {}, 218.62/77.60 safe(purge^#) = {}, safe(c_10) = {} 218.62/77.60 218.62/77.60 and precedence 218.62/77.60 218.62/77.60 purge^# > eq, purge^# > ifrm, eq ~ rm, eq ~ ifrm . 218.62/77.60 218.62/77.60 Following symbols are considered recursive: 218.62/77.60 218.62/77.60 {purge^#} 218.62/77.60 218.62/77.60 The recursion depth is 1. 218.62/77.60 218.62/77.60 Further, following argument filtering is employed: 218.62/77.60 218.62/77.60 pi(eq) = [2], pi(0) = [], pi(true) = [], pi(s) = [], 218.62/77.60 pi(false) = [], pi(rm) = 2, pi(nil) = [], pi(add) = [2], 218.62/77.60 pi(ifrm) = 3, pi(rm^#) = [], pi(purge^#) = [1], pi(c_10) = [1, 2] 218.62/77.60 218.62/77.60 Usable defined function symbols are a subset of: 218.62/77.60 218.62/77.60 {rm, ifrm, rm^#, purge^#} 218.62/77.60 218.62/77.60 For your convenience, here are the satisfied ordering constraints: 218.62/77.60 218.62/77.60 pi(purge^#(add(N, X))) = purge^#(add(; X);) 218.62/77.60 > c_10(purge^#(X;), rm^#();) 218.62/77.60 = pi(c_10(purge^#(rm(N, X)), rm^#(N, X))) 218.62/77.60 218.62/77.60 pi(rm(N, nil())) = nil() 218.62/77.60 >= nil() 218.62/77.60 = pi(nil()) 218.62/77.60 218.62/77.60 pi(rm(N, add(M, X))) = add(; X) 218.62/77.60 >= add(; X) 218.62/77.60 = pi(ifrm(eq(N, M), N, add(M, X))) 218.62/77.60 218.62/77.60 pi(ifrm(true(), N, add(M, X))) = add(; X) 218.62/77.60 > X 218.62/77.60 = pi(rm(N, X)) 218.62/77.60 218.62/77.60 pi(ifrm(false(), N, add(M, X))) = add(; X) 218.62/77.60 >= add(; X) 218.62/77.60 = pi(add(M, rm(N, X))) 218.62/77.60 218.62/77.60 218.62/77.60 The strictly oriented rules are moved into the weak component. 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(1)). 218.62/77.60 218.62/77.60 Weak DPs: 218.62/77.60 { purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 Weak Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(1)) 218.62/77.60 218.62/77.60 The following weak DPs constitute a sub-graph of the DG that is 218.62/77.60 closed under successors. The DPs are removed. 218.62/77.60 218.62/77.60 { purge^#(add(N, X)) -> c_10(purge^#(rm(N, X)), rm^#(N, X)) } 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(1)). 218.62/77.60 218.62/77.60 Weak Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(1)) 218.62/77.60 218.62/77.60 No rule is usable, rules are removed from the input problem. 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(1)). 218.62/77.60 218.62/77.60 Rules: Empty 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(1)) 218.62/77.60 218.62/77.60 Empty rules are trivially bounded 218.62/77.60 218.62/77.60 We return to the main proof. 218.62/77.60 218.62/77.60 We are left with following problem, upon which TcT provides the 218.62/77.60 certificate YES(O(1),O(n^1)). 218.62/77.60 218.62/77.60 Strict DPs: 218.62/77.60 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , rm^#(N, add(M, X)) -> 218.62/77.60 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.60 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.60 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) } 218.62/77.60 Weak DPs: 218.62/77.60 { purge^#(add(N, X)) -> rm^#(N, X) 218.62/77.60 , purge^#(add(N, X)) -> purge^#(rm(N, X)) } 218.62/77.60 Weak Trs: 218.62/77.60 { eq(0(), 0()) -> true() 218.62/77.60 , eq(0(), s(X)) -> false() 218.62/77.60 , eq(s(X), 0()) -> false() 218.62/77.60 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.60 , rm(N, nil()) -> nil() 218.62/77.60 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.60 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.60 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.60 Obligation: 218.62/77.60 innermost runtime complexity 218.62/77.60 Answer: 218.62/77.60 YES(O(1),O(n^1)) 218.62/77.60 218.62/77.60 We use the processor 'matrix interpretation of dimension 2' to 218.62/77.60 orient following rules strictly. 218.62/77.60 218.62/77.60 DPs: 218.62/77.60 { 1: eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.60 , 5: purge^#(add(N, X)) -> rm^#(N, X) } 218.62/77.60 218.62/77.60 Sub-proof: 218.62/77.60 ---------- 218.62/77.60 The following argument positions are usable: 218.62/77.60 Uargs(c_4) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_7) = {1}, 218.62/77.60 Uargs(c_8) = {1} 218.62/77.60 218.62/77.60 TcT has computed the following constructor-based matrix 218.62/77.60 interpretation satisfying not(EDA) and not(IDA(1)). 218.62/77.60 218.62/77.60 [eq](x1, x2) = [0] 218.62/77.60 [0] 218.62/77.60 218.62/77.60 [0] = [0] 218.62/77.60 [0] 218.62/77.60 218.62/77.60 [true] = [0] 218.62/77.60 [0] 218.62/77.60 218.62/77.60 [s](x1) = [1 0] x1 + [4] 218.62/77.60 [0 0] [0] 218.62/77.60 218.62/77.60 [false] = [0] 218.62/77.60 [0] 218.62/77.60 218.62/77.60 [rm](x1, x2) = [1 0] x2 + [0] 218.62/77.60 [1 0] [0] 218.62/77.60 218.62/77.60 [nil] = [4] 218.62/77.60 [0] 218.62/77.60 218.62/77.60 [add](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 218.62/77.60 [0 0] [1 0] [0] 218.62/77.60 218.62/77.60 [ifrm](x1, x2, x3) = [1 0] x3 + [0] 218.62/77.60 [1 0] [0] 218.62/77.60 218.62/77.60 [eq^#](x1, x2) = [1 0] x2 + [0] 218.62/77.60 [0 0] [4] 218.62/77.60 218.62/77.60 [c_4](x1) = [1 0] x1 + [1] 218.62/77.60 [0 0] [3] 218.62/77.60 218.62/77.60 [rm^#](x1, x2) = [4 0] x2 + [0] 218.62/77.60 [0 0] [4] 218.62/77.60 218.62/77.60 [c_6](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 218.62/77.60 [0 0] [0 0] [3] 218.62/77.60 218.62/77.60 [ifrm^#](x1, x2, x3) = [2 2] x3 + [0] 218.62/77.60 [0 0] [0] 218.62/77.60 218.62/77.60 [c_7](x1) = [1 0] x1 + [0] 218.62/77.60 [0 0] [0] 218.62/77.60 218.62/77.60 [c_8](x1) = [1 0] x1 + [0] 218.62/77.60 [0 0] [0] 218.62/77.60 218.62/77.60 [purge^#](x1) = [0 4] x1 + [4] 218.62/77.60 [0 4] [4] 218.62/77.60 218.62/77.60 The order satisfies the following ordering constraints: 218.62/77.60 218.62/77.60 [eq(0(), 0())] = [0] 218.62/77.60 [0] 218.62/77.60 >= [0] 218.62/77.60 [0] 218.62/77.60 = [true()] 218.62/77.60 218.62/77.61 [eq(0(), s(X))] = [0] 218.62/77.61 [0] 218.62/77.61 >= [0] 218.62/77.61 [0] 218.62/77.61 = [false()] 218.62/77.61 218.62/77.61 [eq(s(X), 0())] = [0] 218.62/77.61 [0] 218.62/77.61 >= [0] 218.62/77.61 [0] 218.62/77.61 = [false()] 218.62/77.61 218.62/77.61 [eq(s(X), s(Y))] = [0] 218.62/77.61 [0] 218.62/77.61 >= [0] 218.62/77.61 [0] 218.62/77.61 = [eq(X, Y)] 218.62/77.61 218.62/77.61 [rm(N, nil())] = [4] 218.62/77.61 [4] 218.62/77.61 >= [4] 218.62/77.61 [0] 218.62/77.61 = [nil()] 218.62/77.61 218.62/77.61 [rm(N, add(M, X))] = [1 0] X + [1 0] M + [0] 218.62/77.61 [1 0] [1 0] [0] 218.62/77.61 >= [1 0] X + [1 0] M + [0] 218.62/77.61 [1 0] [1 0] [0] 218.62/77.61 = [ifrm(eq(N, M), N, add(M, X))] 218.62/77.61 218.62/77.61 [ifrm(true(), N, add(M, X))] = [1 0] X + [1 0] M + [0] 218.62/77.61 [1 0] [1 0] [0] 218.62/77.61 >= [1 0] X + [0] 218.62/77.61 [1 0] [0] 218.62/77.61 = [rm(N, X)] 218.62/77.61 218.62/77.61 [ifrm(false(), N, add(M, X))] = [1 0] X + [1 0] M + [0] 218.62/77.61 [1 0] [1 0] [0] 218.62/77.61 >= [1 0] X + [1 0] M + [0] 218.62/77.61 [1 0] [0 0] [0] 218.62/77.61 = [add(M, rm(N, X))] 218.62/77.61 218.62/77.61 [eq^#(s(X), s(Y))] = [1 0] Y + [4] 218.62/77.61 [0 0] [4] 218.62/77.61 > [1 0] Y + [1] 218.62/77.61 [0 0] [3] 218.62/77.61 = [c_4(eq^#(X, Y))] 218.62/77.61 218.62/77.61 [rm^#(N, add(M, X))] = [4 0] X + [4 0] M + [0] 218.62/77.61 [0 0] [0 0] [4] 218.62/77.61 >= [4 0] X + [3 0] M + [0] 218.62/77.61 [0 0] [0 0] [3] 218.62/77.61 = [c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M))] 218.62/77.61 218.62/77.61 [ifrm^#(true(), N, add(M, X))] = [4 0] X + [2 0] M + [0] 218.62/77.61 [0 0] [0 0] [0] 218.62/77.61 >= [4 0] X + [0] 218.62/77.61 [0 0] [0] 218.62/77.61 = [c_7(rm^#(N, X))] 218.62/77.61 218.62/77.61 [ifrm^#(false(), N, add(M, X))] = [4 0] X + [2 0] M + [0] 218.62/77.61 [0 0] [0 0] [0] 218.62/77.61 >= [4 0] X + [0] 218.62/77.61 [0 0] [0] 218.62/77.61 = [c_8(rm^#(N, X))] 218.62/77.61 218.62/77.61 [purge^#(add(N, X))] = [4 0] X + [4] 218.62/77.61 [4 0] [4] 218.62/77.61 > [4 0] X + [0] 218.62/77.61 [0 0] [4] 218.62/77.61 = [rm^#(N, X)] 218.62/77.61 218.62/77.61 [purge^#(add(N, X))] = [4 0] X + [4] 218.62/77.61 [4 0] [4] 218.62/77.61 >= [4 0] X + [4] 218.62/77.61 [4 0] [4] 218.62/77.61 = [purge^#(rm(N, X))] 218.62/77.61 218.62/77.61 218.62/77.61 The strictly oriented rules are moved into the weak component. 218.62/77.61 218.62/77.61 We are left with following problem, upon which TcT provides the 218.62/77.61 certificate YES(O(1),O(n^1)). 218.62/77.61 218.62/77.61 Strict DPs: 218.62/77.61 { rm^#(N, add(M, X)) -> 218.62/77.61 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.61 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.61 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) } 218.62/77.61 Weak DPs: 218.62/77.61 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) 218.62/77.61 , purge^#(add(N, X)) -> rm^#(N, X) 218.62/77.61 , purge^#(add(N, X)) -> purge^#(rm(N, X)) } 218.62/77.61 Weak Trs: 218.62/77.61 { eq(0(), 0()) -> true() 218.62/77.61 , eq(0(), s(X)) -> false() 218.62/77.61 , eq(s(X), 0()) -> false() 218.62/77.61 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.61 , rm(N, nil()) -> nil() 218.62/77.61 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.61 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.61 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.61 Obligation: 218.62/77.61 innermost runtime complexity 218.62/77.61 Answer: 218.62/77.61 YES(O(1),O(n^1)) 218.62/77.61 218.62/77.61 The following weak DPs constitute a sub-graph of the DG that is 218.62/77.61 closed under successors. The DPs are removed. 218.62/77.61 218.62/77.61 { eq^#(s(X), s(Y)) -> c_4(eq^#(X, Y)) } 218.62/77.61 218.62/77.61 We are left with following problem, upon which TcT provides the 218.62/77.61 certificate YES(O(1),O(n^1)). 218.62/77.61 218.62/77.61 Strict DPs: 218.62/77.61 { rm^#(N, add(M, X)) -> 218.62/77.61 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) 218.62/77.61 , ifrm^#(true(), N, add(M, X)) -> c_7(rm^#(N, X)) 218.62/77.61 , ifrm^#(false(), N, add(M, X)) -> c_8(rm^#(N, X)) } 218.62/77.61 Weak DPs: 218.62/77.61 { purge^#(add(N, X)) -> rm^#(N, X) 218.62/77.61 , purge^#(add(N, X)) -> purge^#(rm(N, X)) } 218.62/77.61 Weak Trs: 218.62/77.61 { eq(0(), 0()) -> true() 218.62/77.61 , eq(0(), s(X)) -> false() 218.62/77.61 , eq(s(X), 0()) -> false() 218.62/77.61 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.61 , rm(N, nil()) -> nil() 218.62/77.61 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.61 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.61 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.61 Obligation: 218.62/77.61 innermost runtime complexity 218.62/77.61 Answer: 218.62/77.61 YES(O(1),O(n^1)) 218.62/77.61 218.62/77.61 Due to missing edges in the dependency-graph, the right-hand sides 218.62/77.61 of following rules could be simplified: 218.62/77.61 218.62/77.61 { rm^#(N, add(M, X)) -> 218.62/77.61 c_6(ifrm^#(eq(N, M), N, add(M, X)), eq^#(N, M)) } 218.62/77.61 218.62/77.61 We are left with following problem, upon which TcT provides the 218.62/77.61 certificate YES(O(1),O(n^1)). 218.62/77.61 218.62/77.61 Strict DPs: 218.62/77.61 { rm^#(N, add(M, X)) -> c_1(ifrm^#(eq(N, M), N, add(M, X))) 218.62/77.61 , ifrm^#(true(), N, add(M, X)) -> c_2(rm^#(N, X)) 218.62/77.61 , ifrm^#(false(), N, add(M, X)) -> c_3(rm^#(N, X)) } 218.62/77.61 Weak DPs: 218.62/77.61 { purge^#(add(N, X)) -> c_4(rm^#(N, X)) 218.62/77.61 , purge^#(add(N, X)) -> c_5(purge^#(rm(N, X))) } 218.62/77.61 Weak Trs: 218.62/77.61 { eq(0(), 0()) -> true() 218.62/77.61 , eq(0(), s(X)) -> false() 218.62/77.61 , eq(s(X), 0()) -> false() 218.62/77.61 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.61 , rm(N, nil()) -> nil() 218.62/77.61 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.61 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.61 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.61 Obligation: 218.62/77.61 innermost runtime complexity 218.62/77.61 Answer: 218.62/77.61 YES(O(1),O(n^1)) 218.62/77.61 218.62/77.61 We use the processor 'matrix interpretation of dimension 1' to 218.62/77.61 orient following rules strictly. 218.62/77.61 218.62/77.61 DPs: 218.62/77.61 { 2: ifrm^#(true(), N, add(M, X)) -> c_2(rm^#(N, X)) 218.62/77.61 , 3: ifrm^#(false(), N, add(M, X)) -> c_3(rm^#(N, X)) 218.62/77.61 , 4: purge^#(add(N, X)) -> c_4(rm^#(N, X)) 218.62/77.61 , 5: purge^#(add(N, X)) -> c_5(purge^#(rm(N, X))) } 218.62/77.61 Trs: { ifrm(true(), N, add(M, X)) -> rm(N, X) } 218.62/77.61 218.62/77.61 Sub-proof: 218.62/77.61 ---------- 218.62/77.61 The following argument positions are usable: 218.62/77.61 Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, 218.62/77.61 Uargs(c_4) = {1}, Uargs(c_5) = {1} 218.62/77.61 218.62/77.61 TcT has computed the following constructor-based matrix 218.62/77.61 interpretation satisfying not(EDA). 218.62/77.61 218.62/77.61 [eq](x1, x2) = [0] 218.62/77.61 218.62/77.61 [0] = [0] 218.62/77.61 218.62/77.61 [true] = [0] 218.62/77.61 218.62/77.61 [s](x1) = [1] x1 + [0] 218.62/77.61 218.62/77.61 [false] = [0] 218.62/77.61 218.62/77.61 [rm](x1, x2) = [1] x2 + [0] 218.62/77.61 218.62/77.61 [nil] = [0] 218.62/77.61 218.62/77.61 [add](x1, x2) = [1] x2 + [4] 218.62/77.61 218.62/77.61 [ifrm](x1, x2, x3) = [1] x3 + [0] 218.62/77.61 218.62/77.61 [eq^#](x1, x2) = [7] x1 + [7] x2 + [0] 218.62/77.61 218.62/77.61 [c_4](x1) = [7] x1 + [0] 218.62/77.61 218.62/77.61 [rm^#](x1, x2) = [2] x2 + [0] 218.62/77.61 218.62/77.61 [c_6](x1, x2) = [7] x1 + [7] x2 + [0] 218.62/77.61 218.62/77.61 [ifrm^#](x1, x2, x3) = [2] x3 + [0] 218.62/77.61 218.62/77.61 [c_7](x1) = [7] x1 + [0] 218.62/77.61 218.62/77.61 [c_8](x1) = [7] x1 + [0] 218.62/77.61 218.62/77.61 [purge^#](x1) = [2] x1 + [0] 218.62/77.61 218.62/77.61 [c] = [0] 218.62/77.61 218.62/77.61 [c_1](x1) = [1] x1 + [0] 218.62/77.61 218.62/77.61 [c_2](x1) = [1] x1 + [3] 218.62/77.61 218.62/77.61 [c_3](x1) = [1] x1 + [1] 218.62/77.61 218.62/77.61 [c_4](x1) = [1] x1 + [5] 218.62/77.61 218.62/77.61 [c_5](x1) = [1] x1 + [7] 218.62/77.61 218.62/77.61 The order satisfies the following ordering constraints: 218.62/77.61 218.62/77.61 [eq(0(), 0())] = [0] 218.62/77.61 >= [0] 218.62/77.61 = [true()] 218.62/77.61 218.62/77.61 [eq(0(), s(X))] = [0] 218.62/77.61 >= [0] 218.62/77.61 = [false()] 218.62/77.61 218.62/77.61 [eq(s(X), 0())] = [0] 218.62/77.61 >= [0] 218.62/77.61 = [false()] 218.62/77.61 218.62/77.61 [eq(s(X), s(Y))] = [0] 218.62/77.61 >= [0] 218.62/77.61 = [eq(X, Y)] 218.62/77.61 218.62/77.61 [rm(N, nil())] = [0] 218.62/77.61 >= [0] 218.62/77.61 = [nil()] 218.62/77.61 218.62/77.61 [rm(N, add(M, X))] = [1] X + [4] 218.62/77.61 >= [1] X + [4] 218.62/77.61 = [ifrm(eq(N, M), N, add(M, X))] 218.62/77.61 218.62/77.61 [ifrm(true(), N, add(M, X))] = [1] X + [4] 218.62/77.61 > [1] X + [0] 218.62/77.61 = [rm(N, X)] 218.62/77.61 218.62/77.61 [ifrm(false(), N, add(M, X))] = [1] X + [4] 218.62/77.61 >= [1] X + [4] 218.62/77.61 = [add(M, rm(N, X))] 218.62/77.61 218.62/77.61 [rm^#(N, add(M, X))] = [2] X + [8] 218.62/77.61 >= [2] X + [8] 218.62/77.61 = [c_1(ifrm^#(eq(N, M), N, add(M, X)))] 218.62/77.61 218.62/77.61 [ifrm^#(true(), N, add(M, X))] = [2] X + [8] 218.62/77.61 > [2] X + [3] 218.62/77.61 = [c_2(rm^#(N, X))] 218.62/77.61 218.62/77.61 [ifrm^#(false(), N, add(M, X))] = [2] X + [8] 218.62/77.61 > [2] X + [1] 218.62/77.61 = [c_3(rm^#(N, X))] 218.62/77.61 218.62/77.61 [purge^#(add(N, X))] = [2] X + [8] 218.62/77.61 > [2] X + [5] 218.62/77.61 = [c_4(rm^#(N, X))] 218.62/77.61 218.62/77.61 [purge^#(add(N, X))] = [2] X + [8] 218.62/77.61 > [2] X + [7] 218.62/77.61 = [c_5(purge^#(rm(N, X)))] 218.62/77.61 218.62/77.61 218.62/77.61 We return to the main proof. Consider the set of all dependency 218.62/77.61 pairs 218.62/77.61 218.62/77.61 : 218.62/77.61 { 1: rm^#(N, add(M, X)) -> c_1(ifrm^#(eq(N, M), N, add(M, X))) 218.62/77.61 , 2: ifrm^#(true(), N, add(M, X)) -> c_2(rm^#(N, X)) 218.62/77.61 , 3: ifrm^#(false(), N, add(M, X)) -> c_3(rm^#(N, X)) 218.62/77.61 , 4: purge^#(add(N, X)) -> c_4(rm^#(N, X)) 218.62/77.61 , 5: purge^#(add(N, X)) -> c_5(purge^#(rm(N, X))) } 218.62/77.61 218.62/77.61 Processor 'matrix interpretation of dimension 1' induces the 218.62/77.61 complexity certificate YES(?,O(n^1)) on application of dependency 218.62/77.61 pairs {2,3,4,5}. These cover all (indirect) predecessors of 218.62/77.61 dependency pairs {1,2,3,4,5}, their number of application is 218.62/77.61 equally bounded. The dependency pairs are shifted into the weak 218.62/77.61 component. 218.62/77.61 218.62/77.61 We are left with following problem, upon which TcT provides the 218.62/77.61 certificate YES(O(1),O(1)). 218.62/77.61 218.62/77.61 Weak DPs: 218.62/77.61 { rm^#(N, add(M, X)) -> c_1(ifrm^#(eq(N, M), N, add(M, X))) 218.62/77.61 , ifrm^#(true(), N, add(M, X)) -> c_2(rm^#(N, X)) 218.62/77.61 , ifrm^#(false(), N, add(M, X)) -> c_3(rm^#(N, X)) 218.62/77.61 , purge^#(add(N, X)) -> c_4(rm^#(N, X)) 218.62/77.61 , purge^#(add(N, X)) -> c_5(purge^#(rm(N, X))) } 218.62/77.61 Weak Trs: 218.62/77.61 { eq(0(), 0()) -> true() 218.62/77.61 , eq(0(), s(X)) -> false() 218.62/77.61 , eq(s(X), 0()) -> false() 218.62/77.61 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.61 , rm(N, nil()) -> nil() 218.62/77.61 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.61 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.61 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.61 Obligation: 218.62/77.61 innermost runtime complexity 218.62/77.61 Answer: 218.62/77.61 YES(O(1),O(1)) 218.62/77.61 218.62/77.61 The following weak DPs constitute a sub-graph of the DG that is 218.62/77.61 closed under successors. The DPs are removed. 218.62/77.61 218.62/77.61 { rm^#(N, add(M, X)) -> c_1(ifrm^#(eq(N, M), N, add(M, X))) 218.62/77.61 , ifrm^#(true(), N, add(M, X)) -> c_2(rm^#(N, X)) 218.62/77.61 , ifrm^#(false(), N, add(M, X)) -> c_3(rm^#(N, X)) 218.62/77.61 , purge^#(add(N, X)) -> c_4(rm^#(N, X)) 218.62/77.61 , purge^#(add(N, X)) -> c_5(purge^#(rm(N, X))) } 218.62/77.61 218.62/77.61 We are left with following problem, upon which TcT provides the 218.62/77.61 certificate YES(O(1),O(1)). 218.62/77.61 218.62/77.61 Weak Trs: 218.62/77.61 { eq(0(), 0()) -> true() 218.62/77.61 , eq(0(), s(X)) -> false() 218.62/77.61 , eq(s(X), 0()) -> false() 218.62/77.61 , eq(s(X), s(Y)) -> eq(X, Y) 218.62/77.61 , rm(N, nil()) -> nil() 218.62/77.61 , rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)) 218.62/77.61 , ifrm(true(), N, add(M, X)) -> rm(N, X) 218.62/77.61 , ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)) } 218.62/77.61 Obligation: 218.62/77.61 innermost runtime complexity 218.62/77.61 Answer: 218.62/77.61 YES(O(1),O(1)) 218.62/77.61 218.62/77.61 No rule is usable, rules are removed from the input problem. 218.62/77.61 218.62/77.61 We are left with following problem, upon which TcT provides the 218.62/77.61 certificate YES(O(1),O(1)). 218.62/77.61 218.62/77.61 Rules: Empty 218.62/77.61 Obligation: 218.62/77.61 innermost runtime complexity 218.62/77.61 Answer: 218.62/77.61 YES(O(1),O(1)) 218.62/77.61 218.62/77.61 Empty rules are trivially bounded 218.62/77.61 218.62/77.61 Hurray, we answered YES(O(1),O(n^2)) 218.62/77.69 EOF