Solutions for Chapters 64–66

The supports are $\{b\}$ and $\{b,c\}$, respectively. Moreover $$⟨a⟩(a,b)=⟨c⟩(c,b).$$ To verify the equation, choose fresh $d$. Both transposition actions, $(ad)\cdot (a,b)$ and $(cd)\cdot (c,b)$, give $(d,b)$. The second abstraction cannot equal $⟨c⟩(c,b)$, because equal nominal elements have equal least support, while $\{b,c\}\ne \{b\}$.

Restriction at $a$ discards $z$, retains the later fresh declaration of $b$, discards $y$, removes $a$, and returns $x:X;\mathsf{fresh}b:\beta$. Restriction at $b$ discards $z$, removes $b$, and returns $x:X;\mathsf{fresh}a:\alpha ,y:P(a)$. Rule R-Var discards $y$ because $P(a)$ may mention the name being removed; R-Name retains $b$ because its freshness declaration is stable under removal of the earlier name.

Assume ${\mathrm{\Gamma }}^{\prime };\mathsf{fresh}a:\alpha ⊢M:B$ and $\mathrm{\Gamma }\mathsf{restrict}b:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }$. Name abstraction gives ${\mathrm{\Gamma }}^{\prime }⊢⟨a:\alpha ⟩M:\mathsf{N}a:\alpha .B$, and concretion gives $\mathrm{\Gamma }⊢(⟨a:\alpha ⟩M)@b:B[b/a]$. The name-substitution instance of general substitution gives the same type to $M[b/a]$, hence beta is typed. If $M$ used a variable declared after $b$, it would not type in ${\mathrm{\Gamma }}^{\prime }$, so the concretion premise would fail.

Represent the terms as $⟨a⟩⟨b⟩a$ and $⟨c⟩⟨d⟩c$. Extend by one fresh $e$, restrict the extension back to the common prefix, and concrete both outer abstractions at $e$. Name beta gives $⟨b⟩e$ and $⟨d⟩e$. Extensional equality at the inner abstraction type opens both at another fresh $f$, producing $e$ on each side. Structural name comparison closes the derivation. The first opening is the explicit use of restriction.

Frozen DNTT can introduce an abstraction and open it at a chosen literal, but it cannot inspect whether the opened body is that literal. The proposed function needs a name-equality/name-case eliminator. Adding it changes the canonical neutral heads, so algorithmic-equality completeness and adequacy must be proved again; normalization or canonicalization for the enlarged calculus must also be re-established.

Unfold $\mathrm{\forall }x.fx=gx$; this is the one definition-dependent step. It says that the predicate $\lambda x.fx=gx$ equals the constantly true predicate. Rule COMB specializes this equality at fresh $x$, and EQ-MP with the closed proof of $\mathrm{\top }$ yields $fx=gx$. Rule ABS now gives equality of $\lambda x.fx$ and $\lambda x.gx$. Eta rewrites both sides, and two uses of transitivity give $f=g$.

For ABS, equality of the bodies in every environment satisfying $\mathrm{\Gamma }$ gives equality of the denoted functions. Freshness of $x$ for $\mathrm{\Gamma }$ ensures that changing the argument does not change whether the assumptions hold. Without it, from assumption $x=0$ one could abstract the derivation of $x=0$ and conclude the false equation $(\lambda x.x)=(\lambda x.0)$ on a type with two elements. For DEDUCT-ANTISYM, under the undischarged assumptions the first premise excludes $(p,q)=(0,1)$ and the second excludes $(1,0)$; hence their Boolean denotations agree. The requirement that assumptions and conclusions have type $\mathsf{bool}$ is essential to that truth-value argument.

Transitivity follows pointwise from transitivity of equality on counts. The equation $\mathsf{count}(a,xs++ys)=\mathsf{count}(a,xs)+\mathsf{count}(a,ys)$ proves respectfulness. Apply $\mathsf{rep}$ to two lifted unions; their representatives have the same count at every $a$ by commutativity of addition, so quotient extensionality gives $A\uplus B=B\uplus A$. Nonemptiness is used once to introduce the new HOL type and once to choose the default value of $\mathsf{abs}$ outside the representing subset.

