Theorem 6: Causal IPOMDP's: Any infra-POMDP with transition kernel $K:S\times A\stackrel{ik}{\to }O\times S$ which fulfills the niceness conditions and always produces crisp infradistributions, and starting infradistribution $\psi \in \square S$, produces a causal belief function via $\Theta \left(\pi \right):=p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })$.

So, first up, we can appeal to Theorem 4 on Pseudocausal IPOMDP's, to conclude that all the $K_{:\infty }^{\pi }$ are well-defined, and that this $\Theta$ we defined fulfills all belief function conditions except maybe normalization.

The only things to check are that the resulting $\Theta$ is normalized, and that the resulting $\Theta$ is causal. The second is far more difficult and makes up the bulk of the proof, so we'll just dispose of the first one.

T6.1 First, $K$, since it's crisp by assumption, always has $K(s,a)\left(c\right)=c$ for all constants $c$. The same property extends to all the $K_n^{\pi }$ (they're all crisp too) and then from there to $K_{:\infty }^{\pi }$ by induction. Then we can just use the following argument, where $\pi$ is arbitrary.

$\Theta \left(\pi \right)\left(1\right)=p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{\pi })\left(1\right)=(\psi ⋉K_{:\infty }^{\pi })\left(1\right)=\psi (\lambda s_0.K_{:\infty }^{\pi }(s_0\left)\right(1\left)\right)=\psi \left(1\right)=1$

The last two inequalities were by $K_{:\infty }^{\pi }$ mapping constants to the same constant regardless of $\pi$, and by $\psi$ being normalized since it's an infradistribution. This same proof works if you swap out the 1 with a 0, so we have normalization for $\Theta$. 

T6.2 All that remains is checking the causality condition. We'll be using the alternate rephrasing of causality. We have $\Theta$ defined as

$\Theta \left({\pi }^{\prime }\right):=p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{{\pi }^{\prime }})$

and want to derive our rephrasing of causality, that for any $U$ and ${\pi }^{\prime }$ and $\zeta$ and family $U_{\pi }$, we have

$(\forall e:U({\pi }^{\prime }\cdot e)\ge E_{\pi \sim \zeta }[U_{\pi }(\pi \cdot e)\left]\right)\to \Theta \left({\pi }^{\prime }\right)\left(U\right)\ge E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

Accordingly, we get to fix a $U,{\pi }^{\prime },\zeta$, and family of functions $U_{\pi }$, and assume

$\forall e:U({\pi }^{\prime }\cdot e)\ge E_{\pi \sim \zeta }\left[U_{\pi }\right(\pi \cdot e\left)\right]$

Our proof target is

$\Theta \left({\pi }^{\prime }\right)\left(U\right)\ge E_{\pi \sim \zeta }\left[\Theta \right(\pi \left)\right(U_{\pi }\left)\right]$

Applying our reexpression of $\Theta$ in terms of $\psi$ and $K_{:\infty }^{\pi }$ and projection, we get

