theorem Th4: :: FIB_FUSC:4

for F being NAT -defined the InstructionsF of SCM -valued total Function st Fusc_Program c= F holds
for n, N, A, B being Element of NAT
for s being 0 -started State-consisting of <%2,n,A,B%> st N > 0 & Fusc N = (A * (Fusc n)) + (B * (Fusc (n + 1))) 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 ) )