Theorem 1: Any sequence of infrakernels $K_n:{\prod }_{i=0}^{i=n}{X}_i\stackrel{ik}{\to }{X}_{n+1}$ which fulfill the niceness conditions have the infinite semidirect product $K_{:\infty }$ being well-defined and fulfilling the niceness conditions.

As a recap, the niceness conditions are:

1: Lower-semicontinuity for inputs: For all continuous bounded $f$,  $x_{0:n}\mapsto K_n\left(x_{0:n}\right)\left(f\right)$ is a lower-semicontinuous function.

2: 1-Lipschitzness for functions: For all $x_{0:n}$, $f\mapsto K_n\left(x_{0:n}\right)\left(f\right)$ is 1-Lipschitz.

3: Compact-shared compact-almost-support: For all compact sets $C\subseteq {\prod }_{i=0}^{i=n}{X}_i$ and $ϵ$, there is a compact set $C_{n+1}\subseteq X_{n+1}$ which is an $ϵ$-almost-support for all the $K_n\left(x_{0:n}\right)$ inframeasures where $x_{0:n}\in C$.

4: Constants increase: For all $x_{0:n}$ and constant functions $c$, $K_n\left(x_{0:n}\right)\left(c\right)\ge c$.

5: 1-normalization (only for the $[0,1]$ type signature): For all $x_{0:n}$, $K_n\left(x_{0:n}\right)\left(1\right)=1$

Now, $K_{:\infty }:X_0\stackrel{ik}{\to }{\prod }_{i=1}^{\infty }{X}_i$ is defined as: Fixing an arbitrary sequence of compact sets $C_i\subseteq X_i$,

$K_{:\infty }\left(x_0\right)\left(f\right):={lim}_{n\to \infty }{K}_{:n}\left(x_0\right)\left(\lambda x_{1:n+1}{inf}_{x_{n+2:\infty }\in {\prod }_{i=n+2}^{\infty }{C}_i}f\right(x_{1:n+1},x_{n+2:\infty }\left)\right)$

Our task is to show that $K_{:\infty }$ is a well-defined infrakernel which fulfills these five properties.

We will be reusing the proofs from "Less Basic Inframeasure Theory" (henceforth abbreviated as LBIT) when possible, and commenting on the differences when applicable.

The proof sketch is:

Part 1: Show that the functions you're feeding into those $K_{:n}$ infrakernels are guaranteed to be continuous.

Part 2: Show that all the $K_{:n}$ are infrakernels which fulfill the niceness conditions, via induction.

Part 3: Show that if a function only depends on the first n coordinates of the input, then the $K_{:n+m}\left(x_0\right)\left(f\right)$ values monotonically increase as m does.

Part 4: Give a general procedure for taking a compact subset of the space $X_0$ and making a compact subset of the space ${\prod }_{i=1}^{\infty }{X}_i$ with nice properties related to compact almost-support, that preserves its nice properties when projected down to any finite stage.

Almost-Monotone Lemma: This is a sufficiently useful utility tool in other theorems to be broken out into its own result. It says you can take any $f$ and $ϵ$ and compact set $C_0\subseteq X_0$ and pick a sequence of compact sets $C_i$ for the defining sequence of the infinite semidirect product such that the defining sequence for all the $K_{:\infty }\left(x_0\right)\left(f\right)$ (with $x_0\in C_0$) is $4ϵ||f||$-almost-monotone.

Part 5: Use parts 2, 3, and 4 to show that for any two different $C_i$ sequences, the defining sequences for the infinite infrakernel will limit to each each other (so if one converges, all do, if one diverges, all do, and if one wiggles around forever, all do), and then apply the Almost-Monotone Lemma to rule out the "wiggle around forever" case. Thus, the limit to define $K_{:\infty }\left(x_0\right)\left(f\right)$ exists, and doesn't depend on the choice of the sequence of compact sets. This solves well-definedness.

