set c2 = dl. 0 ;
set n = dl. 1;
set a = dl. 2;
set b = dl. 3;
set aux = dl. 4;
set L6 = 6;
set L7 = 7;
set L8 = 8;
set L0 = 0 ;
set L1 = 1;
set L2 = 2;
set L3 = 3;
set L4 = 4;
set L5 = 5;
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 (ProgramPart s),s) . (dl. 3) = Fusc N & LifeSpan (ProgramPart s),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 (ProgramPart s),s) . (dl. 3) = Fusc N & LifeSpan (ProgramPart s),s = (6 * ([\(log 2,N)/] + 1)) + 1 )
set k = [\(log 2,N)/];
(log 2,N) - 1 < [\(log 2,N)/] by INT_1:def 4;
then A2: log 2,N < [\(log 2,N)/] + 1 by XREAL_1:21;
N >= 0 + 1 by A1, NAT_1:13;
then log 2,N >= log 2,1 by PRE_FF:12;
then log 2,N >= 0 by POWER:59;
then [\(log 2,N)/] + 1 > 0 by A2, XXREAL_0:2;
then reconsider k = [\(log 2,N)/] as Element of NAT by INT_1:16, INT_1:20;
2 to_power (k + 1) > 2 to_power (log 2,N) by A2, POWER:44;
then 2 to_power (k + 1) > N by A1, POWER:def 3;
then A3: 2 |^ (k + 1) > N by POWER:46;
let S be State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*N*>) ^ <*1*>) ^ <*0 *>; :: thesis: ( ProgramPart S halts_on S & (Result (ProgramPart S),S) . (dl. 3) = Fusc N & LifeSpan (ProgramPart S),S = (6 * ([\(log 2,N)/] + 1)) + 1 )
consider s being State of SCM such that
A4: s = S ;
defpred S₁[ Element of NAT ] means ( $1 <= (log 2,N) + 1 implies for u being State of SCM st u = Comput (ProgramPart s),s,(6 * $1) holds
( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ $1) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) ) );
A5: s . 0 = (dl. 1) =0_goto 8 by A4, SCM_1:14;
A6: s . 7 = SCM-goto 0 by A4, SCM_1:14;
A7: s . 1 = (dl. 4) := (dl. 0 ) by A4, SCM_1:14;
A8: s . 4 = AddTo (dl. 3),(dl. 2) by A4, SCM_1:14;
A9: s . 2 = Divide (dl. 1),(dl. 4) by A4, SCM_1:14;
A10: s . 6 = AddTo (dl. 2),(dl. 3) by A4, SCM_1:14;
A11: s . 3 = (dl. 4) =0_goto 6 by A4, SCM_1:14;
A12: s . 5 = SCM-goto 0 by A4, SCM_1:14;
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: ( k <= (log 2,N) + 1 implies for u being State of SCM st u = Comput (ProgramPart s),s,(6 * k) holds
( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ k) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) ) ) ; :: thesis: S₁[k + 1]
set t = 6 * k;
set t0 = Comput (ProgramPart s),s,(6 * k);
assume A15: k + 1 <= (log 2,N) + 1 ; :: thesis: for u being State of SCM st u = Comput (ProgramPart s),s,(6 * (k + 1)) holds
( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
then k <= log 2,N by XREAL_1:8;
then 2 to_power k <= 2 to_power (log 2,N) by PRE_FF:10;
then 2 to_power k <= N by A1, POWER:def 3;
then A16: 2 |^ k <= N by POWER:46;
A17: k <= k + 1 by NAT_1:11;
then A18: (Comput (ProgramPart s),s,(6 * k)) . (dl. 1) is Element of NAT by A14, A15, XXREAL_0:2;
A19: (Comput (ProgramPart s),s,(6 * k)) . (dl. 1) = N div (2 |^ k) by A14, A15, A17, XXREAL_0:2;
A20: IC (Comput (ProgramPart s),s,(6 * k)) = 0 by A14, A15, A17, XXREAL_0:2;
set t3 = Comput (ProgramPart s),s,((6 * k) + 3);
set t2 = Comput (ProgramPart s),s,((6 * k) + 2);
set t1 = Comput (ProgramPart s),s,((6 * k) + 1);
A21: ((6 * k) + 1) + 1 = (6 * k) + 2 ;
2 |^ k > 0 by NEWTON:102;
then (Comput (ProgramPart s),s,(6 * k)) . (dl. 1) <> 0 by A19, A16, PRE_FF:3;
then A22: IC (Comput (ProgramPart s),s,((6 * k) + 1)) = 0 + 1 by A5, A20, SCM_1:24;
then A23: IC (Comput (ProgramPart s),s,((6 * k) + 2)) = 1 + 1 by A7, A21, SCM_1:18;
A24: ((6 * k) + 2) + 1 = (6 * k) + 3 ;
then A25: IC (Comput (ProgramPart s),s,((6 * k) + 3)) = 2 + 1 by A9, A23, Lm14, SCM_1:22;
(Comput (ProgramPart s),s,((6 * k) + 1)) . (dl. 1) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 1) by A5, A20, SCM_1:24;
then A26: (Comput (ProgramPart s),s,((6 * k) + 2)) . (dl. 1) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 1) by A7, A22, A21, Lm14, SCM_1:18;
A27: ((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) mod 2 = ((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) - ((((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) div 2) * 2) by INT_1:def 8;
let u be State of SCM ; :: thesis: ( u = Comput (ProgramPart s),s,(6 * (k + 1)) implies ( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) ) )
assume A28: u = Comput (ProgramPart s),s,(6 * (k + 1)) ; :: thesis: ( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
(Comput (ProgramPart s),s,(6 * k)) . (dl. 0 ) = 2 by A14, A15, A17, XXREAL_0:2;
then A29: (Comput (ProgramPart s),s,((6 * k) + 1)) . (dl. 0 ) = 2 by A5, A20, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 2)) . (dl. 0 ) = 2 by A7, A22, A21, Lm13, SCM_1:18;
then A30: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 0 ) = 2 by A9, A23, A24, Lm7, Lm13, Lm14, SCM_1:22;
A31: (Comput (ProgramPart s),s,((6 * k) + 2)) . (dl. 4) = 2 by A7, A22, A29, A21, SCM_1:18;
then A32: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) = ((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) div 2 by A9, A23, A26, A24, Lm14, SCM_1:22;
then A33: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) = N div ((2 |^ k) * 2) by A19, PRE_FF:5
.= N div (2 |^ (k + 1)) by NEWTON:11 ;
A34: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 4) = ((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) mod 2 by A9, A23, A31, A26, A24, Lm14, SCM_1:22;
set t6 = Comput (ProgramPart s),s,((6 * k) + 6);
set t5 = Comput (ProgramPart s),s,((6 * k) + 5);
set t4 = Comput (ProgramPart s),s,((6 * k) + 4);
A35: ((6 * k) + 3) + 1 = (6 * k) + 4 ;
(Comput (ProgramPart s),s,((6 * k) + 1)) . (dl. 3) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) by A5, A20, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 2)) . (dl. 3) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) by A7, A22, A21, Lm16, SCM_1:18;
then A36: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 3) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) by A9, A23, A24, Lm11, Lm14, Lm16, SCM_1:22;
A37: ((6 * k) + 5) + 1 = (6 * k) + 6 ;
(Comput (ProgramPart s),s,((6 * k) + 1)) . (dl. 2) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2) by A5, A20, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 2)) . (dl. 2) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2) by A7, A22, A21, Lm15, SCM_1:18;
then A38: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 2) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2) by A9, A23, A24, Lm10, Lm14, Lm15, SCM_1:22;
A39: ((6 * k) + 4) + 1 = (6 * k) + 5 ;

