theorem :: FIB_FUSC:5

for F being NAT -defined the InstructionsF of SCM -valued total Function st Fusc_Program c= F holds
for N being Element of NAT st N > 0 holds
for s being 0 -started State-consisting of <%2,N,1,0%> holds
( F halts_on s & (Result (F,s)) . (dl. 3) = Fusc N & ( N = 0 implies LifeSpan (F,s) = 1 ) & ( N > 0 implies LifeSpan (F,s) = (6 * ([\(log (2,N))/] + 1)) + 1 ) )