$p{r}_{(A\times O{)}^{\omega }\ast }(\psi ⋉K_{:\infty }^{{\pi }^{\prime }})(\lambda a{o}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)\ge E_{\pi \sim \zeta }\left[p{r}_{(A\times O{)}^{\omega }\ast }\right(\psi ⋉K_{:\infty }^{\pi }\left)\right(\lambda a{o}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

Undoing the projections on both sides, we get

$(\psi ⋉K_{:\infty }^{{\pi }^{\prime }})(\lambda s_0,ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)\ge E_{\pi \sim \zeta }\left[\right(\psi ⋉K_{:\infty }^{\pi }\left)\right(\lambda s_0,ao{s}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

Unpacking the semidirect product, we get

$\psi (\lambda s_0.K_{:\infty }^{{\pi }^{\prime }}(s_0\left)\right(\lambda ao{s}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)\ge E_{\pi \sim \zeta }\left[\psi \right(\lambda s_0.K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left)\right]$

Now, we can notice something interesting here. By concavity for infradistributions, we have

$\psi (\lambda s_0.E_{\pi \sim \zeta }[K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left]\right)\ge E_{\pi \sim \zeta }\left[\psi \right(\lambda s_0.K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left)\right]$

So, our new proof target becomes

$\psi (\lambda s_0.K_{:\infty }^{{\pi }^{\prime }}(s_0\left)\right(\lambda ao{s}_{1:\infty }.U\left(a{o}_{1:\infty }\right)\left)\right)\ge \psi (\lambda s_0.E_{\pi \sim \zeta }[K_{:\infty }^{\pi }\left(s_0\right)(\lambda ao{s}_{1:\infty }.U_{\pi }(a{o}_{1:\infty }\left)\right)\left]\right)$

Because if we hit that, we can stitch the inequalities together. The obvious move to show this new result is to apply monotonicity of infradistributions. If the inner function on the left hand side was always above the inner function on the right hand side, we'd have our result by infradistribution monotonicity. So, our new proof target becomes

$\forall s_0:K_{:\infty }^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)\ge E_{\pi \sim \zeta }\left[K_{:\infty }^{\pi }\right(s_0\left)\right(\lambda ao{s}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

At this point, now that we've gotten rid of $\psi$, we can use the full power of crisp infradistributions. Crisp infradistributions are just a set of probability distributions! Remember that the semidirect product, $\psi ⋉K$, can be viewed as taking a probability distribution from $\psi$, and for each $x$, picking a conditional probability distribution from $K\left(x\right)$, and all the probability distributions of that form make up $\psi ⋉K$.

In particular, the infinitely iterated semidirect product here can be written as a repeated process where, for each history of the form $s_0,ao{s}_{1:n},a,$ Murphy gets to select a probability distribution over the next observation and state from $K(s_n,a)$ (as a set of probability distributions) to fill in the next part of the action-observation-state tree. Accordingly every single probability distribution in $K_{:\infty }^{\pi }\left(s_0\right)$ can be written as $\pi$ interacting with an expanded probabilistic environment $e^{\Delta +}$ of type $(A\times O\times S{)}^{<\omega }\times A\to \Delta (O\times S)$ (which gives Murphy's choice wherever it needs to pick the next observation and state), subject to the constraints that

$e^{\Delta +}(ao{s}_{1:n},a)\in K(s_n,a)$

and

$e^{\Delta +}(\varnothing ,a)\in K(s_0,a)$

We'll abbreviate this property that $e^{\Delta +}$ always picks stuff from the appropriate $K$ set and starts off picking from $K(s_0,a)$ as $e^{\Delta +}\sim K,s_0$. 

Our old proof goal of

$\forall s_0:K_{:\infty }^{{\pi }^{\prime }}\left(s_0\right)(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)\ge E_{\pi \sim \zeta }\left[K_{:\infty }^{\pi }\right(s_0\left)\right(\lambda ao{s}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

can be rephrased as

$\forall s_0:{inf}_{{\mu }^{\prime }\in K_{:\infty }^{{\pi }^{\prime }}\left(s_0\right)}{\mu }^{\prime }(\lambda ao{s}_{1:\infty }.U(a{o}_{1:\infty }\left)\right)\ge E_{\pi \sim \zeta }\left[{inf}_{{\mu }_{\pi }\in K_{:\infty }^{\pi }\left(s_0\right)}{\mu }_{\pi }\right(\lambda ao{s}_{1:\infty }.U_{\pi }\left(a{o}_{1:\infty }\right)\left)\right]$

and then rephrased as

$\forall s_0:{inf}_{{\mu }^{\prime }\in K_{:\infty }^{{\pi }^{\prime }}\left(s_0\right)}{E}_{ao{s}_{1:\infty }\sim {\mu }^{\prime }}\left[U\right(a{o}_{1:\infty }\left)\right]\ge E_{\pi \sim \zeta }\left[{inf}_{{\mu }_{\pi }\in K_{:\infty }^{\pi }\left(s_0\right)}{E}_{ao{s}_{1:\infty }\sim {\mu }_{\pi }}\right[U_{\pi }\left(a{o}_{1:\infty }\right)\left]\right]$

And now, by our earlier discussion, we can rephrase this statement in terms of picking expanded probabilistic environments.

$\forall s_0:{inf}_{e^{{\Delta }^{\prime }+}\sim K,s_0}{E}_{ao{s}_{1:\infty }\sim {\pi }^{\prime }\cdot e^{{\Delta }^{\prime }+}}\left[U\right(a{o}_{1:\infty }\left)\right]\ge E_{\pi \sim \zeta }\left[{inf}_{e_{\pi }^{\Delta +}\sim K,s_0}{E}_{ao{s}_{1:\infty }\sim \pi \cdot e_{\pi }^{\Delta +}}\right[U_{\pi }\left(a{o}_{1:\infty }\right)\left]\right]$

Now, on the right side, since the set we're selecting the expanded environments from is the same each time and doesn't depend on $\pi$, we can freely move the inf outside of the expectation. It is unconditionally true that

${inf}_{e^{\Delta +}\sim K,s_0}{E}_{\pi \sim \zeta }\left[E_{ao{s}_{1:\infty }\sim \pi \cdot e^{\Delta +}}\right[U_{\pi }\left(a{o}_{1:\infty }\right)\left]\right]\ge E_{\pi \sim \zeta }\left[{inf}_{e_{\pi }^{\Delta +}\sim K,s_0}{E}_{ao{s}_{1:\infty }\sim \pi \cdot e_{\pi }^{\Delta +}}\right[U_{\pi }\left(a{o}_{1:\infty }\right)\left]\right]$

So now, our proof goal shifts to

$\forall s_0:{inf}_{e^{{\Delta }^{\prime }+}\sim K,s_0}{E}_{ao{s}_{1:\infty }\sim {\pi }^{\prime }\cdot e^{{\Delta }^{\prime }+}}\left[U\right(a{o}_{1:\infty }\left)\right]\ge {inf}_{e^{\Delta +}\sim K,s_0}{E}_{\pi \sim \zeta }\left[E_{ao{s}_{1:\infty }\sim \pi \cdot e^{\Delta +}}\right[U_{\pi }\left(a{o}_{1:\infty }\right)\left]\right]$

because if that were true, we could pair it up with the always-true inequality to hit our old proof goal. And we'd be able to show this proof goal if we showed the following, more ambitious result.

$\forall e^{\Delta +}:E_{ao{s}_{1:\infty }\sim {\pi }^{\prime }\cdot e^{\Delta +}}\left[U\right(a{o}_{1:\infty }\left)\right]\ge E_{\pi \sim \zeta }\left[E_{ao{s}_{1:\infty }\sim \pi \cdot e^{\Delta +}}\right[U_{\pi }\left(a{o}_{1:\infty }\right)\left]\right]$

Note that we're not restricting to compatibility with $K$ and $s_0$, we're trying to show it for any expanded probabilistic environment of type $(A\times O\times S{)}^{<\omega }\times A\to \Delta (O\times S)$. We can rephrase this new proof goal slightly, viewing ourselves as selecting an action and observation history.

$\forall e^{\Delta +}:E_{a{o}_{1:\infty }\sim p{r}_{(A\times O{)}^{\omega }\ast }({\pi }^{\prime }\cdot e^{\Delta +})}\left[U\right(a{o}_{1:\infty }\left)\right]\ge E_{\pi \sim \zeta }\left[E_{a{o}_{1:\infty }\sim p{r}_{(A\times O{)}^{\omega }\ast }(\pi \cdot e^{\Delta +})}\right[U_{\pi }\left(a{o}_{1:\infty }\right)\left]\right]$

Now, for any expanded probabilistic environment $e^{\Delta +}:(A\times O\times S{)}^{<\omega }\times A\to \Delta (O\times S)$, there is a unique corresponding probabilistic environment $e^{\Delta }$ of type $(A\times O{)}^{<\omega }\times A\to \Delta O$ where, for any policy, $p{r}_{(A\times O{)}^{\omega }\ast }(\pi \cdot e^{\Delta +})=\pi \cdot e^{\Delta }$. This is just the classical result that any POMDP can be viewed as a MDP with a state space consisting of finite histories, it still behaves the same. Using this swap, our new proof goal is:

$\forall e^{\Delta }:E_{a{o}_{1:\infty }\sim {\pi }^{\prime }\cdot e^{\Delta }}\left[U\right(a{o}_{1:\infty }\left)\right]\ge E_{\pi \sim \zeta }\left[E_{a{o}_{1:\infty }\sim \pi \cdot e^{\Delta }}\right[U_{\pi }\left(a{o}_{1:\infty }\right)\left]\right]$

Where $e^{\Delta }$ is an arbitrary probabilistic environment. Now, you can take any probabilistic environment $e^{\Delta }$ and view it as a mixture of deterministic environments $e$. So we can rephrase $e^{\Delta }$ as, at the start of time, picking a $e$ from $\xi \in \Delta E$ for some particular $\xi$. This is our mixture of deterministic environments that makes up $e^{\Delta }$. This mixture isn't necessarily unique, but there's always some mixture of deterministic enivironments that works to make $e^{\Delta }$ where $e^{\Delta }$ is arbitrary. So, our new proof goal becomes:

$\forall \xi \in \Delta E:E_{e\sim \xi }\left[E_{a{o}_{1:\infty }\sim {\pi }^{\prime }\cdot e}\right[U\left(a{o}_{1:\infty }\right)\left]\right]\ge E_{\pi \sim \zeta }\left[E_{e\sim \xi }\right[E_{a{o}_{1:\infty }\sim \pi \cdot e}\left[U_{\pi }\right(a{o}_{1:\infty }\left)\right]\left]\right]$

Since $\pi \cdot e$ is just a dirac-delta distribution on a particular history, we can substitute that in to get the equivalent

$\forall \xi \in \Delta E:E_{e\sim \xi }\left[U\right({\pi }^{\prime }\cdot e\left)\right]\ge E_{\pi \sim \zeta }\left[E_{e\sim \xi }\right[U_{\pi }(\pi \cdot e)\left]\right]$

Now we just swap the two expectations.

$\forall \xi \in \Delta E:E_{e\sim \xi }\left[U\right({\pi }^{\prime }\cdot e\left)\right]\ge E_{e\sim \xi }\left[E_{\pi \sim \zeta }\right[U_{\pi }(\pi \cdot e)\left]\right]$

And then we remember that our starting assumption was

$\forall e:U({\pi }^{\prime }\cdot e)\ge E_{\pi \sim \zeta }\left[U_{\pi }\right(\pi \cdot e\left)\right]$

So we've managed to hit our proof target and we're done, this propagates back to show causality for $\Theta$.

Theorem 7: Pseudocausal to Causal Translation: The following diagram commutes when the bottom belief function $\Theta$ is pseudocausal. The upwards arrows are the causal translation procedures, and the top arrows are the usual morphisms between the type signatures. The new belief function ${\Theta }^c$ is causal. Also, if $U:(A\times O{)}^{\omega }\to [0,1]$, and $U^N:(A\times (O+N){)}^{\omega }\to [0,1]$ is defined as $1$ for any history containing Nirvana, and $U\left(h\right)$ for any nirvana-free history, then $\forall \pi :{\Theta }^c\left(\pi \right)\left(U^N\right)=\Theta \left(\pi \right)\left(U\right)$.

T7.0 Preliminaries. Let's restate what the translations are. The notation $d(e,h)$ is that $e$"defends" $h$. $e$ defends $h$ if it responds to any prefix of $h$ which ends in an action with either the next observation in $h$, or Nirvana, and responds to any non-prefixes of $h$ with Nirvana.

Also, we'll write $h^N\sim {\pi }^{\prime },h$ if $h^N$ is "compatible" with ${\pi }^{\prime }$ and $h$. The criterion for this is that $h^N\sim {\pi }^{\prime }$, and that any prefix of $h^N$ which ends in an action and contains no Nirvana observations must either be a prefix of $h$, or only deviate from $h$ in the last action. An alternate way to state that is that $h^N$ is capable of being produced by a copolicy which defends $h$, interacting with ${\pi }^{\prime }$.

With these two notes, we introduce the infrakernels $K_d:(A\times O{)}^{\omega }\stackrel{ik}{\to }E$, and $K_{{\pi }^{\prime }}:(A\times O{)}^{\omega }\stackrel{ik}{\to }(A\times (O+N){)}^{\omega }$.

$K_d\left(h\right)$ is total uncertainty over $e$ such that $e$ defends $h$. $K_d\left(h\right)\left(f\right):={inf}_{e:d(e,h)}f\left(e\right)$

And $K_{{\pi }^{\prime }}\left(h\right)$ is total uncertainty over $h^N$ such that $h^N$ is compatible with ${\pi }^{\prime }$ and $h$. $K_{{\pi }^{\prime }}\left(h\right)\left(U^N\right):={inf}_{h^N\sim {\pi }^{\prime },h}{U}^N\left(h^N\right)$

Now, to briefly recap the three translations.For first-person static translation, we have

${\Theta }^c\left({\pi }^{\prime }\right):=p{r}_{(A\times (O+N){)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta ⋉K_{{\pi }^{\prime }})$

Where $\Theta$ is the original belief function.

For third-person static translation, we have

$E:=p{r}_{E\ast }(D⋉K_d)$

Where $D$ is the original infradistribution over $(A\times O{)}^{\omega }$.

For first-person dynamic translation, the new infrakernel has type signature

$\left(\right(A\times O{)}^{\omega }+N)\times A\stackrel{ik}{\to }((O+N)\times \left(\right(A\times O{)}^{\omega }+N\left)\right)$

Ie, the state space is destinies plus a single Nirvana state, and the observation state is the old space of observations plus a Nirvana observation. $N$ is used for the Nirvana observation, and $N$ is used for the Nirvana state. The transition dynamics are:

$\forall a^{\prime }\in A:{\to }_N(N,a^{\prime }):={\delta }_{N,N}$

and, if $a^{\prime }\ne a$, then ${\to }_N(aoh,a^{\prime }):={\delta }_{N,N}$

and otherwise, ${\to }_N(aoh,a):={\delta }_{o,h}\vee {\delta }_{N,N}$

The initial infradistribution is $i_{\ast }\left({\psi }_F\right)$, the obvious injection of ${\psi }_F$ from $(A\times O{)}^{\omega }$ to $(A\times O{)}^{\omega }+N$.

The obvious way to show this theorem is that we can assume the bottom part of the diagram commutes and ${\psi }_F,\Theta ,D$ are all pseudocausal, and then show that all three paths to ${\Theta }^c$ produce the same result, and it's causal. Then we just wrap up that last part about the utility functions.

Fortunately, assuming all three paths produce the same ${\Theta }^c$ belief function, it's trivial to show that it's causal. $i_{\ast }\left({\psi }_F\right)$ is an infradistribution since ${\psi }_F$ is, and ${\to }_N$ is a crisp infrakernel, so we can just invoke Theorem 6 that crisp infrakernels produce causal belief functions to show causality for ${\Theta }^c$. So we only have to check that all three paths produce the same result, and show the result about the utility functions. Rephrasing one of the proofs is one phase, and then there are two more phases showing that the other two phases hit the same target, and the last phase showing our result about the utility functions.

 We want to show that

${\Theta }^c\left({\pi }^{\prime }\right)=({\pi }^{\prime }\cdot {)}_{\ast }(E)=p{r}_{(A\times (O+N){)}^{\omega }\ast }(i_{\ast }\left({\psi }_F\right)⋉{\to }_{N:\infty }^{{\pi }^{\prime }})$

T7.1 First, let's try to rephrase ${\Theta }^c\left({\pi }^{\prime }\right)\left(U^N\right)$ into a more handy form for future use. Invoking our definition of ${\Theta }^c\left({\pi }^{\prime }\right)$, we have:

${\Theta }^c\left({\pi }^{\prime }\right)\left(U^N\right)=p{r}_{(A\times (O+N){)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta ⋉K_{{\pi }^{\prime }})\left(U^N\right)$

Then, we undo the projection

$=({\top }_{\Pi }⋉\Theta ⋉K_{{\pi }^{\prime }})(\lambda \pi ,h,h^N.U^N(h^N\left)\right)$

And unpack the semidirect product

$={\top }_{\Pi }(\lambda \pi .\Theta (\pi \left)\right(\lambda h.K_{{\pi }^{\prime }}\left(h\right)(\lambda h^N.U^N(h^N\left)\right)\left)\right)$

And unpack what ${\top }_{\Pi }$ means

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.K_{{\pi }^{\prime }}(h\left)\right(\lambda h^N.U^N\left(h^N\right)\left)\right)$

And then apply the definition of $K_{{\pi }^{\prime }}\left(h\right)$

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.{inf}_{h^N\sim {\pi }^{\prime },h}{U}^N(h^N\left)\right)$

This will be our final rephrasing of ${\Theta }^c\left({\pi }^{\prime }\right)\left(U^N\right)$. Our job is to derive this result for the other two paths.

T7.2 First up, the third-person static translation. We can start with definitions.

$({\pi }^{\prime }\cdot {)}_{\ast }(E\left)\right(U^N)=({\pi }^{\prime }\cdot {)}_{\ast }\left(p{r}_{E\ast }\right(D⋉K_d\left)\right)\left(U^N\right)$

And then, we can recall that since $D$ and $\Theta$ are assumed to commute, we can define $D$ in terms of $\Theta$ via $D=p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta )$. Making this substitution, we get

$=({\pi }^{\prime }\cdot {)}_{\ast }(p{r}_{E\ast }\left(\right(p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta ))⋉K_d)\left)\right(U^N)$

We undo the first pushforward

$=p{r}_{E\ast }\left(\right(p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta ))⋉K_d)(\lambda e.U^N({\pi }^{\prime }\cdot e\left)\right)$

And then the projection

$=\left(\right(p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta ))⋉K_d)(\lambda h,e.U^N({\pi }^{\prime }\cdot e\left)\right)$

And unpack the semidirect product

$=p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta )(\lambda h.K_d(h\left)\right(\lambda e.U^N({\pi }^{\prime }\cdot e)\left)\right)$

And remove the projection

$=({\top }_{\Pi }⋉\Theta )(\lambda \pi ,h.K_d(h\left)\right(\lambda e.U^N({\pi }^{\prime }\cdot e)\left)\right)$

and unpack the semidirect product and what ${\top }_{\Pi }$ is

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.K_d(h\left)\right(\lambda e.U^N({\pi }^{\prime }\cdot e)\left)\right)$

Now, we recall that $K_d\left(h\right)$ is all the $e$ that defend $h$, to get

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.{inf}_{e:d(e,h)}{U}^N({\pi }^{\prime }\cdot e\left)\right)$

At this point we can realize that for any $e$ which defends $h$, when $e$ interacts with ${\pi }^{\prime }$, it makes a $h^N$ that is compatible with ${\pi }^{\prime }$ and $h$. Further, all $h^N$ compatible with ${\pi }^{\prime }$ and $h$ have an $e$ which produces them. If $h^N$ has its nirvana-free prefix not being a prefix of $h$, then the defending $e$ which doesn't end $h$ early, just sends deviations to Nirvana, is capable of producing it. If $h^N$ looks like $h$ but ended early with Nirvana, you can just have a defending $e$ which ends with Nirvana at the same time. So we can rewrite this as

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.{inf}_{h^N\sim {\pi }^{\prime },h}:U^N(h^N\left)\right)$

And this is exactly the form we got for $\Theta \left({\pi }^{\prime }\right)\left(U^N\right)$.

T7.3 Time for the third and final translation. We want to show that

$p{r}_{(A\times (O+N){)}^{\omega }\ast }\left(i_{\ast }\right({\psi }_F)⋉{\to }_{N:\infty }^{{\pi }^{\prime }})\left(U^N\right)$

is what we want. Because the pseudocausal square commutes, we have that ${\psi }^F=p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta )$, so we can make that substitution to yield