per cases ( (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 4) <> 0 or (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 4) = 0 ) ;

suppose A40: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 4) <> 0 ; :: thesis: ( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )

reconsider ta = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2), tb = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) as Integer ;
A41: (Comput (ProgramPart s),s,((6 * k) + 4)) . (dl. 2) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2) by A11, A25, A38, A35, SCM_1:24;
A42: IC (Comput (ProgramPart s),s,((6 * k) + 4)) = 3 + 1 by A11, A25, A35, A40, SCM_1:24;
then A43: IC (Comput (ProgramPart s),s,((6 * k) + 5)) = 4 + 1 by A8, A39, SCM_1:19;
(Comput (ProgramPart s),s,((6 * k) + 4)) . (dl. 1) = (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) by A11, A25, A35, SCM_1:24;
then A44: (Comput (ProgramPart s),s,((6 * k) + 5)) . (dl. 1) = (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) by A8, A39, A42, Lm11, SCM_1:19;
then A45: (Comput (ProgramPart s),s,((6 * k) + 6)) . (dl. 1) = (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) by A12, A37, A43, SCM_1:23;
then reconsider un = u . (dl. 1), tn = (Comput (ProgramPart s),s,(6 * k)) . (dl. 1) as Element of NAT by A28, A18, A32, PRE_FF:7;
A46: tn = ((((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) div 2) * 2) + (((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) mod 2) by A27
.= (2 * un) + 1 by A28, A32, A34, A40, A45, PRE_FF:6 ;
then A47: tn + 1 = 2 * (un + 1) ;
(Comput (ProgramPart s),s,((6 * k) + 4)) . (dl. 0 ) = 2 by A11, A25, A30, A35, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 5)) . (dl. 0 ) = 2 by A8, A39, A42, Lm9, SCM_1:19;
hence ( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) ) by A12, A28, A33, A37, A43, A44, SCM_1:23; :: thesis: ( u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
thus u . (dl. 1) is Element of NAT by A28, A18, A32, A45, PRE_FF:7; :: thesis: Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1)))
A48: Fusc' (((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) + 1) = Fusc (tn + 1) by Def2
.= Fusc (un + 1) by A47, PRE_FF:17
.= Fusc' ((u . (dl. 1)) + 1) by Def2 ;
(Comput (ProgramPart s),s,((6 * k) + 4)) . (dl. 3) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) by A11, A25, A36, A35, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 5)) . (dl. 3) = ((Comput (ProgramPart s),s,(6 * k)) . (dl. 3)) + ((Comput (ProgramPart s),s,(6 * k)) . (dl. 2)) by A8, A39, A42, A41, SCM_1:19;
then A49: (Comput (ProgramPart s),s,((6 * k) + 6)) . (dl. 3) = ((Comput (ProgramPart s),s,(6 * k)) . (dl. 3)) + ((Comput (ProgramPart s),s,(6 * k)) . (dl. 2)) by A12, A37, A43, SCM_1:23;
A50: Fusc' ((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) = Fusc tn by Def2
.= (Fusc un) + (Fusc (un + 1)) by A46, PRE_FF:17
.= (Fusc' (u . (dl. 1))) + (Fusc (un + 1)) by Def2
.= (Fusc' (u . (dl. 1))) + (Fusc' ((u . (dl. 1)) + 1)) by Def2 ;
reconsider un = u . (dl. 1), tn = (Comput (ProgramPart s),s,(6 * k)) . (dl. 1) as Integer ;
(Comput (ProgramPart s),s,((6 * k) + 5)) . (dl. 2) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2) by A8, A39, A42, A41, Lm12, SCM_1:19;
then (Comput (ProgramPart s),s,((6 * k) + 6)) . (dl. 2) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2) by A12, A37, A43, SCM_1:23;
then (ta * (Fusc' tn)) + (tb * (Fusc' (tn + 1))) = ((u . (dl. 2)) * (Fusc' un)) + ((u . (dl. 3)) * (Fusc' (un + 1))) by A28, A49, A50, A48;
hence Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) by A14, A15, A17, XXREAL_0:2; :: thesis: verum

