environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions ;
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;
registrations XREAL_0, INT_1, AMI_3, ORDINAL1, AFINSQ_1, SCM_1, PBOOLE, COMPOS_0, MEMSTR_0, NAT_1, NEWTON;
constructors HIDDEN, REAL_1, NEWTON, POWER, PRE_FF, SCM_1, ENUMSET1, PRE_POLY;
requirements HIDDEN, REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
equalities ;
expansions ;
Lm1:
0 = [\(log (2,1))/]
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 )
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
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 )
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
Lm6:
for N being Nat st N <> 0 holds
(6 * N) - 4 > 0
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;
Lm17:
for F being NAT -defined the InstructionsF of SCM -valued total Function
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 )
theorem Th4:
for
F being
NAT -defined the
InstructionsF of
SCM -valued total Function st
Fusc_Program c= F holds
for
n,
N,
A,
B being
Element of
NAT for
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 ) )