$=p{r}_{(A\times (O+N){)}^{\omega }\ast }\left(i_{\ast }\right(p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta ))⋉{\to }_{N:\infty }^{{\pi }^{\prime }})\left(U^N\right)$

Remove the projection, to get

$=\left(i_{\ast }\right(p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta ))⋉{\to }_{N:\infty }^{{\pi }^{\prime }})(\lambda s_0^N,ao{s}_{1:\infty }^N.U^N(a{o}_{1:\infty }^N\left)\right)$

For this notation, we're using $s^N$ to refer to an element of $(A\times O{)}^{\omega }+N$, the state space. $ao{s}_{1:\infty }^N$ is an element of $(A\times (O+N)\times ((A\times O{)}^{\omega }+N){)}^{\omega }$, a full unrolling. $a{o}_{1:\infty }^N$ is the projection of this to $(A\times (O+N){)}^{\omega }$.

We unpack the semidirect product to yield

$=i_{\ast }\left(p{r}_{(A\times O{)}^{\omega }\ast }\right({\top }_{\Pi }⋉\Theta \left)\right)(\lambda s_0^N.{\to }_{N:\infty }^{{\pi }^{\prime }}(s_0^N\left)\right(\lambda ao{s}_{1:\infty }^N.U^N\left(a{o}_{1:\infty }^N\right)\left)\right)$