end;

suppose A51: (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 4) = 0 ; :: thesis: ( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )

then A52: IC (Comput (ProgramPart s),s,((6 * k) + 4)) = 6 by A11, A25, A35, SCM_1:24;
then A53: IC (Comput (ProgramPart s),s,((6 * k) + 5)) = 6 + 1 by A10, A39, SCM_1:19;
(Comput (ProgramPart s),s,((6 * k) + 4)) . (dl. 1) = (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) by A11, A25, A35, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 5)) . (dl. 1) = (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) by A10, A39, A52, Lm10, SCM_1:19;
then A54: (Comput (ProgramPart s),s,((6 * k) + 6)) . (dl. 1) = (Comput (ProgramPart s),s,((6 * k) + 3)) . (dl. 1) by A6, A37, A53, SCM_1:23;
then reconsider un = u . (dl. 1), tn = (Comput (ProgramPart s),s,(6 * k)) . (dl. 1) as Element of NAT by A28, A18, A32, PRE_FF:7;
A55: Fusc' (((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) + 1) = Fusc (tn + 1) by Def2
.= (Fusc un) + (Fusc (un + 1)) by A28, A32, A34, A27, A51, A54, PRE_FF:17
.= (Fusc un) + (Fusc' ((u . (dl. 1)) + 1)) by Def2
.= (Fusc' (u . (dl. 1))) + (Fusc' ((u . (dl. 1)) + 1)) by Def2 ;
A56: (Comput (ProgramPart s),s,((6 * k) + 4)) . (dl. 3) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) by A11, A25, A36, A35, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 5)) . (dl. 3) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) by A10, A39, A52, Lm12, SCM_1:19;
then A57: (Comput (ProgramPart s),s,((6 * k) + 6)) . (dl. 3) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) by A6, A37, A53, SCM_1:23;
(Comput (ProgramPart s),s,((6 * k) + 4)) . (dl. 0 ) = 2 by A11, A25, A30, A35, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 5)) . (dl. 0 ) = 2 by A10, A39, A52, Lm8, SCM_1:19;
hence ( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ (k + 1)) & u . (dl. 1) is Element of NAT ) by A6, A28, A18, A32, A33, A37, A53, A54, PRE_FF:7, SCM_1:23; :: thesis: Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1)))
A58: Fusc' ((Comput (ProgramPart s),s,(6 * k)) . (dl. 1)) = Fusc tn by Def2
.= Fusc un by A28, A32, A34, A27, A51, A54, PRE_FF:17
.= Fusc' (u . (dl. 1)) by Def2 ;
(Comput (ProgramPart s),s,((6 * k) + 4)) . (dl. 2) = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2) by A11, A25, A38, A35, SCM_1:24;
then (Comput (ProgramPart s),s,((6 * k) + 5)) . (dl. 2) = ((Comput (ProgramPart s),s,(6 * k)) . (dl. 2)) + ((Comput (ProgramPart s),s,(6 * k)) . (dl. 3)) by A10, A39, A52, A56, SCM_1:19;
then A59: (Comput (ProgramPart s),s,((6 * k) + 6)) . (dl. 2) = ((Comput (ProgramPart s),s,(6 * k)) . (dl. 2)) + ((Comput (ProgramPart s),s,(6 * k)) . (dl. 3)) by A6, A37, A53, SCM_1:23;
reconsider un = u . (dl. 1), tn = (Comput (ProgramPart s),s,(6 * k)) . (dl. 1), ta = (Comput (ProgramPart s),s,(6 * k)) . (dl. 2), tb = (Comput (ProgramPart s),s,(6 * k)) . (dl. 3) as Integer ;
(ta * (Fusc' tn)) + (tb * (Fusc' (tn + 1))) = ((ta + tb) * (Fusc' un)) + (tb * (Fusc' (un + 1))) by A58, A55;
hence Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) by A14, A15, A28, A17, A59, A57, XXREAL_0:2; :: thesis: verum

