-- FIBPROOF



Derivation of

fibL(N) = fib(N)

Creating a Hoare invariant for the iterative program

fibL(n) = loopF(n,0,1)

applied at position [0] of the preceding formula leads to the formula

INV(N,N,0,1)
& (loopF(z1,z2,z3) = z0
       & INV(N,z1,z2,z3)
   ==> z0 = fib(N))

The tree has been decomposed. The current formula is given by

INV(N,N,0,1)

Narrowing applied to the preceding formula leads to the factor

0 = fib(0)
& 1 = fib(1)

Narrowing applied to the preceding formula leads to a new one. The current factor is given by

True

Simplification applied to the preceding formula leads to a new one. The current factor is given by

1 = fib(1)

Narrowing applied to the preceding formula leads to the factor

True

Simplification applied to the preceding formula leads to a new one. The current formula is given by

loopF(z1,z2,z3) = z0
    & INV(N,z1,z2,z3)
==> z0 = fib(N)

Fixpoint induction w.r.t.

loopF(0,x0,y0) = x0
& (loopF(suc(n0),x1,y1) = z5
   <=== loopF(n0,y1,x1+y1) = z5)

applied to the preceding formula leads to the formula

All x0 y0 n0 x1 y1 z5:
(All N0:
   (INV(N0,0,x0,y0)
    ==> x0 = fib(N0))
 & (All N1:
         (INV(N1,suc(n0),x1,y1)
          ==> z5 = fib(N1))
    <=== All N2:
         (INV(N2,n0,y1,x1+y1)
          ==> z5 = fib(N2))))

The axiom

INV(n,x,y,z)
<=== n >= x
     & y = fib(n-x)
     & z = fib((n-x)+1)

applied at positions [0,0,0,0],[0,1,0,0,0],[0,1,1,0,0] of the preceding formula leads to the formula

All x0 y0 n0 x1 y1 z5:
(All N0:
   (N0 >= 0
        & x0 = fib(N0-0)
        & y0 = fib((N0-0)+1)
    ==> x0 = fib(N0))
 & (All N1:
         (N1 >= suc(n0)
              & x1 = fib(N1-suc(n0))
              & y1 = fib((N1-suc(n0))+1)
          ==> z5 = fib(N1))
    <=== All N2:
         (N2 >= n0
              & y1 = fib(N2-n0)
              & x1+y1 = fib((N2-n0)+1)
          ==> z5 = fib(N2))))

Simplification applied to the preceding formula leads to the formula

All n0 z5 N1:
(All N2:
       (N2 >= n0
            & fib(suc(N1-suc(n0))) = fib(N2-n0)
            & fib(N1-suc(n0))+fib(suc(N1-suc(n0))) = fib(suc(N2-n0))
        ==> z5 = fib(N2))
     & N1 >= suc(n0)
 ==> z5 = fib(N1))

The theorem

fib(n)+fib(suc(n)) = fib(suc(suc(n)))

applied at position [0,0,0,0,0,2,0] of the preceding formula leads to the formula

All n0 z5 N1:
(All N2:
       (N2 >= n0
            & fib(suc(N1-suc(n0))) = fib(N2-n0)
            & fib(suc(suc(N1-suc(n0)))) = fib(suc(N2-n0))
        ==> z5 = fib(N2))
     & N1 >= suc(n0)
 ==> z5 = fib(N1))

The theorem

suc(x-suc(y)) = x-y
<=== x > y

applied at positions [0,0,0,0,0,2,0,0,0],[0,0,0,0,0,1,0,0] of the preceding formula leads to the formula

All n0 z5 N1:
(All N2:
       (N2 >= n0
            & (fib(N1-n0) = fib(N2-n0)
               & N1 > n0)
            & (fib(suc(N1-n0)) = fib(suc(N2-n0))
               & N1 > n0)
        ==> z5 = fib(N2))
     & N1 >= suc(n0)
 ==> z5 = fib(N1))

Simplification applied to the preceding formula leads to the formula

All n0 z5 N1:
(All N2:
       (N2 >= n0
            & fib(N1-n0) = fib(N2-n0)
            & N1 > n0
            & fib(suc(N1-n0)) = fib(suc(N2-n0))
        ==> z5 = fib(N2))
     & N1 >= suc(n0)
 ==> z5 = fib(N1))

Substituting N1 for N2 applied at position [0,0,0] of the preceding formula leads to the formula

All n0 z5 N1:
((N1 >= n0
            & fib(N1-n0) = fib(N1-n0)
            & N1 > n0
            & fib(suc(N1-n0)) = fib(suc(N1-n0))
        ==> z5 = fib(N1))
     & N1 >= suc(n0)
 ==> z5 = fib(N1))

Simplification applied to the preceding formula leads to the formula

All n0 z5 N1:
((N1 >= n0
            & N1 > n0
        ==> z5 = fib(N1))
     & N1 >= suc(n0)
 ==> z5 = fib(N1))

The theorem

x >= suc(y)
===> x > y

applied at position [0,0,1] of the preceding formula leads to the formula

All n0 z5 N1:
((N1 >= n0
            & N1 > n0
        ==> z5 = fib(N1))
     & N1 > n0
 ==> z5 = fib(N1))

The theorem

x >= y
<=== x > y

applied at position [0,0,0,0,0] of the preceding formula leads to the formula

All n0 z5 N1:
((N1 > n0
            & N1 > n0
        ==> z5 = fib(N1))
     & N1 > n0
 ==> z5 = fib(N1))

Simplification applied to the entire formula leads to True.