and rewrite the injection pushforward

$=p{r}_{(A\times O{)}^{\omega }\ast }({\top }_{\Pi }⋉\Theta )(\lambda h.{\to }_{N:\infty }^{{\pi }^{\prime }}(h\left)\right(\lambda ao{s}_{1:\infty }^N.U^N\left(a{o}_{1:\infty }^N\right)\left)\right)$

and remove the projection

$=({\top }_{\Pi }⋉\Theta )(\lambda \pi ,h.{\to }_{N:\infty }^{{\pi }^{\prime }}(h\left)\right(\lambda ao{s}_{1:\infty }^N.U^N\left(a{o}_{1:\infty }^N\right)\left)\right)$

And unpack the semidirect product along with ${\top }_{\Pi }$.

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.{\to }_{N:\infty }^{{\pi }^{\prime }}(h\left)\right(\lambda ao{s}_{1:\infty }^N.U^N\left(a{o}_{1:\infty }^N\right)\left)\right)$

Now we rewrite this as a projection to yield

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.p{r}_{(A\times (O+N){)}^{\omega }\ast }({\to }_{N:\infty }^{{\pi }^{\prime }}\left(h\right)\left)\right(\lambda a{o}_{1:\infty }^N.U^N\left(a{o}_{1:\infty }^N\right)\left)\right)$

