MAYBE 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, !a, !b, !c, !d) -> return(!d) [not(<=(!c, !n))] v(!n, !a, !b, !c, !d) -> v(!n, !b, +(!a, !b), +(!c, 1), +(!a, !b)) [<=(!c, !n)] u(!n, !a, !b, !c, !d) -> v(!n, !a, !b, 2, !d) [and(not(<(!n, 0)), not(!n = 1))] u(!n, !a, !b, !c, !d) -> return(1) [and(not(<(!n, 0)), !n = 1)] u(!n, !a, !b, !c, !d) -> return(0) [<(!n, 0)] fastfib(!n) -> u(!n, 0, 1, !rnd3, !rnd4) No termination info given. Elapsed Time: 42.59 ms