YES LCTRS Theories Core, Ints Sorts Unit Signature fastfib: Int -> Unit return: Int -> Unit u: (Int, Int, Int, Int) -> Unit v: (Int, Int, Int, Int) -> Unit Rules v(!x, !i, !p, !q) -> return(!q) [not(<(!i, !x))] v(!x, !i, !p, !q) -> v(!x, +(!i, 1), +(!p, !q), !p) [<(!i, !x)] u(!x, !i, !p, !q) -> v(!x, 1, !p, !q) [and(not(!x = 0), not(!x = 1))] u(!x, !i, !p, !q) -> return(1) [and(not(!x = 0), !x = 1)] u(!x, !i, !p, !q) -> return(0) [!x = 0] fastfib(!x) -> u(!x, !rnd, 1, 0) * DPGraph approximation on the DP problem dependency pairs: {v#(!x, !i, !p, !q) -> v#(!x, +(!i, 1), +(!p, !q), !p) [<(!i, !x)] , u#(!x, !i, !p, !q) -> v#(!x, 1, !p, !q) [and(not(=(!x, 0)), not(=(!x, 1)))] , fastfib#(!x) -> u#(!x, !rnd, 1, 0)} rules: {v(!x, !i, !p, !q) -> return(!q) [not(<(!i, !x))] , v(!x, !i, !p, !q) -> v(!x, +(!i, 1), +(!p, !q), !p) [<(!i, !x)] , u(!x, !i, !p, !q) -> v(!x, 1, !p, !q) [and(not(=(!x, 0)), not(=(!x, 1)))] , u(!x, !i, !p, !q) -> return(1) [and(not(=(!x, 0)), =(!x, 1))] , u(!x, !i, !p, !q) -> return(0) [=(!x, 0)] , fastfib(!x) -> u(!x, !rnd, 1, 0)} resulting in the DP graph DPGraph with indexed dependency pairs {1: v#(!x, !i, !p, !q) -> v#(!x, +(!i, 1), +(!p, !q), !p) [<(!i, !x)] , 2: u#(!x, !i, !p, !q) -> v#(!x, 1, !p, !q) [and(not(=(!x, 0)), not(=(!x, 1)))] , 3: fastfib#(!x) -> u#(!x, !rnd, 1, 0)} and edges 1 -> {1} 2 -> {1} 3 -> {2} with 1 SCC(s) SCC: {v#(!x, !i, !p, !q) -> v#(!x, +(!i, 1), +(!p, !q), !p) [<(!i, !x)]} * Value criterion after 1 iteration(s) with the linear poly projections: Iteration 1: projection(s): v(v#(x1, x2, x3, x4)) = x1 + -1 * x2 removing the rule(s): {v#(!x, !i, !p, !q) -> v#(!x, +(!i, 1), +(!p, !q), !p) [<(!i, !x)]} Elapsed Time: 53.05 ms