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