Functional variant of Polynomial Analogue
of Gandy’s Fixed Point Theorem

Andrey Nechesov

Sobolev Insitute of Mathematics, Novosibirsk

nechesoff@gmail.com

Abstact In this work, a functional variant of the polynomial analogue of the classical Gandy’s fixed point theorem is obtained. Sufficient conditions have been found to ensure that the complexity of the recursive function does not go beyond the polynomial.

Introduction In 2021, we proved a polynomial analogue of the classical Gandy’s fixed point theorem [1]. This became an important impetus for the construction of p-complete programming languages. And such a language was first built by us in 2022. The main result of that work was: a solution of the problem P=L𝑃𝐿P=Litalic_P = italic_L. [2] Next are the followers of the works on building a new high-level language and the idea of building a general programming methodology. But there was one gap in our research: classes of recursive functions whose complexity was polynomial were not described.

In this work we found sufficient conditions for such functions. In many ways, the main ideas of this work are similar to the ideas that we used in the proof of the polynomial analogue of Gandy’s fixed point theorem. But there are also striking differences. Functions, as such, differ quite strongly from predicates precisely in the multitude of their values. If a predicate is either true or false, then a function can generally take on a variety of values.

Moreover, even if there are not many values, but there is recursion and simple multiplication, then powers and factorials may arise during the calculations, which, of course, can violate the polynomial computational complexity of this function. Therefore, finding these restrictions on recursive functions that would be soft enough for the class of functions to be large, and at the same time tough enough not to go beyond polynomiality, has been a problem for us for the last 3 years, after the proof of the polynomial analogue Gandy’s fixed point theorem in the case of predicate extensions.

In this work, we will inductively expand the function itself, and not the truth set of the predicate, which fundamentally distinguishes these two approaches.

Let <HW(𝔐𝔐\mathfrak{M}fraktur_M),σ𝜎\sigmaitalic_σ> – p-computable hereditary finite list superstructure from [1].
Let f1,,fnsubscript𝑓1subscript𝑓𝑛f_{1},\dots,f_{n}italic_f start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT – p-computable functions and all fisubscript𝑓𝑖f_{i}italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT in the signature σ𝜎\sigmaitalic_σ. Then we can define a new finite or countable generative family of the terms Tisubscript𝑇𝑖T_{i}italic_T start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT of the signature σ𝜎\sigmaitalic_σ for each fisubscript𝑓𝑖f_{i}italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT:

Ti={tj(x1,,xkj)|jN},i[1,,n]formulae-sequencesubscript𝑇𝑖conditional-setsubscript𝑡𝑗subscript𝑥1subscript𝑥subscript𝑘𝑗𝑗𝑁𝑖1𝑛T_{i}=\{t_{j}(x_{1},\dots,x_{k_{j}})\ |\ j\in N\},\ i\in[1,\dots,n]italic_T start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT = { italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_x start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_x start_POSTSUBSCRIPT italic_k start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT end_POSTSUBSCRIPT ) | italic_j ∈ italic_N } , italic_i ∈ [ 1 , … , italic_n ] (1)

by default we assume that any fjsubscript𝑓𝑗f_{j}italic_f start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT can be included in any term tksubscript𝑡𝑘t_{k}italic_t start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT of any family Tisubscript𝑇𝑖T_{i}italic_T start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT.

Let also for each family of terms Tisubscript𝑇𝑖T_{i}italic_T start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT is defined p-computable function γisubscript𝛾𝑖\gamma_{i}italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT:

γi:HW(M)Ti{false}:subscript𝛾𝑖𝐻𝑊𝑀subscript𝑇𝑖𝑓𝑎𝑙𝑠𝑒\gamma_{i}:HW(M)\to T_{i}\cup\{false\}italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT : italic_H italic_W ( italic_M ) → italic_T start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∪ { italic_f italic_a italic_l italic_s italic_e } (2)

By default, we assume that the false element falseM𝑓𝑎𝑙𝑠𝑒𝑀false\in Mitalic_f italic_a italic_l italic_s italic_e ∈ italic_M. And in the future, if the function f(w)𝑓𝑤f(w)italic_f ( italic_w ) (fσ𝑓𝜎f\in\sigmaitalic_f ∈ italic_σ) takes the value false𝑓𝑎𝑙𝑠𝑒falseitalic_f italic_a italic_l italic_s italic_e, then we will denote this as f(w)𝑓𝑤absentf(w)\uparrowitalic_f ( italic_w ) ↑, and denote f(w)𝑓𝑤absentf(w)\downarrowitalic_f ( italic_w ) ↓ otherwise. The domain of definition dom(f)𝑑𝑜𝑚𝑓dom(f)italic_d italic_o italic_m ( italic_f ) of a function f𝑓fitalic_f will be considered to be all elements w𝑤witalic_w on which f(w)𝑓𝑤absentf(w)\downarrowitalic_f ( italic_w ) ↓.

