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) }