 Solution

An Oberon recursive procedure can implement the defining recurrence relation directly. Its precondition is $n\ge 1$; arithmetic is assumed to remain in the representable integer range.

PROCEDURE Fib(n: INTEGER): INTEGER;
  VAR result: INTEGER;
BEGIN
  IF n <= 2 THEN
    result := 1
  ELSE
    result := Fib(n-1) + Fib(n-2)
  END;
  RETURN result
END Fib;

Correctness follows by strong induction: the two base inputs give $1$, and for $n>2$ the returned sum is $F_{n-1}+F_{n-2}=F_n$. On each recursive branch the positive integer argument strictly decreases, while recursion stops at $1$ or $2$. The well-ordering principle therefore proves algorithm termination.The method repeats many subproblems and has exponential time complexity; termination alone does not make it efficient.