And do a little bit of reindexing for convenience, swapping out the symbol $a{o}_{1:\infty }^N$ for $h^N$, getting

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.p{r}_{(A\times (O+N){)}^{\omega }\ast }({\to }_{N:\infty }^{{\pi }^{\prime }}\left(h\right)\left)\right(\lambda h^N.U^N\left(h^N\right)\left)\right)$

And now, we can ask what $p{r}_{(A\times (O+N){)}^{\omega }\ast }\left({\to }_{N:\infty }^{{\pi }^{\prime }}\right(h\left)\right)$ is. Basically, the starting state is the destiny $h$, and then ${\pi }^{\prime }$ interacts with it through the kernel ${\to }_N$. Due to how ${\to }_N$ is defined, it can do one of three things. First, it could just unroll $h$ all the way to completion, if $h$ is the sort of history that's compatible with ${\pi }^{\prime }$. Second, it could partially unroll $h$ and deviate to Nirvana early, even if ${\pi }^{\prime }$ is compatible with more, because of how ${\to }_N(aoh,a)$ is defined. Finally, ${\pi }^{\prime }$ could deviate from $h$ and then ${\to }_N$ would have to respond with Nirvana. And of course, once you're in a Nirvana state, you're in there for good. Hm, you have total uncertainty over histories $h^N$ compatible with ${\pi }^{\prime }$ and $h$, any of them at all could be made by $p{r}_{(A\times (O+N){)}^{\omega }\ast }\left({\to }_{N:\infty }^{{\pi }^{\prime }}\right(h\left)\right)$. So, this projection of the infrakernel unrolling $h$ is just $K_{{\pi }^{\prime }}\left(h\right)$. We get

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.K_{{\pi }^{\prime }}(h\left)\right(\lambda h^N.U^N\left(h^N\right)\left)\right)$

And then we use what $K_{{\pi }^{\prime }}\left(h\right)$ does to functions, to get

$={inf}_{\pi }\Theta \left(\pi \right)(\lambda h.{inf}_{h^N\sim {\pi }^{\prime },h}{U}^N(h^N\left)\right)$

Which is exactly the form we need. So, all three translation procedures produce identical belief functions.

T7.4 The only thing which remains to wrap this result up is guaranteeing that, if $U^N:(A\times (O+N){)}^{\omega }\to [0,1]$ is 1 if the history contains Nirvana, (or infinity for the $R$ type signature), and $U$ otherwise, then ${\Theta }^c\left({\pi }^{\prime }\right)\left(U^N\right)=\Theta \left({\pi }^{\prime }\right)\left(U\right)$.