let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: ( Fusc_Program c= F implies for N being Element of NAT st N > 0 holds
for s being 0 -started State-consisting of 0 ,((<*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 ) ) )
assume Z: Fusc_Program c= F ; :: thesis: for N being Element of NAT st N > 0 holds
for s being 0 -started State-consisting of 0 ,((<*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 ) )
let N be Element of NAT ; :: thesis: ( N > 0 implies for s being 0 -started State-consisting of 0 ,((<*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 ) ) )
Fusc N = (1 * (Fusc N)) + (0 * (Fusc (N + 1))) ;
hence ( N > 0 implies for s being 0 -started State-consisting of 0 ,((<*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 ) ) ) by Z, Th5; :: thesis: verum