YES(?,O(n^1)) 0.00/0.30 YES(?,O(n^1)) 0.00/0.30 0.00/0.30 We are left with following problem, upon which TcT provides the 0.00/0.30 certificate YES(?,O(n^1)). 0.00/0.30 0.00/0.30 Strict Trs: 0.00/0.30 { p(m, n, s(r)) -> p(m, r, n) 0.00/0.30 , p(m, s(n), 0()) -> p(0(), n, m) 0.00/0.30 , p(m, 0(), 0()) -> m } 0.00/0.30 Obligation: 0.00/0.30 innermost runtime complexity 0.00/0.30 Answer: 0.00/0.30 YES(?,O(n^1)) 0.00/0.30 0.00/0.30 The input was oriented with the instance of 'Small Polynomial Path 0.00/0.30 Order (PS)' as induced by the safe mapping 0.00/0.30 0.00/0.30 safe(p) = {}, safe(s) = {1}, safe(0) = {} 0.00/0.30 0.00/0.30 and precedence 0.00/0.30 0.00/0.30 empty . 0.00/0.30 0.00/0.30 Following symbols are considered recursive: 0.00/0.30 0.00/0.30 {p} 0.00/0.30 0.00/0.30 The recursion depth is 1. 0.00/0.30 0.00/0.30 For your convenience, here are the satisfied ordering constraints: 0.00/0.30 0.00/0.30 p(m, n, s(; r);) > p(m, r, n;) 0.00/0.30 0.00/0.30 p(m, s(; n), 0();) > p(0(), n, m;) 0.00/0.30 0.00/0.30 p(m, 0(), 0();) > m 0.00/0.30 0.00/0.30 0.00/0.30 Hurray, we answered YES(?,O(n^1)) 0.00/0.30 EOF