Use $\mathsf{VecPred}(A,n,xs)\equiv \mathsf{All}(A,xs)\wedge \mathsf{length}(xs)=n$. A translated function $f$ must satisfy $\mathrm{\forall }n,xs.\mathsf{VecPred}(A,n,xs)\Rightarrow \mathsf{length}(fnxs)=n+1$, together with its chosen codomain predicate. HOL assigns $f$ an ordinary simple type; dependency appears in the theorem guarding admissible arguments and results, not in its typing judgment.

Beta is a primitive rule. Eta, choice, and infinity are closed axioms. Functional and propositional extensionality are derived theorems; the latter also uses the two-valued Boolean encoding. The choice function and the infinite set interpreting $\mathsf{ind}$ are semantic constructions that validate the corresponding axioms, not additional inference rules.

The oracle lies inside the trusted base because it manufactures abstract theorem values without a kernel trace. Confinement is recovered exactly if every returned $\mathsf{oracle}(s)$ is semantically valid at its recorded assumptions and conclusion. Decidability, completeness, and termination of the oracle are unnecessary for soundness.

Take $$F={\mathsf{R}}_{\mathbb{N}\to \mathbb{N}}(\lambda x.x)(\lambda n.\lambda h.\lambda x.h(\mathsf{S}x)).$$ Then $F04\to 4$, $F14\to F05\to 4+1$, and repeating gives $F34\to F25\to F16\to F07\to 7$.

For candidate closure at $\sigma \to \tau$, apply a reduct of the function to arbitrary $u\in {\mathcal{R}}_{\sigma }$ and use closure at $\tau$. For neutral expansion, reductions of $tu$ reduce $t$, reduce $u$, or expose a head redex; induct lexicographically on the type and the sum of their finite reduction heights. Candidate fact 1 follows by applying an arrow term to a fresh reducible variable. Finally, reducible $n$ is strongly normalizing. Every reduction of $\mathsf{S}n$ is induced by a reduction of $n$, so $\mathsf{S}n$ is strongly normalizing and therefore belongs to ${\mathcal{R}}_{\mathbb{N}}$.

The first formula becomes $\mathrm{\exists }{F}^{\mathbb{N}\to \mathbb{N}}\mathrm{\forall }n.P(n,Fn)$. The implication becomes $$\mathrm{\exists }{U}^{(\mathbb{N}\to \mathbb{N})\to \mathbb{N}},Y^{(\mathbb{N}\to \mathbb{N})\to \mathbb{N}}\mathrm{\forall }F.(P(YF,F(YF))\to Q(UF)).$$ Here $U$ turns the premise’s candidate witness function into the existential witness for $Q$, while $Y$ chooses the premise input to challenge.

At zero choose zero. If $m=n^2$, choose $m+(n+n+1)$; arithmetic gives $m+2n+1=(n+1{)}^2$. Extraction yields $$\lambda n.{\mathsf{R}}_{\mathbb{N}}0(\lambda k.\lambda r.r+(k+k+1))n.$$ At $3$ it reduces through accumulators $0,1,4,9$. The reduction trace calculates the numeral; the target induction, using the recursor equations and ring equalities, proves that the numeral satisfies $m=n\cdot n$.

The witness player maps a proposed witness $x$ for $A$ forward to $Ux$ for $B$. Given a challenge $v$ to that result, the same strategy maps backwards to $Yxv$, a challenge to $A$. For $(\mathrm{\forall }n\mathrm{\exists }m.P(n,m))\to \mathrm{\exists }k.Q(k)$, deleting $Y$ loses the input $n=YF$ at which the premise function must be tested before concluding $Q(UF)$.

The chapter proves the direct $\mathsf{HA}$-to-$T$ theorem. The selected intensional, weakly extensional, and type-zero-equality higher-type variants, including ${\mathsf{HA}}_0^{\omega }$, admit corresponding direct variants. Full $E\text{-}{\mathsf{HA}}^{\omega }$ first needs a formal interpretation into the type-zero-equality system at the stated low-type boundary. Classical arithmetic first needs negative translation. General countable choice and classical analysis are not covered here; their selected realizers use the separately developed bar-recursive extension.

The final maximizing selector always chooses one. Hence the continuation at stage one is $x_1\mapsto 3x_0+x_1+5$, whose minimizing selector chooses zero. The first continuation is $x_0\mapsto 3x_0+5$, so the maximizing selector chooses one. Thus the tuple is $(1,0,1)$ and its score is eight. No comparison at stage zero is a tie, so reversing only its tie convention changes nothing.