Define the extention fi(n+1)subscriptsuperscript𝑓𝑛1𝑖f^{(n+1)}_{i}italic_f start_POSTSUPERSCRIPT ( italic_n + 1 ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT for each fi(n)subscriptsuperscript𝑓𝑛𝑖f^{(n)}_{i}italic_f start_POSTSUPERSCRIPT ( italic_n ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT (where fi(0)=fisubscriptsuperscript𝑓0𝑖subscript𝑓𝑖f^{(0)}_{i}=f_{i}italic_f start_POSTSUPERSCRIPT ( 0 ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT = italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT) and

fi(n+1)|dom(fi(n))=fi(n)|dom(fi(n))evaluated-atsubscriptsuperscript𝑓𝑛1𝑖𝑑𝑜𝑚subscriptsuperscript𝑓𝑛𝑖evaluated-atsubscriptsuperscript𝑓𝑛𝑖𝑑𝑜𝑚subscriptsuperscript𝑓𝑛𝑖f^{(n+1)}_{i}|_{dom(f^{(n)}_{i})}=f^{(n)}_{i}|_{dom(f^{(n)}_{i})}italic_f start_POSTSUPERSCRIPT ( italic_n + 1 ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT | start_POSTSUBSCRIPT italic_d italic_o italic_m ( italic_f start_POSTSUPERSCRIPT ( italic_n ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) end_POSTSUBSCRIPT = italic_f start_POSTSUPERSCRIPT ( italic_n ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT | start_POSTSUBSCRIPT italic_d italic_o italic_m ( italic_f start_POSTSUPERSCRIPT ( italic_n ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) end_POSTSUBSCRIPT (3)

using a p-computable function γi:HW(M)Ti{false}:subscript𝛾𝑖𝐻𝑊𝑀subscript𝑇𝑖𝑓𝑎𝑙𝑠𝑒\gamma_{i}:HW(M)\to T_{i}\cup\{false\}italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT : italic_H italic_W ( italic_M ) → italic_T start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∪ { italic_f italic_a italic_l italic_s italic_e } such that on (n+1)-iteration we have:

fi(n+1)(w)={fi(w), if fi(w), else γi(w)w¯x¯, if γi(w)false and |x¯|=|w¯|false, otherwise f^{(n+1)}_{i}(w)=\left\{\begin{array}[]{lr}f_{i}(w)\text{, if }f_{i}(w)% \downarrow,\text{ else }\\ \gamma_{i}(w)^{\overline{x}}_{\overline{w}}\text{, if }\gamma_{i}(w)\neq false% \text{ and }|\overline{x}|=|\overline{w}|\\ false\text{, otherwise }\end{array}\right.italic_f start_POSTSUPERSCRIPT ( italic_n + 1 ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) = { start_ARRAY start_ROW start_CELL italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) , if italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ↓ , else end_CELL start_CELL end_CELL end_ROW start_ROW start_CELL italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) start_POSTSUPERSCRIPT over¯ start_ARG italic_x end_ARG end_POSTSUPERSCRIPT start_POSTSUBSCRIPT over¯ start_ARG italic_w end_ARG end_POSTSUBSCRIPT , if italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ≠ italic_f italic_a italic_l italic_s italic_e and | over¯ start_ARG italic_x end_ARG | = | over¯ start_ARG italic_w end_ARG | end_CELL start_CELL end_CELL end_ROW start_ROW start_CELL italic_f italic_a italic_l italic_s italic_e , otherwise end_CELL start_CELL end_CELL end_ROW end_ARRAY (4)

and then we are expanding the function fisubscript𝑓𝑖f_{i}italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT to fi(n+1)subscriptsuperscript𝑓𝑛1𝑖f^{(n+1)}_{i}italic_f start_POSTSUPERSCRIPT ( italic_n + 1 ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT and go to the next iteration.

Define, fgdom(f)dom(g) and f|dom(f)=g|dom(f)𝑓𝑔𝑑𝑜𝑚𝑓evaluated-at𝑑𝑜𝑚𝑔 and 𝑓𝑑𝑜𝑚𝑓evaluated-at𝑔𝑑𝑜𝑚𝑓f\subseteq g\Leftrightarrow dom(f)\subseteq dom(g)\text{ and }f|_{dom(f)}=g|_{% dom(f)}italic_f ⊆ italic_g ⇔ italic_d italic_o italic_m ( italic_f ) ⊆ italic_d italic_o italic_m ( italic_g ) and italic_f | start_POSTSUBSCRIPT italic_d italic_o italic_m ( italic_f ) end_POSTSUBSCRIPT = italic_g | start_POSTSUBSCRIPT italic_d italic_o italic_m ( italic_f ) end_POSTSUBSCRIPT.

Using families of the terms Tisubscript𝑇𝑖T_{i}italic_T start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT, p-computable functions γisubscript𝛾𝑖\gamma_{i}italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT and equality 4 we can define the operator:

Γf1,,fn<HW(𝔐),σ>:{g|g:HW(M)HW(M)}n{g|g:HW(M)HW(M)}n:subscriptsuperscriptΓabsent𝐻𝑊𝔐𝜎absentsubscript𝑓1subscript𝑓𝑛superscriptconditional-set𝑔:𝑔𝐻𝑊𝑀𝐻𝑊𝑀𝑛superscriptconditional-set𝑔:𝑔𝐻𝑊𝑀𝐻𝑊𝑀𝑛\Gamma^{<HW(\mathfrak{M}),\sigma>}_{f_{1},\dots,f_{n}}:\{g|\ g:HW(M)\to HW(M)% \}^{n}\to\{g|\ g:HW(M)\to HW(M)\}^{n}roman_Γ start_POSTSUPERSCRIPT < italic_H italic_W ( fraktur_M ) , italic_σ > end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_f start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT end_POSTSUBSCRIPT : { italic_g | italic_g : italic_H italic_W ( italic_M ) → italic_H italic_W ( italic_M ) } start_POSTSUPERSCRIPT italic_n end_POSTSUPERSCRIPT → { italic_g | italic_g : italic_H italic_W ( italic_M ) → italic_H italic_W ( italic_M ) } start_POSTSUPERSCRIPT italic_n end_POSTSUPERSCRIPT (5)

satisfying the following rules

Γf1,,fn<HW(𝔐),σ>(g1(k),,gn(k))=(g1(k+1),,gn(k+1))subscriptsuperscriptΓabsent𝐻𝑊𝔐𝜎absentsubscript𝑓1subscript𝑓𝑛subscriptsuperscript𝑔𝑘1subscriptsuperscript𝑔𝑘𝑛subscriptsuperscript𝑔𝑘11subscriptsuperscript𝑔𝑘1𝑛\Gamma^{<HW(\mathfrak{M}),\sigma>}_{f_{1},\dots,f_{n}}(g^{(k)}_{1},\dots,g^{(k% )}_{n})=(g^{(k+1)}_{1},\dots,g^{(k+1)}_{n})roman_Γ start_POSTSUPERSCRIPT < italic_H italic_W ( fraktur_M ) , italic_σ > end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_f start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT end_POSTSUBSCRIPT ( italic_g start_POSTSUPERSCRIPT ( italic_k ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_g start_POSTSUPERSCRIPT ( italic_k ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT ) = ( italic_g start_POSTSUPERSCRIPT ( italic_k + 1 ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_g start_POSTSUPERSCRIPT ( italic_k + 1 ) end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT ) (6)

where gi(k)gi(k+1)superscriptsubscript𝑔𝑖𝑘superscriptsubscript𝑔𝑖𝑘1g_{i}^{(k)}\subseteq g_{i}^{(k+1)}italic_g start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ( italic_k ) end_POSTSUPERSCRIPT ⊆ italic_g start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ( italic_k + 1 ) end_POSTSUPERSCRIPT.

The operator Γf1,,fn<HW(𝔐),σ>subscriptsuperscriptΓabsent𝐻𝑊𝔐𝜎absentsubscript𝑓1subscript𝑓𝑛\Gamma^{<HW(\mathfrak{M}),\sigma>}_{f_{1},\dots,f_{n}}roman_Γ start_POSTSUPERSCRIPT < italic_H italic_W ( fraktur_M ) , italic_σ > end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_f start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT end_POSTSUBSCRIPT is monotonic and has the property of a fixed point (g1,,gn)subscriptsuperscript𝑔1subscriptsuperscript𝑔𝑛(g^{*}_{1},\dots,g^{*}_{n})( italic_g start_POSTSUPERSCRIPT ∗ end_POSTSUPERSCRIPT start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_g start_POSTSUPERSCRIPT ∗ end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT ); moreover, the fixed point is reached in ω𝜔\omegaitalic_ω steps:

Γf1,,fn<HW(𝔐),σ>(f1,,fn)=(f1,,fn)subscriptsuperscriptΓabsent𝐻𝑊𝔐𝜎absentsubscript𝑓1subscript𝑓𝑛subscriptsuperscript𝑓1subscriptsuperscript𝑓𝑛subscriptsuperscript𝑓1subscriptsuperscript𝑓𝑛\Gamma^{<HW(\mathfrak{M}),\sigma>}_{f_{1},\dots,f_{n}}(f^{*}_{1},\dots,f^{*}_{% n})=(f^{*}_{1},\dots,f^{*}_{n})roman_Γ start_POSTSUPERSCRIPT < italic_H italic_W ( fraktur_M ) , italic_σ > end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_f start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT end_POSTSUBSCRIPT ( italic_f start_POSTSUPERSCRIPT ∗ end_POSTSUPERSCRIPT start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUPERSCRIPT ∗ end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT ) = ( italic_f start_POSTSUPERSCRIPT ∗ end_POSTSUPERSCRIPT start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUPERSCRIPT ∗ end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT ) (7)

where gi=gi(ω)superscriptsubscript𝑔𝑖superscriptsubscript𝑔𝑖𝜔g_{i}^{*}=g_{i}^{(\omega)}italic_g start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ∗ end_POSTSUPERSCRIPT = italic_g start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT start_POSTSUPERSCRIPT ( italic_ω ) end_POSTSUPERSCRIPT, i[1,,n]𝑖1𝑛i\in[1,\dots,n]italic_i ∈ [ 1 , … , italic_n ]

Define a set of free variables of a term or formula as V(t(x¯))𝑉𝑡¯𝑥V(t(\overline{x}))italic_V ( italic_t ( over¯ start_ARG italic_x end_ARG ) ) and V(φ(x¯))𝑉𝜑¯𝑥V(\varphi(\overline{x}))italic_V ( italic_φ ( over¯ start_ARG italic_x end_ARG ) ) respectively, where x¯=(x1,,xn)¯𝑥subscript𝑥1subscript𝑥𝑛\overline{x}=(x_{1},\dots,x_{n})over¯ start_ARG italic_x end_ARG = ( italic_x start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_x start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT ) for some nN𝑛𝑁n\in Nitalic_n ∈ italic_N. Denote Vx(φ(x¯,y¯))subscript𝑉𝑥𝜑¯𝑥¯𝑦V_{x}(\varphi(\overline{x},\overline{y}))italic_V start_POSTSUBSCRIPT italic_x end_POSTSUBSCRIPT ( italic_φ ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) ) and Vy(φ(x¯,y¯))subscript𝑉𝑦𝜑¯𝑥¯𝑦V_{y}(\varphi(\overline{x},\overline{y}))italic_V start_POSTSUBSCRIPT italic_y end_POSTSUBSCRIPT ( italic_φ ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) ) the set of variable {xi}subscript𝑥𝑖\{x_{i}\}{ italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT } such that xiV(x¯)subscript𝑥𝑖𝑉¯𝑥x_{i}\in V(\overline{x})italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∈ italic_V ( over¯ start_ARG italic_x end_ARG ) and {yi}subscript𝑦𝑖\{y_{i}\}{ italic_y start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT } such that yiV(y¯)subscript𝑦𝑖𝑉¯𝑦y_{i}\in V(\overline{y})italic_y start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∈ italic_V ( over¯ start_ARG italic_y end_ARG ). Also denote fpor ty¯(x¯,y¯)superscript𝑡¯𝑦¯𝑥¯𝑦t^{\overline{y}}(\overline{x},\overline{y})italic_t start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) is term where we replaced all occurences fj(xi)subscript𝑓𝑗subscript𝑥𝑖f_{j}(x_{i})italic_f start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) on yisubscript𝑦𝑖y_{i}italic_y start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT in the term t(x¯,y¯)𝑡¯𝑥¯𝑦t(\overline{x},\overline{y})italic_t ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ).

As in the case of the polynomial analogue of Gandy’s fixed point theorem, we define the concept of a GNF-system as a tuple:

GNF=(Σ,σ,Ω,L,HW(M),Ω,F,T,G)𝐺𝑁𝐹Σ𝜎Ω𝐿𝐻𝑊𝑀Ω𝐹𝑇𝐺GNF=(\Sigma,\sigma,\Omega,L,HW(M),\Omega,F,T,G)italic_G italic_N italic_F = ( roman_Σ , italic_σ , roman_Ω , italic_L , italic_H italic_W ( italic_M ) , roman_Ω , italic_F , italic_T , italic_G )

We will say that a GNF-system is a p-computable if the model HW(𝔐)𝐻𝑊𝔐HW(\mathfrak{M})italic_H italic_W ( fraktur_M ) is a p-computable, all γiGsubscript𝛾𝑖𝐺\gamma_{i}\in Gitalic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∈ italic_G is a p-computable and if the following conditions are met:

  • if fjsubscript𝑓𝑗f_{j}italic_f start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT is included in some tksubscript𝑡𝑘t_{k}italic_t start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT then only of the form fj(xi)subscript𝑓𝑗subscript𝑥𝑖f_{j}(x_{i})italic_f start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) for any xisubscript𝑥𝑖x_{i}italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT

  • fj(xi)subscript𝑓𝑗subscript𝑥𝑖f_{j}(x_{i})italic_f start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) and fk(xi)subscript𝑓𝑘subscript𝑥𝑖f_{k}(x_{i})italic_f start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT ( italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) do not belong to any term simultaneosly for any xisubscript𝑥𝑖x_{i}italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT

  • for any tjy¯(x¯,y¯)superscriptsubscript𝑡𝑗¯𝑦¯𝑥¯𝑦t_{j}^{\overline{y}}(\overline{x},\overline{y})italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) it’s not true that there is such iN𝑖𝑁i\in Nitalic_i ∈ italic_N that xiV(tjy¯(x¯,y¯))subscript𝑥𝑖𝑉superscriptsubscript𝑡𝑗¯𝑦¯𝑥¯𝑦x_{i}\in V(t_{j}^{\overline{y}}(\overline{x},\overline{y}))italic_x start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∈ italic_V ( italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) ) and yiV(tjy¯(x¯,y¯))subscript𝑦𝑖𝑉superscriptsubscript𝑡𝑗¯𝑦¯𝑥¯𝑦y_{i}\in V(t_{j}^{\overline{y}}(\overline{x},\overline{y}))italic_y start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∈ italic_V ( italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) )

  • for any Tksubscript𝑇𝑘T_{k}italic_T start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT there exists C and p such that for any tjTksubscript𝑡𝑗subscript𝑇𝑘t_{j}\in T_{k}italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ∈ italic_T start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT computational complexity t(tjy¯(x¯,y¯))𝑡superscriptsubscript𝑡𝑗¯𝑦¯𝑥¯𝑦t(t_{j}^{\overline{y}}(\overline{x},\overline{y}))italic_t ( italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) ) do not exceed C(|x¯|+|y¯|)p𝐶superscript¯𝑥¯𝑦𝑝C\cdot(|\overline{x}|+|\overline{y}|)^{p}italic_C ⋅ ( | over¯ start_ARG italic_x end_ARG | + | over¯ start_ARG italic_y end_ARG | ) start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT

  • if Vy(tjy¯(x¯,y¯))subscript𝑉𝑦superscriptsubscript𝑡𝑗¯𝑦¯𝑥¯𝑦V_{y}(t_{j}^{\overline{y}}(\overline{x},\overline{y}))\neq\varnothingitalic_V start_POSTSUBSCRIPT italic_y end_POSTSUBSCRIPT ( italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) ) ≠ ∅ then the value of the term |tjy¯(w¯,l¯)|superscriptsubscript𝑡𝑗¯𝑦¯𝑤¯𝑙|t_{j}^{\overline{y}}(\overline{w},\overline{l})|| italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ( over¯ start_ARG italic_w end_ARG , over¯ start_ARG italic_l end_ARG ) | do not exceed |w¯|+|l¯|¯𝑤¯𝑙|\overline{w}|+|\overline{l}|| over¯ start_ARG italic_w end_ARG | + | over¯ start_ARG italic_l end_ARG | for any tjTksubscript𝑡𝑗subscript𝑇𝑘t_{j}\in T_{k}italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ∈ italic_T start_POSTSUBSCRIPT italic_k end_POSTSUBSCRIPT, for any evaluates wi,ljHW(M)subscript𝑤𝑖subscript𝑙𝑗𝐻𝑊𝑀w_{i},l_{j}\in HW(M)italic_w start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT , italic_l start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ∈ italic_H italic_W ( italic_M ) of the tuples x¯¯𝑥\overline{x}over¯ start_ARG italic_x end_ARG and y¯¯𝑦\overline{y}over¯ start_ARG italic_y end_ARG respectively.

