YES(?,O(1)) 0.00/0.23 YES(?,O(1)) 0.00/0.23 0.00/0.23 We are left with following problem, upon which TcT provides the 0.00/0.23 certificate YES(?,O(1)). 0.00/0.23 0.00/0.23 Strict Trs: 0.00/0.23 { b(x, y) -> c(a(c(y), a(0(), x))) 0.00/0.23 , a(y, x) -> y 0.00/0.23 , a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()) } 0.00/0.23 Obligation: 0.00/0.23 innermost runtime complexity 0.00/0.23 Answer: 0.00/0.23 YES(?,O(1)) 0.00/0.23 0.00/0.23 Arguments of following rules are not normal-forms: 0.00/0.23 0.00/0.23 { a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()) } 0.00/0.23 0.00/0.23 All above mentioned rules can be savely removed. 0.00/0.23 0.00/0.23 We are left with following problem, upon which TcT provides the 0.00/0.23 certificate YES(?,O(1)). 0.00/0.23 0.00/0.23 Strict Trs: 0.00/0.23 { b(x, y) -> c(a(c(y), a(0(), x))) 0.00/0.23 , a(y, x) -> y } 0.00/0.23 Obligation: 0.00/0.23 innermost runtime complexity 0.00/0.23 Answer: 0.00/0.23 YES(?,O(1)) 0.00/0.23 0.00/0.23 The input was oriented with the instance of 'Small Polynomial Path 0.00/0.23 Order (PS,0-bounded)' as induced by the safe mapping 0.00/0.23 0.00/0.23 safe(b) = {1}, safe(c) = {1}, safe(a) = {1, 2}, safe(0) = {} 0.00/0.23 0.00/0.23 and precedence 0.00/0.23 0.00/0.23 b > a . 0.00/0.23 0.00/0.23 Following symbols are considered recursive: 0.00/0.23 0.00/0.23 {} 0.00/0.23 0.00/0.23 The recursion depth is 0. 0.00/0.23 0.00/0.23 For your convenience, here are the satisfied ordering constraints: 0.00/0.24 0.00/0.24 b(y; x) > c(; a(; c(; y), a(; 0(), x))) 0.00/0.24 0.00/0.24 a(; y, x) > y 0.00/0.24 0.00/0.24 0.00/0.24 Hurray, we answered YES(?,O(1)) 0.00/0.24 EOF