defpred S₁[ Nat] means for N, A, B being Element of NAT
for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*$1*>) ^ <*A*>) ^ <*B*> st N > 0 & Fusc N = (A * (Fusc $1)) + (B * (Fusc ($1 + 1))) holds
( s is halting & (Result s) . (dl. 3) = Fusc N & ( $1 = 0 implies LifeSpan s = 1 ) & ( $1 > 0 implies LifeSpan s = (6 * ([\(log 2,$1)/] + 1)) + 1 ) );
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let nn be Nat; :: thesis: ( ( for n being Nat st n < nn holds
S₁[n] ) implies S₁[nn] )
assume A2: for n' being Nat st n' < nn holds
for N, A, B being Element of NAT
for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*n'*>) ^ <*A*>) ^ <*B*> st N > 0 & Fusc N = (A * (Fusc n')) + (B * (Fusc (n' + 1))) holds
( s is halting & (Result s) . (dl. 3) = Fusc N & ( n' = 0 implies LifeSpan s = 1 ) & ( n' > 0 implies LifeSpan s = (6 * ([\(log 2,n')/] + 1)) + 1 ) ) ; :: thesis: S₁[nn]
let N, A, B be Element of NAT ; :: thesis: for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*nn*>) ^ <*A*>) ^ <*B*> st N > 0 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) holds
( s is halting & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
let s be State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*nn*>) ^ <*A*>) ^ <*B*>; :: thesis: ( N > 0 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) implies ( s is halting & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) ) )
assume A3: ( N > 0 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) ) ; :: thesis: ( s is halting & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
set c2 = dl. 0 ;
set n = dl. 1;
set a = dl. 2;
set b = dl. 3;
set aux = dl. 4;
reconsider n2 = nn as Element of NAT by ORDINAL1:def 13;
A4: IC s = il. 0 by SCM_1:14;
A5: s . (il. 0 ) = (dl. 1) =0_goto (il. 8) by SCM_1:14;
A6: s . (il. 1) = (dl. 4) := (dl. 0 ) by SCM_1:14;
A7: s . (il. 2) = Divide (dl. 1),(dl. 4) by SCM_1:14;
A8: s . (il. 3) = (dl. 4) =0_goto (il. 6) by SCM_1:14;
A9: s . (il. 4) = AddTo (dl. 3),(dl. 2) by SCM_1:14;
A10: s . (il. 5) = goto (il. 0 ) by SCM_1:14;
A11: s . (il. 6) = AddTo (dl. 2),(dl. 3) by SCM_1:14;
A12: s . (il. 7) = goto (il. 0 ) by SCM_1:14;
A13: s . (il. 8) = halt SCM by SCM_1:14;
A14: ( s . (dl. 0 ) = 2 & s . (dl. 1) = nn & s . (dl. 2) = A & s . (dl. 3) = B ) by SCM_1:14;
set s0 = Computation s,0 ;
A15: s = Computation s,0 by AMI_1:13;
set s1 = Computation s,(0 + 1);
A16: ( (Computation s,(0 + 1)) . (dl. 0 ) = 2 & (Computation s,(0 + 1)) . (dl. 1) = nn & (Computation s,(0 + 1)) . (dl. 2) = A & (Computation s,(0 + 1)) . (dl. 3) = B ) by A4, A5, A14, A15, SCM_1:24;
A17: nn >= 0 by NAT_1:2;

A18: now

assume A19: nn = 0 ; :: thesis: ( s is halting & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
then A20: s . (IC (Computation s,(0 + 1))) = halt SCM by A4, A5, A13, A14, A15, SCM_1:24;
hence s is halting by SCM_1:3; :: thesis: ( (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
thus (Result s) . (dl. 3) = (Computation s,(0 + 1)) . (dl. 3) by A20, SCM_1:4
.= Fusc N by A3, A16, A19, PRE_FF:20 ; :: thesis: ( ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )

hereby :: thesis: ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 )

assume nn = 0 ; :: thesis: LifeSpan s = 1
halt SCM <> (dl. 1) =0_goto (il. 8) by SCM_1:26;
hence LifeSpan s = 1 by A4, A5, A15, A20, SCM_1:17; :: thesis: verum

end;

thus ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) by A19; :: thesis: verum

end;

now

assume A21: nn > 0 ; :: thesis: ( s is halting & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
then A22: IC (Computation s,(0 + 1)) = il. (0 + 1) by A4, A5, A14, A15, SCM_1:24;
set s2 = Computation s,(1 + 1);
A23: IC (Computation s,(1 + 1)) = il. (1 + 1) by A6, A22, SCM_1:18;
A24: (Computation s,(1 + 1)) . (dl. 4) = 2 by A6, A16, A22, SCM_1:18;
A25: ( (Computation s,(1 + 1)) . (dl. 0 ) = 2 & (Computation s,(1 + 1)) . (dl. 1) = nn & (Computation s,(1 + 1)) . (dl. 2) = A & (Computation s,(1 + 1)) . (dl. 3) = B ) by A6, A16, A22, Lm8, SCM_1:18;
set s3 = Computation s,(2 + 1);
A26: IC (Computation s,(2 + 1)) = il. (2 + 1) by A7, A23, Lm8, SCM_1:22;
A27: (Computation s,(2 + 1)) . (dl. 1) = n2 div 2 by A7, A23, A24, A25, Lm8, SCM_1:22;
A28: (Computation s,(2 + 1)) . (dl. 4) = nn mod 2 by A7, A23, A24, A25, Lm8, SCM_1:22;
A29: ( (Computation s,(2 + 1)) . (dl. 0 ) = 2 & (Computation s,(2 + 1)) . (dl. 2) = A & (Computation s,(2 + 1)) . (dl. 3) = B ) by A7, A23, A25, Lm7, Lm8, SCM_1:22;
reconsider nn' = (Computation s,(2 + 1)) . (dl. 1) as Element of NAT by A27, PRE_FF:7;
set s4 = Computation s,(3 + 1);
set s5 = Computation s,(4 + 1);
set s6 = Computation s,(5 + 1);
A30: nn mod 2 = nn - ((nn div 2) * 2) by INT_1:def 8;

per cases ( (Computation s,(2 + 1)) . (dl. 4) <> 0 or (Computation s,(2 + 1)) . (dl. 4) = 0 ) ;

suppose A31: (Computation s,(2 + 1)) . (dl. 4) <> 0 ; :: thesis: ( s is halting & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )

then A32: (Computation s,(2 + 1)) . (dl. 4) = 1 by A28, PRE_FF:6;
A33: IC (Computation s,(3 + 1)) = il. (3 + 1) by A8, A26, A31, SCM_1:24;
A34: ( (Computation s,(3 + 1)) . (dl. 0 ) = 2 & (Computation s,(3 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1) & (Computation s,(3 + 1)) . (dl. 2) = A & (Computation s,(3 + 1)) . (dl. 3) = B ) by A8, A26, A29, SCM_1:24;
A35: IC (Computation s,(4 + 1)) = il. (4 + 1) by A9, A33, SCM_1:19;
A36: (Computation s,(4 + 1)) . (dl. 3) = B + A by A9, A33, A34, SCM_1:19;
A37: ( (Computation s,(4 + 1)) . (dl. 0 ) = 2 & (Computation s,(4 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1) & (Computation s,(4 + 1)) . (dl. 2) = A ) by A9, A33, A34, Lm7, SCM_1:19;
A38: IC (Computation s,(5 + 1)) = il. 0 by A10, A35, SCM_1:23;
A39: ( (Computation s,(5 + 1)) . (dl. 0 ) = 2 & (Computation s,(5 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1) & (Computation s,(5 + 1)) . (dl. 2) = A & (Computation s,(5 + 1)) . (dl. 3) = (Computation s,(4 + 1)) . (dl. 3) ) by A10, A35, A37, SCM_1:23;
A40: (nn mod 2) + ((nn div 2) * 2) = nn by A30;
( (Computation s,(5 + 1)) . (il. 0 ) = (dl. 1) =0_goto (il. 8) & (Computation s,(5 + 1)) . (il. 1) = (dl. 4) := (dl. 0 ) & (Computation s,(5 + 1)) . (il. 2) = Divide (dl. 1),(dl. 4) & (Computation s,(5 + 1)) . (il. 3) = (dl. 4) =0_goto (il. 6) & (Computation s,(5 + 1)) . (il. 4) = AddTo (dl. 3),(dl. 2) & (Computation s,(5 + 1)) . (il. 5) = goto (il. 0 ) & (Computation s,(5 + 1)) . (il. 6) = AddTo (dl. 2),(dl. 3) & (Computation s,(5 + 1)) . (il. 7) = goto (il. 0 ) & (Computation s,(5 + 1)) . (il. 8) = halt SCM ) by A5, A6, A7, A8, A9, A10, A11, A12, A13, AMI_1:54;
then A41: Computation s,(5 + 1) is State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*nn'*>) ^ <*A*>) ^ <*(B + A)*> by A36, A38, A39, SCM_1:30;
A42: nn' < nn by A27, A28, A32, A40, PRE_FF:19;
Fusc N = (A * (Fusc nn')) + ((B + A) * (Fusc (nn' + 1))) by A3, A27, A28, A32, A40, PRE_FF:21;
then A43: ( Computation s,(5 + 1) is halting & (Result (Computation s,(5 + 1))) . (dl. 3) = Fusc N & ( nn' = 0 implies LifeSpan (Computation s,(5 + 1)) = 1 ) & ( nn' > 0 implies LifeSpan (Computation s,(5 + 1)) = (6 * ([\(log 2,nn')/] + 1)) + 1 ) ) by A2, A3, A41, A42;
hence s is halting by AMI_1:93; :: thesis: ( (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
thus (Result s) . (dl. 3) = Fusc N by A43, SCM_1:29; :: thesis: ( ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
thus ( nn = 0 implies LifeSpan s = 1 ) by A21; :: thesis: ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 )
thus ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) :: thesis: verum

proof

assume nn > 0 ; :: thesis: LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1

per cases ( nn' = 0 or nn' <> 0 ) ;

suppose nn' = 0 ; :: thesis: LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1

hence LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 by A27, A28, A30, A32, A43, Lm1, SCM_1:28; :: thesis: verum

end;

suppose A44: nn' <> 0 ; :: thesis: LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1

then A45: nn' > 0 by NAT_1:3;
then reconsider F = [\(log 2,nn')/] as Element of NAT by Lm2;
(6 * (F + 1)) + 1 > 0 by A45, Lm2;
hence LifeSpan s = 6 + ((6 * (F + 1)) + 1) by A43, A44, NAT_1:3, SCM_1:28
.= (6 * ([\(log 2,nn)/] + 1)) + 1 by A27, A28, A32, A40, A45, Lm3 ;
:: thesis: verum

end;

end;

end;

end;

suppose A46: (Computation s,(2 + 1)) . (dl. 4) = 0 ; :: thesis: ( s is halting & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )

then A47: IC (Computation s,(3 + 1)) = il. 6 by A8, A26, SCM_1:24;
A48: ( (Computation s,(3 + 1)) . (dl. 0 ) = 2 & (Computation s,(3 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1) & (Computation s,(3 + 1)) . (dl. 2) = A & (Computation s,(3 + 1)) . (dl. 3) = B ) by A8, A26, A29, SCM_1:24;
A49: IC (Computation s,(4 + 1)) = il. (6 + 1) by A11, A47, SCM_1:19;
A50: (Computation s,(4 + 1)) . (dl. 2) = A + B by A11, A47, A48, SCM_1:19;
A51: ( (Computation s,(4 + 1)) . (dl. 0 ) = 2 & (Computation s,(4 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1) & (Computation s,(4 + 1)) . (dl. 3) = B ) by A11, A47, A48, Lm7, SCM_1:19;
A52: IC (Computation s,(5 + 1)) = il. 0 by A12, A49, SCM_1:23;
A53: ( (Computation s,(5 + 1)) . (dl. 0 ) = 2 & (Computation s,(5 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1) & (Computation s,(5 + 1)) . (dl. 2) = (Computation s,(4 + 1)) . (dl. 2) & (Computation s,(5 + 1)) . (dl. 3) = B ) by A12, A49, A51, SCM_1:23;
reconsider nn' = (Computation s,(2 + 1)) . (dl. 1) as Element of NAT by A27, PRE_FF:7;
( (Computation s,(5 + 1)) . (il. 0 ) = (dl. 1) =0_goto (il. 8) & (Computation s,(5 + 1)) . (il. 1) = (dl. 4) := (dl. 0 ) & (Computation s,(5 + 1)) . (il. 2) = Divide (dl. 1),(dl. 4) & (Computation s,(5 + 1)) . (il. 3) = (dl. 4) =0_goto (il. 6) & (Computation s,(5 + 1)) . (il. 4) = AddTo (dl. 3),(dl. 2) & (Computation s,(5 + 1)) . (il. 5) = goto (il. 0 ) & (Computation s,(5 + 1)) . (il. 6) = AddTo (dl. 2),(dl. 3) & (Computation s,(5 + 1)) . (il. 7) = goto (il. 0 ) & (Computation s,(5 + 1)) . (il. 8) = halt SCM ) by A5, A6, A7, A8, A9, A10, A11, A12, A13, AMI_1:54;
then A54: Computation s,(5 + 1) is State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*nn'*>) ^ <*(A + B)*>) ^ <*B*> by A50, A52, A53, SCM_1:30;
A55: nn' < nn by A21, A27, A28, A30, A46, PRE_FF:18;
Fusc N = ((A + B) * (Fusc nn')) + (B * (Fusc (nn' + 1))) by A3, A27, A28, A30, A46, PRE_FF:22;
then A56: ( Computation s,(5 + 1) is halting & (Result (Computation s,(5 + 1))) . (dl. 3) = Fusc N & ( nn' = 0 implies LifeSpan (Computation s,(5 + 1)) = 1 ) & ( nn' > 0 implies LifeSpan (Computation s,(5 + 1)) = (6 * ([\(log 2,nn')/] + 1)) + 1 ) ) by A2, A3, A54, A55;
hence s is halting by AMI_1:93; :: thesis: ( (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
thus (Result s) . (dl. 3) = Fusc N by A56, SCM_1:29; :: thesis: ( ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
thus ( nn = 0 implies LifeSpan s = 1 ) by A21; :: thesis: ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 )
thus ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) :: thesis: verum

proof

assume nn > 0 ; :: thesis: LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1

per cases ( nn' = 0 or nn' <> 0 ) ;

suppose nn' = 0 ; :: thesis: LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1

hence LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 by A7, A21, A23, A24, A25, A27, A30, A46, Lm8, SCM_1:22; :: thesis: verum

end;

suppose A57: nn' <> 0 ; :: thesis: LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1

then A58: nn' > 0 by NAT_1:3;
then reconsider F = [\(log 2,nn')/] as Element of NAT by Lm2;
(6 * (F + 1)) + 1 > 0 by A58, Lm2;
hence LifeSpan s = 6 + ((6 * (F + 1)) + 1) by A56, A57, NAT_1:3, SCM_1:28
.= (6 * ([\(log 2,nn)/] + 1)) + 1 by A27, A28, A30, A46, A58, Lm5 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

hence ( s is halting & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) ) by A17, A18, XXREAL_0:1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A1);
hence for n, N, A, B being Element of NAT
for s being State-consisting of 0 , 0 , 0 , Fusc_Program ,((<*2*> ^ <*n*>) ^ <*A*>) ^ <*B*> st N > 0 & Fusc N = (A * (Fusc n)) + (B * (Fusc (n + 1))) holds
( s is halting & (Result s) . (dl. 3) = Fusc N & ( n = 0 implies LifeSpan s = 1 ) & ( n > 0 implies LifeSpan s = (6 * ([\(log 2,n)/] + 1)) + 1 ) ) ; :: thesis: verum