Theorem (Functional variant of Polynomial Analogue
 of Gandy’s Fixed Point Theorem)
:
:Theorem (Functional variant of Polynomial Analogue
 of Gandy’s Fixed Point Theorem)
absent
\textbf{Theorem (Functional variant of Polynomial Analogue}\\ \textbf{ of Gandy's Fixed Point Theorem)}:bold_Theorem bold_(Functional bold_variant bold_of bold_Polynomial bold_Analogue bold_of bold_Gandy’s bold_Fixed bold_Point bold_Theorem) :
Let p-computable GNF-system with p-computable initial functions f1,,fnsubscript𝑓1subscript𝑓𝑛f_{1},\dots,f_{n}italic_f start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT be given, then the smallest fixed point Γ(f¯)Γ¯𝑓\Gamma(\overline{f})roman_Γ ( over¯ start_ARG italic_f end_ARG ) of the operator Γf1,,fn<HW(𝔐),σ>subscriptsuperscriptΓabsent𝐻𝑊𝔐𝜎absentsubscript𝑓1subscript𝑓𝑛\Gamma^{<HW(\mathfrak{M}),\sigma>}_{f_{1},\dots,f_{n}}roman_Γ start_POSTSUPERSCRIPT < italic_H italic_W ( fraktur_M ) , italic_σ > end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_f start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_f start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT end_POSTSUBSCRIPT is p-computable.

Proof: By induction on the rank r(w)𝑟𝑤r(w)italic_r ( italic_w ) of the element w𝑤witalic_w we prove two statements simultaneously. First,

|fi(w)|C|w|psubscript𝑓𝑖𝑤𝐶superscript𝑤𝑝|f_{i}(w)|\leq C\cdot|w|^{p}| italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) | ≤ italic_C ⋅ | italic_w | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT (8)

and second, that the computational complexity of the algorithm does not exceed the following:

t(fi(w))36Cp+1(r(w)+1)|w|p2+1𝑡subscript𝑓𝑖𝑤36superscript𝐶𝑝1𝑟𝑤1superscript𝑤superscript𝑝21t(f_{i}(w))\leq 36\cdot C^{p+1}\cdot(r(w)+1)\cdot|w|^{p^{2}+1}italic_t ( italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ) ≤ 36 ⋅ italic_C start_POSTSUPERSCRIPT italic_p + 1 end_POSTSUPERSCRIPT ⋅ ( italic_r ( italic_w ) + 1 ) ⋅ | italic_w | start_POSTSUPERSCRIPT italic_p start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT + 1 end_POSTSUPERSCRIPT (9)

Base of induction: n=0𝑛0n=0italic_n = 0. Then for some aM𝑎𝑀a\in Mitalic_a ∈ italic_M we have |fi(a)|C|a|psubscript𝑓𝑖𝑎𝐶superscript𝑎𝑝|f_{i}(a)|\leq C\cdot|a|^{p}| italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_a ) | ≤ italic_C ⋅ | italic_a | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT and t(fi(a))C|a|p𝑡subscript𝑓𝑖𝑎𝐶superscript𝑎𝑝t(f_{i}(a))\leq C\cdot|a|^{p}italic_t ( italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_a ) ) ≤ italic_C ⋅ | italic_a | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT because initial function fisubscript𝑓𝑖f_{i}italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT is a polynomial computable.
Step of induction: Let the statement be true for everyone k<n𝑘𝑛k<nitalic_k < italic_n then show that for k=n𝑘𝑛k=nitalic_k = italic_n:

