Copyright (c) 1993 Association of Mizar Users
environ
vocabulary AMI_3, INT_1, POWER, ARYTM_1, FINSEQ_1, AMI_1, SCM_1, FUNCT_1,
PRE_FF, GROUP_1, NAT_1, FIB_FUSC;
notation XCMPLX_0, XREAL_0, INT_1, NAT_1, POWER, FINSEQ_1, AMI_1, SCM_1,
AMI_3, PRE_FF, CARD_4;
constructors NAT_1, POWER, SCM_1, PRE_FF, CARD_4, MEMBERED, XBOOLE_0;
clusters INT_1, AMI_1, AMI_3, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems AXIOMS, REAL_1, NAT_1, INT_1, POWER, NEWTON, SCM_1, PRE_FF, AMI_3,
AMI_1, HEINE, XCMPLX_1;
schemes NAT_1;
begin
Lm1: 6 + 1 = 6 * ([\ log(2, 1) /] + 1)+1
proof
thus 6+1 = 6 * (0+1) + 1
.= 6 * ( [\ 0 /] + 1) + 1 by INT_1:47
.= 6 * ([\ log(2, 1) /] + 1)+1 by POWER:59;
end;
Lm2: for nn' being Nat st nn' > 0 holds
[\ log(2, nn') /] is Nat &
6 * ([\ log(2, nn') /] + 1) + 1 > 0
proof let nn' be Nat;
assume nn' > 0;
then nn' >= 0+1 by NAT_1:38;
then nn' >= 1 & log(2, 1) = 0 by POWER:59;
then log(2, nn') >= 0 by PRE_FF:12;
then [\ log(2, nn') /] >= [\ 0 /] by PRE_FF:11;
then [\ log(2, nn') /] >= 0 by INT_1:47;
then reconsider F = [\ log(2, nn') /] as Nat by INT_1:16;
F is Nat;
hence [\ log(2, nn') /] is Nat;
6 * F + 6 * 1 >= 0 by NAT_1:37;
then 6 * (F + 1) >= 0 by XCMPLX_1:8;
hence 6 * ([\ log(2, nn') /] + 1) + 1 > 0 by NAT_1:38;
end;
Lm3: for nn, nn' being Nat st nn = 2*nn'+1 & nn' > 0 holds
6+(6*([\ log(2, nn')/]+1)+1)=6*([\ log(2,nn)/]+1) + 1
proof let nn, nn' be Nat such that
A1: nn = 2*nn'+1 and
A2: nn' > 0;
set F = [\ log(2, nn') /];
thus 6 + (6 * (F+1)+1) = 6 * 1 + 6 * (F + 1) + 1 by XCMPLX_1:1
.= 6 * (1 + (F + 1)) + 1 by XCMPLX_1:8
.= 6 * ([\ log(2, nn) /] + 1) + 1 by A1,A2,PRE_FF:16;
end;
Lm4: for n being Nat st n > 0 holds log (2, 2*n) = 1+log(2,n) &
log (2, 2*n) = log(2,n)+1 proof
let n be Nat; assume
n > 0;
hence log (2,2*n) = log (2,2)+log (2, n) by POWER:61
.= 1+log (2, n) by POWER:60;
hence thesis;
end;
Lm5: for nn, nn' being Nat st nn = 2*nn' & nn' > 0 holds
6+(6*([\ log(2, nn')/]+1)+1)=6*([\ log(2,nn)/]+1) + 1
proof let nn, nn' be Nat such that
A1: nn = 2*nn' and
A2: nn' > 0;
set F = [\ log(2, nn') /];
thus 6 + (6 * (F+1)+1) = 6 * 1 + 6 * (F + 1) + 1 by XCMPLX_1:1
.= 6 * (1 + (F + 1)) + 1 by XCMPLX_1:8
.= 6 * (1 + [\ log(2, nn')+1 /]) + 1 by INT_1:51
.= 6 * ([\ log(2, nn) /] + 1) + 1 by A1,A2,Lm4;
end;
Lm6: for N being Nat st N <> 0 holds 6*N - 4 > 0
proof let N be Nat; assume
N<>0; then consider L being Nat such that
A1: N = L+1 by NAT_1:22;
A2: 6 * N - 4 = 6 * L + 6 * 1 - 4 by A1,XCMPLX_1:8
.= 6 * L + (2 + 4 - 4) by XCMPLX_1:29
.= 6 * L + 2; 6 * L + 2 <> 0 by NAT_1:23;
hence thesis by A2,NAT_1:19;
end;
Lm7: for N being Nat holds 6+(6*N-4)=6*(N+1)-4
proof let N be Nat;
thus 6 + (6 * N - 4) = 6 * 1 + 6 * N - 4 by XCMPLX_1:29
.= 6 * (N+1) - 4 by XCMPLX_1:8;
end;
Lm8: dl.0<>dl.1 & dl.0<>dl.2 & dl.0<>dl.3 & dl.1<>dl.2 & dl.1<>dl.3 &
dl.2<>dl.3 by AMI_3:52;
Lm9: dl.0<>dl.4 & dl.1<>dl.4 & dl.2<>dl.4 & dl.3<>dl.4 by AMI_3:52;
definition
func Fib_Program -> FinSequence of the Instructions of SCM equals
:Def1: <* dl.1 >0_goto il.2 *>^
<* halt SCM *>^
<* dl.3 := dl.0 *>^
<* SubFrom(dl.1, dl.0) *>^
<* dl.1 =0_goto il.1 *>^
<* dl.4 := dl.2 *>^
<* dl.2 := dl.3 *>^
<* AddTo(dl.3, dl.4) *>^
<* goto il.3 *>;
coherence;
end;
theorem
for N being Nat,
s being State-consisting of 0, 0, 0,
Fib_Program,
<*1*>^<*N*>^<*0*>^<*0*>
holds s is halting &
(N = 0 implies Complexity s = 1) &
(N > 0 implies Complexity s = 6 * N - 2) &
(Result s).dl.3 = Fib N
proof
set L0 = il.0, L1 = il.1, L2 = il.2, L3 = il.3, L4 = il.4, L5 = il.5;
set L6 = il.6, L7 = il.7, L8 = il.8;
set C1 = dl.0, n = dl.1, FP = dl.2, FC = dl.3, AUX = dl.4;
let N be Nat, s be State-consisting of 0, 0, 0,
Fib_Program,
<*1*>^<*N*>^<*0*>^<*0*>;
A1: IC s = L0 by SCM_1:def 1;
A2: s.L0 = n >0_goto L2 by Def1,SCM_1:14;
A3: s.L1 = halt SCM by Def1,SCM_1:14;
A4: s.L2 = FC := C1 by Def1,SCM_1:14;
A5: s.L3 = SubFrom(n, C1) by Def1,SCM_1:14;
A6: s.L4 = n =0_goto L1 by Def1,SCM_1:14;
A7: s.L5 = AUX := FP by Def1,SCM_1:14;
A8: s.L6 = FP := FC by Def1,SCM_1:14;
A9: s.L7 = AddTo(FC, AUX) by Def1,SCM_1:14;
A10: s.L8 = goto L3 by Def1,SCM_1:14;
A11: s.C1 = 1 & s.n = N & s.FP = 0 & s.FC = 0 by Def1,SCM_1:14;
set s0 = (Computation s).0;
A12: s = s0 by AMI_1:def 19;
set s1 = (Computation s).(0+1);
A13: s1.C1 = 1 & s1.n = N & s1.FP = 0 & s1.FC = 0
by A1,A2,A11,A12,SCM_1:25;
defpred P[Nat] means
$1 < N implies for u being State of SCM
st u = (Computation s).(6*$1+3) holds
u.C1 = 1 & u.n = N-1-$1 & u.FP = Fib $1 & u.FC = Fib ($1+1) & IC u = L4;
A14: P[0] proof assume 0 < N;
then A15: IC s1 = L2 by A1,A2,A11,A12,SCM_1:25;
let t be State of SCM; assume
A16: t = (Computation s).(6*0+3);
set s2 = (Computation s).(1+1);
A17: s2.FC = 1 by A4,A13,A15,SCM_1:18;
A18: s2.C1 = 1 & s2.n = N & s2.FP = 0 by A4,A13,A15,Lm8,SCM_1:18;
A19: IC s2 = il.(2+1) by A4,A15,SCM_1:18;
set s3 = (Computation s).(2+1);
IC s3 = il.(3+1) by A5,A19,SCM_1:20;
hence t.C1 = 1 & t.n = N-1-0 & t.FP = Fib 0 & t.FC = Fib (0+1) & IC t = L4
by A5,A16,A17,A18,A19,Lm8,PRE_FF:1,SCM_1:20;
end;
A20: for k being Nat st P[k] holds P[k+1]
proof let k be Nat such that
A21: k < N implies
for u being State of SCM st u = (Computation s).(6*k+3)
holds u.C1 = 1 & u.n = N-1-k & u.FP = Fib k & u.FC = Fib (k+1) &
IC u = L4 and
A22: k+1 < N;
let t be State of SCM; assume
A23: t = (Computation s).(6*(k+1)+3);
set s4 = (Computation s).(6*k+3);
A24: s4.C1 = 1 & s4.n = N-1-k & s4.FP = Fib k & s4.FC = Fib (k+1) &
IC s4 = L4 by A21,A22,NAT_1:38;
N-1 > k & 0+k = k by A22,REAL_1:86;
then A25: s4.n <> 0 by A24,REAL_1:86;
set b = 6*k+3;
set s5 = (Computation s).(b+1);
A26: IC s5 = il.(4+1) by A6,A24,A25,SCM_1:24;
A27: s5.C1 = 1 & s5.n = N-1-k & s5.FP = Fib k & s5.FC = Fib (k+1)
by A6,A24,SCM_1:24;
set s6 = (Computation s).(b+1+1);
A28: IC s6 = il.(5+1) by A7,A26,SCM_1:18;
A29: s6.AUX = Fib k by A7,A26,A27,SCM_1:18;
A30: s6.C1 = 1 & s6.n = N-1-k & s6.FP = Fib k & s6.FC = Fib (k+1)
by A7,A26,A27,Lm9,SCM_1:18;
set s7 = (Computation s).(b+1+1+1);
A31: IC s7 = il.(6+1) by A8,A28,SCM_1:18;
A32: s7.FP = Fib (k+1) by A8,A28,A30,SCM_1:18;
A33: s7.C1 = 1 & s7.n = N-1-k & s7.FC = Fib (k+1) & s7.AUX = Fib k
by A8,A28,A29,A30,Lm8,Lm9,SCM_1:18;
set s8 = (Computation s).(b+1+1+1+1);
A34: IC s8 = il.(7+1) by A9,A31,SCM_1:19;
A35: s8.FC = s7.AUX + s7.FC by A9,A31,SCM_1:19
.= Fib (k+1+1) by A33,PRE_FF:1;
A36: s8.C1 = 1 & s8.n = N-1-k & s8.FP = Fib (k+1)
by A9,A31,A32,A33,Lm8,SCM_1:19;
set s9 = (Computation s).(b+1+1+1+1+1);
A37: IC s9 = L3 by A10,A34,SCM_1:23;
A38: s9.C1 = 1 & s9.n = N-1-k & s9.FP = Fib (k+1) & s9.FC = Fib (k+1+1)
by A10,A34,A35,A36,SCM_1:23;
set s10 = (Computation s).(b+1+1+1+1+1+1);
A39: IC s10 = il.(3+1) by A5,A37,SCM_1:20;
A40: s10.n = N-1-k - 1 by A5,A37,A38,SCM_1:20;
b+1+1+1+1+1+1 = b+1+1+1+1+(1+1) by XCMPLX_1:1
.= b+1+1+1+(1+2) by XCMPLX_1:1
.= b+1+1+(1+3) by XCMPLX_1:1
.= b+1+(1+4) by XCMPLX_1:1
.= b+(1+5) by XCMPLX_1:1
.= 6*k+6*1+3 by XCMPLX_1:1
.= 6*(k+1)+3 by XCMPLX_1:8;
hence t.C1 = 1 & t.n = N-1-(k+1) & t.FP = Fib (k+1) &
t.FC = Fib (k+1+1) & IC t = L4 by A5,A23,A37,A38,A39,A40,Lm8,SCM_1:20,
XCMPLX_1:36;
end;
A41: for k being Nat holds P[k] from Ind(A14, A20);
per cases by NAT_1:22;
suppose
A42: N = 0;
then A43: s.(IC s1) = halt SCM by A1,A2,A3,A11,A12,SCM_1:25;
hence s is halting by SCM_1:3;
hereby assume N = 0; halt SCM <> n >0_goto L2 by SCM_1:26;
hence Complexity s = 1 by A1,A2,A12,A43,SCM_1:17;
end;
thus N > 0 implies Complexity s = 6 * N - 2 by A42;
thus (Result s).FC = Fib N by A13,A42,A43,PRE_FF:1,SCM_1:4;
suppose ex k being Nat st N = k+1; then consider k being Nat such that
A44: N = k+1;
set r = (Computation s).(6*k+3);
k < N by A44,NAT_1:38;
then A45: r.C1 = 1 & r.n = N-1-k & r.FP = Fib k & r.FC = Fib (k+1) & IC r = L4
by A41;
set t = (Computation s).(6*k+3+1);
r.n = k+(1-1)-k by A44,A45,XCMPLX_1:29 .=
0 by XCMPLX_1:14;
then A46: IC t = L1 by A6,A45,SCM_1:24;
hence s is halting by A3,SCM_1:3;
thus N = 0 implies Complexity s = 1 by A44,NAT_1:21;
hereby assume N > 0; halt SCM <> n =0_goto L1 by SCM_1:26;
hence Complexity s = 6*k+(6-6)+3+1 by A3,A6,A45,A46,SCM_1:17
.= 6*k+6*1-6+3+1 by XCMPLX_1:29 .= 6*N-6+3+1 by A44,XCMPLX_1:8
.= 6*N-6+(3+1) by XCMPLX_1:1 .= 6*N-(2+4-4) by XCMPLX_1:37
.= 6 * N - 2;
end;
thus (Result s).FC = t.FC by A3,A46,SCM_1:4
.= Fib N by A6,A44,A45,SCM_1:24;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Fusc
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let i be Integer;
func Fusc' i -> Nat means
:Def2:
(ex n being Nat st i = n & it = Fusc n) or i is not Nat & it = 0;
existence proof
per cases;
suppose i is Nat; then reconsider n = i as Nat;
take Fusc n; thus thesis;
suppose i is not Nat;
hence thesis;
end;
uniqueness;
end;
definition
func Fusc_Program -> FinSequence of the Instructions of SCM equals
:Def3: <* dl.1 =0_goto il.8 *>^
<* dl.4 := dl.0 *>^
<* Divide(dl.1, dl.4) *>^
<* dl.4 =0_goto il.6 *>^
<* AddTo(dl.3, dl.2) *>^
<* goto il.0 *>^
<* AddTo(dl.2, dl.3) *>^
<* goto il.0 *>^
<* halt SCM *>;
coherence;
end;
theorem
for N being Nat st N > 0
for s being State-consisting of 0, 0, 0,
Fusc_Program,
<*2*>^<*N*>^<*1*>^<*0*>
holds s is halting &
(Result s).dl.3 = Fusc N &
Complexity s = 6 * ([\ log(2, N) /] + 1) + 1
proof
set L0 = il.0, L1 = il.1, L2 = il.2, L3 = il.3, L4 = il.4, L5 = il.5;
set L6 = il.6, L7 = il.7, L8 = il.8;
set c2 = dl.0, n = dl.1, a = dl.2, b = dl.3, aux = dl.4;
let N be Nat such that
A1: N > 0;
let S be State-consisting of 0, 0, 0,
Fusc_Program,
<*2*>^<*N*>^<*1*>^<*0*>;
consider s being State of SCM such that
A2: s = S;
A3: s.L0 = n =0_goto L8 by A2,Def3,SCM_1:14;
A4: s.L1 = aux := c2 by A2,Def3,SCM_1:14;
A5: s.L2 = Divide(n, aux) by A2,Def3,SCM_1:14;
A6: s.L3 = aux =0_goto L6 by A2,Def3,SCM_1:14;
A7: s.L4 = AddTo(b, a) by A2,Def3,SCM_1:14;
A8: s.L5 = goto L0 by A2,Def3,SCM_1:14;
A9: s.L6 = AddTo(a, b) by A2,Def3,SCM_1:14;
A10: s.L7 = goto L0 by A2,Def3,SCM_1:14;
A11: s.L8 = halt SCM by A2,Def3,SCM_1:14;
A12: s.c2 = 2 & s.n = N & s.a = 1 & s.b = 0 by A2,Def3,SCM_1:14;
A13: 0 <= N by NAT_1:18;
defpred P[Nat] means
$1 <= log(2, N) + 1 implies
for u being State of SCM st u = (Computation s).(6*$1) holds
IC u = L0 & u.c2 = 2 & u.n = N qua Integer div (2 |^ $1) & u.n is Nat &
Fusc N = u.a*Fusc' u.n + u.b*Fusc' (u.n+1);
A14: P[0] proof assume 0 <= log(2, N) + 1;
let u be State of SCM; assume
u = (Computation s).(6*0);
then A15: u = s by AMI_1:def 19;
hence IC u = L0 & u.c2 = 2 by A2,Def3,SCM_1:14;
thus u.n = N qua Integer div 1 by A12,A15,PRE_FF:2
.= N qua Integer div (2 |^ 0) by NEWTON:9;
thus u.n is Nat by A2,A15,Def3,SCM_1:14;
thus Fusc N = u.a*Fusc' u.n + u.b*Fusc' (u.n+1) by A12,A15,Def2;
end;
A16: for k being Nat st P[k] holds P[k+1]
proof let k be Nat; assume
A17: k <= log(2, N) + 1 implies
for u being State of SCM st u = (Computation s).(6*k) holds
IC u = L0 & u.c2 = 2 & u.n = N qua Integer div (2 |^ k) & u.n is Nat &
Fusc N = u.a*Fusc' u.n + u.b*Fusc' (u.n+1);
assume
A18: k+1 <= log(2, N) + 1;
let u be State of SCM; assume
A19: u = (Computation s).(6*(k+1));
set t = 6*k;
set t0 = (Computation s).t;
A20: k <= k+1 by NAT_1:29;
then A21: IC t0 = L0 & t0.c2 = 2 & t0.n = N qua Integer div (2 |^ k) & t0.n
is Nat
by A17,A18,AXIOMS:22;
k <= log(2, N) by A18,REAL_1:53;
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 A22: 2 |^ k <= N & (2 |^ k) > 0 by HEINE:5,POWER:48;
then A23: t0.n <> 0 by A21,PRE_FF:3;
set t1 = (Computation s).(t+1);
A24: IC t1 = il.(0+1) by A3,A21,A23,SCM_1:24;
A25: t1.c2 = 2 & t1.n = t0.n & t1.a = t0.a & t1.b = t0.b
by A3,A21,SCM_1:24;
set t2 = (Computation s).(t+2);
A26: t+1+1 = t+(1+1) by XCMPLX_1:1 .= t + 2;
then A27: IC t2 = il.(1+1) by A4,A24,SCM_1:18;
A28: t2.aux = 2 by A4,A24,A25,A26,SCM_1:18;
A29: t2.c2 = 2 & t2.n = t0.n & t2.a = t0.a & t2.b = t0.b
by A4,A24,A25,A26,Lm9,SCM_1:18;
set t3 = (Computation s).(t+3);
A30: t+2+1 = t+(2+1) by XCMPLX_1:1 .= t+3;
then A31: IC t3 = il.(2+1) by A5,A27,Lm9,SCM_1:22;
A32: t3.n = t0.n div 2 by A5,A27,A28,A29,A30,Lm9,SCM_1:22;
then A33: t3.n = N qua Integer div (2|^k)*2 by A21,A22,PRE_FF:5
.= N qua Integer div (2|^(k+1)) by NEWTON:11;
A34: t3.aux = t0.n mod 2
by A5,A27,A28,A29,A30,Lm9,SCM_1:22;
A35: t3.c2 = 2 & t3.a = t0.a & t3.b = t0.b
by A5,A27,A29,A30,Lm8,Lm9,SCM_1:22;
set t4 = (Computation s).(t+4);
A36: t+3+1 = t+(3+1) by XCMPLX_1:1 .= t+4;
set t5 = (Computation s).(t+5);
A37: t+4+1 = t+(4+1) by XCMPLX_1:1 .= t+5;
set t6 = (Computation s).(t+6);
A38: t+5+1 = t+(5+1) by XCMPLX_1:1 .= t+6;
A39: t+6 = 6*k + 6*1 .= 6*(k+1) by XCMPLX_1:8;
A40:
t0.n mod 2 = t0.n - (t0.n div 2)*2 by INT_1:def 8;
per cases;
suppose
A41: t3.aux <> 0;
then A42: IC t4 = il.(3+1) by A6,A31,A36,SCM_1:24;
A43: t4.c2 = 2 & t4.n = t3.n & t4.a = t0.a & t4.b = t0.b
by A6,A31,A35,A36,SCM_1:24;
A44: IC t5 = il.(4+1) by A7,A37,A42,SCM_1:19;
A45: t5.b = t0.b + t0.a by A7,A37,A42,A43,SCM_1:19;
A46: t5.c2 = 2 & t5.n = t3.n & t5.a = t0.a
by A7,A37,A42,A43,Lm8,SCM_1:19;
then A47: t6.c2 = 2 & t6.n = t3.n by A8,A38,A44,SCM_1:23;
A48: t6.a = t0.a & t6.b = t0.b+t0.a by A8,A38,A44,A45,A46,SCM_1:23;
thus IC u = L0 & u.c2 = 2 & u.n = N qua Integer div (2 |^ (k+1))
by A8,A19,A33,A38,A39,A44,A46,SCM_1:23;
thus u.n is Nat by A19,A21,A32,A39,A47,PRE_FF:7;
reconsider un = u.n, tn = t0.n as Nat by A19,A21,A32,A39,A47,PRE_FF:7;
A49: tn = un * 2 + (t0.n mod 2) by A19,A32,A39,A40,A47,XCMPLX_1:27
.= 2 * un + 1 by A34,A41,PRE_FF:6;
then A50: tn+1 = 2*un +(1+1) by XCMPLX_1:1
.= 2*un + 2*1
.= 2*(un+1) by XCMPLX_1:8;
A51: Fusc' t0.n = Fusc tn by Def2
.= Fusc un + Fusc (un+1) by A49,PRE_FF:17
.= Fusc' u.n + Fusc (un+1) by Def2
.= Fusc' u.n + Fusc' (u.n+1) by Def2;
A52: Fusc' (t0.n+1) = Fusc (tn+1) by Def2
.= Fusc (un+1) by A50,PRE_FF:17
.= Fusc' (u.n+1) by Def2;
reconsider un = u.n, tn = t0.n as Integer;
reconsider ta = t0.a, tb = t0.b as Integer;
(ta * Fusc' tn) + (tb * Fusc' (tn+1))
= (ta*Fusc' un)+(ta*Fusc' (un+1))+(tb*Fusc' (un+1))
by A51,A52,XCMPLX_1:8
.= (ta*Fusc' un)+((ta*Fusc' (un+1))+(tb*Fusc' (un+1)))
by XCMPLX_1:1
.= (u.a * Fusc' un) + (u.b) * Fusc' (un+1) by A19,A39,A48,XCMPLX_1:8;
hence Fusc N = (u.a*Fusc' u.n)+(u.b*(Fusc' (u.n+1))) by A17,A18,A20,AXIOMS:
22;
suppose
A53: t3.aux = 0;
then A54: IC t4 = il.6 by A6,A31,A36,SCM_1:24;
A55: t4.c2 = 2 & t4.n = t3.n & t4.a = t0.a & t4.b = t0.b
by A6,A31,A35,A36,SCM_1:24;
A56: IC t5 = il.(6+1) by A9,A37,A54,SCM_1:19;
A57: t5.a = t0.a + t0.b by A9,A37,A54,A55,SCM_1:19;
A58: t5.c2 = 2 & t5.n = t3.n & t5.b = t0.b
by A9,A37,A54,A55,Lm8,SCM_1:19;
then A59: t6.c2 = 2 & t6.n = t3.n by A10,A38,A56,SCM_1:23;
A60: t6.a = t0.a+t0.b & t6.b = t0.b by A10,A38,A56,A57,A58,SCM_1:23;
thus IC u = L0 & u.c2 = 2 & u.n = N qua Integer div (2 |^ (k+1)) &
u.n is Nat by A10,A19,A21,A32,A33,A38,A39,A56,A59,PRE_FF:7,SCM_1:23;
reconsider un = u.n, tn = t0.n as Nat by A19,A21,A32,A39,A59,PRE_FF:7;
A61: tn = 2 * un + 0 by A19,A32,A34,A39,A40,A53,A59,XCMPLX_1:27
.= 2 * un;
A62: Fusc' t0.n = Fusc tn by Def2
.= Fusc un by A61,PRE_FF:17
.= Fusc' u.n by Def2;
A63: Fusc' (t0.n+1) = Fusc (tn+1) by Def2
.= Fusc un + Fusc (un+1) by A61,PRE_FF:17
.= Fusc un + Fusc' (u.n+1) by Def2
.= Fusc' u.n + Fusc' (u.n+1) by Def2;
reconsider un = u.n, tn = t0.n, ta = t0.a, tb = t0.b as Integer;
(ta * Fusc' tn) + (tb * Fusc' (tn+1))
= (ta * Fusc' un)+((tb * Fusc' un)+(tb * Fusc' (un+1)))
by A62,A63,XCMPLX_1:8
.= (ta * Fusc' un + tb * Fusc' un) + tb * Fusc' (un+1)
by XCMPLX_1:1
.= (ta+tb) * Fusc' un + tb * Fusc' (un+1) by XCMPLX_1:8;
hence Fusc N = u.a*Fusc' u.n + u.b*Fusc' (u.n+1)
by A17,A18,A19,A20,A39,A60,AXIOMS:22;
end;
A64: for k being Nat holds P[k] from Ind( A14, A16 );
set k = [\log(2, N)/];
A65: log(2, N) - 1 < k by INT_1:def 4;
N >= 0+1 by A1,NAT_1:38;
then log (2, N) >= log (2, 1) by PRE_FF:12;
then A66: log (2, N) >= 0 & log(2, N) < k+1 by A65,POWER:59,REAL_1:84;
then k+1 > 0 by AXIOMS:22;
then 0 <= k by INT_1:20;
then reconsider k as Nat by INT_1:16;
set u = (Computation s).(6*(k+1));
[\log(2, N)/] <= log(2, N) by INT_1:def 4;
then k+1 <= log(2, N)+1 by AXIOMS:24;
then A67: IC u = L0 & u.n = N qua Integer div (2 |^ (k+1)) &
Fusc N = u.a*Fusc' u.n + u.b*Fusc' (u.n+1) by A64;
2 to_power (k+1) > 2 to_power log(2, N) by A66,POWER:44;
then 2 to_power (k+1) > N by A1,POWER:def 3;
then 2 |^ (k+1) > N by POWER:48;
then A68: u.n = 0 by A13,A67,PRE_FF:4;
then A69: u.a*Fusc' u.n + u.b*Fusc' (u.n+1)
= u.a * 0 + u.b * Fusc' (u.n+1) by Def2,PRE_FF:17
.= u.b * Fusc (0+1) by A68,Def2
.= u.b by PRE_FF:17;
set h = (Computation s).(6*(k+1)+1);
A70: IC h = L8 by A3,A67,A68,SCM_1:24;
A71: h.b = u.b by A3,A67,SCM_1:24;
thus S is halting by A2,A11,A70,SCM_1:3;
thus (Result S).dl.3 = Fusc N by A2,A11,A67,A69,A70,A71,SCM_1:4;
s.(IC h)=halt SCM & s.(IC u)<>halt SCM by A2,A3,A67,A70,Def3,SCM_1:14,26;
hence Complexity S = 6 * ([\ log(2, N) /] + 1) + 1
by A2,SCM_1:17;
end;
theorem
for N being Nat, k, Fk, Fk1 being Nat,
s being State-consisting of 3, 0, 0,
Fib_Program,
<* 1 *>^<* N *>^<* Fk *>^<* Fk1 *>
st N > 0 & Fk = Fib k & Fk1 = Fib (k+1)
holds s is halting &
Complexity s = 6 * N - 4 &
ex m being Nat st m = k+N-1 &
(Result s).dl.2 = Fib m & (Result s).dl.3 = Fib (m+1)
proof
defpred P[Nat] means for k, Fk, Fk1 be Nat,
s be State-consisting of 3, 0, 0,
Fib_Program,
<* 1 *>^<* $1 *>^<* Fk *>^<* Fk1 *> st
$1 > 0 & Fk = Fib k & Fk1 = Fib (k+1) holds
s is halting &
Complexity s = 6 * $1 - 4 &
ex m being Nat st m = k+$1-1 &
(Result s).dl.2 = Fib m & (Result s).dl.3 = Fib (m+1);
A1: P[0];
A2: for N be Nat st P[N] holds P[N+1]
proof let N be Nat; assume
A3: P[N];
let k, Fk, Fk1 be Nat,
s be State-consisting of 3, 0, 0,
Fib_Program,
<* 1 *>^<* N+1 *>^<* Fk *>^<* Fk1 *>;
assume
A4: (N+1) > 0 & Fk = Fib k & Fk1 = Fib (k+1);
set C1 = dl.0, n = dl.1, FP = dl.2, FC = dl.3, AUX = dl.4;
A5: IC s = il.3 by SCM_1:def 1;
A6: s.il.0 = n >0_goto il.2 by Def1,SCM_1:14;
A7: s.il.1 = halt SCM by Def1,SCM_1:14;
A8: s.il.2 = FC := C1 by Def1,SCM_1:14;
A9: s.il.3 = SubFrom(n, C1) by Def1,SCM_1:14;
A10: s.il.4 = n =0_goto il.1 by Def1,SCM_1:14;
A11: s.il.5 = AUX := FP by Def1,SCM_1:14;
A12: s.il.6 = FP := FC by Def1,SCM_1:14;
A13: s.il.7 = AddTo(FC, AUX) by Def1,SCM_1:14;
A14: s.il.8 = goto il.3 by Def1,SCM_1:14;
A15: s.C1 = 1 & s.n = N+1 & s.FP = Fk & s.FC = Fk1 by Def1,SCM_1:14;
set s0 = (Computation s).0;
A16: s = s0 by AMI_1:def 19;
set s1 = (Computation s).(0+1);
A17: s1.n = (N+1)-1 by A5,A9,A15,A16,SCM_1:20
.= N by XCMPLX_1:26;
A18: s1.C1=1 & s1.FP=Fk & s1.FC=Fk1 by A5,A9,A15,A16,Lm8,SCM_1:20;
A19: IC s1 = il.(3+1) by A5,A9,A16,SCM_1:20
.= il.4;
set s2 = (Computation s).(1+1);
A20: s2.C1=1 & s2.n=N & s2.FP=Fk & s2.FC=Fk1 by A10,A17,A18,A19,SCM_1:24;
A21: N >= 0 by NAT_1:18;
per cases by A21,REAL_1:def 5;
suppose
A22: N = 0;
then A23: s.(IC s2) = halt SCM by A7,A10,A17,A19,SCM_1:24;
hence
s is halting by SCM_1:3; s.(IC s1) <> halt SCM by A10,A19,SCM_1:26;
hence Complexity s = 6 * (N+1) - 4 by A22,A23,SCM_1:16;
take m = k;
thus m = k+(N+1)-1 by A22,XCMPLX_1:26;
thus (Result s).dl.2 = Fib m & (Result s).dl.3 = Fib (m+1)
by A4,A20,A23,SCM_1:4;
suppose
A24: N > 0;
then A25: IC s2 = il.(4+1) by A10,A17,A19,SCM_1:24;
set s3 = (Computation s).(2+1);
A26: IC s3 = il.(5+1) by A11,A25,SCM_1:18;
A27: s3.AUX = Fib k by A4,A11,A20,A25,SCM_1:18;
A28: s3.C1 = 1 & s3.n = N & s3.FP = Fib k & s3.FC = Fib (k+1)
by A4,A11,A20,A25,Lm9,SCM_1:18;
set s4 = (Computation s).(3+1);
A29: IC s4 = il.(6+1) by A12,A26,SCM_1:18;
A30: s4.FP = Fib (k+1) by A12,A26,A28,SCM_1:18;
A31: s4.C1 = 1 & s4.n = N & s4.FC = Fib (k+1) & s4.AUX = Fib k
by A12,A26,A27,A28,Lm8,Lm9,SCM_1:18;
set s5 = (Computation s).(4+1);
A32: IC s5 = il.(7+1) by A13,A29,SCM_1:19;
A33: s5.FC = s4.AUX + s4.FC by A13,A29,SCM_1:19
.= Fib (k+1+1) by A31,PRE_FF:1;
A34: s5.C1 = 1 & s5.n = N & s5.FP = Fib (k+1)
by A13,A29,A30,A31,Lm8,SCM_1:19;
set s6 = (Computation s).(5+1);
A35: IC s6 = il.3 by A14,A32,SCM_1:23;
A36: s6.C1 = 1 & s6.n = N & s6.FP = Fib (k+1) & s6.FC = Fib (k+1+1)
by A14,A32,A33,A34,SCM_1:23;
A37: s6.il.0=n >0_goto il.2 & s6.il.1=halt SCM & s6.il.2=FC := C1 &
s6.il.3=SubFrom(n, C1) & s6.il.4=n =0_goto il.1 & s6.il.5=AUX := FP &
s6.il.6=FP := FC & s6.il.7=AddTo(FC, AUX) & s6.il.8=goto il.3
by A6,A7,A8,A9,A10,A11,A12,A13,A14,AMI_1:54;
set Fk2 = Fib (k+1+1);
A38: s6 is State-consisting of 3, 0, 0,
Fib_Program,
<* 1 *>^<* N *>^<* Fk1 *>^<* Fk2 *>
by A4,A35,A36,A37,Def1,SCM_1:30;
then A39: s6 is halting &
Complexity s6 = 6 * N - 4 &
ex m being Nat st m = (k+1)+N-1 &
(Result s6).dl.2 = Fib m & (Result s6).dl.3 = Fib (m+1) by A3,A4,A24;
hence s is halting by SCM_1:27;
6 * N - 4 > 0 by A24,Lm6;
hence Complexity s = 6 + (6 * N - 4) by A39,SCM_1:28
.= 6 * (N+1) - 4 by Lm7;
consider m being Nat such that
A40: m = (k+1)+N-1 &
(Result s6).dl.2 = Fib m & (Result s6).dl.3 = Fib (m+1) by A3,A4,A24,A38;
take m;
thus m = k+(N+1)-1 by A40,XCMPLX_1:1;
thus (Result s).dl.2 = Fib m & (Result s).dl.3 = Fib (m+1)
by A39,A40,SCM_1:29;
end;
thus for N be Nat holds P[N] from Ind ( A1, A2 );
end;
canceled;
theorem Th5:
for n being Nat,
N, A, B being Nat,
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 Complexity s = 1) &
(n > 0 implies Complexity s = 6 * ([\ log(2, n) /] + 1) + 1)
proof
defpred P[Nat] means
for N, A, B being Nat,
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 Complexity s = 1) &
($1 > 0 implies Complexity s = 6 * ([\ log(2, $1) /] + 1)+1);
A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof let nn be Nat; assume
A2: for n' being Nat st n' < nn holds
for N, A, B being Nat,
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 Complexity s = 1) &
(n' > 0 implies Complexity s = 6 * ([\ log(2, n') /] + 1)+1);
let N, A, B be Nat,
s be State-consisting of 0, 0, 0,
Fusc_Program,
<*2*>^<*nn*>^<*A*>^<*B*>;
assume
A3: N > 0 & Fusc N = A * Fusc nn + B * Fusc (nn+1);
set c2 = dl.0, n = dl.1, a = dl.2, b = dl.3, aux = dl.4;
A4: IC s = il.0 by Def3,SCM_1:14;
A5: s.il.0 = n =0_goto il.8 by Def3,SCM_1:14;
A6: s.il.1 = aux := c2 by Def3,SCM_1:14;
A7: s.il.2 = Divide(n, aux) by Def3,SCM_1:14;
A8: s.il.3 = aux =0_goto il.6 by Def3,SCM_1:14;
A9: s.il.4 = AddTo(b, a) by Def3,SCM_1:14;
A10: s.il.5 = goto il.0 by Def3,SCM_1:14;
A11: s.il.6 = AddTo(a, b) by Def3,SCM_1:14;
A12: s.il.7 = goto il.0 by Def3,SCM_1:14;
A13: s.il.8 = halt SCM by Def3,SCM_1:14;
A14: s.c2 = 2 & s.n = nn & s.a = A & s.b = B by Def3,SCM_1:14;
set s0 = (Computation s).0;
A15: s = s0 by AMI_1:def 19;
set s1 = (Computation s).(0+1);
A16: s1.c2 = 2 & s1.n = nn & s1.a = A & s1.b = B
by A4,A5,A14,A15,SCM_1:24;
A17: nn >= 0 by NAT_1:18;
A18: now assume
A19: nn = 0;
then A20: s.(IC s1) = halt SCM by A4,A5,A13,A14,A15,SCM_1:24;
hence s is halting by SCM_1:3;
thus (Result s).b = s1.b by A20,SCM_1:4
.= Fusc N by A3,A16,A19,PRE_FF:20;
hereby assume nn = 0; halt SCM <> n =0_goto il.8 by SCM_1:26;
hence Complexity s = 1 by A4,A5,A15,A20,SCM_1:17;
end;
thus nn>0 implies Complexity s=6 * ([\ log(2, nn) /] + 1)+1 by A19;
end;
now assume A21: nn > 0;
then A22: IC s1 = il.(0+1) by A4,A5,A14,A15,SCM_1:24;
set s2 = (Computation s).(1+1);
A23: IC s2 = il.(1+1) by A6,A22,SCM_1:18;
A24: s2.aux = 2 by A6,A16,A22,SCM_1:18;
A25: s2.c2 = 2 & s2.n = nn & s2.a = A & s2.b = B
by A6,A16,A22,Lm9,SCM_1:18;
set s3 = (Computation s).(2+1);
A26: IC s3 = il.(2+1) by A7,A23,Lm9,SCM_1:22;
A27: s3.n = nn qua Integer div 2 by A7,A23,A24,A25,Lm9,SCM_1:22;
A28: s3.aux = nn qua Integer mod 2 by A7,A23,A24,A25,Lm9,SCM_1:22;
A29: s3.c2 =2 & s3.a =A & s3.b =B by A7,A23,A25,Lm8,Lm9,SCM_1:22;
reconsider nn' = s3.n as 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 qua Integer mod 2 = nn - (nn qua Integer div 2) * 2 by INT_1:def 8;
per cases;
suppose
A31: s3.aux <> 0;
then A32: s3.aux = 1 by A28,PRE_FF:6;
A33: IC s4 = il.(3+1) by A8,A26,A31,SCM_1:24;
A34: s4.c2 = 2 & s4.n = s3.n & s4.a = A & s4.b = B
by A8,A26,A29,SCM_1:24;
A35: IC s5 = il.(4+1) by A9,A33,SCM_1:19;
A36: s5.b = B + A by A9,A33,A34,SCM_1:19;
A37: s5.c2 = 2 & s5.n = s3.n & s5.a = A by A9,A33,A34,Lm8,SCM_1:19;
A38: IC s6 = il.0 by A10,A35,SCM_1:23;
A39: s6.c2 = 2 & s6.n = s3.n & s6.a = A & s6.b = s5.b
by A10,A35,A37,SCM_1:23;
A40: nn = 2 * nn' + 1 by A27,A28,A30,A32,XCMPLX_1:27;
s6.il.0 = n =0_goto il.8 & s6.il.1 = aux := c2 &
s6.il.2 = Divide(n, aux) &
s6.il.3 = aux =0_goto il.6 & s6.il.4 = AddTo(b, a) & s6.il.5 = goto il.0 &
s6.il.6 = AddTo(a, b) & s6.il.7 = goto il.0 & s6.il.8 = halt SCM
by A5,A6,A7,A8,A9,A10,A11,A12,A13,AMI_1:54;
then A41: s6 is State-consisting of 0, 0, 0,
Fusc_Program,
<*2*>^<*nn'*>^<*A*>^<*B+A*>
by A36,A38,A39,Def3,SCM_1:30;
A42: nn' < nn by A40,PRE_FF:19;
Fusc N = A * Fusc nn' + (B+A)*Fusc (nn'+1) by A3,A40,PRE_FF:21;
then A43: s6 is halting &
(Result s6).dl.3 = Fusc N &
(nn' = 0 implies Complexity s6 = 1) &
(nn' > 0 implies Complexity s6 = 6 * ([\ log(2, nn') /] + 1)+1)
by A2,A3,A41,A42;
hence s is halting by SCM_1:27;
thus (Result s).dl.3 = Fusc N by A43,SCM_1:29;
thus nn = 0 implies Complexity s = 1 by A21;
thus nn > 0 implies Complexity s = 6 * ([\ log(2, nn) /] + 1)+1
proof assume nn > 0;
per cases;
suppose nn' = 0;
hence Complexity s = 6 * ([\ log(2, nn) /] + 1)+1 by A27,A28,A30,A32,A43,
Lm1,SCM_1:28;
suppose A44: nn' <> 0;
then A45: nn' > 0 by NAT_1:19;
then reconsider F = [\ log(2, nn') /] as Nat by Lm2;
6 * (F+1)+1 > 0 by A45,Lm2;
hence Complexity s=6 + (6 * (F+1)+1) by A43,A44,NAT_1:19,SCM_1:28
.= 6 * ([\ log(2, nn) /] + 1) + 1 by A40,A45,Lm3;
end;
suppose
A46: s3.aux = 0;
then A47: IC s4 = il.6 by A8,A26,SCM_1:24;
A48: s4.c2 = 2 & s4.n = s3.n & s4.a = A & s4.b = B
by A8,A26,A29,SCM_1:24;
A49: IC s5 = il.(6+1) by A11,A47,SCM_1:19;
A50: s5.a = A + B by A11,A47,A48,SCM_1:19;
A51: s5.c2 = 2 & s5.n = s3.n & s5.b = B by A11,A47,A48,Lm8,SCM_1:19;
A52: IC s6 = il.0 by A12,A49,SCM_1:23;
A53: s6.c2 = 2 & s6.n = s3.n & s6.a = s5.a & s6.b = B
by A12,A49,A51,SCM_1:23;
reconsider nn' = s3.n as Nat by A27,PRE_FF:7;
A54: nn = nn' * 2 + 0 by A27,A28,A30,A46,XCMPLX_1:27
.= 2 * nn';
s6.il.0 = n =0_goto il.8 & s6.il.1 = aux := c2 &
s6.il.2 = Divide(n, aux) &
s6.il.3 = aux =0_goto il.6 & s6.il.4 = AddTo(b, a) & s6.il.5 = goto il.0 &
s6.il.6 = AddTo(a, b) & s6.il.7 = goto il.0 & s6.il.8 = halt SCM
by A5,A6,A7,A8,A9,A10,A11,A12,A13,AMI_1:54;
then A55: s6 is State-consisting of 0, 0, 0,
Fusc_Program,
<*2*>^<*nn'*>^<*A+B*>^<*B*>
by A50,A52,A53,Def3,SCM_1:30;
A56: nn' < nn by A21,A54,PRE_FF:18;
Fusc N = (A+B)*Fusc nn' + B*Fusc (nn'+1) by A3,A54,PRE_FF:22;
then A57: s6 is halting &
(Result s6).dl.3 = Fusc N &
(nn' = 0 implies Complexity s6 = 1) &
(nn' > 0 implies Complexity s6 = 6 * ([\ log(2, nn') /] + 1)+1)
by A2,A3,A55,A56;
hence s is halting by SCM_1:27;
thus (Result s).dl.3 = Fusc N by A57,SCM_1:29;
thus nn = 0 implies Complexity s = 1 by A21;
thus nn > 0 implies Complexity s = 6 * ([\ log(2, nn) /] + 1)+1
proof assume nn > 0;
per cases;
suppose
nn' = 0;
hence thesis by A21,A54;
suppose A58: nn' <> 0;
then A59: nn' > 0 by NAT_1:19;
then reconsider F = [\ log(2, nn') /] as Nat by Lm2;
6 * (F+1)+1 > 0 by A59,Lm2;
hence Complexity s=6 + (6 * (F+1)+1) by A57,A58,NAT_1:19,SCM_1:28
.= 6 * ([\ log(2, nn) /] + 1) + 1 by A54,A59,Lm5;
end;
end;
hence s is halting &
(Result s).dl.3 = Fusc N &
(nn = 0 implies Complexity s = 1) &
(nn > 0 implies Complexity s = 6 * ([\ log(2, nn) /] + 1) + 1)
by A17,A18,REAL_1:def 5;
end;
thus for n being Nat holds P[n] from Comp_Ind ( A1 );
end;
theorem
for N being Nat st N > 0
for s being State-consisting of 0, 0, 0,
Fusc_Program,
<*2*>^<*N*>^<*1*>^<*0*>
holds s is halting &
(Result s).dl.3 = Fusc N &
(N = 0 implies Complexity s = 1) &
(N > 0 implies Complexity s = 6 * ([\ log(2, N) /] + 1)+1)
proof
let N be Nat such that
A1: N > 0;
let S be State-consisting of 0, 0, 0,
Fusc_Program,
<*2*>^<*N*>^<*1*>^<*0*>;
Fusc N = 1 * Fusc N + 0 * Fusc (N+1);
hence thesis by A1,Th5;
end;