The printed test asks , which is false, and therefore computes $c={\epsilon }_2(p_2)$ before recursing. The mutant asks $2\le 2$, which is true, and returns the zero stream. Consequently the mutant may have $\alpha (2)=0_X$ while the printed equation requires $\alpha (2)={\epsilon }_2(p_2)$. A selector that always returns $1_X\ne 0_X$ witnesses the failure.

At $|s|=2$, $$q_s^{\omega }:X^{\mathbb{N}}\to X^{\mathbb{N}}\times \mathbb{N},l:X^{\mathbb{N}}\times \mathbb{N}\to \mathbb{N},$$ $$P:X\to X^{\mathbb{N}}\times \mathbb{N},{\tilde{\delta }}_s(P)={\delta }_s(\lambda x.{\pi }_1(Px)):X,c:X.$$ The streams $s\ast (x\ast \beta )$ and $(s\ast x)\ast \beta$ agree coordinatewise. For , both return $s(i)$; at $i=2$, both return $x$; and above two both return $\beta (i-3)$. Hence $s\ast (x\ast \beta )=(s\ast x)\ast \beta$. Substitution of that identity into the definition of $q_s^{\omega }$ gives $(q_s^{\omega }{)}_x=q_{s\ast x}^{\omega }$. Therefore the EPS recursive branch has exactly the child SBR call required by the SBR equation. Since that child has the form $(s\ast x)\ast \beta$, it already preserves $s$. Therefore $\mathsf{put}(s,{\mathsf{SBR}}_{s\ast x})={\mathsf{SBR}}_{s\ast x}$, while the EPS branch is $s\ast (x\ast \beta )=(s\ast x)\ast \beta$. This is the final prefix-preservation step.

Choose $n=\alpha (0)+2$. Since $n\ge 1$, the zero extension ${\hat{\alpha }}_n$ retains coordinate zero, and For the second specification, continuity at a stream with no zero would require a finite prefix deciding the value zero. Extend any such prefix by a zero at a later coordinate. The value then becomes that later index, a contradiction. Thus the finite observation bound used in lemma 67.15 is unavailable.

Apply DNS to $B(n)\equiv \mathrm{\exists }x.A(n,x)$: $$(\mathrm{\forall }n\mathrm{\neg }\mathrm{\neg }\mathrm{\exists }x.A(n,x))\to \mathrm{\neg }\mathrm{\neg }\mathrm{\forall }n\mathrm{\exists }x.A(n,x).$$ Inside the final double negation, intuitionistic countable choice gives $\mathrm{\exists }f\mathrm{\forall }n.A(n,fn)$, which is ${\mathsf{cAC}}_{\mathbb{N}}$. In Spector’s equations, ${\epsilon }_n$ is the premise selector, $q$ is the outcome challenger, $\omega$ selects the challenged coordinate, $\alpha$ is the proposed choice sequence, and $p_n$ is its local counterexample continuation. A fixed horizon $m$ fails for a control that reads coordinate $m$, as in proposition 67.7.

Assume $i\le l(q(\alpha ))$. If the stage-$i$ call stopped, prefix factorization would give $\alpha =[\alpha ](i)\ast \mathbf{0}$, and hence a contradiction. The recursive equation therefore gives $\alpha (i)={\epsilon }_i(p_i)$. Prefix factorization at $i+1$ then rewrites the tail in $p_i(\alpha (i))$ to the tail of $\alpha$, yielding $p_i(\alpha (i))=q(\alpha )$.

At the all-one stream the proposed control returns one. For every finite prefix of that stream, append a zero beyond the prefix. The altered stream agrees on the entire observed prefix but receives value zero. Thus no finite observation determines the value at the all-one stream. Without continuity, Spector’s condition is not obtained, so is not known to be a bar.

The forward ledger is $$\mathsf{EPS}⟶\mathsf{SBR}:R^{\prime }=X^{\mathbb{N}}\times \mathbb{N},l={\pi }_2,q_s^{\omega },{\tilde{\delta }}_s;$$ it is verified in finite-type arithmetic and uses neither ${\mathrm{BI}}_{\mathrm{rel}}$ nor SPEC. The reverse ledger is $$\mathsf{SBR}\to \mathsf{BR}\to \mathsf{EPQ}\to \mathsf{epq}\to \mathsf{eps}\to \mathsf{EPS}.$$ The $\mathsf{BR}\to \mathsf{EPQ}$ and $\mathsf{epq}\to \mathsf{eps}$ arrows use ${\mathrm{BI}}_{\mathrm{rel}}$; the former also uses SPEC. The forward adapter therefore cannot establish the reverse arrow: definability in one direction is not symmetric.

