YES(?,O(n^1)) 2.68/1.39 YES(?,O(n^1)) 2.68/1.39 2.68/1.39 We are left with following problem, upon which TcT provides the 2.68/1.39 certificate YES(?,O(n^1)). 2.68/1.39 2.68/1.39 Strict Trs: 2.68/1.39 { a(c(d(x))) -> c(x) 2.68/1.39 , u(b(d(d(x)))) -> b(x) 2.68/1.39 , v(a(a(x))) -> u(v(x)) 2.68/1.39 , v(a(c(x))) -> u(b(d(x))) 2.68/1.39 , v(c(x)) -> b(x) 2.68/1.39 , w(a(a(x))) -> u(w(x)) 2.68/1.39 , w(a(c(x))) -> u(b(d(x))) 2.68/1.39 , w(c(x)) -> b(x) } 2.68/1.39 Obligation: 2.68/1.39 innermost runtime complexity 2.68/1.39 Answer: 2.68/1.39 YES(?,O(n^1)) 2.68/1.39 2.68/1.39 The input was oriented with the instance of 'Small Polynomial Path 2.68/1.39 Order (PS,1-bounded)' as induced by the safe mapping 2.68/1.39 2.68/1.39 safe(a) = {1}, safe(c) = {1}, safe(d) = {1}, safe(u) = {1}, 2.68/1.39 safe(b) = {1}, safe(v) = {}, safe(w) = {} 2.68/1.39 2.68/1.39 and precedence 2.68/1.39 2.68/1.39 v > u, w > u, v ~ w . 2.68/1.39 2.68/1.39 Following symbols are considered recursive: 2.68/1.39 2.68/1.39 {v, w} 2.68/1.39 2.68/1.39 The recursion depth is 1. 2.68/1.39 2.68/1.39 For your convenience, here are the satisfied ordering constraints: 2.68/1.39 2.68/1.39 a(; c(; d(; x))) > c(; x) 2.68/1.39 2.68/1.39 u(; b(; d(; d(; x)))) > b(; x) 2.68/1.39 2.68/1.39 v(a(; a(; x));) > u(; v(x;)) 2.68/1.39 2.68/1.39 v(a(; c(; x));) > u(; b(; d(; x))) 2.68/1.39 2.68/1.39 v(c(; x);) > b(; x) 2.68/1.39 2.68/1.39 w(a(; a(; x));) > u(; w(x;)) 2.68/1.39 2.68/1.39 w(a(; c(; x));) > u(; b(; d(; x))) 2.68/1.39 2.68/1.39 w(c(; x);) > b(; x) 2.68/1.39 2.68/1.39 2.68/1.39 Hurray, we answered YES(?,O(n^1)) 2.68/1.39 EOF