If initial polynomial function f(w)𝑓𝑤absentf(w)\downarrowitalic_f ( italic_w ) ↓ then obviosly.
Else if γ(w)=false𝛾𝑤𝑓𝑎𝑙𝑠𝑒\gamma(w)=falseitalic_γ ( italic_w ) = italic_f italic_a italic_l italic_s italic_e then obviously.
Else if γ(w)false𝛾𝑤𝑓𝑎𝑙𝑠𝑒\gamma(w)\neq falseitalic_γ ( italic_w ) ≠ italic_f italic_a italic_l italic_s italic_e then consider two cases for I={i|yitjy¯(x¯,y¯)}𝐼conditional-set𝑖subscript𝑦𝑖subscriptsuperscript𝑡¯𝑦𝑗¯𝑥¯𝑦I=\{i|y_{i}\in t^{\overline{y}}_{j}(\overline{x},\overline{y})\}italic_I = { italic_i | italic_y start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∈ italic_t start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( over¯ start_ARG italic_x end_ARG , over¯ start_ARG italic_y end_ARG ) }:
1) I=𝐼I=\varnothingitalic_I = ∅ then by conditions for p-computable GNF-system:

|fi(w)||[γ(w)](w¯)|=|tj(w1,,wn)|C|w|psubscript𝑓𝑖𝑤delimited-[]𝛾𝑤¯𝑤subscript𝑡𝑗subscript𝑤1subscript𝑤𝑛𝐶superscript𝑤𝑝|f_{i}(w)|\leq|[\gamma(w)](\overline{w})|=|t_{j}(w_{1},\dots,w_{n})|\leq C% \cdot|w|^{p}| italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) | ≤ | [ italic_γ ( italic_w ) ] ( over¯ start_ARG italic_w end_ARG ) | = | italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_w start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_w start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT ) | ≤ italic_C ⋅ | italic_w | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT (10)

