defpred S1[ 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
( ProgramPart s halts_on s & (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
S1[n] ) holds
S1[k]
proof
set c2 =
dl. 0 ;
set n =
dl. 1;
set a =
dl. 2;
set b =
dl. 3;
set aux =
dl. 4;
let nn be
Nat;
( ( for n being Nat st n < nn holds
S1[n] ) implies S1[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
(
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 ) )
;
S1[nn]
reconsider n2 =
nn as
Element of
NAT by ORDINAL1:def 13;
let N,
A,
B be
Element of
NAT ;
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
( ProgramPart s halts_on s & (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*>;
( N > 0 & Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1))) implies ( ProgramPart s halts_on s & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) ) )
assume that A3:
N > 0
and A4:
Fusc N = (A * (Fusc nn)) + (B * (Fusc (nn + 1)))
;
( ProgramPart s halts_on s & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
A5:
s . (dl. 1) = nn
by SCM_1:14;
set s0 =
Computation s,
0 ;
A6:
s . (il. 0 ) = (dl. 1) =0_goto (il. 8)
by SCM_1:14;
set s1 =
Computation s,
(0 + 1);
A7:
s . (il. 8) = halt SCM
by SCM_1:14;
A8:
s . (il. 3) = (dl. 4) =0_goto (il. 6)
by SCM_1:14;
A9:
(
IC s = il. 0 &
s = Computation s,
0 )
by AMI_1:13, SCM_1:14;
s . (dl. 2) = A
by SCM_1:14;
then A10:
(Computation s,(0 + 1)) . (dl. 2) = A
by A6, A9, SCM_1:24;
s . (dl. 0 ) = 2
by SCM_1:14;
then A11:
(Computation s,(0 + 1)) . (dl. 0 ) = 2
by A6, A9, SCM_1:24;
A12:
s . (il. 2) = Divide (dl. 1),
(dl. 4)
by SCM_1:14;
s . (dl. 3) = B
by SCM_1:14;
then A13:
(Computation s,(0 + 1)) . (dl. 3) = B
by A6, A9, SCM_1:24;
A14:
now assume A15:
nn = 0
;
( ProgramPart s halts_on s & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )then A16:
s . (IC (Computation s,(0 + 1))) = halt SCM
by A6, A7, A5, A9, SCM_1:24;
hence
ProgramPart s halts_on s
by SCM_1:3;
( (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 A16, SCM_1:4
.=
Fusc N
by A4, A13, A15, PRE_FF:20
;
( ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )thus
(
nn > 0 implies
LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 )
by A15;
verum end;
A17:
s . (il. 1) = (dl. 4) := (dl. 0 )
by SCM_1:14;
A18:
s . (il. 5) = goto (il. 0 )
by SCM_1:14;
A19:
s . (il. 4) = AddTo (dl. 3),
(dl. 2)
by SCM_1:14;
A20:
s . (il. 7) = goto (il. 0 )
by SCM_1:14;
A21:
s . (il. 6) = AddTo (dl. 2),
(dl. 3)
by SCM_1:14;
A22:
(Computation s,(0 + 1)) . (dl. 1) = nn
by A6, A5, A9, SCM_1:24;
A23:
now set s6 =
Computation s,
(5 + 1);
set s5 =
Computation s,
(4 + 1);
set s4 =
Computation s,
(3 + 1);
set s3 =
Computation s,
(2 + 1);
set s2 =
Computation s,
(1 + 1);
A24:
nn mod 2
= nn - ((nn div 2) * 2)
by INT_1:def 8;
assume A25:
nn > 0
;
( ProgramPart s halts_on s & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )then A26:
IC (Computation s,(0 + 1)) = il. (0 + 1)
by A6, A5, A9, SCM_1:24;
then A27:
IC (Computation s,(1 + 1)) = il. (1 + 1)
by A17, SCM_1:18;
then A28:
IC (Computation s,(2 + 1)) = il. (2 + 1)
by A12, Lm14, SCM_1:22;
(Computation s,(1 + 1)) . (dl. 2) = A
by A17, A10, A26, Lm15, SCM_1:18;
then A29:
(Computation s,(2 + 1)) . (dl. 2) = A
by A12, A27, Lm10, Lm14, Lm15, SCM_1:22;
(Computation s,(1 + 1)) . (dl. 0 ) = 2
by A17, A11, A26, Lm13, SCM_1:18;
then A30:
(Computation s,(2 + 1)) . (dl. 0 ) = 2
by A12, A27, Lm7, Lm13, Lm14, SCM_1:22;
(Computation s,(1 + 1)) . (dl. 3) = B
by A17, A13, A26, Lm16, SCM_1:18;
then A31:
(Computation s,(2 + 1)) . (dl. 3) = B
by A12, A27, Lm11, Lm14, Lm16, SCM_1:22;
A32:
(
(Computation s,(1 + 1)) . (dl. 4) = 2 &
(Computation s,(1 + 1)) . (dl. 1) = nn )
by A17, A11, A22, A26, Lm14, SCM_1:18;
then A33:
(Computation s,(2 + 1)) . (dl. 1) = n2 div 2
by A12, A27, Lm14, SCM_1:22;
then reconsider nn' =
(Computation s,(2 + 1)) . (dl. 1) as
Element of
NAT by PRE_FF:7;
A34:
(Computation s,(2 + 1)) . (dl. 4) = nn mod 2
by A12, A27, A32, Lm14, SCM_1:22;
per cases
( (Computation s,(2 + 1)) . (dl. 4) <> 0 or (Computation s,(2 + 1)) . (dl. 4) = 0 )
;
suppose A35:
(Computation s,(2 + 1)) . (dl. 4) <> 0
;
( ProgramPart s halts_on s & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )then A36:
IC (Computation s,(3 + 1)) = il. (3 + 1)
by A8, A28, SCM_1:24;
then A37:
IC (Computation s,(4 + 1)) = il. (4 + 1)
by A19, SCM_1:19;
A38:
(Computation s,(3 + 1)) . (dl. 2) = A
by A8, A28, A29, SCM_1:24;
then
(Computation s,(4 + 1)) . (dl. 2) = A
by A19, A36, Lm12, SCM_1:19;
then A39:
(Computation s,(5 + 1)) . (dl. 2) = A
by A18, A37, SCM_1:23;
(Computation s,(3 + 1)) . (dl. 3) = B
by A8, A28, A31, SCM_1:24;
then A40:
(Computation s,(4 + 1)) . (dl. 3) = B + A
by A19, A36, A38, SCM_1:19;
A41:
(Computation s,(2 + 1)) . (dl. 4) = 1
by A34, A35, PRE_FF:6;
(Computation s,(3 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1)
by A8, A28, SCM_1:24;
then
(Computation s,(4 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1)
by A19, A36, Lm11, SCM_1:19;
then A42:
(Computation s,(5 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1)
by A18, A37, SCM_1:23;
A43:
(
(Computation s,(5 + 1)) . (il. 0 ) = (dl. 1) =0_goto (il. 8) &
(Computation s,(5 + 1)) . (il. 1) = (dl. 4) := (dl. 0 ) )
by A6, A17, AMI_1:54;
A44:
(Computation s,(5 + 1)) . (il. 8) = halt SCM
by A7, AMI_1:54;
(Computation s,(3 + 1)) . (dl. 0 ) = 2
by A8, A28, A30, SCM_1:24;
then
(Computation s,(4 + 1)) . (dl. 0 ) = 2
by A19, A36, Lm9, SCM_1:19;
then A45:
(Computation s,(5 + 1)) . (dl. 0 ) = 2
by A18, A37, SCM_1:23;
A46:
(
(Computation s,(5 + 1)) . (il. 6) = AddTo (dl. 2),
(dl. 3) &
(Computation s,(5 + 1)) . (il. 7) = goto (il. 0 ) )
by A21, A20, AMI_1:54;
A47:
(
(Computation s,(5 + 1)) . (il. 4) = AddTo (dl. 3),
(dl. 2) &
(Computation s,(5 + 1)) . (il. 5) = goto (il. 0 ) )
by A19, A18, AMI_1:54;
A48:
(
(Computation s,(5 + 1)) . (il. 2) = Divide (dl. 1),
(dl. 4) &
(Computation s,(5 + 1)) . (il. 3) = (dl. 4) =0_goto (il. 6) )
by A12, A8, AMI_1:54;
(
IC (Computation s,(5 + 1)) = il. 0 &
(Computation s,(5 + 1)) . (dl. 3) = (Computation s,(4 + 1)) . (dl. 3) )
by A18, A37, SCM_1:23;
then A49:
Computation s,
(5 + 1) is
State-consisting of
0 ,
0 ,
0 ,
Fusc_Program ,
((<*2*> ^ <*nn'*>) ^ <*A*>) ^ <*(B + A)*>
by A40, A45, A42, A39, A43, A48, A47, A46, A44, SCM_1:30;
A50:
(nn mod 2) + ((nn div 2) * 2) = nn
by A24;
then A51:
nn' < nn
by A33, A34, A41, PRE_FF:19;
A52:
Fusc N = (A * (Fusc nn')) + ((B + A) * (Fusc (nn' + 1)))
by A4, A33, A34, A41, A50, PRE_FF:21;
then A53:
(
nn' > 0 implies
LifeSpan (Computation s,(5 + 1)) = (6 * ([\(log 2,nn')/] + 1)) + 1 )
by A2, A3, A49, A51;
A54:
ProgramPart (Computation s,(5 + 1)) halts_on Computation s,
(5 + 1)
by A2, A3, A49, A51, A52;
then Y:
ProgramPart s halts_on Computation s,
(5 + 1)
by A2, A3, A49, A51, A52, AMI_1:144;
hence
ProgramPart s halts_on s
by AMI_1:93;
( (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )X:
Result (Computation s,(5 + 1)) = Result s
by A54, SCM_1:29, Y;
(Result (Computation s,(5 + 1))) . (dl. 3) = Fusc N
by A2, A3, A49, A51, A52;
hence
(Result s) . (dl. 3) = Fusc N
by A54, SCM_1:29, X;
( ( 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 A25;
( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 )A55:
(
nn' = 0 implies
LifeSpan (Computation s,(5 + 1)) = 1 )
by A2, A3, A33, A34, A24, A41, A49, A52;
thus
(
nn > 0 implies
LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 )
verumproof
assume
nn > 0
;
LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1
per cases
( nn' = 0 or nn' <> 0 )
;
suppose A56:
nn' <> 0
;
LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1then A57:
nn' > 0
by NAT_1:3;
then reconsider F =
[\(log 2,nn')/] as
Element of
NAT by Lm2;
(6 * (F + 1)) + 1
> 0
by A57, Lm2;
hence LifeSpan s =
6
+ ((6 * (F + 1)) + 1)
by A54, A53, A56, NAT_1:3, SCM_1:28
.=
(6 * ([\(log 2,nn)/] + 1)) + 1
by A33, A34, A41, A50, A57, Lm3
;
verum end;
end; end; suppose A58:
(Computation s,(2 + 1)) . (dl. 4) = 0
;
( ProgramPart s halts_on s & (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )then A59:
IC (Computation s,(3 + 1)) = il. 6
by A8, A28, SCM_1:24;
then A60:
IC (Computation s,(4 + 1)) = il. (6 + 1)
by A21, SCM_1:19;
(Computation s,(3 + 1)) . (dl. 0 ) = 2
by A8, A28, A30, SCM_1:24;
then
(Computation s,(4 + 1)) . (dl. 0 ) = 2
by A21, A59, Lm8, SCM_1:19;
then A61:
(Computation s,(5 + 1)) . (dl. 0 ) = 2
by A20, A60, SCM_1:23;
A62:
(
(Computation s,(5 + 1)) . (il. 6) = AddTo (dl. 2),
(dl. 3) &
(Computation s,(5 + 1)) . (il. 7) = goto (il. 0 ) )
by A21, A20, AMI_1:54;
A63:
(Computation s,(3 + 1)) . (dl. 3) = B
by A8, A28, A31, SCM_1:24;
then
(Computation s,(4 + 1)) . (dl. 3) = B
by A21, A59, Lm12, SCM_1:19;
then A64:
(Computation s,(5 + 1)) . (dl. 3) = B
by A20, A60, SCM_1:23;
(Computation s,(3 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1)
by A8, A28, SCM_1:24;
then
(Computation s,(4 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1)
by A21, A59, Lm10, SCM_1:19;
then A65:
(Computation s,(5 + 1)) . (dl. 1) = (Computation s,(2 + 1)) . (dl. 1)
by A20, A60, SCM_1:23;
A66:
(
(Computation s,(5 + 1)) . (il. 4) = AddTo (dl. 3),
(dl. 2) &
(Computation s,(5 + 1)) . (il. 5) = goto (il. 0 ) )
by A19, A18, AMI_1:54;
A67:
(
(Computation s,(5 + 1)) . (il. 2) = Divide (dl. 1),
(dl. 4) &
(Computation s,(5 + 1)) . (il. 3) = (dl. 4) =0_goto (il. 6) )
by A12, A8, AMI_1:54;
(Computation s,(3 + 1)) . (dl. 2) = A
by A8, A28, A29, SCM_1:24;
then A68:
(Computation s,(4 + 1)) . (dl. 2) = A + B
by A21, A59, A63, SCM_1:19;
reconsider nn' =
(Computation s,(2 + 1)) . (dl. 1) as
Element of
NAT by A33, PRE_FF:7;
A69:
(Computation s,(5 + 1)) . (il. 8) = halt SCM
by A7, AMI_1:54;
A70:
(
(Computation s,(5 + 1)) . (il. 0 ) = (dl. 1) =0_goto (il. 8) &
(Computation s,(5 + 1)) . (il. 1) = (dl. 4) := (dl. 0 ) )
by A6, A17, AMI_1:54;
(
IC (Computation s,(5 + 1)) = il. 0 &
(Computation s,(5 + 1)) . (dl. 2) = (Computation s,(4 + 1)) . (dl. 2) )
by A20, A60, SCM_1:23;
then A71:
Computation s,
(5 + 1) is
State-consisting of
0 ,
0 ,
0 ,
Fusc_Program ,
((<*2*> ^ <*nn'*>) ^ <*(A + B)*>) ^ <*B*>
by A68, A61, A65, A64, A70, A67, A66, A62, A69, SCM_1:30;
A72:
(
nn' < nn &
Fusc N = ((A + B) * (Fusc nn')) + (B * (Fusc (nn' + 1))) )
by A4, A25, A33, A34, A24, A58, PRE_FF:18, PRE_FF:22;
then A73:
ProgramPart (Computation s,(5 + 1)) halts_on Computation s,
(5 + 1)
by A2, A3, A71;
then Y:
ProgramPart s halts_on Computation s,
(5 + 1)
by AMI_1:144;
hence
ProgramPart s halts_on s
by AMI_1:93;
( (Result s) . (dl. 3) = Fusc N & ( nn = 0 implies LifeSpan s = 1 ) & ( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )X:
Result (Computation s,(5 + 1)) = Result s
by A73, SCM_1:29, Y;
(Result (Computation s,(5 + 1))) . (dl. 3) = Fusc N
by A2, A3, A71, A72;
hence
(Result s) . (dl. 3) = Fusc N
by A73, SCM_1:29, X;
( ( 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 A25;
( nn > 0 implies LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 )A74:
(
nn' > 0 implies
LifeSpan (Computation s,(5 + 1)) = (6 * ([\(log 2,nn')/] + 1)) + 1 )
by A2, A3, A71, A72;
thus
(
nn > 0 implies
LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 )
verumproof
assume
nn > 0
;
LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1
per cases
( nn' = 0 or nn' <> 0 )
;
suppose A75:
nn' <> 0
;
LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1then A76:
nn' > 0
by NAT_1:3;
then reconsider F =
[\(log 2,nn')/] as
Element of
NAT by Lm2;
(6 * (F + 1)) + 1
> 0
by A76, Lm2;
hence LifeSpan s =
6
+ ((6 * (F + 1)) + 1)
by A73, A74, A75, NAT_1:3, SCM_1:28
.=
(6 * ([\(log 2,nn)/] + 1)) + 1
by A33, A34, A24, A58, A76, Lm5
;
verum end;
end; end; end;
nn >= 0
by NAT_1:2;
hence
(
ProgramPart s halts_on s &
(Result s) . (dl. 3) = Fusc N & (
nn = 0 implies
LifeSpan s = 1 ) & (
nn > 0 implies
LifeSpan s = (6 * ([\(log 2,nn)/] + 1)) + 1 ) )
by A14, A23, XXREAL_0:1;
verum
end;
for n being Nat holds S1[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
( 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 ) )
; verum