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