and it is true by definition of p-computable GNF-system.

For complexion we have next:

t(fi(w))rin+rγi+t([γi(w)](w¯))+r1=t([γi(w)y¯](w¯x,v¯y))+r1+rin+rγi𝑡subscript𝑓𝑖𝑤subscript𝑟𝑖𝑛subscript𝑟subscript𝛾𝑖𝑡delimited-[]subscript𝛾𝑖𝑤¯𝑤subscript𝑟1𝑡delimited-[]subscript𝛾𝑖superscript𝑤¯𝑦subscript¯𝑤𝑥subscript¯𝑣𝑦subscript𝑟1subscript𝑟𝑖𝑛subscript𝑟subscript𝛾𝑖absentt(f_{i}(w))\leq r_{in}+r_{\gamma_{i}}+t([\gamma_{i}(w)](\overline{w}))+r_{1}=t% ([\gamma_{i}(w)^{\overline{y}}](\overline{w}_{x},\overline{v}_{y}))+r_{1}+r_{% in}+r_{\gamma_{i}}\leqitalic_t ( italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ) ≤ italic_r start_POSTSUBSCRIPT italic_i italic_n end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT + italic_t ( [ italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ] ( over¯ start_ARG italic_w end_ARG ) ) + italic_r start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT = italic_t ( [ italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ] ( over¯ start_ARG italic_w end_ARG start_POSTSUBSCRIPT italic_x end_POSTSUBSCRIPT , over¯ start_ARG italic_v end_ARG start_POSTSUBSCRIPT italic_y end_POSTSUBSCRIPT ) ) + italic_r start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_i italic_n end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT ≤
C(|w¯x|+|v¯y|)p+r1+rin+rγiabsent𝐶superscriptsubscript¯𝑤𝑥subscript¯𝑣𝑦𝑝subscript𝑟1subscript𝑟𝑖𝑛subscript𝑟subscript𝛾𝑖absent\leq C\cdot(|\overline{w}_{x}|+|\overline{v}_{y}|)^{p}+r_{1}+r_{in}+r_{\gamma_% {i}}\leq≤ italic_C ⋅ ( | over¯ start_ARG italic_w end_ARG start_POSTSUBSCRIPT italic_x end_POSTSUBSCRIPT | + | over¯ start_ARG italic_v end_ARG start_POSTSUBSCRIPT italic_y end_POSTSUBSCRIPT | ) start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT + italic_r start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_i italic_n end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT ≤
C|w¯|p+r1+rin+rγi36Cp+1(r(w)+1)|w|p2+1absent𝐶superscript¯𝑤𝑝subscript𝑟1subscript𝑟𝑖𝑛subscript𝑟subscript𝛾𝑖36superscript𝐶𝑝1𝑟𝑤1superscript𝑤superscript𝑝21\leq C\cdot|\overline{w}|^{p}+r_{1}+r_{in}+r_{\gamma_{i}}\leq 36\cdot C^{p+1}% \cdot(r(w)+1)\cdot|w|^{p^{2}+1}≤ italic_C ⋅ | over¯ start_ARG italic_w end_ARG | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT + italic_r start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_i italic_n end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT ≤ 36 ⋅ italic_C start_POSTSUPERSCRIPT italic_p + 1 end_POSTSUPERSCRIPT ⋅ ( italic_r ( italic_w ) + 1 ) ⋅ | italic_w | start_POSTSUPERSCRIPT italic_p start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT + 1 end_POSTSUPERSCRIPT (11)