end;

end;

end;

set h = Comput (ProgramPart s),s,((6 * (k + 1)) + 1);
set u = Comput (ProgramPart s),s,(6 * (k + 1));
A60: s . (dl. 1) = N by A4, SCM_1:14;
A61: ( s . (dl. 2) = 1 & s . (dl. 3) = 0 ) by A4, SCM_1:14;
A62: S₁[ 0 ]

proof

assume 0 <= (log 2,N) + 1 ; :: thesis: for u being State of SCM st u = Comput (ProgramPart s),s,(6 * 0 ) holds
( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ 0 ) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
let u be State of SCM ; :: thesis: ( u = Comput (ProgramPart s),s,(6 * 0 ) implies ( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ 0 ) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) ) )
assume u = Comput (ProgramPart s),s,(6 * 0 ) ; :: thesis: ( IC u = 0 & u . (dl. 0 ) = 2 & u . (dl. 1) = N div (2 |^ 0 ) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
then A63: u = s by AMI_1:13;
hence ( IC u = 0 & u . (dl. 0 ) = 2 ) by A4, SCM_1:14; :: thesis: ( u . (dl. 1) = N div (2 |^ 0 ) & u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
thus u . (dl. 1) = N div 1 by A60, A63, PRE_FF:2
.= N div (2 |^ 0 ) by NEWTON:9 ; :: thesis: ( u . (dl. 1) is Element of NAT & Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) )
thus u . (dl. 1) is Element of NAT by A4, A63, SCM_1:14; :: thesis: Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1)))
thus Fusc N = ((u . (dl. 2)) * (Fusc' (u . (dl. 1)))) + ((u . (dl. 3)) * (Fusc' ((u . (dl. 1)) + 1))) by A60, A61, A63, Def2; :: thesis: verum