Part 6: Using parts 2 and 5, clean up the basic inframeasure conditions for $K_{:\infty }\left(x_0\right)$ (monotonicity and concavity), and show 1-Lipschitzness, increase of constants, and 1-normalization for $K_{:\infty }$ while we're at it. That's 3/5 niceness conditions down, and all inframeasure conditions except for compact almost-support.

Part 7: Use our trick from Part 4 and our freedom of picking our compact set sequence from Part 5 to show the compact-shared compact-almost-support property for $K_{:\infty }$. This also means that individual outputs of the kernel fulfill CAS, which verifies the last condition we need to conclude that $K_{:\infty }\left(x_0\right)$ is always an inframeasure. Only lower-semicontinuity of the kernel remains to be verified.

Part 8: We use the Almost-Monotone Lemma to wrap up the last condition, the lower-semicontinuity of the infinite infrakernel.

We often use the usual "start with thing we're trying to prove, and keep reducing it to a simpler problem" technique from the last time this proof path was used.

T1.1 Our desired result is whether the function $\lambda x_{1:n+1}.{inf}_{x_{n+2:\infty }\in {\prod }_{i=n+2}^{\infty }{C}_i}f(x_{1:n+1},x_{n+2:\infty })$
is continuous. This was already shown in "Less Basic Inframeasure Theory" (LBIT).

T1.2 The desired result is "if all the $K_n$ have the five niceness properties, then all the $K_{:n}$ are infrakernels with the five niceness properties as well".

The proof sketch for this is that this splits into 6 properties we need to show induct up. Monotonicity (phase 1), concavity (phase 2), 1-Lipschitzness (phase 3), increasing constants (phase 4), shared compact-almost-support (phase 5), and lower-semicontinuity (phase 6), which splits into two parts, one where we show a particular function is continuous, and then show lower-semicontinuity in general. Then, we finish up by arguing that this gets everything we need.

For the base case, because $K_{:0}:=K_0$ and we're assuming all the $K_n$ have the niceness properties and are infrakernels, $K_{:0}$ trivially fulfills them.

Time for the induction step. Remember that $K_{:n+1}\left(x_0\right):=K_{:n}\left(x_0\right)⋉(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right)$

T1.2.1 Proof of monotonicity: Assume $f^{\prime }\ge f$. Then

$K_{:n+1}\left(x_0\right)\left(f^{\prime }\right)=K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2})\left)\right)$

And the same goes for $f$ so if we could prove

$K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2})\left)\right)$
$\ge K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2})\left)\right)$

we'd be successful. Now, by monotonicity for $K_{:n}$ (by induction assumption), we'd have that result if

$\forall x_{1:n+1}:K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2}\left)\right)$
$\ge K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)$

Letting $x_{1:n+1}$ be arbitrary, by applying monotonicity for $K_{n+1}$, we'd have that result if

$\forall x_{n+2}:f^{\prime }(x_{1:n+1},x_{n+2})\ge f(x_{1:n+1},x_{n+2})$

Which is true since $f^{\prime }\ge f$. And so we're done, montonicity inducts up.

T1.2.2 Proof of concavity:

$K_{:n+1}\left(x_0\right)(pf+(1-p\left)f^{\prime }\right)$

$=K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.pf(x_{1:n+1},x_{n+2})+(1-p)f^{\prime }(x_{1:n+1},x_{n+2})\left)\right)$

and then, by concavity for all $K_{n+1}$, and monotonicity for $K_{:n}$ (by induction assumption), we have

$\ge K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.p{K}_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}))$
$+(1-p)K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2}\left)\right))$

and then, by concavity for $K_{:n}$ (by induction assumption), we have

$\ge p{K}_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2})\left)\right)$
$+(1-p)K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2})\left)\right)$

and then this packs up as

$=p{K}_{:n+1}\left(x_0\right)\left(f\right)+(1-p)K_{:n+1}\left(f^{\prime }\right)$

and concavity inducts on up.

T1.2.3 Proof of 1-Lipschitzness: we have

