let N be Element of NAT ; :: thesis: ( N > 0 implies for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0 *> holds
( ProgramPart s halts_on s & (Result s) . (dl. 3) = Fusc N & ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * ([\(log 2,N)/] + 1)) + 1 ) ) )
assume A1: N > 0 ; :: thesis: for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0 *> holds
( ProgramPart s halts_on s & (Result s) . (dl. 3) = Fusc N & ( N = 0 implies LifeSpan s = 1 ) & ( N > 0 implies LifeSpan s = (6 * ([\(log 2,N)/] + 1)) + 1 ) )
let S be State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0 *>; :: thesis: ( ProgramPart S halts_on S & (Result S) . (dl. 3) = Fusc N & ( N = 0 implies LifeSpan S = 1 ) & ( N > 0 implies LifeSpan S = (6 * ([\(log 2,N)/] + 1)) + 1 ) )
Fusc N = (1 * (Fusc N)) + (0 * (Fusc (N + 1))) ;
hence ( ProgramPart S halts_on S & (Result S) . (dl. 3) = Fusc N & ( N = 0 implies LifeSpan S = 1 ) & ( N > 0 implies LifeSpan S = (6 * ([\(log 2,N)/] + 1)) + 1 ) ) by A1, Th5; :: thesis: verum