:: Two Programs for {\bf SCM}. Part II - Proofs
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, CARD_1, INT_1, POWER, SUBSET_1, XXREAL_0, RELAT_1,
ARYTM_3, ARYTM_1, NAT_1, AMI_3, AFINSQ_1, AMI_1, ORDINAL4, GRAPHSP,
SCM_1, FINSEQ_1, MSUALG_1, FUNCT_1, PRE_FF, FSM_1, NEWTON, FIB_FUSC,
EXTPRO_1, PARTFUN1, TARSKI;
notations ENUMSET1, XCMPLX_0, SUBSET_1, ORDINAL1, NUMBERS, INT_1, NAT_1,
NEWTON, POWER, RELAT_1, FUNCT_1, PARTFUN1, AFINSQ_1, FINSEQ_1, MEMSTR_0,
COMPOS_1, EXTPRO_1, SCM_1, AMI_3, PRE_FF, XXREAL_0;
constructors REAL_1, NEWTON, POWER, PRE_FF, SCM_1, ENUMSET1, PRE_POLY;
registrations XREAL_0, INT_1, AMI_3, ORDINAL1, AFINSQ_1, SCM_1, PBOOLE,
COMPOS_0, MEMSTR_0, NAT_1, NEWTON;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems NAT_1, INT_1, POWER, NEWTON, SCM_1, PRE_FF, AMI_3, XREAL_1, XXREAL_0,
ORDINAL1, EXTPRO_1, AFINSQ_1, GRFUNC_1, CARD_1, ENUMSET1, MEMSTR_0;
schemes NAT_1;
begin
Lm1: 0 = [\ log(2, 1) /]
proof
thus 0 = [\ 0 /]
.= [\ log(2, 1) /] by POWER:51;
end;
Lm2: for nn9 being Element of NAT st nn9 > 0 holds
[\ log(2, nn9) /] is Element of NAT & 6 * ([\ log(2, nn9) /] + 1) + 1 > 0
proof
let nn9 be Element of NAT;
assume nn9 > 0;
then
A1: nn9 >= 0+1 by NAT_1:13;
log(2, 1) = 0 by POWER:51;
then log(2, nn9) >= 0 by A1,PRE_FF:10;
then [\ log(2, nn9) /] >= [\ 0 /];
then [\ log(2, nn9) /] >= 0;
then reconsider F = [\ log(2, nn9) /] as Element of NAT by INT_1:3;
F is Element of NAT;
hence [\ log(2, nn9) /] is Element of NAT;
6 * F + 6 * 1 >= 0;
hence thesis;
end;
Lm3: for nn, nn9 being Element of NAT st nn = 2*nn9+1 & nn9 > 0 holds 6+(6*([\
log(2, nn9)/]+1)+1)=6*([\ log(2,nn)/]+1) + 1
proof
let nn, nn9 be Element of NAT such that
A1: nn = 2*nn9+1 & nn9 > 0;
set F = [\ log(2, nn9) /];
thus 6 + (6 * (F+1)+1) = 6 * (1 + (F + 1)) + 1
.= 6 * ([\ log(2, nn) /] + 1) + 1 by A1,PRE_FF:14;
end;
Lm4: for n being Element of 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 Element of NAT;
assume n > 0;
hence log (2,2*n) = log (2,2)+log (2, n) by POWER:53
.= 1+log (2, n) by POWER:52;
hence thesis;
end;
Lm5: for nn, nn9 being Element of NAT st nn = 2*nn9 & nn9 > 0 holds 6+(6*([\
log(2, nn9)/]+1)+1)=6*([\ log(2,nn)/]+1) + 1
proof
let nn, nn9 be Element of NAT such that
A1: nn = 2*nn9 & nn9 > 0;
set F = [\ log(2, nn9) /];
thus 6 + (6 * (F+1)+1) = 6 * (1 + (F + 1)) + 1
.= 6 * (1 + [\ log(2, nn9)+1 /]) + 1 by INT_1:28
.= 6 * ([\ log(2, nn) /] + 1) + 1 by A1,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:6;
reconsider L as Element of NAT by ORDINAL1:def 12;
6 * L + 2 <> 0;
hence thesis by A1;
end;
Lm7: dl.0<>dl.1 by AMI_3:10;
Lm8: dl.0<>dl.2 by AMI_3:10;
Lm9: dl.0<>dl.3 by AMI_3:10;
Lm10: dl.1<>dl.2 by AMI_3:10;
Lm11: dl.1<>dl.3 by AMI_3:10;
Lm12: dl.2<>dl.3 by AMI_3:10;
Lm13: dl.0<>dl.4 by AMI_3:10;
Lm14: dl.1<>dl.4 by AMI_3:10;
Lm15: dl.2<>dl.4 by AMI_3:10;
Lm16: dl.3<>dl.4 by AMI_3:10;
definition
func Fib_Program -> XFinSequence of the InstructionsF of SCM equals
<% dl.1>0_goto 2 %> ^ <% halt SCM %> ^ <% dl.3 := dl.0 %> ^
<% SubFrom(dl.1, dl.0) %> ^ <% dl.1 =0_goto 1 %> ^
<% dl.4 := dl.2 %> ^ <% dl.2 := dl.3 %> ^ <% AddTo(dl.3,dl.4) %> ^
<% SCM-goto 3 %>;
coherence;
end;
reserve F for total
NAT-defined (the InstructionsF of SCM)-valued Function;
Lm17:
for I1, I2, I3, I4, I5, I6, I7, I8, I9 being Instruction of SCM
st
<%I1%>^<%I2%>^<%I3%>^<%I4%>^<%I5%>^<%I6%>^<%I7%>^<%I8%>^<%I9%> c= F
holds
F.0 = I1 & F.1 = I2 & F.2 = I3 & F.3 = I4 & F.4 = I5 & F.5 = I6 & F.6 = I7 &
F.7 = I8 & F.8 = I9
proof
let I1, I2, I3, I4, I5, I6, I7, I8, I9 be Instruction of SCM such that
A1: <%I1%>^<%I2%>^<%I3%>^<%I4%>^<%I5%>^<%I6%>^<%I7%>^<%I8%>^<%I9%> c= F;
set I = <%I1%>^<%I2%>^<%I3%>^<%I4%>^<%I5%>^<%I6%>^<%I7%>^<%I8%>^<%I9%>;
A2: I.2 = I3 & I.3 = I4 by AFINSQ_1:50;
A3: I.6 = I7 & I.7 = I8 by AFINSQ_1:50;
A4: I.4=I5 & I.5 = I6 by AFINSQ_1:50;
A5: I.8 = I9 & len I=9 by AFINSQ_1:50;
len I = 9 by AFINSQ_1:50;
then
A6: 0 in dom I & 1 in dom I & 2 in dom I & 3 in dom I &
4 in dom I & 5 in dom I & 6 in dom I & 7 in dom I &
8 in dom I by CARD_1:57,ENUMSET1:def 7;
I.0 = I1 & I.1 = I2 by AFINSQ_1:50;
hence F.0 = I1 & F.1 = I2 & F.2 = I3 & F.3 = I4 & F.4 = I5 &
F.5 = I6 & F.6 = I7 & F.7 = I8 & F.8 = I9
by A2,A4,A3,A5,A6,A1,GRFUNC_1:2;
end;
theorem
Fib_Program c= F implies
for N being Element of NAT,
s being 0-started State-consisting of <%1,N,0,0%>
holds F halts_on s &
(N = 0 implies LifeSpan(F,s) = 1) &
(N > 0 implies LifeSpan(F,s) = 6 * N - 2) &
(Result(F,s)).dl.3 = Fib N
proof
assume
A1: Fib_Program c= F;
let N be Element of NAT,
s be 0-started State-consisting of <%1,N,0,0%>;
set C1 = dl.0, n = dl.1, FP = dl.2, FC = dl.3, AUX = dl.4;
set L6 = 6, L7 = 7, L8 = 8;
set L0 = 0, L1 = 1, L2 = 2, L3 = 3, L4 = 4, L5 = 5;
A2: IC s = L0 & F.L0 = n >0_goto L2 by A1,Lm17,MEMSTR_0:def 12;
set s1 = Comput(F,s,0+1);
set s0 = Comput(F,s,0);
A3: s = s0 by EXTPRO_1:2;
s.C1 = 1 by SCM_1:1;
then
A4: s1.C1 = 1 by A2,A3,SCM_1:11;
A5: F.L3 = SubFrom(n, C1) by A1,Lm17;
s.FP = 0 by SCM_1:1;
then
A6: s1.FP = 0 by A2,A3,SCM_1:11;
A7: F.L4 = n =0_goto L1 by A1,Lm17;
s.FC = 0 by SCM_1:1;
then
A8: s1.FC = 0 by A2,A3,SCM_1:11;
A9: F.L6 = FP := FC by A1,Lm17;
defpred P[Nat] means $1 < N implies for u being State of SCM st u
= Comput(F,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;
A10: F.L2 = FC := C1 by A1,Lm17;
A11: F.L7 = AddTo(FC, AUX) by A1,Lm17;
A12: F.L8 = SCM-goto L3 by A1,Lm17;
A13: F.L5 = AUX := FP by A1,Lm17;
A14: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A15: k < N implies for u being State of SCM st u = Comput(F,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
A16: k+1 < N;
set b = 6*k+3;
set s5 = Comput(F,s,b+1);
set s6 = Comput(F,s,b+1+1);
set s7 = Comput(F,s,b+1+1+1);
set s8 = Comput(F,s,b+1+1+1+1);
set s9 = Comput(F,s,b+1+1+1+1+1);
set s10 = Comput(F,s,b+1+1+1+1+1+1);
set s4 = Comput(F,s,6*k+3);
A17: IC s4 = L4 by A15,A16,NAT_1:13;
let t be State of SCM;
assume
A18: t = Comput(F,s,6*(k+1)+3);
A19: s4.n = N-1-k by A15,A16,NAT_1:13;
then s4.n <> 0 by A16;
then
A20: IC s5 = (4+1) by A7,A17,SCM_1:10;
then
A21: IC s6 = (5+1) by A13,SCM_1:4;
then
A22: IC s7 = (6+1) by A9,SCM_1:4;
then
A23: IC s8 = (7+1) by A11,SCM_1:5;
then
A24: IC s9 = L3 by A12,SCM_1:9;
then
A25: IC s10 = (3+1) by A5,SCM_1:6;
s4.C1 = 1 by A15,A16,NAT_1:13;
then s5.C1 = 1 by A7,A17,SCM_1:10;
then s6.C1 = 1 by A13,A20,Lm13,SCM_1:4;
then s7.C1 = 1 by A9,A21,Lm8,SCM_1:4;
then s8.C1 = 1 by A11,A22,Lm9,SCM_1:5;
then
A26: s9.C1 = 1 by A12,A23,SCM_1:9;
s4.FC = Fib (k+1) by A15,A16,NAT_1:13;
then s5.FC = Fib (k+1) by A7,A17,SCM_1:10;
then
A27: s6.FC = Fib (k+1) by A13,A20,Lm16,SCM_1:4;
then
A28: s7.FC = Fib (k+1) by A9,A21,Lm12,SCM_1:4;
s4.FP = Fib k by A15,A16,NAT_1:13;
then s5.FP = Fib k by A7,A17,SCM_1:10;
then s6.AUX = Fib k by A13,A20,SCM_1:4;
then
A29: s7.AUX = Fib k by A9,A21,Lm15,SCM_1:4;
s8.FC = s7.AUX + s7.FC by A11,A22,SCM_1:5
.= Fib (k+1+1) by A28,A29,PRE_FF:1;
then
A30: s9.FC = Fib (k+1+1) by A12,A23,SCM_1:9;
s7.FP = Fib (k+1) by A9,A21,A27,SCM_1:4;
then s8.FP = Fib (k+1) by A11,A22,Lm12,SCM_1:5;
then
A31: s9.FP = Fib (k+1) by A12,A23,SCM_1:9;
s5.n = N-1-k by A7,A19,A17,SCM_1:10;
then s6.n = N-1-k by A13,A20,Lm14,SCM_1:4;
then s7.n = N-1-k by A9,A21,Lm10,SCM_1:4;
then s8.n = N-1-k by A11,A22,Lm11,SCM_1:5;
then s9.n = N-1-k by A12,A23,SCM_1:9;
then s10.n = N-1-k - 1 by A5,A24,A26,SCM_1:6;
hence thesis by A5,A18,A24,A26,A31,A30,A25,Lm7,Lm10,Lm11,SCM_1:6;
end;
A32: F.L1 = halt SCM by A1,Lm17;
A33: s.n = N by SCM_1:1;
then
A34: s1.n = N by A2,A3,SCM_1:11;
A35: P[0]
proof
set s3 = Comput(F,s,2+1);
set s2 = Comput(F,s,1+1);
assume 0 < N;
then
A36: IC s1 = L2 by A2,A33,A3,SCM_1:11;
then
A37: s2.FC = 1 & s2.C1 = 1 by A10,A4,A8,SCM_1:4;
let t be State of SCM;
assume
A38: t = Comput(F,s,6*0+3);
A39: s2.n = N & s2.FP = 0 by A10,A34,A6,A36,Lm11,Lm12,SCM_1:4;
A40: IC s2 = (2+1) by A10,A36,SCM_1:4;
then IC s3 = (3+1) by A5,SCM_1:6;
hence thesis by A5,A38,A37,A39,A40,Lm7,Lm10,Lm11,PRE_FF:1,SCM_1:6;
end;
A41: for k being Nat holds P[k] from NAT_1:sch 2(A35, A14);
per cases by NAT_1:6;
suppose
A42: N = 0;
then
A43: F.(IC s1) = halt SCM by A2,A32,A33,A3,SCM_1:11;
hence F halts_on s by EXTPRO_1:30;
hereby
assume N = 0;
halt SCM <> n >0_goto L2 by SCM_1:12;
hence LifeSpan(F,s) = 1 by A2,A3,A43,EXTPRO_1:33;
end;
thus N > 0 implies LifeSpan(F,s) = 6 * N - 2 by A42;
thus thesis by A8,A42,A43,EXTPRO_1:7,PRE_FF:1;
end;
suppose
ex k being Nat st N = k+1;
then consider k being Nat such that
A44: N = k+1;
reconsider k as Element of NAT by ORDINAL1:def 12;
set r = Comput(F,s,6*k+3);
A45: k < N by A44,NAT_1:13;
then
A46: IC r = L4 by A41;
A47: r.FC = Fib (k+1) by A41,A45;
set t = Comput(F,s,6*k+3+1);
r.n = k+(1-1)-k by A41,A44,A45
.= 0;
then
A48: IC t = L1 by A7,A46,SCM_1:10;
hence F halts_on s by A32,EXTPRO_1:30;
thus N = 0 implies LifeSpan(F,s) = 1 by A44;
thus N > 0 implies LifeSpan(F,s) = 6 * N - 2 by A32,A44,A46,A48,EXTPRO_1:33
;
thus (Result(F,s)).FC = t.FC by A32,A48,EXTPRO_1:7
.= Fib N by A7,A44,A47,A46,SCM_1:10;
end;
end;
:: Fusc
definition
let i be Integer;
func Fusc' i -> Element of NAT means
:Def2:
(ex n being Element of NAT st i = n & it = Fusc n) or
i is not Element of NAT & it = 0;
existence
proof
per cases;
suppose
i is Element of NAT;
then reconsider n = i as Element of NAT;
take Fusc n;
thus thesis;
end;
suppose
i is not Element of NAT;
hence thesis;
end;
end;
uniqueness;
end;
definition
func Fusc_Program -> XFinSequence of the InstructionsF of SCM equals
<% dl.1 =0_goto 8 %> ^
<% dl.4 := dl.0 %> ^
<% Divide(dl.1, dl.4) %> ^
<% dl.4 =0_goto 6 %> ^
<% AddTo(dl.3, dl.2) %> ^
<% SCM-goto 0 %> ^
<% AddTo(dl.2, dl.3) %> ^
<% SCM-goto 0 %> ^
<% halt SCM %>;
coherence;
end;
theorem
Fusc_Program c= F implies
for N being Element of NAT st N > 0
for s being 0-started State-consisting of <%2,N,1,0%>
holds F halts_on s &
(Result(F,s)).dl.3 = Fusc N &
LifeSpan(F,s) = 6 * ([\ log(2, N) /] + 1) + 1
proof
set c2 = dl.0, n = dl.1, a = dl.2, b = dl.3, aux = dl.4;
set L6 = 6, L7 = 7, L8 = 8;
set L0 = 0, L1 = 1, L2 = 2, L3 = 3, L4 = 4, L5 = 5;
assume
A1: Fusc_Program c= F;
let N be Element of NAT such that
A2: N > 0;
set k = [\log(2, N)/];
log(2, N) - 1 < k by INT_1:def 6;
then
A3: log(2, N) < k+1 by XREAL_1:19;
N >= 0+1 by A2,NAT_1:13;
then log (2, N) >= log (2, 1) by PRE_FF:10;
then log (2, N) >= 0 by POWER:51;
then k+1 > 0;
then reconsider k as Element of NAT by INT_1:3,7;
2 to_power (k+1) > 2 to_power log(2, N) by A3,POWER:39;
then 2 to_power (k+1) > N by A2,POWER:def 3;
then
A4: 2 |^ (k+1) > N by POWER:41;
let S be 0-started State-consisting of <%2,N,1,0%>;
consider s being State of SCM such that
A5: s = S;
defpred P[Nat] means $1 <= log(2, N) + 1 implies for u being
State of SCM st u = Comput(F,s,6*$1) holds IC u = L0 & u.c2 = 2
& u.n = N
qua Integer div (2 |^ $1) & u.n is Element of NAT & Fusc N = u.a*Fusc' u.n + u.
b*Fusc' (u.n+1);
A6: F.L0 = n =0_goto L8 by A1,Lm17;
A7: F.L7 = SCM-goto L0 by A1,Lm17;
A8: F.L1 = aux := c2 by A1,Lm17;
A9: F.L4 = AddTo(b, a) by A1,Lm17;
A10: F.L2 = Divide(n, aux) by A1,Lm17;
A11: F.L6 = AddTo(a, b) by A1,Lm17;
A12: F.L3 = aux =0_goto L6 by A1,Lm17;
A13: F.L5 = SCM-goto L0 by A1,Lm17;
A14: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A15: k <= log(2, N) + 1 implies for u being State of SCM st u =
Comput(F,s,6*k) holds IC u = L0 & u.c2 = 2 & u.n = N qua Integer
div (2 |^ k
) & u.n is Element of NAT & Fusc N = u.a*Fusc' u.n + u.b*Fusc' (u.n+1);
set t = 6*k;
set t0 = Comput(F,s,t);
assume
A16: k+1 <= log(2, N) + 1;
then k <= log(2, N) by XREAL_1:6;
then 2 to_power k <= 2 to_power log(2, N) by PRE_FF:8;
then 2 to_power k <= N by A2,POWER:def 3;
then
A17: 2 |^ k <= N by POWER:41;
A18: k <= k+1 by NAT_1:11;
then
A19: t0.n is Element of NAT by A15,A16,XXREAL_0:2;
A20: t0.n = N qua Integer div (2 |^ k) by A15,A16,A18,XXREAL_0:2;
A21: IC t0 = L0 by A15,A16,A18,XXREAL_0:2;
set t3 = Comput(F,s,t+3);
set t2 = Comput(F,s,t+2);
set t1 = Comput(F,s,t+1);
A22: t+1+1 = t + 2;
(2 |^ k) > 0 by NEWTON:83;
then t0.n <> 0 by A20,A17,PRE_FF:3;
then
A23: IC t1 = (0+1) by A6,A21,SCM_1:10;
then
A24: IC t2 = (1+1) by A8,A22,SCM_1:4;
A25: t+2+1 = t+3;
then
A26: IC t3 = (2+1) by A10,A24,Lm14,SCM_1:8;
t1.n = t0.n by A6,A21,SCM_1:10;
then
A27: t2.n = t0.n by A8,A23,A22,Lm14,SCM_1:4;
A28: t0.n mod 2 = t0.n - (t0.n div 2)*2 by INT_1:def 10;
let u be State of SCM;
assume
A29: u = Comput(F,s,6*(k+1));
t0.c2 = 2 by A15,A16,A18,XXREAL_0:2;
then
A30: t1.c2 = 2 by A6,A21,SCM_1:10;
then t2.c2 = 2 by A8,A23,A22,Lm13,SCM_1:4;
then
A31: t3.c2 = 2 by A10,A24,A25,Lm7,Lm13,Lm14,SCM_1:8;
A32: t2.aux = 2 by A8,A23,A30,A22,SCM_1:4;
then
A33: t3.n = t0.n div 2 by A10,A24,A27,A25,Lm14,SCM_1:8;
then
A34: t3.n = N qua Integer div (2|^k)*2 by A20,PRE_FF:5
.= N qua Integer div (2|^(k+1)) by NEWTON:6;
A35: t3.aux = t0.n mod 2 by A10,A24,A32,A27,A25,Lm14,SCM_1:8;
set t6 = Comput(F,s,t+6);
set t5 = Comput(F,s,t+5);
set t4 = Comput(F,s,t+4);
A36: t+3+1 = t+4;
t1.b = t0.b by A6,A21,SCM_1:10;
then t2.b = t0.b by A8,A23,A22,Lm16,SCM_1:4;
then
A37: t3.b = t0.b by A10,A24,A25,Lm11,Lm14,Lm16,SCM_1:8;
A38: t+5+1 = t+6;
t1.a = t0.a by A6,A21,SCM_1:10;
then t2.a = t0.a by A8,A23,A22,Lm15,SCM_1:4;
then
A39: t3.a = t0.a by A10,A24,A25,Lm10,Lm14,Lm15,SCM_1:8;
A40: t+4+1 = t+5;
per cases;
suppose
A41: t3.aux <> 0;
reconsider ta = t0.a, tb = t0.b as Integer;
A42: t4.a = t0.a by A12,A26,A39,A36,SCM_1:10;
A43: IC t4 = (3+1) by A12,A26,A36,A41,SCM_1:10;
then
A44: IC t5 = (4+1) by A9,A40,SCM_1:5;
t4.n = t3.n by A12,A26,A36,SCM_1:10;
then
A45: t5.n = t3.n by A9,A40,A43,Lm11,SCM_1:5;
then
A46: t6.n = t3.n by A13,A38,A44,SCM_1:9;
then reconsider un = u.n, tn = t0.n as Element of NAT by A29,A19,A33,
PRE_FF:7;
A47: tn = (t0.n div 2)*2 + (t0.n mod 2) by A28
.= 2 * un + 1 by A29,A33,A35,A41,A46,PRE_FF:6;
then
A48: tn+1 = 2*(un+1);
t4.c2 = 2 by A12,A26,A31,A36,SCM_1:10;
then t5.c2 = 2 by A9,A40,A43,Lm9,SCM_1:5;
hence IC u = L0 & u.c2 = 2 & u.n = N qua Integer div (2 |^ (k+1)) by A13
,A29,A34,A38,A44,A45,SCM_1:9;
thus u.n is Element of NAT by A29,A19,A33,A46,PRE_FF:7;
A49: Fusc' (t0.n+1) = Fusc (tn+1) by Def2
.= Fusc (un+1) by A48,PRE_FF:15
.= Fusc' (u.n+1) by Def2;
t4.b = t0.b by A12,A26,A37,A36,SCM_1:10;
then t5.b = t0.b + t0.a by A9,A40,A43,A42,SCM_1:5;
then
A50: t6.b = t0.b+t0.a by A13,A38,A44,SCM_1:9;
A51: Fusc' t0.n = Fusc tn by Def2
.= Fusc un + Fusc (un+1) by A47,PRE_FF:15
.= Fusc' u.n + Fusc (un+1) by Def2
.= Fusc' u.n + Fusc' (u.n+1) by Def2;
reconsider un = u.n, tn = t0.n as Integer;
t5.a = t0.a by A9,A40,A43,A42,Lm12,SCM_1:5;
then t6.a = t0.a by A13,A38,A44,SCM_1:9;
then (ta * Fusc' tn) + (tb * Fusc' (tn+1)) = (u.a * Fusc' un) + (u.b) *
Fusc' (un+1) by A29,A50,A51,A49;
hence thesis by A15,A16,A18,XXREAL_0:2;
end;
suppose
A52: t3.aux = 0;
then
A53: IC t4 = 6 by A12,A26,A36,SCM_1:10;
then
A54: IC t5 = (6+1) by A11,A40,SCM_1:5;
t4.n = t3.n by A12,A26,A36,SCM_1:10;
then t5.n = t3.n by A11,A40,A53,Lm10,SCM_1:5;
then
A55: t6.n = t3.n by A7,A38,A54,SCM_1:9;
then reconsider un = u.n, tn = t0.n as Element of NAT by A29,A19,A33,
PRE_FF:7;
A56: Fusc' (t0.n+1) = Fusc (tn+1) by Def2
.= Fusc un + Fusc (un+1) by A29,A33,A35,A28,A52,A55,PRE_FF:15
.= Fusc un + Fusc' (u.n+1) by Def2
.= Fusc' u.n + Fusc' (u.n+1) by Def2;
A57: t4.b = t0.b by A12,A26,A37,A36,SCM_1:10;
then t5.b = t0.b by A11,A40,A53,Lm12,SCM_1:5;
then
A58: t6.b = t0.b by A7,A38,A54,SCM_1:9;
t4.c2 = 2 by A12,A26,A31,A36,SCM_1:10;
then t5.c2 = 2 by A11,A40,A53,Lm8,SCM_1:5;
hence IC u = L0 & u.c2 = 2 & u.n = N qua Integer div (2 |^ (k+1)) & u.n
is Element of NAT by A7,A29,A19,A33,A34,A38,A54,A55,PRE_FF:7,SCM_1:9;
A59: Fusc' t0.n = Fusc tn by Def2
.= Fusc un by A29,A33,A35,A28,A52,A55,PRE_FF:15
.= Fusc' u.n by Def2;
t4.a = t0.a by A12,A26,A39,A36,SCM_1:10;
then t5.a = t0.a + t0.b by A11,A40,A53,A57,SCM_1:5;
then
A60: t6.a = t0.a+t0.b by A7,A38,A54,SCM_1:9;
reconsider un = u.n, tn = t0.n, ta = t0.a, tb = t0.b as Integer;
(ta * Fusc' tn) + (tb * Fusc' (tn+1)) = (ta+tb) * Fusc' un + tb *
Fusc' (un+1) by A59,A56;
hence thesis by A15,A16,A29,A18,A60,A58,XXREAL_0:2;
end;
end;
set h = Comput(F,s,6*(k+1)+1);
set u = Comput(F,s,6*(k+1));
A61: s.n = N by A5,SCM_1:1;
A62: s.a = 1 & s.b = 0 by A5,SCM_1:1;
A63: P[0]
proof
assume 0 <= log(2, N) + 1;
let u be State of SCM;
assume u = Comput(F,s,6*0);
then
A64: u = s by EXTPRO_1:2;
hence IC u = L0 & u.c2 = 2 by A5,MEMSTR_0:def 12,SCM_1:1;
thus u.n = N qua Integer div 1 by A61,A64
.= N qua Integer div (2 |^ 0) by NEWTON:4;
thus u.n is Element of NAT by A5,A64,SCM_1:1;
thus thesis by A61,A62,A64,Def2;
end;
A65: for k being Nat holds P[k] from NAT_1:sch 2( A63, A14 );
[\log(2, N)/] <= log(2, N) by INT_1:def 6;
then
A66: k+1 <= log(2, N)+1 by XREAL_1:6;
then
A67: Fusc N = u.a*Fusc' u.n + u.b*Fusc' (u.n+1) by A65;
A68: IC u = L0 by A65,A66;
then
A69: h.b = u.b by A6,SCM_1:10;
u.n = N qua Integer div (2 |^ (k+1)) by A65,A66;
then
A70: u.n = 0 by A4,PRE_FF:4;
then
A71: IC h = L8 by A6,A68,SCM_1:10;
A72: F.IC u<>halt SCM by A6,A68,SCM_1:12;
A73: F.L8 = halt SCM by A1,Lm17;
hence F halts_on S by A5,A71,EXTPRO_1:30;
u.a*Fusc' u.n + u.b*Fusc' (u.n+1) = u.a * 0 + u.b * Fusc' (u.n+1) by A70,Def2
,PRE_FF:15
.= u.b * Fusc (0+1) by A70,Def2
.= u.b by PRE_FF:15;
hence (Result(F,S)).dl.3 = Fusc N by A5,A73,A67,A71,A69,EXTPRO_1:7;
F.IC h=halt SCM by A71,A1,Lm17;
hence thesis by A5,A72,EXTPRO_1:33;
end;
theorem
Fib_Program c= F implies
for N being Nat, k, Fk, Fk1 being Nat,
s being 3-started State-consisting of
<% 1, N, Fk, Fk1 %> st N > 0 & Fk = Fib k &
Fk1 = Fib (k+1) holds F halts_on s &
LifeSpan(F,s) = 6 * N - 4 &
ex m being Element of NAT st m = k+N-1 &
(Result(F,s)).dl.2 = Fib m &
Result(F, s).dl.3 = Fib (m+1)
proof
assume
A1: Fib_Program c= F;
defpred P[Nat] means for k, Fk, Fk1 be Nat,
s be 3-started State-consisting of <% 1, $1, Fk, Fk1 %>
st $1 > 0 & Fk = Fib k & Fk1 = Fib (k+1) holds F halts_on s &
LifeSpan(F,s) = 6 *
$1 - 4 & ex m being Element of NAT st m = k+$1-1 & (Result(F,s)).
dl.2 = Fib m & (
Result(F,s)).dl.3 = Fib (m+1);
A2: for N be Nat st P[N] holds P[N+1]
proof
set C1 = dl.0, n = dl.1, FP = dl.2, FC = dl.3, AUX = dl.4;
let N be Nat;
assume
A3: P[N];
let k, Fk, Fk1 be Nat,
s be 3-started State-consisting of <% 1, N+1, Fk, Fk1 %>;
assume that
(N+1) > 0 and
A4: Fk = Fib k and
A5: Fk1 = Fib (k+1);
A6: F.3 = SubFrom(n, C1) by A1,Lm17;
set s0 = Comput(F,s,0);
set s1 = Comput(F,s,0+1);
A7: F.1 = halt SCM by A1,Lm17;
A8: IC s = 3 & s = s0 by EXTPRO_1:2,MEMSTR_0:def 12;
then
A9: IC s1 = (3+1) by A6,SCM_1:6
.= 4;
set s2 = Comput(F,s,1+1);
A10: F.4 = n =0_goto 1 by A1,Lm17;
s.FC = Fk1 by SCM_1:1;
then s1.FC=Fk1 by A6,A8,Lm11,SCM_1:6;
then
A11: s2.FC=Fk1 by A10,A9,SCM_1:10;
A12: F.7 = AddTo(FC, AUX) by A1,Lm17;
s.FP = Fk by SCM_1:1;
then s1.FP=Fk by A6,A8,Lm10,SCM_1:6;
then
A13: s2.FP=Fk by A10,A9,SCM_1:10;
A14: F.6 = FP := FC by A1,Lm17;
A15: s.C1 = 1 by SCM_1:1;
then s1.C1=1 by A6,A8,Lm7,SCM_1:6;
then
A16: s2.C1=1 by A10,A9,SCM_1:10;
s.n = N+1 by SCM_1:1;
then
A17: s1.n = (N+1)-1 by A6,A15,A8,SCM_1:6
.= N;
then
A18: s2.n=N by A10,A9,SCM_1:10;
A19: F.5 = AUX := FP by A1,Lm17;
A20: F.8 = SCM-goto 3 by A1,Lm17;
per cases;
suppose
A21: N = 0;
then
A22: F.IC s2 = halt SCM by A7,A10,A17,A9,SCM_1:10;
hence F halts_on s by EXTPRO_1:30;
F.IC s1 <> halt SCM by A10,A9,SCM_1:12;
hence LifeSpan(F,s) = 6 * (N+1) - 4 by A21,A22,EXTPRO_1:32;
reconsider m = k as Element of NAT by ORDINAL1:def 12;
take m;
thus m = k+(N+1)-1 by A21;
thus thesis by A4,A5,A13,A11,A22,EXTPRO_1:7;
end;
suppose
A23: N > 0;
then
A24: 6 * N - 4 > 0 by Lm6;
set Fk2 = Fib (k+1+1);
set s6 = Comput(F,s,5+1);
set s5 = Comput(F,s,4+1);
set s4 = Comput(F,s,3+1);
set s3 = Comput(F,s,2+1);
A25: IC s2 = (4+1) by A10,A17,A9,A23,SCM_1:10;
then
A26: IC s3 = (5+1) by A19,SCM_1:4;
then
A27: IC s4 = (6+1) by A14,SCM_1:4;
then
A28: IC s5 = (7+1) by A12,SCM_1:5;
A29: s3.FC = Fib (k+1) by A5,A19,A11,A25,Lm16,SCM_1:4;
then
A30: s4.FC = Fib (k+1) by A14,A26,Lm12,SCM_1:4;
s4.FP = Fib (k+1) by A14,A26,A29,SCM_1:4;
then s5.FP = Fib (k+1) by A12,A27,Lm12,SCM_1:5;
then
A31: s6.FP = Fib (k+1) by A20,A28,SCM_1:9;
s3.C1 = 1 by A19,A16,A25,Lm13,SCM_1:4;
then s4.C1 = 1 by A14,A26,Lm8,SCM_1:4;
then s5.C1 = 1 by A12,A27,Lm9,SCM_1:5;
then
A32: s6.C1 = 1 by A20,A28,SCM_1:9;
s3.AUX = Fib k by A4,A19,A13,A25,SCM_1:4;
then
A33: s4.AUX = Fib k by A14,A26,Lm15,SCM_1:4;
s5.FC = s4.AUX + s4.FC by A12,A27,SCM_1:5
.= Fib (k+1+1) by A30,A33,PRE_FF:1;
then
A34: s6.FC = Fib (k+1+1) by A20,A28,SCM_1:9;
s3.n = N by A19,A18,A25,Lm14,SCM_1:4;
then s4.n = N by A14,A26,Lm10,SCM_1:4;
then s5.n = N by A12,A27,Lm11,SCM_1:5;
then
A35: s6.n = N by A20,A28,SCM_1:9;
IC s6 = 3 by A20,A28,SCM_1:9;
then
A36: s6 is 3-started State-consisting of <%1,N,Fk1,Fk2%>
by A5,A32,A35,A31,A34,MEMSTR_0:def 12,SCM_1:13;
then consider m being Element of NAT such that
A37: m = (k+1)+N-1 and
(Result(F,s6)).dl.2 = Fib m and
(Result(F,s6)).dl.3 = Fib (m+1) by A3,A5,A23;
F halts_on s6 by A3,A5,A23,A36;
hence F halts_on s by EXTPRO_1:22;
LifeSpan(F,s6) = 6 * N - 4 by A3,A5,A23,A36;
hence LifeSpan(F,s) = 6 + (6 * N - 4) by A3,A5,A23,A36,A24,EXTPRO_1:34
.= 6 * (N+1) - 4;
take m;
thus m = k+(N+1)-1 by A37;
ex m being Element of NAT st m = (k+1)+N-1 & (Result(F,s6))
.dl.2 = Fib
m & (Result(F,s6)).dl.3 = Fib (m+1) by A3,A5,A23,A36;
hence thesis by A37,A3,A5,A23,A36,EXTPRO_1:35;
end;
end;
A38: P[0];
thus for N be Nat holds P[N] from NAT_1:sch 2( A38, A2 );
end;
theorem Th4:
Fusc_Program c= F implies
for n being Element of NAT, N, A, B being Element of NAT,
s being 0-started State-consisting of <%2,n,A,B%>
st N > 0 &
Fusc N = A * Fusc n + B * Fusc (n+1)
holds F halts_on s &
(Result(F,s)).dl.3 = Fusc N &
(n = 0 implies LifeSpan(F,s) = 1) &
(n > 0 implies LifeSpan(F,s) = 6 * ([\log(2, n) /] + 1) + 1)
proof
assume
A1: Fusc_Program c= F;
defpred P[Nat] means for N, A, B being Element of NAT, s being
0-started State-consisting of <%2,$1,A,B%>
st N > 0 &
Fusc N = A * Fusc $1 + B * Fusc ($1+1) holds F halts_on s &
(Result(F,s)).dl.3 =
Fusc N & ($1 = 0 implies LifeSpan(F,s) = 1) & ($1 > 0 implies
LifeSpan(F,s) = 6 * ([\
log(2, $1) /] + 1)+1);
A2: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
proof
set c2 = dl.0, n = dl.1, a = dl.2, b = dl.3, aux = dl.4;
let nn be Nat;
assume
A3: for n9 being Nat st n9 < nn holds for N, A, B being Element of NAT
, s being 0-started State-consisting of <%2,n9,A,B%>
st N > 0 & Fusc N = A * Fusc n9 + B * Fusc (n9+1)
holds F halts_on s & Result(F,
s).dl.3 = Fusc N & (n9 = 0 implies LifeSpan(F,s) = 1) & (n9 > 0
implies LifeSpan(F,s)
= 6 * ([\ log(2, n9) /] + 1)+1);
reconsider n2 = nn as Element of NAT by ORDINAL1:def 12;
let N, A, B be Element of NAT,
s be 0-started State-consisting of <%2,nn,A,B%>;
assume that
A4: N > 0 and
A5: Fusc N = A * Fusc nn + B * Fusc (nn+1);
A6: s.n = nn by SCM_1:1;
set s0 = Comput(F,s,0);
A7: F.0 = n =0_goto 8 by A1,Lm17;
set s1 = Comput(F,s,0+1);
A8: F.8 = halt SCM by A1,Lm17;
A9: F.3 = aux =0_goto 6 by A1,Lm17;
A10: IC s = 0 & s = s0 by EXTPRO_1:2,MEMSTR_0:def 12;
s.a = A by SCM_1:1;
then
A11: s1.a = A by A7,A10,SCM_1:10;
s.c2 = 2 by SCM_1:1;
then
A12: s1.c2 = 2 by A7,A10,SCM_1:10;
A13: F.2 = Divide(n, aux) by A1,Lm17;
s.b = B by SCM_1:1;
then
A14: s1.b = B by A7,A10,SCM_1:10;
A15: now
assume
A16: nn = 0;
then
A17: F.IC s1 = halt SCM by A7,A8,A6,A10,SCM_1:10;
hence F halts_on s by EXTPRO_1:30;
thus (Result(F,s)).b = s1.b by A17,EXTPRO_1:7
.= Fusc N by A5,A14,A16,PRE_FF:18;
hereby
assume nn = 0;
halt SCM <> n =0_goto 8 by SCM_1:12;
hence LifeSpan(F,s) = 1 by A7,A10,A17,EXTPRO_1:33;
end;
thus nn>0 implies LifeSpan(F,s)=6 * ([\ log(2, nn) /] + 1)+1
by A16;
end;
A18: F.1 = aux := c2 by A1,Lm17;
A19: F.5 = SCM-goto 0 by A1,Lm17;
A20: F.4 = AddTo(b, a) by A1,Lm17;
A21: F.7 = SCM-goto 0 by A1,Lm17;
A22: F.6 = AddTo(a, b) by A1,Lm17;
A23: s1.n = nn by A7,A6,A10,SCM_1:10;
A24: now
set s6 = Comput(F,s,5+1);
set s5 = Comput(F,s,4+1);
set s4 = Comput(F,s,3+1);
set s3 = Comput(F,s,2+1);
set s2 = Comput(F,s,1+1);
A25: nn mod 2 = nn - (nn div 2) * 2 by INT_1:def 10;
assume
A26: nn > 0;
then
A27: IC s1 = (0+1) by A7,A6,A10,SCM_1:10;
then
A28: IC s2 = (1+1) by A18,SCM_1:4;
then
A29: IC s3 = (2+1) by A13,Lm14,SCM_1:8;
s2.a = A by A18,A11,A27,Lm15,SCM_1:4;
then
A30: s3.a =A by A13,A28,Lm10,Lm14,Lm15,SCM_1:8;
s2.c2 = 2 by A18,A12,A27,Lm13,SCM_1:4;
then
A31: s3.c2 =2 by A13,A28,Lm7,Lm13,Lm14,SCM_1:8;
s2.b = B by A18,A14,A27,Lm16,SCM_1:4;
then
A32: s3.b =B by A13,A28,Lm11,Lm14,Lm16,SCM_1:8;
A33: s2.aux = 2 & s2.n = nn by A18,A12,A23,A27,Lm14,SCM_1:4;
then
A34: s3.n = n2 div 2 by A13,A28,Lm14,SCM_1:8;
then reconsider nn9 = s3.n as Element of NAT by PRE_FF:7;
A35: s3.aux = nn mod 2 by A13,A28,A33,Lm14,SCM_1:8;
per cases;
suppose
A36: s3.aux <> 0;
then
A37: IC s4 = (3+1) by A9,A29,SCM_1:10;
then
A38: IC s5 = (4+1) by A20,SCM_1:5;
A39: s4.a = A by A9,A29,A30,SCM_1:10;
then s5.a = A by A20,A37,Lm12,SCM_1:5;
then
A40: s6.a = A by A19,A38,SCM_1:9;
s4.b = B by A9,A29,A32,SCM_1:10;
then
A41: s5.b = B + A by A20,A37,A39,SCM_1:5;
A42: s3.aux = 1 by A35,A36,PRE_FF:6;
s4.n = s3.n by A9,A29,SCM_1:10;
then s5.n = s3.n by A20,A37,Lm11,SCM_1:5;
then
A43: s6.n = s3.n by A19,A38,SCM_1:9;
s4.c2 = 2 by A9,A29,A31,SCM_1:10;
then s5.c2 = 2 by A20,A37,Lm9,SCM_1:5;
then
A44: s6.c2 = 2 by A19,A38,SCM_1:9;
IC s6 = 0 & s6.b = s5.b by A19,A38,SCM_1:9;
then
A45: s6 is 0-started State-consisting of <%2,nn9,A,B+A%>
by A41,A44,A43,A40,MEMSTR_0:def 12,SCM_1:13;
A46: nn mod 2 + (nn div 2) * 2 = nn by A25;
then
A47: nn9 < nn by A34,A35,A42,PRE_FF:17;
A48: Fusc N = A * Fusc nn9 + (B+A)*Fusc (nn9+1) by A5,A34,A35,A42,A46,
PRE_FF:19;
then
A49: nn9 > 0 implies LifeSpan(F,s6) = 6 * ([\ log(2, nn9) /] +
1)+1 by A3,A4,A45,A47;
A50: F halts_on s6 by A3,A4,A45,A47,A48;
hence F halts_on s by EXTPRO_1:22;
(Result(F,s6)).dl.3 = Fusc N by A3,A4,A45,A47,A48;
hence (Result(F,s)).dl.3 = Fusc N by A50,EXTPRO_1:35;
thus nn = 0 implies LifeSpan(F,s) = 1 by A26;
A51: nn9 = 0 implies LifeSpan(F,s6) = 1 by A3,A4,A34,A35,A25,A42,A45,A48;
thus nn > 0 implies LifeSpan(F,s) = 6 * ([\ log(2, nn) /]
+ 1)+1
proof
assume nn > 0;
per cases;
suppose
nn9 = 0;
hence thesis by A34,A35,A25,A42,A50,A51,Lm1,EXTPRO_1:34;
end;
suppose
A52: nn9 <> 0;
then
A53: nn9 > 0;
then reconsider m = [\ log(2, nn9) /] as Element of NAT by Lm2;
thus LifeSpan(F,s)=6 + (6 * (m+1)+1)
by A50,A49,A52,EXTPRO_1:34
.= 6 * ([\ log(2, nn) /] + 1) + 1 by A34,A35,A42,A46,A53,Lm3;
end;
end;
end;
suppose
A54: s3.aux = 0;
then
A55: IC s4 = 6 by A9,A29,SCM_1:10;
then
A56: IC s5 = (6+1) by A22,SCM_1:5;
s4.c2 = 2 by A9,A29,A31,SCM_1:10;
then s5.c2 = 2 by A22,A55,Lm8,SCM_1:5;
then
A57: s6.c2 = 2 by A21,A56,SCM_1:9;
A58: s4.b = B by A9,A29,A32,SCM_1:10;
then s5.b = B by A22,A55,Lm12,SCM_1:5;
then
A59: s6.b = B by A21,A56,SCM_1:9;
s4.n = s3.n by A9,A29,SCM_1:10;
then s5.n = s3.n by A22,A55,Lm10,SCM_1:5;
then
A60: s6.n = s3.n by A21,A56,SCM_1:9;
s4.a = A by A9,A29,A30,SCM_1:10;
then
A61: s5.a = A + B by A22,A55,A58,SCM_1:5;
reconsider nn9 = s3.n as Element of NAT by A34,PRE_FF:7;
IC s6 = 0 & s6.a = s5.a by A21,A56,SCM_1:9;
then
A62: s6 is 0-started State-consisting of <%2,nn9,A+B,B%>
by A61,A57,A60,A59,MEMSTR_0:def 12,SCM_1:13;
A63: nn9 < nn & Fusc N = (A+B)*Fusc nn9 + B*Fusc (nn9+1) by A5,A26,A34,A35
,A25,A54,PRE_FF:16,20;
then
A64: F halts_on s6 by A3,A4,A62;
hence F halts_on s by EXTPRO_1:22;
(Result(F,s6)).dl.3 = Fusc N by A3,A4,A62,A63;
hence (Result(F,s)).dl.3 = Fusc N by A64,EXTPRO_1:35;
thus nn = 0 implies LifeSpan(F,s) = 1 by A26;
A65: nn9 > 0 implies LifeSpan(F,s6) = 6 * ([\ log(2, nn9) /] +
1)+1 by A3,A4,A62,A63;
thus nn > 0 implies LifeSpan(F,s) = 6 * ([\ log(2, nn) /]
+ 1)+1
proof
assume nn > 0;
per cases;
suppose
nn9 = 0;
hence thesis by A13,A26,A28,A33,A34,A25,A54,Lm14,SCM_1:8;
end;
suppose
A66: nn9 <> 0;
then
A67: nn9 > 0;
then reconsider m = [\ log(2, nn9) /] as Element of NAT by Lm2;
thus LifeSpan(F,s)=6 + (6 * (m+1)+1) by A64,A65,A66,EXTPRO_1:34
.= 6 * ([\ log(2, nn) /] + 1) + 1 by A34,A35,A25,A54,A67,Lm5;
end;
end;
end;
end;
thus thesis by A15,A24;
end;
for n being Nat holds P[n] from NAT_1:sch 4 ( A2 );
hence thesis;
end;
theorem
Fusc_Program c= F implies
for N being Element of NAT st N > 0
for s being 0-started State-consisting of <%2,N,1,0%>
holds F halts_on s &
Result(F ,s).dl.3 = Fusc N &
(N = 0 implies LifeSpan(F,s) = 1) &
(N > 0 implies LifeSpan(F,s) = 6 * ([\ log(2, N) /] + 1)+1)
proof
assume
A1: Fusc_Program c= F;
let N be Element of NAT;
Fusc N = 1 * Fusc N + 0 * Fusc (N+1);
hence thesis by A1,Th4;
end;