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