Write $W$ for the loop followed by the final assertion and write $A_1,A_2,D$ for the two body assertions and decrement. For input $n$, the loop-head stores are exactly $(i,n)$, $0\le i\le n$. At every positive $i$, the reachable control suffixes are $$A_1;A_2;D;W,A_2;D;W,D;W,$$ all at store $(i,n)$, followed by $W$ at $(i-1,n)$; the while-unrolling conditional and the administrative $\mathbf{skip};c$ residuals add no stores. At $i=0$, the false guard reaches the final assertion and then $\mathbf{skip}$, still at $(0,n)$. Taking $n=0,1,2$ gives the six distinct loop-head stores $$(0,0),(1,1),(0,1),(2,2),(1,2),(0,2).$$ Each positive-body store satisfies $0\le i\le n$, and each exit store has $i=0$. Hence no reachable configuration is a predecessor of $\mathsf{error}$.

Let the bad entry be $\{0,+\}{-}^{\mathrm{♭}}\{0,+\}=\{0,+\}$. The smallest witness is $0-1=-1$: both operands lie in the declared concretizations, but the result does not. The best entry is $${\alpha }_{\mathsf{s}}\{m-n\mid m,n\ge 0\}=\{-,0,+\},$$ because $0-1$, $0-0$, and $1-0$ witness the three signs.

For decrement by one, the loop-head iteration is $\mathrm{\perp }$, then $x,y\mapsto [0,4]$, then the same store: the true filter gives $x\mapsto [1,4]$, decrement gives $[0,3]$, and joining with entry restores $[0,4]$. The false filter gives $x=[0,0]$. Thus $0\le x$ and the final $x=0$ are proved; independent intervals report the relational assertion $x\le y$ as possible error.

With decrement by two, the loop-head sequence is $\mathrm{\perp }$, $[0,4]$, $[-1,4]$, then stable at $[-1,4]$ for $x$, while $y=[0,4]$. The true filter $[1,4]$ maps to $[-1,2]$; the false exit is $[-1,0]$. Inputs $1$ and $3$ reach $x=-1$, so both the body nonnegativity assertion and final equality can fail.

Adjoin $\pm \mathrm{\infty }$ to the ordered threshold set $T=\{-1,0,1,10\}$. When a lower bound decreases, replace it by the greatest threshold not above the proposal; when an upper bound increases, replace it by the least threshold not below the proposal. Otherwise retain the old endpoint. The chosen interval contains both arguments, so coverage holds. Each endpoint moves only upward through the finite threshold list and then to infinity, so every finite product iteration terminates. On the counter chain the upper endpoints are $$0,1,10,+\mathrm{\infty },$$ whereas ordinary widening jumps from $0$ directly to $+\mathrm{\infty }$.

Before assignment, intervals give $x,y\in [0,+\mathrm{\infty }]$ and the DBM gives $x-y\le 0$. Assignment $z:=y$ copies the entire row and column of $y$: $D_{zw}^{\prime }=D_{yw}$ and $D_{wz}^{\prime }=D_{wy}$. Hence $z-y\le 0$, $y-z\le 0$, and closure with $x-y\le 0$ yields $x-z\le 0$, that is, $x\le z$. Interval reduction alone leaves $z\in [0,+\mathrm{\infty }]$, but the relational component proves the comparison. The rule $D_{zw}^{\prime }=D_{yw}$ while leaving the column of $z$ unchanged is unsound: from $y=0,z=1$, executing $z:=y$ makes $y-z=0$, contradicting the retained old bound $y-z\le -1$.

Before deleting $u$, add $\mathsf{Borrow}(a,p::q,b)$. Concretely, if $a.p$ reaches the reference stored at $u$, and following $q$ from that reference reaches the reference at $b$, then $a.(p::q)$ reaches $b$. Omitting the edge makes $b$ an unrooted live reference after $u$ is popped, violating the no-dangling-reference/rooted-path clause of $\mathsf{Inv}$.

