:: Two Programs for {\bf SCM}. Part II - Proofs
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received October 8, 1993
:: Copyright (c) 1993-2021 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;
begin
definition
func Fib_Program -> XFinSequence of the InstructionsF of SCM equals
:: FIB_FUSC:def 1
<% 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 %>;
end;
reserve F for total
NAT-defined (the InstructionsF of SCM)-valued Function;
theorem :: FIB_FUSC:1
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;
:: Fusc
definition
let i be Integer;
func Fusc' i -> Element of NAT means
:: FIB_FUSC:def 2
(ex n being Element of NAT st i = n & it = Fusc n) or
i is not Element of NAT & it = 0;
end;
definition
func Fusc_Program -> XFinSequence of the InstructionsF of SCM equals
:: FIB_FUSC:def 3
<% 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 %>;
end;
theorem :: FIB_FUSC:2
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;
theorem :: FIB_FUSC:3
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);
theorem :: FIB_FUSC:4
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);
theorem :: FIB_FUSC:5
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);