$|K_{:n+1}\left(x_0\right)\left(f\right)-K_{:n+1}\left(x_0\right)\left(f^{\prime }\right)|$

$=|K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2})\left)\right)$
$-K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2})\left)\right)|$

And by 1-Lipschitzness for $K_{:n}$ (by induction assumption), we have

$\le {sup}_{x_{1:n+1}}|K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)$
$-K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2}\left)\right)|$

And by 1-Lipschitzness for $K_{n+1}$, we have

$\le {sup}_{x_{1:n+1},x_{n+2}}|f(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2})|=d(f,f^{\prime })$

And 1-Lipschitzness inducts on up.

T1.2.4 Proof of increasing constants (and 1-normalization): We have

$K_{:n+1}\left(x_0\right)\left(c\right)=K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(c\left)\right)$

And then by increasing constants for $K_{n+1}$, and monotonicity for $K_{:n}$ (induction assumption), we have

$\ge K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.c)$

Now just apply increasing constants for $K_{:n}$ (induction assumption) to get $\ge c$

For 1-normalization in the $[0,1]$ type signature, we can have $c=1$, and then instead of an inequality, we have an equality, and the same proof path works, just using 1-normalization instead of increasing constants. They both induct up.

T1.2.5 Proof of the compact-shared CAS property: Our task is to take an arbitrary compact set $C^{X_0}\subseteq X_0$, and find a compact set $C_{ϵ}^{{\prod }_{i=1}^{i=n+2}{X}_i}\subseteq {\prod }_{i=1}^{i=n+2}{X}_i$ where two functions $f,f^{\prime }$ identical on the set only differ in expectation by $ϵd(f,f^{\prime })$ according to all $K_{:n+1}\left(x_0\right)$ with $x_0\in C^{X_0}$.

Let $x_0\in C^{X_0}$, and define the set $C_{ϵ}^{{\prod }_{i=1}^{i=n+2}{X}_i}$ as $C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}\times C_{\frac{ϵ}{2}}^{X_{n+2}}$

where the first compact set is a shared $\frac{ϵ}{2}$-almost-support for the $K_{:n}\left(x_0\right)$ where $x_0\in C^{X_0}$ (exists by compact-shared CAS for $K_{:n}$, an induction assumption) and the second compact set is a shared $\frac{ϵ}{2}$-almost-support for the $K_{n+1}(x_0,x_{1:n+1})$ where $x_0,x_{1:n+1}$ is in $C^{X_0}\times C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}$ (exists by compact-shared CAS for $K_{n+1}$, an assumed niceness condition). Let $f,f^{\prime }$ be continuous and identical on $C_{ϵ}^{{\prod }_{i=1}^{i=n+2}{X}_i}$. Then, we have

$|K_{:n+1}\left(x_0\right)\left(f\right)-K_{:n+1}\left(x_0\right)\left(f^{\prime }\right)|$

$=|K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2})\left)\right)$
$-K_{:n}\left(x_0\right)(\lambda x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1}\left)\right(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2})\left)\right)|$

Now, we apply Lemma 2 from LBIT, where we can upper-bound this quantity by "Lipschitz constant of the inframeasure times how much the functions differ on the almost-support + level of almost-support times how much the functions differ in general". We use $C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}$ as our compact set for the inner function. It was defined as a $\frac{ϵ}{2}$-almost support for all $K_{:n}\left(x_0\right)$ with $x_0\in C^{X_0}$, and $K_{:n}$ is 1-Lipschitz (induction assumption). So our upper bound is:

$\le {sup}_{x_{1:n+1}\in C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}}|K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)$
$-K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2}\left)\right)|$
$+\frac{ϵ}{2}\cdot {sup}_{x_{1:n+1}}|K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)$
$-K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2}\left)\right)|$

Focusing on that second chunk, we can apply 1-Lipschitzness of $K_{n+1}$ to yield

$\le {sup}_{x_{1:n+1}\in C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}}|K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)$
$-K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f^{\prime }(x_{1:n+1},x_{n+2}\left)\right)|$
$+\frac{ϵ}{2}\cdot {sup}_{x_{1:n+1},x_{n+2}}|f(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2})|$