Order types by inclusion of concretizations and take join to be $\vee$. The constant-guard term has type $\mathsf{Int}\vee \mathsf{Bool}$ under a purely structural branch rule; a filter that evaluates the guard reduces it to $\mathsf{Int}$. The union rules are sound by set union. They remain incomplete for safe higher-order programs that require intersections, polymorphism, or relational facts. Principality is not a proposition in this fragment: there are no type variables, substitutions, or instantiation preorder from which to define a most general type.

Let $\widehat{\mathsf{alloc}}$ return $(x,\ell )$, where $\ell$ is the most recent call site. Map a concrete binding address created at $\ell$ to that pair; then ${\alpha }_a(\mathsf{alloc}(\varsigma ))=\widehat{\mathsf{alloc}}(\alpha \varsigma )$ by definition, which is the allocation premise of the simulation. Monovariant allocation joins the two arguments to $x$ in $\{0,\mathsf{true}\}$. Call-site allocation stores $\{0\}$ at the first $(x,{\ell }_1)$ and $\{\mathsf{true}\}$ at the second $(x,{\ell }_2)$; the closure for $f$ may still be shared.

Use the chapter’s two-condition program. The edge combination $x\ne 0;y:=1;y=0$ is a syntactic path but has no concrete trace. Joining after the first conditional gives $x$ top and $y=[0,1]$; the second true filter leaves $x$ top, so the syntactic-path interval result reports a possible failure of $x=0$. Every semantic trace taking the second true edge previously took the first true edge and therefore has $x=0,y=0$; its assertion succeeds. The first claim follows by abstract edge composition; the second follows by induction over concrete transitions.

The concrete sum set is $\{-1,0,\dots ,7\}$, so its interval hull is $[-1,7]$. This is exactly the endpoint calculation $[1+(-2),3+4]$. The result $[-\mathrm{\infty },7]$ is also sound but less precise, because $[-1,7]⊊[-\mathrm{\infty },7]$; optimality of the hull excludes any strictly smaller sound interval.

For $c_1;c_2$, a terminal execution first reaches a terminal store of $c_1$ and then one of $c_2$. Apply the two induction hypotheses in that order. An error occurs either in $c_1$, or in $c_2$ after such a terminal store, exactly matching the disjunction in ${\mathsf{err}}^{\mathrm{♯}}$. For a loop, induction on completed iterations puts every head store in every $X$ satisfying ${\mathrm{\Phi }}_A(X)⊑X$; hence it lies in the selected least pre-fixed invariant. A false guard uses the exit refinement, while an error during a true-guard body uses the body error flag.

At entry, $(D_{xy},D_{yx})=(0,0)$. One body step proposes $(-1,1)$, and entrywise join gives $(0,1)$. The next two proposals and joins give $(0,2)$ and $(0,3)$. Widening retains stable $D_{xy}=0$ and drops the weakened reverse entry to $+\mathrm{\infty }$. Applying the body again proposes $(-1,+\mathrm{\infty })$; join with entry returns $(0,+\mathrm{\infty })$, so the widened matrix is pre-fixed and still entails $x-y\le 0$.

