fmod FIB is
    protecting INT .
    
    sort Fib .
    
    op _,_ : Int Int -> Fib .
    
    op F : Int Fib -> Fib .
    op next : Fib -> Fib .
    
    vars T M N : Int .
    
    eq F(0,M,N) = (1,1) .
    eq F(T,M,N) = next(F(T - 1,M,N)) [owise] .
    eq next(M,N) = (N,M + N) .
endfm