end;

A64: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A62, A13);
[\(log 2,N)/] <= log 2,N by INT_1:def 4;
then A65: k + 1 <= (log 2,N) + 1 by XREAL_1:8;
then A66: Fusc N = (((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 2)) * (Fusc' ((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 1)))) + (((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 3)) * (Fusc' (((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 1)) + 1))) by A64;
A67: IC (Comput (ProgramPart s),s,(6 * (k + 1))) = 0 by A64, A65;
then A68: (Comput (ProgramPart s),s,((6 * (k + 1)) + 1)) . (dl. 3) = (Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 3) by A5, SCM_1:24;
(Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 1) = N div (2 |^ (k + 1)) by A64, A65;
then A69: (Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 1) = 0 by A3, NAT_1:2, PRE_FF:4;
then A70: IC (Comput (ProgramPart s),s,((6 * (k + 1)) + 1)) = 8 by A5, A67, SCM_1:24;
A71: s . (IC (Comput (ProgramPart s),s,(6 * (k + 1)))) <> halt SCM by A5, A67, SCM_1:26;
A72: s . 8 = halt SCM by A4, SCM_1:14;
hence ProgramPart S halts_on S by A4, A70, SCM_1:3; :: thesis: ( (Result (ProgramPart S),S) . (dl. 3) = Fusc N & LifeSpan (ProgramPart S),S = (6 * ([\(log 2,N)/] + 1)) + 1 )
(((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 2)) * (Fusc' ((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 1)))) + (((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 3)) * (Fusc' (((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 1)) + 1))) = (((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 2)) * 0 ) + (((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 3)) * (Fusc' (((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 1)) + 1))) by A69, Def2, PRE_FF:17
.= ((Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 3)) * (Fusc (0 + 1)) by A69, Def2
.= (Comput (ProgramPart s),s,(6 * (k + 1))) . (dl. 3) by PRE_FF:17 ;
hence (Result (ProgramPart S),S) . (dl. 3) = Fusc N by A4, A72, A66, A70, A68, SCM_1:4; :: thesis: LifeSpan (ProgramPart S),S = (6 * ([\(log 2,N)/] + 1)) + 1
s . (IC (Comput (ProgramPart s),s,((6 * (k + 1)) + 1))) = halt SCM by A4, A70, SCM_1:14;
hence LifeSpan (ProgramPart S),S = (6 * ([\(log 2,N)/] + 1)) + 1 by A4, A71, SCM_1:17; :: thesis: verum