because v¯¯𝑣\overline{v}over¯ start_ARG italic_v end_ARG is empty and where

  • rinsubscript𝑟𝑖𝑛r_{in}italic_r start_POSTSUBSCRIPT italic_i italic_n end_POSTSUBSCRIPT the complexity of checking the value of the initial function f(w)𝑓𝑤f(w)italic_f ( italic_w ), complexity does not exceed C|w|p𝐶superscript𝑤𝑝C\cdot|w|^{p}italic_C ⋅ | italic_w | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT

  • rγisubscript𝑟subscript𝛾𝑖r_{\gamma_{i}}italic_r start_POSTSUBSCRIPT italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT the complexity of the function γi(w)subscript𝛾𝑖𝑤\gamma_{i}(w)italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) for construction the term tj(x1,,xn)subscript𝑡𝑗subscript𝑥1subscript𝑥𝑛t_{j}(x_{1},\dots,x_{n})italic_t start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_x start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT , … , italic_x start_POSTSUBSCRIPT italic_n end_POSTSUBSCRIPT ), complexity does not exceed C|w|p𝐶superscript𝑤𝑝C\cdot|w|^{p}italic_C ⋅ | italic_w | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT

  • r1subscript𝑟1r_{1}italic_r start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT complexity of the replacement function which replace fj(wi)subscript𝑓𝑗subscript𝑤𝑖f_{j}(w_{i})italic_f start_POSTSUBSCRIPT italic_j end_POSTSUBSCRIPT ( italic_w start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) on visubscript𝑣𝑖v_{i}italic_v start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT.

