theorem :: FIB_FUSC:3

for F being NAT -defined the InstructionsF of SCM -valued total Function st Fib_Program c= F holds
for N, k, Fk, Fk1 being Nat
for s being 3 -started State-consisting of <%1,N,Fk,Fk1%> st N > 0 & Fk = Fib k & Fk1 = Fib (k + 1) holds
( F halts_on s & LifeSpan (F,s) = (6 * N) - 4 & ex m being Element of NAT st
( m = (k + N) - 1 & (Result (F,s)) . (dl. 2) = Fib m & (Result (F,s)) . (dl. 3) = Fib (m + 1) ) )