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