For the first chunk, we can apply Lemma 2 from LBIT again, with $C_{\frac{ϵ}{2}}^{X_{n+2}}$ as our compact set, which is a $\frac{ϵ}{2}$-almost support for all $K_{n+1}(x_0,x_{1:n+1})$ with $x_0,x_{1:n+1}\in C^{X_0}\times C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}$, and $K_{n+1}$ is 1-Lipschitz. So our upper bound is:

$\le {sup}_{x_{1:n+1}\in C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}}\left({sup}_{x_{n+2}\in C_{\frac{ϵ}{2}}^{X_{n+2}}}|f\right(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2})|$
$+\frac{ϵ}{2}\cdot {sup}_{x_{n+2}}|f(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2})|)$
$+\frac{ϵ}{2}\cdot {sup}_{x_{1:n+1},x_{n+2}}|f(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2})|$

Now, since $f$ and $f^{\prime }$ are identical on $C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}\times C_{\frac{ϵ}{2}}^{X_{n+2}}$ that first term just vanishes, yielding

$={sup}_{x_{1:n+1}\in C_{\frac{ϵ}{2}}^{{\prod }_{i=1}^{i=n+1}{X}_i}}(\frac{ϵ}{2}\cdot {sup}_{x_{n+2}}|f(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2}\left)|\right)$
$+\frac{ϵ}{2}\cdot {sup}_{x_{1:n+1},x_{n+2}}|f(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2})|$

We upper-bound this by

$\le \frac{ϵ}{2}{sup}_{x_{1:n+1},x_{n+2}}|f(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2})|$
$+\frac{ϵ}{2}\cdot {sup}_{x_{1:n+1},x_{n+2}}|f(x_{1:n+1},x_{n+2})-f^{\prime }(x_{1:n+1},x_{n+2})|$

Which then clearly just reduces to

$=ϵd(f,f^{\prime })$

And we're done, the compact-shared CAS property inducts up.

T1.2.6.1 Proof of lower-semicontinuity: We'll start by taking an extended detour to show that the function 

$\lambda x_0,x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)$

is lower-semicontinuous. Fix a convergent sequence of inputs, $x_0^m,x_{1:n+1}^m$ which limit to $x_0^{\infty },x_{1:n+1}^{\infty }$. First up, the set

$\{x_0^m,x_{1:n+1}^m{\}}_{m\in N\bigsqcup \left\{\infty \right\}}$

is compact in ${\prod }_{i=0}^{i=n+1}{X}_i$ since it converges and we have the limit point added in. By the compact-shared CAS property for $K_{n+1}$, we can take any $ϵ$ and make a compact set $C_{ϵ}^{X_{n+2}}\subseteq X_{n+2}$ which is a shared $ϵ$-almost-support for all the $K_{n+1}(x_0^m,x_{1:n+1}^m)$ inframeasures. For any m, we can then apply the Lemma 2 (from LBIT) decomposition with the $C_{ϵ}^{X_{n+2}}$ $ϵ$-almost-support for all the $K_{n+1}(x_0^m,x_{1:n+1}^m)$ inframeasures (and 1-Lipschitzness of $K_{n+1}$) to get the inequality

$|K_{n+1}(x_0^m,x_{1:n+1}^m)(\lambda x_{n+2}.f(x_{1:n+1}^m,x_{n+2}\left)\right)-K_{n+1}(x_0^m,x_{1:n+1}^m)(\lambda x_{n+2}.f(x_{1:n+1}^{\infty },x_{n+2}\left)\right)|$

$\le {sup}_{x_{n+2}\in C_{ϵ}^{X_{n+2}}}|f(x_{1:n+1}^m,x_{n+2})-f(x_{1:n+1}^{\infty },x_{n+2})|$
$+ϵ{sup}_{x_{n+2}}|f(x_{1:n+1}^m,x_{n+2})-f(x_{1:n+1}^{\infty },x_{n+2})|$