2) if I𝐼I\neq\varnothingitalic_I ≠ ∅ then:

|fi(w)|=|[γi(w)](w¯)|=|[γi(w)]y¯(w¯x,v¯y)||w¯x|+|v¯y|C|w¯|psubscript𝑓𝑖𝑤delimited-[]subscript𝛾𝑖𝑤¯𝑤superscriptdelimited-[]subscript𝛾𝑖𝑤¯𝑦subscript¯𝑤𝑥subscript¯𝑣𝑦subscript¯𝑤𝑥subscript¯𝑣𝑦𝐶superscript¯𝑤𝑝|f_{i}(w)|=|[\gamma_{i}(w)](\overline{w})|=|[\gamma_{i}(w)]^{\overline{y}}(% \overline{w}_{x},\overline{v}_{y})|\leq|\overline{w}_{x}|+|\overline{v}_{y}|% \leq C\cdot|\overline{w}|^{p}| italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) | = | [ italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ] ( over¯ start_ARG italic_w end_ARG ) | = | [ italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ] start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ( over¯ start_ARG italic_w end_ARG start_POSTSUBSCRIPT italic_x end_POSTSUBSCRIPT , over¯ start_ARG italic_v end_ARG start_POSTSUBSCRIPT italic_y end_POSTSUBSCRIPT ) | ≤ | over¯ start_ARG italic_w end_ARG start_POSTSUBSCRIPT italic_x end_POSTSUBSCRIPT | + | over¯ start_ARG italic_v end_ARG start_POSTSUBSCRIPT italic_y end_POSTSUBSCRIPT | ≤ italic_C ⋅ | over¯ start_ARG italic_w end_ARG | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT (12)

