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, !now, !next, !i, !tmp) -> return(!next) [not(<=(!i, !n))] v(!n, !now, !next, !i, !tmp) -> v(!n, !next, +(!next, !now), +(!i, 1), !now) [<=(!i, !n)] u(!n, !now, !next, !i, !tmp) -> v(!n, 1, 1, 3, !tmp) [and(not(<=(!n, 0)), not(!n = 1))] u(!n, !now, !next, !i, !tmp) -> return(1) [and(not(<=(!n, 0)), !n = 1)] u(!n, !now, !next, !i, !tmp) -> return(0) [<=(!n, 0)] fastfib(!n) -> u(!n, !rnd1, !rnd2, !rnd3, !rnd4) No termination info given. Elapsed Time: 54.60 ms