Prove the following using our axiomatic scheme.
The notation fib(i) is used to represent the ith Fibonacci
number.
{ a = fib(i) AND b = fib(i - 1) }
c := a + b;
{ c = fib(i + 1) AND a = fib(i) }
1. a = fib(i) AND b = fib(i - 1) (mathematical fact)
IMPLIES a + b = fib(i + 1) AND a = fib(i)
2. { a = fib(i) AND b = fib(i - 1) } (Consequence: 1)
{ a + b = fib(i + 1) AND a = fib(i) }
3. { a + b = fib(i + 1) AND a = fib(i) } (Assignment)
c := a + b;
{ c = fib(i + 1) AND a = fib(i) }
4. { a = fib(i) AND b = fib(i - 1) } (Sequence: 2, 3)
c := a + b;
{ c = fib(i + 1) AND a = fib(i) }