where vi=fji(wi)subscript𝑣𝑖subscript𝑓subscript𝑗𝑖subscript𝑤𝑖v_{i}=f_{j_{i}}(w_{i})italic_v start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT = italic_f start_POSTSUBSCRIPT italic_j start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT ( italic_w start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) for viv¯ysubscript𝑣𝑖subscript¯𝑣𝑦v_{i}\in\overline{v}_{y}italic_v start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ∈ over¯ start_ARG italic_v end_ARG start_POSTSUBSCRIPT italic_y end_POSTSUBSCRIPT and |vi|C|wi|psubscript𝑣𝑖𝐶superscriptsubscript𝑤𝑖𝑝|v_{i}|\leq C\cdot|w_{i}|^{p}| italic_v start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT | ≤ italic_C ⋅ | italic_w start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT by induction.

For complexion we have next:

t(fi(w))rγi+t([γi(w)](w¯))+r1t([γi(w)y¯](w¯x,v¯y))+r1+r2+rγi+iIt(f(wi))𝑡subscript𝑓𝑖𝑤subscript𝑟subscript𝛾𝑖𝑡delimited-[]subscript𝛾𝑖𝑤¯𝑤subscript𝑟1𝑡delimited-[]subscript𝛾𝑖superscript𝑤¯𝑦subscript¯𝑤𝑥subscript¯𝑣𝑦subscript𝑟1subscript𝑟2subscript𝑟subscript𝛾𝑖subscript𝑖𝐼𝑡𝑓subscript𝑤𝑖absentt(f_{i}(w))\leq r_{\gamma_{i}}+t([\gamma_{i}(w)](\overline{w}))+r_{1}\leq t([% \gamma_{i}(w)^{\overline{y}}](\overline{w}_{x},\overline{v}_{y}))+r_{1}+r_{2}+% r_{\gamma_{i}}+\sum_{i\in I}t(f(w_{i}))\leqitalic_t ( italic_f start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ) ≤ italic_r start_POSTSUBSCRIPT italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT + italic_t ( [ italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) ] ( over¯ start_ARG italic_w end_ARG ) ) + italic_r start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT ≤ italic_t ( [ italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ( italic_w ) start_POSTSUPERSCRIPT over¯ start_ARG italic_y end_ARG end_POSTSUPERSCRIPT ] ( over¯ start_ARG italic_w end_ARG start_POSTSUBSCRIPT italic_x end_POSTSUBSCRIPT , over¯ start_ARG italic_v end_ARG start_POSTSUBSCRIPT italic_y end_POSTSUBSCRIPT ) ) + italic_r start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT + ∑ start_POSTSUBSCRIPT italic_i ∈ italic_I end_POSTSUBSCRIPT italic_t ( italic_f ( italic_w start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT ) ) ≤
C(C|w|p)p+r1+r2+rγi+i=1n36Cp+1(r(w)1+1)|wi|p2+1absent𝐶superscript𝐶superscript𝑤𝑝𝑝subscript𝑟1subscript𝑟2subscript𝑟subscript𝛾𝑖superscriptsubscript𝑖1𝑛36superscript𝐶𝑝1𝑟𝑤11superscriptsubscript𝑤𝑖superscript𝑝21absent\leq C\cdot(C\cdot|w|^{p})^{p}+r_{1}+r_{2}+r_{\gamma_{i}}+\sum_{i=1}^{n}36% \cdot C^{p+1}\cdot(r(w)-1+1)\cdot|w_{i}|^{p^{2}+1}\leq≤ italic_C ⋅ ( italic_C ⋅ | italic_w | start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT ) start_POSTSUPERSCRIPT italic_p end_POSTSUPERSCRIPT + italic_r start_POSTSUBSCRIPT 1 end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT 2 end_POSTSUBSCRIPT + italic_r start_POSTSUBSCRIPT italic_γ start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT end_POSTSUBSCRIPT + ∑ start_POSTSUBSCRIPT italic_i = 1 end_POSTSUBSCRIPT start_POSTSUPERSCRIPT italic_n end_POSTSUPERSCRIPT 36 ⋅ italic_C start_POSTSUPERSCRIPT italic_p + 1 end_POSTSUPERSCRIPT ⋅ ( italic_r ( italic_w ) - 1 + 1 ) ⋅ | italic_w start_POSTSUBSCRIPT italic_i end_POSTSUBSCRIPT | start_POSTSUPERSCRIPT italic_p start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT + 1 end_POSTSUPERSCRIPT ≤
36Cp+1(r(w)+1)|w|p2+1absent36superscript𝐶𝑝1𝑟𝑤1superscript𝑤superscript𝑝21\leq 36\cdot C^{p+1}\cdot(r(w)+1)\cdot|w|^{p^{2}+1}≤ 36 ⋅ italic_C start_POSTSUPERSCRIPT italic_p + 1 end_POSTSUPERSCRIPT ⋅ ( italic_r ( italic_w ) + 1 ) ⋅ | italic_w | start_POSTSUPERSCRIPT italic_p start_POSTSUPERSCRIPT 2 end_POSTSUPERSCRIPT + 1 end_POSTSUPERSCRIPT (13)

References