That second term can be upper-bounded by $2||f||$, so doing that, we have

$\le {sup}_{x_{n+2}\in C_{ϵ}^{X_{n+2}}}|f(x_{1:n+1}^m,x_{n+2})-f(x_{1:n+1}^{\infty },x_{n+2})|+2ϵ||f||$

Now, the set $\{x_0^m,x_{1:n+1}^m{\}}_{m\in N\bigsqcup \left\{\infty \right\}}\times C_{ϵ}^{X_{n+2}}$ is a compact set, so any continuous bounded function $f$ is uniformly continuous on it. For all $ϵ$, there is some $\delta$ where two points only $\delta$ apart within this set have $f$ only differing by $ϵ$ on them. Since $x_{1:n+1}^m$ limits to $x_{1:n+1}^{\infty }$, for sufficiently large m, those two points will be within $\delta$ of each either, so eventually 

${sup}_{x_{n+2}\in C_{ϵ}^{X_{n+2}}}|f(x_{1:n+1}^m,x_{n+2})-f(x_{1:n+1}^{\infty },x_{n+2})|$

will be $ϵ$ or less for late enough m. So, for late enough m, we have 

$|K_{n+1}(x_0^m,x_{1:n+1}^m)(\lambda x_{n+2}.f(x_{1:n+1}^m,x_{n+2}\left)\right)-K_{n+1}(x_0^m,x_{1:n+1}^m)(\lambda x_{n+2}.f(x_{1:n+1}^{\infty },x_{n+2}\left)\right)|$

$\le ϵ+2ϵ||f||$

Since $ϵ$ can be arbitrary, we have that the sequences 

$K_{n+1}(x_0^m,x_{1:n+1}^m)(\lambda x_{n+2}.f(x_{1:n+1}^m,x_{n+2}\left)\right)$

and

$K_{n+1}(x_0^m,x_{1:n+1}^m)(\lambda x_{n+2}.f(x_{1:n+1}^{\infty },x_{n+2}\left)\right)$

limit to each other. Therefore,

${liminf}_{m\to \infty }{K}_{n+1}(x_0^m,x_{1:n+1}^m)(\lambda x_{n+2}.f(x_{1:n+1}^m,x_{n+2}\left)\right)$

$={liminf}_{m\to \infty }{K}_{n+1}(x_0^m,x_{:n+1}^m)(\lambda x_{n+2}.f(x_{1:n+1}^{\infty },x_{n+2}\left)\right)$

And then, by lower-semicontinuity for $K_{n+1}$, we have

$\ge K_{n+1}(x_0^{\infty },x_{1:n+1}^{\infty })(\lambda x_{n+2}.f(x_{1:n+1}^{\infty },x_{n+2}\left)\right)$

and so, lower-semicontinuity of the function

$\lambda x_0,x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)$

is shown. Time to return to the usual induction proof.

T1.2.6.2 For lower-semicontinuity in inputs, we first unpack the semidirect product. Fix a sequence $x_0^m$ which limits to $x_0^{\infty }$.

${liminf}_{m\to \infty }{K}_{:n+1}\left(x_0^m\right)\left(f\right)$

$={liminf}_{m\to \infty }{K}_{:n}\left(x_0^m\right)(\lambda x_{1:n+1}.K_{n+1}(x_0^m,x_{1:n+1}\left)\right(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2})\left)\right)$

Since we showed that the function 

$\lambda x_0,x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)$

is lower-semicontinuous, we can apply the monotone convergence theorem for inframeasures and rewrite as

$={liminf}_{m\to \infty }{sup}_{f^{\prime }\le \lambda x_0,x_{1:n+1}.K_{n+1}(x_0,x_{1:n+1})(\lambda x_{n+2}.f(x_{1:n+1},x_{n+2}\left)\right)}{K}_{:n}\left(x_0^m\right)(\lambda x_{1:n+1}.f^{\prime }(x_0^m,x_{1:n+1}\left)\right)$