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