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