The local analyzer assumes the concrete semantics, concretizations, local transformer proofs, and checked pre-fixed point. The machine theorem assumes the CEK/CESK rules, abstraction map, finite store order, and tick/allocation contracts. Verasco’s imported theorem additionally fixes its C$\mathrm{\#}$minor semantics and five section parameters. The interval-trace bound assumes the paper’s typed probabilistic language plus countability and compatibility or exhaustivity. For example, moving exhaustivity to the local interval analyzer would not justify an upper measure bound: ordinary store coverage is not an almost-everywhere trace cover.

The left branch stores $\sigma (y)={\alpha }_0+1$. At $\rho (0)=-2$, the instance is $s(x)=-2,s(y)=-1$. Both $-2\le 0$ and $-1\le 2$ hold.

S-If-T adds ${\alpha }_0\le 0$, and S-If-F adds $0-{\alpha }_0\le -1$. The feasible pass models are $-2$ on the left and $1$ on the right. The right failure has model $4$. Replays yield $(x,y)=(-2,-1),(1,0),(4,3)$, with only the last assertion failing. The left failure condition ${\alpha }_0\le 0\wedge {\alpha }_0\ge 2$ has no model.

Take $s(x)=0$, $\sigma (x)={\alpha }_0$, and $\rho (0)=0$. Concrete assignment sets $y=1$, while the erroneous symbolic store instantiates to $y=0$. The repaired rule stores $[x+1{]}_{\sigma }={\alpha }_0+1$; the copy-plus-constant line of expression correspondence then proves both sides equal to $1$.

The stronger state $x\le -1\wedge y\le 1$ is subsumed by $x\le 0\wedge y\le 1$. For the first consequent, add its complement $x\ge 1$; the edges for $x\le -1$ and $-x\le -1$ form a cycle of total weight $-2$. The second consequent is already an atom. If the stores differ, the two path conditions may describe equal inputs but instantiate different concrete stores, so the representation inclusion used by the proof does not follow.

Use $m$ inputs and branch independently on $x_i\le 0$, with skip in both branches. Every Boolean branch vector has a model, hence there are $2^m$ feasible leaves. Depth-first reaches one complete vector before siblings; breadth-first reaches all depth-$d$ prefixes first; concolic negation follows one vector and schedules selected prefixes. Completeness requires that every pending node, respectively every retained branch-negation obligation, is eventually selected and that each supported solver query eventually returns checkable evidence.

Assignment maps each guarded term through the same copy-plus-constant operation. Evaluation distributes over $\mathsf{ite}$, so the branch selected by ${\mathrm{\Phi }}_i$ produces exactly the post-store obtained by assigning in ${\sigma }_i$. For a near miss, merge $x=0,y=0,z=0$ and $x=1,y=1,z=1$ with the disjunctive condition but select the first store for $y$ and the second for $z$. Input $x=0$ then yields $y=0,z=1$, represented by neither input state.

Extend representation by requiring equal domains and $H(a)=[[\hat{H}(a){]]}_{\rho }$ at every allocated address. The read rules require $[[\sigma (p){]]}_{\rho }$ to lie in both domains. They update $x$ with $H(s(p))$ and $\hat{H}(\sigma (p))$, respectively. Heap representation makes those values equal, while all other variables and heap cells are unchanged.

Without the pc premise, each branch derives $l:=0$ or $l:=1$ from a low constant. Stores $s_0(h)=0,s_1(h)=7$ agreeing on $l$ select opposite branches and finish with public values $0$ and $1$. Thus the derived program violates low equivalence.

From $p{⊑}_{\mathsf{sec}}{p}^{\prime }$, join monotonicity gives $p\bigsqcup \ell {⊑}_{\mathsf{sec}}{p}^{\prime }\bigsqcup \ell$. An IF-While derivation at $p^{\prime }$ types its body at $p^{\prime }\bigsqcup \ell$; the induction hypothesis therefore types the body at $p\bigsqcup \ell$, and IF-While rebuilds the conclusion at $p$.

Relabel $l$ as $H$; each branch then satisfies $H\bigsqcup \mathrm{\perp }{⊑}_{\mathsf{sec}}H$. Alternatively make both branches assign $0$. The latter has equal public results in all terminating runs, but the checker still requires $H{⊑}_{\mathsf{sec}}L$, so it is a secure rejected program.

(a) is accepted and secure. (b) is rejected but secure: both runs write zero. (c) is rejected and leaks by the two stores from exercise 70.1. (d) is accepted and secure because a public value may flow into a secret location and the public projection does not change.

Let the guard label be $\ell \text{⧸}{⊑}_{\mathsf{sec}}o$. Every body derivation is typed at $p\bigsqcup \ell \text{⧸}{⊑}_{\mathsf{sec}}o$, so confinement relates its input and output. Induction on the finite first loop evaluation composes those relations until its exit store is low-equivalent to its initial store; repeat independently for the second run. Symmetry and transitivity compose $s_1^{\prime }{\approx }_{\mathrm{\Gamma }}^o{s}_1$, $s_1{\approx }_{\mathrm{\Gamma }}^o{s}_2$, and $s_2{\approx }_{\mathrm{\Gamma }}^o{s}_2^{\prime }$.

Take $\mathbf{while}h=0\mathbf{do}\mathbf{skip}$. Stores agreeing on all low variables but with secrets $0$ and $1$ yield divergence and termination. An observation with a termination bit distinguishes them. TINI requires two terminating derivations, so termination-sensitive noninterference must relate divergence as well as final stores.

Let be the intended release. A policy may relate two initial stores only when their secrets have equal parity; the required conclusion is ordinary low equivalence of outputs. Original low equivalence relates all secret values, including different parity, so the command violates the old theorem even though it meets the new policy.