Proof. Define parallel contraction \(\Rightarrow\) by reflexive variable and sort clauses, homomorphic clauses for all expression constructors, and the additional clause \[\frac{D\Rightarrow D'\qquad M\Rightarrow M'\qquad N\Rightarrow N'} {(\lambda x:D.M)N\Rightarrow M'[x:=N']}.\] In particular the homomorphic binder clauses reduce both children. Induction on a parallel derivation proves parallel substitution: if \(M\Rightarrow M'\) and \(N\Rightarrow N'\), then \(M[x:=N]\Rightarrow M'[x:=N']\). For its contracting case, rename the contracted binder fresh and use composition of substitutions; the other cases reapply the corresponding homomorphic clause.

Define \(M^*\), its complete development, recursively by developing every child, with \[((\lambda x:D.P)Q)^*=P^*[x:=Q^*]\] at an application whose original function is a lambda. At any other application use \((PQ)^*=P^*Q^*\). We claim that \(M\Rightarrow N\) implies \(N\Rightarrow M^*\). Prove this by induction on the parallel derivation. At an original root redex, either the first parallel step was homomorphic, in which case contract the root in the second step, or it contracted the root, in which case parallel substitution applies. At an original nonredex application, use the homomorphic clause in the second step, even if its function has become a lambda. The remaining cases follow by the corresponding homomorphic clauses and induction. Thus any two parallel reducts of \(M\) parallel-reduce to \(M^*\), proving the diamond property.

Every ordinary step is parallel. Conversely, every parallel step is a finite sequence of ordinary steps: first reduce the children and then perform its root contraction, if any. Hence the reflexive-transitive closures of the two relations coincide, and beta reduction is confluent. Convertible expressions consequently have a common reduct. Reducing a product never removes its outer constructor, whereas a sort is irreducible. Comparing the common reducts gives all the asserted compatibility and separation properties. ◻

Proof. It suffices to consider one step. Induct on the typing derivation. There are no steps from sorts or variables. At a final weakening or conversion, apply induction to its subject premise and reapply the same rule.

At product formation, a step in the domain preserves its original sort by induction. Lemma 5 transports the codomain sorting to the changed binder context, and the same product rule re-forms the result. A codomain step is handled by induction on its typing premise.

At abstraction, a step in the body is immediate by induction. For an annotation step \(D\to_\beta D'\), the supporting judgment \(\Gamma\vdash\Pi x:D.E:c\) is a strictly smaller premise derivation. Apply induction to its corresponding domain step to get \(\Gamma\vdash\Pi x:D'.E:c\). Product generation sorts \(D'\); context conversion then transports the body judgment to \(\Gamma,x:D'\). Abstraction gives the changed lambda its new product type. Convert back to the old product type, which is sorted by the original supporting premise.

At application, a step in the function preserves its product type by induction. A step \(N\to_\beta N'\) in the argument gives the new result type \(E[x:=N']\); convert this to \(E[x:=N]\), whose sorting was proved in Lemma 7.

It remains to treat a root contraction \((\lambda x:D_0.P)N\to_\beta P[x:=N]\). Suppose the application premises assign the function type \(\Pi x:D.E\) and the argument type \(D\). Generation of the function judgment gives some \(E_0,c\) such that \[\Gamma,x:D_0\vdash P:E_0, \qquad\Gamma\vdash\Pi x:D_0.E_0:c, \qquad\Pi x:D_0.E_0=_\beta\Pi x:D.E.\] Product compatibility gives \(D_0=_\beta D\) and \(E_0=_\beta E\). Generation of the supporting product sorts \(D_0\), so convert \(N:D\) to \(N:D_0\). Substitution yields \(\Gamma\vdash P[x:=N]:E_0[x:=N]\). Convert to the old application type \(E[x:=N]\), which is sorted by Lemma 7. This completes every reduction position, including positions inside annotations. ◻

Proof. Induct on the length of the neutral spine. At a variable, generation identifies both types with its declaration type up to conversion. For \(HN\), generation of its two typings gives function product types \(\Pi x:D.E\) and \(\Pi x:D'.E'\). Induction makes these convertible. Product compatibility gives \(E=_\beta E'\), so substitution makes their instantiated codomains convertible. These codomains are convertible to the original two result types by generation.

If a variable has type \(s\), its declaration type \(D\) is sorted by validity and thinning, and \(D=_\beta s\) by generation. Confluence and irreducibility of \(s\) give \(D\to_\beta^*s\). Subject reduction therefore sorts \(s\). For a nonempty neutral spine, the stronger application assertion in Lemma 7 sorts its expected type directly.

Finally, the head of a normal application cannot be a lambda, since that would give a redex. It cannot be a sort or product: generation makes any type of either head convertible to a sort, whereas the first application requires a product type. Product/sort separation excludes this. The only remaining head is a variable. ◻

Proof. Weak normalization supplies normal forms; confluence gives uniqueness. Subject reduction proves the first judgment and the assertion about sorting. Correctness of types says that \(A\) is sorted or is a literal sort. In the first case subject reduction sorts \(A^\#\), allowing conversion of the expected type. In the second case \(A^\#=A\), so there is nothing to convert if that sort is unsorted. Finally a normal application is neutral by Lemma 10, and a lambda cannot have a sort type by generation and product/sort separation. ◻

Proof. First recall how legality relates to typability. If \(E\) is a subject, it is typable by definition. If \(E\) is an expected type, correctness of types says that either \(E\) is a literal sort or \(\Gamma\vdash E:s\) for some context \(\Gamma\) and sort \(s\). Thus every nonliteral legal expression is typable. Also, context validity says that each declaration type is sorted in its preceding context, so declaration types introduce no further kind of untypable expression. Literal sorts have no \(\beta\)-redexes.

Choose a legal expression \(E\) that is not strongly normalizing. It is not a literal sort, so fix a finite derivation of a judgment \(\Gamma\vdash E:B\). For every use of conversion in this derivation, choose a finite raw \(\beta\)-conversion chain witnessing its side condition. Let \(\mathcal S_0\) contain all sorts occurring in the derivation and these chains. Let \(\mathcal A_0\) and \(\mathcal R_0\) contain the axiom pairs and formation triples used in the derivation, enlarging \(\mathcal S_0\) to contain their entries if necessary. These sets are finite, and the same derivation and conversion chains establish \(\Gamma\vdash E:B\) in \(\mathcal P_0\).

A full \(\beta\)-step introduces no new sort symbol: substitution can only copy symbols already present in the redex, and contextual reduction has the same property, including reduction in annotations. Consequently the infinite reduction from \(E\) witnessing failure of strong normalization is also a reduction in the raw syntax over \(\mathcal S_0\).

Conversely, every judgment derivable in \(\mathcal P_0\) is derivable in \(\mathcal P\). If \(F\) is legal in \(\mathcal P_0\), the weak-normalization hypothesis therefore supplies a finite reduction \(F\to_\beta^*N\) in \(\mathcal P\) with \(N\) normal. No term in this reduction contains a sort outside \(\mathcal S_0\). The reduction is thus available in \(\mathcal P_0\), and normality is unchanged, since it is the absence of a syntactic \(\beta\)-redex. This proves weak normalization of every legal expression of \(\mathcal P_0\), while \(E\) remains a legal expression that is not strongly normalizing. ◻

Proof. Partition the variable names into disjoint infinite sets \(V_0\) and \(V_1\). Only names in \(V_0\) will be declared in \(\Omega\); names in \(V_1\) remain available for bound variables. Because \(\mathcal S\) and the variable set are countable, the set of finite raw expressions is countable. We work up to \(\alpha\)-equivalence, or equivalently choose representatives when enumerating expressions.

Choose a sequence of pairs \((p,D)\), with \(p\) a nonnegative integer and \(D\) a raw expression, in which every pair occurs infinitely often. Construct finite contexts \(\Delta_n\) starting with the empty context. At stage \(n\), consider the scheduled pair \((p,D)\). If \(\Delta_n\) has at least \(p\) declarations and its initial segment of length \(p\) derives \(D:s\) for some sort \(s\), append a declaration \(y:D\), choosing \(y\in V_0\setminus\operatorname{dom}(\Delta_n)\). Otherwise leave \(\Delta_n\) unchanged. This is a set-theoretic construction and does not require a decision procedure for typing. In the append case, scope gives \(\mathrm{FV}(D)\subseteq \operatorname{dom}(\Delta_n)\), and thinning gives \(\Delta_n\vdash D:s\). Thus the new declaration is fresh and the extended context is valid. Induction proves validity at every stage.

Let \(\Omega\) be the sequence obtained by retaining all declarations appended in this construction. Every finite initial segment appears at some stage and is valid. No name from \(V_1\) is declared. If \(P\vdash D:s\) and \(P\) has length \(p\), then, once \(P\) has been constructed, every later occurrence of the pair \((p,D)\) appends a new declaration of type \(D\). There are infinitely many such occurrences. This proves the first two clauses, including the case where no declaration is ever possible and \(\Omega\) is empty.

For the embedding clause, write a finite valid context as \[\Gamma=(x_1:D_1,\ldots,x_m:D_m).\] Induct on its prefixes. Suppose an injective renaming \(\rho_i\) embeds the first \(i\) declarations, in their original order, into a finite initial segment \(P_i\) of \(\Omega\). Validity supplies \[x_1:D_1,\ldots,x_i:D_i\vdash D_{i+1}:s\] for some sort \(s\). Renaming and then thinning yield \(P_i\vdash D_{i+1}\rho_i:s\). By the second clause, a later declaration has the form \(y:D_{i+1}\rho_i\), with \(y\) fresh for the already chosen names. Set \(\rho_{i+1}(x_{i+1})=y\) and take an initial segment through this declaration. This retains all previously embedded declarations unchanged and in order. The induction begins with the empty context and proves the desired embedding.

Renaming a derivation gives \(\Gamma\rho\vdash M\rho:A\rho\). The chosen initial segment is a valid extension by insertion of \(\Gamma\rho\), so thinning gives the asserted judgment over that initial segment. All substitutions and renamings here are capture-avoiding; the reserved names permit bound variables to be renamed away from the declarations whenever needed.

For the fourth clause, only finitely many of the infinitely many declarations of type \(D\) after \(P\) can have their declared names in \(F\). Choose any other one and let \(Q\) be the initial segment ending there. Thinning the judgment for \(D\) to the prefix immediately before that declaration, followed by the variable rule, gives \(Q\vdash y:D\). In particular, when finitely many substitution images have their free variables in \(P\), this \(y\) is fresh for all those images.

Finally, take the longest among finitely many initial segments witnessing judgments over \(\Omega\) and thin all the judgments to it. An injective renaming of the finitely many variables of a context can be extended to a bijective renaming of the whole variable set. Such a renaming commutes with full \(\beta\)-reduction and its inverse does too. It therefore preserves and reflects normal forms, finite normalizing reductions, and infinite reductions. This proves the last assertions. ◻

Proof. A normal application is variable-headed: a lambda head would be a redex, and a sort or product cannot have a product type by generation and product compatibility. A lambda cannot have a literal sort type for the same reason. Generation for a sort gives exactly its axiom targets. Generation and product formation give the two inclusions in the formula for a product, separately for every applicable rule.

For a neutral expression, its type is unique up to conversion. Indeed, the assertion for its head variable follows from its declaration. Inductively, generation and compatibility of convertible products identify the domain and instantiated codomain at each further application. Thus two literal sort types of a neutral are identical. Its literal sort type \(s\) is itself sorted. For a lone variable its declaration type is sorted and convertible to \(s\); confluence makes that declaration type reduce to \(s\), and subject reduction sorts \(s\). For a nonempty application spine, correctness of the expected type already gives a sorting of \(s\). Generation for \(s\) now implies \(\operatorname{Ax}(s)\ne\varnothing\).

Thinning preserves the profile by induction on normal syntax. At a neutral, an existing sort is retained and uniqueness excludes any new one. At a product apply the induction also in its extended binder context. Literal sorts do not depend on the context. Context conversion preserves all relevant judgments in both directions, hence preserves profiles as well.

Finally, if \(s\in\pi_\Gamma(T)\), substitution gives \(\Delta\vdash T^\#\xi:s\). Reduction of \(T\) to \(T^\#\) commutes with substitution, so \(T^\#\xi\) and \(T\xi\) have the same normal form. Subject reduction therefore gives \(\Delta\vdash(T\xi)^\#:s\). This proves the inclusion. For a substituted product the outer product persists, and its components normalize separately; context conversion transports the open codomain to the normalized domain. The same inclusion consequently holds at corresponding product children. ◻

Proof. Necessity follows by induction on a sorted normal expression, using Lemma 14. Conversely, \(s\) witnesses \(\operatorname{Ax}(s)\), and a variable declared at type \(s\) witnesses \(\{s\}\). Given normal witnesses for \(I\) and \(J\), rename their finite contexts apart and combine those contexts by thinning. Form a product with the first witness as domain and the second as a codomain independent of its fresh binder. Its profile is exactly \(\operatorname{Out}(I,J)\). These witnesses are normal. ◻

Proof. The empty stack gives the inclusion; at a literal sort it is the only stack. A variable followed by finitely many strongly normalizing arguments is strongly normalizing: its head never contracts, and a reduction decreases the sum of the arguments’ reduction heights. This proves the assertion for variables. For propagation, append any tested stack at \(T_n\) to \(n\) and apply the definition of \(G_T\). Application and conversion give the required exact typing at \(T_n\). ◻

Proof. Every strongly normalizing expression has a finite maximal reduction length. Indeed, reduction is finitely branching; if lengths were unbounded, at least one immediate reduct would again have unbounded lengths, and iterating this choice would give an infinite reduction. Write \(\ell(Q)\) for this maximal length and induct on \[\ell(D)+\ell(P)+\ell(n)+\sum_{i=1}^k\ell(m_i).\] The head reduct is strongly normalizing by hypothesis. Every other immediate reduct changes one displayed component and strictly lowers this sum. Its head contractum is either unchanged or is a reduct of the old head contractum. For a step in \(n\), contract the corresponding step in each of its finitely many copies in \(P[x:=n]\); there may be zero copies. For a step in the annotation, the contractum is unchanged. Thus the new contractum is strongly normalizing, and the induction applies. Every immediate reduct is strongly normalizing, which proves the claim. ◻

Proof. Lemma 17 shows that \(\top_T\) is a candidate. Intersections of candidates preserve all three requirements of Definition 4; take the empty intersection to be \(\top_T\). Therefore every family has a meet, and its join is the intersection of its common upper bounds. This family of upper bounds is nonempty because it contains \(\top_T\). In particular, the least candidate is the intersection of all candidates.

For (4), a term in \(G_T\) passes every test by Lemma 16 and the containment \(G_{T_n}\subseteq C_{n,a}\). Suppose a head contractum belongs to (4) and its expansion has strongly normalizing components. Lemma 17 gives the expansion’s membership in \(\top_T\). Append a prescribed \(n\in A\) to its spine. The enlarged head contractum lies in \(C_{n,a}\) for every \(a\), and all enlarged components are strongly normalizing. Head expansion in \(C_{n,a}\) gives the required membership of the enlarged spine. This proves every test, without using reduction closure of a candidate. ◻

Proof. Induct lexicographically on \((\ell(M),|M|)\), where \(|M|\) is syntax size including annotations. The induction is simultaneous over all typings, contexts, and admissible environments. A proper subexpression has no larger reduction height and smaller size; a beta reduct has strictly smaller height. Typed substitution gives all required actual typings throughout.

We shall repeatedly use a fresh-variable extension. If a binder has raw generic annotation \(B\), then \(B\xi\) is sorted over a finite prefix of \(\Omega\). Saturation supplies a fresh variable \(z\) declared at that raw type, beyond a common prefix for the finite expressions in question. Choose \(z\) outside the free names of all other images. It belongs to \(G_{(B\xi)^\#}\) by Lemma 16, and hence satisfies whichever of the three admissibility conditions applies. Any allowed parameter extension can be used. Invariance retains the assumptions on old variables. If the induction proves the body with \(x\) sent to \(z\) strongly normalizing, renaming \(z\) back to a bound \(x\) proves strong normalization of the open substituted body.

For a sort, \(M\xi=M\) is normal, and its expected normal type is a literal sort. At a literal sort \(G\) equals top, so this suffices for membership in any candidate. For a product, apply the induction to its domain and to its open codomain under a fresh-variable extension. The two substituted components are strongly normalizing, so the product is strongly normalizing. Its expected normal type is again a literal sort, giving the conclusion.

Let \(M=\lambda x:B.P\). The induction on \(B\), and on \(P\) under a fresh-variable extension, proves strong normalization of the actual annotation and open body. Hence \(M\xi\) is strongly normalizing. This already proves the conclusion unless both the generic and the actual normalized expected types have profiles in \(S\). In the latter case write \(A^\#=\Pi x:D.E\). Generation and product compatibility identify \(D\) with the normal form of \(B\) and identify \(E\) with the normal body type, after context conversion under the binder.

Context-convert the generic body judgment to \(\Gamma,x:D\vdash P:E\). Take an arbitrary \(n\in R_D\) and arbitrary prescribed parameter extension in \(Q_{A^\#,n}\). Convert \(n\) to the actualized type \(D\xi\) and extend this context’s substitution by \(x\mapsto n\). This is admissible: the generic domain profile is in \(U\cup S\), and the test condition is exactly the required candidate or SN condition. Apply the induction to the context-converted judgment for \(P\) in this very extension. It gives the required codomain candidate for the head contractum of \((M\xi)n\). The actual annotation, open body and \(n\) are strongly normalizing. Head expansion in that codomain candidate proves the test. If the actual codomain profile is in \(U\), use any compatible parameter extension, the body’s strong normalization, and Lemma 17. We have verified every product test; the introduction direction of the product-equality requirement proves the conclusion.

For an application, inspect its entire left-associated spine. If its head is a lambda, write \[M=(\lambda x:B.P)N\,\vec L.\] Contract its first redex generically to \(M'\). Subject reduction gives \(\Gamma\vdash M':A\) and \(\ell(M')<\ell(M)\), so the induction gives \(M'\xi\in R_{A^\#}\). The components \(B,P,N,\vec L\) are proper subexpressions. Their inductions, using a fresh-variable extension for the open \(P\), give strong normalization of every component after substitution. Substitution commutes with the displayed contraction up to alpha conversion. Head expansion in \(R_{A^\#}\) therefore proves the result. This step does not invoke reduction closure of a candidate.

The remaining case is a neutral spine \(xN_1\cdots N_k\), including \(k=0\). Starting at the normal form of the declaration type of \(x\), generation and neutral uniqueness determine its successive normal expected types. Whenever a next argument occurs, the preceding type is a product; convert that argument to its normalized domain and take the normalized instantiated codomain as the next type. The induction applied to each \(N_i\) at this exact domain gives its candidate membership and, in particular, strong normalization after substitution. Typed substitution and confluence identify the actual successive types with the normal forms of the corresponding generic types.

Track membership along the spine. A \(G\) prefix propagates by Lemma 16. If the head declaration has profile in \(U\), admissibility and profile growth put it in actual top in \(U\), hence in \(G\) by (3). If a prefix has generic profile in \(S\), an actual profile in \(U\) likewise gives \(G\). Otherwise its candidate product test applies to the next argument, and (5) gives the next candidate. That next generic profile lies in \(U\cup S\) by the positive codomain path; on reaching \(U\) its membership is again in \(G\). A head declaration outside \(U\cup S\) starts in \(G\) by admissibility and requires no further restriction on profiles. Thus the final prefix belongs either to the desired candidate or to its subset \(G\). No other spine head can type as an application. This completes the induction. ◻

Proof. Fix \(h\in\top_T\) with \(\pi(T)\in S\) and any tested stack \((n_1,\ldots,n_k)\) at \(T\). Choose a common finite prefix \(\Gamma\) of \(\Omega\) supporting the relevant exact typings and use the identity substitution. Choose parameters successively; all variable images lie in \(G\) and therefore the environment is admissible. Apply Lemma 19 separately to \(h\) and to each \(n_i\) at its exact successive domain. Each is strongly normalizing by hypothesis or by the definition of a tested stack.

Start with the resulting candidate membership of \(h\) and iterate the product tests and specialization along the stack. Each encountered type has profile in \(U\cup S\). In \(S\) specialization supplies the next candidate membership; in \(U\) the invariant supplies \(G\), which propagates across every remaining frame. Thus \(h n_1\cdots n_k\) is strongly normalizing. The argument never assumes strong normalization of an intermediate generic application and never applies the fundamental lemma to such an application. Since the stack was arbitrary, \(h\in G_T\). The reverse inclusion is Lemma 16. ◻

Proof. Process the finitely many components and apply Proposition 20. At the end, \(G_T=\top_T\) for every actual type with nonempty profile. Empty-profile actual types are literal sorts, for which this equality already holds by Lemma 16.

Suppose a typable expression is not strongly normalizing and choose one of least syntax size, among all valid contexts and typings. Its proper syntactic children are typable in the corresponding contexts, including under binders, and so are strongly normalizing. A variable or sort is normal; a product or lambda with strongly normalizing children is strongly normalizing. The expression must therefore be an application \(f n\), with \(f,n\) strongly normalizing. Generation types \(f\) at a product and \(n\) at its domain. Normalize that product, convert these typings, and embed the finite context into \(\Omega\). The resulting normal product is an actual type with nonempty profile: it is sorted by correctness of types and cannot be a literal sort. The equality \(G_T=\top_T\) and its one-frame test now give strong normalization of \(f n\), a contradiction. This also handles an empty feasible-profile graph, since the hypothetical application would itself produce a feasible product profile.

Finally, every legal expression is typable by validity and correctness of types, or is a literal sort. Literal sorts are normal. Hence the conclusion holds with the full legal-expression and open-context scope. ◻

Proof. Choose a vertex of \(S\). Assign to each vertex the parity of any path from the chosen vertex to it. This is well defined: append a return path to two proposed paths; different parities would produce an odd closed walk. Give even vertices sign \(+\) and odd vertices sign \(-\). Every internal positive edge preserves sign, and every internal negative edge reverses sign.

Let \(\mathcal T_S\) be the set of actual types with profile in \(S\). It is a set, since these are finite syntax over the countable context \(\Omega\). On \[\mathcal L= \prod_{T\in\mathcal T_S}\mathcal C(T)\] use inclusion in coordinates with sign \(+\) and reverse inclusion in coordinates with sign \(-\). This is a complete lattice by Lemma 18. Extend a vector \(v\) to actual types in \(U\) by \(v_T=\top_T\).

Define an operator \(F:\mathcal L\to\mathcal L\). At a nonproduct type set \(F(v)_T=\top_T\). At \(T=\Pi x:D.E\), let \[F(v)_T=\{h\in\top_T:\text{for every }n\in v_D, \ h n\in v_{(E[x:=n])^\#}\}.\] All indices belong to \(U\cup S\) by the dependency graph, and this is a candidate by Lemma 18.

The operator is monotone in the mixed order. In the usual inclusion order its product clause is antitone in the domain coordinate and monotone in every instantiated-codomain coordinate. An internal domain has the opposite sign to \(T\) by its negative edge. An instantiated codomain in \(S\) has the same sign as \(T\) by its positive path through the open codomain: the intermediate vertex must also lie in \(S\), since a vertex in \(U\) has all its predecessors in \(U\). Coordinates in \(U\) are constant. These observations give exactly the required coordinatewise monotonicity, in either sign of the output.

Tarski’s fixed-point theorem (Tarski 1955, Theorem 1) gives a fixed point. We recall its short existence proof, which needs no continuity assumption. Let \(a\) be the supremum of all \(v\) satisfying \(v\le F(v)\). For every such \(v\), monotonicity gives \(v\le F(v)\le F(a)\), so \(a\le F(a)\). Then \(F(a)\le F(F(a))\), making \(F(a)\) one of the elements whose supremum is \(a\); hence \(F(a)\le a\). Fix such a vector \(a\).

No auxiliary parameters are needed. For a generic normal type \(T\) with profile in \(S\), define \(R_T=a_{(T\xi)^\#}\) if its actual profile is in \(S\), and top otherwise. At a generic product with actual profile in \(S\), its actual normalized domain and all actual instantiated codomains are exactly the indices in the operator clause. Thus the fixed-point equality gives the required product equality, with the unique parameter extension.

The actual normalized type determines the candidate, so thinning, context conversion and pointwise convertible images preserve it. For specialization the two actual type expressions \[E(\xi[x\mapsto N\xi]) \quad\hbox{and}\quad ((E[x:=N])^\#)\xi\] are convertible by substitution composition and normalization. Their normal forms are identical. The two candidates are consequently equal when that profile is in \(S\), and both are top in \(U\). A generic child in \(U\) remains there under substitution, so no additional case arises. This proves all interface requirements. ◻

Proof. Induct on the normal type. Sorts and actual-\(U\) cases do not use bits. A neutral uses only its head bit. At a product, any child in \(U\) is interpreted as top; only the unique \(S\) child can depend on old bits. Its support is propagated to the parent unless it is the product’s own binder, whose bit is fixed by the displayed rule. This proves the dependence assertion. Profile invariance preserves the same product path and its domain parity under thinning and context conversion. In those operations and under convertible images, the actual normal types agree. The recursive product tests then have identical domains, codomains and prescribed bits, proving the stated invariances. ◻

Proof. Induct on the pre-substitution syntax of \(T\). The actual normal types agree by substitution composition and confluence. If their profile lies in \(U\), both candidates are top. Otherwise that profile lies in \(S\), and so does the generic profile of \(T'\): profile growth puts it in \(U\cup S\), and a generic profile in \(U\) could only have actual profile in \(U\).

A sort is unchanged. A neutral whose head is not \(y\) remains a neutral with the same head after substitution and normalization; if its actual profile is in \(S\), the supported head is common and its bit agrees. At a neutral headed by \(y\), its polarity is positive and the prescribed bit chooses the least candidate for forward inclusion, or the greatest candidate for reverse inclusion. This compares it with every possible candidate of \(T'\). In particular we do not recurse into the possibly larger normal expression obtained by substituting for \(y\).

Let \(T=\Pi x:D.E\), choosing \(x\) fresh for \(N\) and for the substitution data. The post-substitution type is again a product, with its two substituted components normalized. Context-convert the open codomain to the normalized post domain. To compare the product test candidates in direction \(\delta\), compare their domain candidates in direction \(-\delta\). On each common test compare their codomain candidates in direction \(\delta\), extending the actual images by that same raw test and using the respective prescribed bits for \(x\). For example, for forward inclusion every post domain test must be a pre domain test, and its pre codomain candidate must be contained in its post codomain candidate.

If a pre child is in \(U\), its generic substitute remains in \(U\) and both actual child candidates are top. If its generic substitute grows into \(U\), the common actual child profile is again in \(U\), with the same conclusion. In all other required child comparisons, both generic child profiles are in \(S\). Such a post child must be the same unique \(S\) child as before substitution: a pre off-path child in \(U\) cannot grow into \(S\). Every common supported variable other than the new binder \(x\) therefore inherits the agreement condition from the parent. If \(y\) supports the child, the prescribed extremum condition is also inherited: a domain step reverses both the comparison direction and the support polarity, and a codomain step reverses neither.

It remains to check the bits of \(x\) when it is supported in both open codomains. The pre support path ends at a neutral with head \(x\), which substitution for \(y\) cannot change. Every product on that path persists. The post support path must follow the same positions: a pre off-path child remains in \(U\), while truncation of the path into \(U\) would prevent the post codomain from being supported by \(x\). Thus both paths have the same number of domain steps, their polarities agree, and the prescribed bits of \(x\) agree. If substitution exposes \(x\) through a neutral headed by \(y\), that portion of the induction instead stops at the extremum case already proved; it imposes no further shared-support condition.

All hypotheses of the child inductions now hold. Their inclusions give the desired product inclusion by the universal test definition, in either direction. This completes the induction. ◻

Proof. Candidate existence and product equality follow from the recursion. Lemma 23 gives the required invariances. To verify specialization, let \(T=\Pi x:D.E\), take \(\Gamma\vdash N:D\) with \(N\xi\in R_D\), and let \(h\in R_T\). Its product test gives \[h(N\xi)\in R_E(\xi[x\mapsto N\xi],\theta_x)\] when the actual codomain profile lies in \(S\); here \(\theta_x\) is the prescribed binder extension. Apply Lemma 24 to substitution for \(x\) in \(E\), with comparison direction \(+\). All old bits agree. The prescribed bit of \(x\) is exactly \(0\) for positive support and \(1\) for negative support, as that lemma requires. It follows that the last candidate is contained in \(R_{(E[x:=N])^\#}(\xi,\theta)\), proving specialization. At an actual codomain profile in \(U\), the strong-normalization test gives specialization directly. Arbitrary bits are allowed on the starting context, and every prescribed or arbitrary binder extension exists. All interface requirements are satisfied. ◻

Proof. Prepending the edge in question to paths to a direct vertex proves the sign statements. Profile growth and the product edge give the positive path \[L\longrightarrow J\longrightarrow K,\] where the first edge is omitted when \(L=J\). Since \(L\in H\) and \(H\) is positive-path closed, \(J\in H\). Its path to the active vertex \(K\) makes \(J\) active. If \(I\in H\), the negative edge of \((I,J,K)\) is retained, so \(I\) is active too. When \(K,L\in S\), the displayed path cannot leave their primary strongly connected component. Thus \(J\in S\), and the definition of direct applies. ◻

Proof. Process the finitely many plain secondary components in source order. Suppose first that a component \(C\) has no internal negative edge. Every active domain used by a legal frame at a type of layer in \(C\) then lies in an earlier component: otherwise the frame’s triple, whose open codomain is active, would contribute an internal negative edge. Thus all frame alphabets can be specified without using a space whose layer belongs to \(C\).

For \(\pi(T)\in C\), consider finite paths of legal frames beginning at \(T\). A continuing path has all its target layers in \(C\), and includes the empty path. An exiting path has all but its final target layer in \(C\) and its final target in an earlier component. Define \(\mathcal K_T\) to be the set of tables assigning a member of \(\mathcal B\) to each continuing path and a member of the final target space to each exiting path. Split a table according to the empty path and the first frame. For a frame staying in \(C\), its suffix table is exactly a table of the same kind starting at its target. For an exiting frame its output is already a value of the target space. This gives the bijection (8) in both directions. The constant top outputs and previously chosen exit defaults define the distinguished table.

Now let \(C\) have an internal negative edge. For every normalized type \(T\) of layer in \(C\), define a positive integer \(p_C(T)\) as follows. Count its root. At a product with child layers \(I,J\), continue into the codomain when \(J\in C\), and into the domain when \(I\in C\) and \(J\) is active. Apply the same rule recursively at counted children, using the binder context in the codomain. This counts a subset of a finite syntax tree. Profile invariance makes the count independent of the prefix and unchanged by valid thinning or context conversion.

For a legal frame at \(T=\Pi x:D.E\), write \(I=\pi(D)\), \(J=\pi(E)\), \(K=\pi(T)\), and \(L=\pi(T_q)\). A same-\(C\) domain has smaller count. We claim that its same-\(C\) target also satisfies \[ p_C(T_q)\le p_C(E)<p_C(T). \tag{9}\] Here \(J\in C\) follows from the positive ascent in Lemma 26; hence \(p_C(E)\) is defined.

To prove the first inequality, thin \(T\) and \(q\) to a common prefix, choosing the displayed binder fresh. Associate to every counted node of \((E[q/x])^\#\) its position string. We show that the same position is a counted node of \(E\). The induction along a position maintains that the corresponding pre- and post-substitution parent profiles both lie in \(C\); at the root these are \(J\) and \(L\). At a pre-substitution product the post normal form is a product with componentwise substituted normal forms. Write \(I_0,J_0,K_0\) for its pre domain, codomain, and parent profiles, and \(I_1,J_1,K_1\) for the post profiles. Profile growth gives \(I_1\supseteq I_0\) and \(J_1\supseteq J_0\), also under binders after context conversion.

If the post codomain is counted, then \(J_1\in C\), and the positive path \(J_1\longrightarrow J_0\longrightarrow K_0\) has both endpoints in \(C\). Hence \(J_0\in C\), so the pre codomain is counted too. If the post domain is counted, then \(I_1\in C\) and \(J_1\) is active. The inclusion paths put \(I_0,J_0\) in \(H\). Since \(K_0\in C\subseteq H\), the pre triple has a retained negative edge \(I_0\longrightarrow K_0\). The path \[I_1\longrightarrow I_0\longrightarrow K_0\] again has endpoints in \(C\), so \(I_0\in C\). Also the positive edge \(J_0\longrightarrow K_0\) makes \(J_0\) active. Thus the pre domain is counted. In either case the pre- and post-substitution profiles of the selected child lie in \(C\), which preserves the induction invariant for the next position. Inclusion edges in these paths are omitted when the profiles are equal.

The association could fail only if a pre neutral leaf became a product. Sorts are unchanged, and a neutral with any other head remains neutral after substitution and normalization. Its head must therefore be the substituted variable \(x\). Let its singleton profile be \(\{s\}\); this lies in \(C\). The sort \(s\) is sorted, so \(\operatorname{Ax}(s)\ne\varnothing\). Trace the original \(x\)-headed spine backward through its normalized successive typing products. At each application the result layer has a primary positive path to the function layer. Starting with the layer \(\operatorname{Ax}(s)\) of its type \(s\), concatenate these paths to obtain a positive path to \(\pi(D)=I\). The outer product has \(J,K\in C\). This is forbidden by (7). No leaf therefore expands. Position strings give the required injection of counted nodes and prove (9).

Define (8) by induction on \(p_C(T)\), simultaneously for all types with the same count. Every same-component space on its right is already constructed by the strict inequalities just proved; all other spaces come from earlier components. The product of the specified nonempty sets is nonempty, with the explicit element whose base is \(\mathbf t\) and whose next values are the already specified defaults. This completes the construction. ◻

Proof. Structural invariance follows by the same recursion as for evaluation, matching all typed raw binder extensions by conversion. For the base projection assertion, the sort case gives top on both sides, the product case is exactly the override, and all other cases use (28). In the product case its literal core sort equals \(s\) because it is convertible to \(s\). The goodness clauses agree for the same reason.

Prove the normal-syntax claims simultaneously in the Val/Read syntax order and universally over typed raw substitutions. Normal applications are variable-headed, so skipped ones are good. Lambda bodies are normal and the induction hypothesis applies to every typed extension. At an overridden normal product, its generic profile contains the core sort \(s\), with \(\{s\}\in S\). The positive inclusion edge places that generic profile, and hence both child profiles, in \(U\cup S\). The child Read induction hypotheses prove all required goodness conditions. The same predecessor argument applies at product Read. For a nonsort, nonproduct normal Read whose actual profile is in \(S\), the generic profile cannot be in \(U\), since growth from \(U\) stays in \(U\). It is therefore in \(S\). The normal expression is neutral and has singleton generic profile \(\{s\}\), giving exactly the required Read condition; its Val, when needed, is good by induction. ◻

Proof. Composition of capture-avoiding substitutions makes corresponding actual images convertible and corresponding actual types equal. Induct on the original tree in the Val/Read order. An active lookup of \(x\) is exactly the chosen value of \(u\); thinning and retargeting preserve it by structural invariance. Other lookups agree.

At a binder, rename its variable fresh for \(N\). The same raw binder image and payload extend both environments, the hypotheses on \(I\) remain unchanged, and the induction hypothesis applies. This gives equality at every legal frame or every raw observation and proves all universally quantified goodness requirements. At a product the root persists. Domain Reads agree by induction; for every raw tester and payload the codomain Reads agree by the binder argument. Thus the entire product candidates agree and remain good. At an unskipped application, the evaluated children agree by induction and its normal argument keys agree by conversion, so it extracts the same output.

It remains to justify the skipped clauses, where an arbitrary change of head would invalidate the argument. Suppose a skipped, variable-headed application had head \(x\). Trace its successive actual typing products backward along the spine. There is a primary positive path from its active result layer to \(I\), passing through its supposedly inactive function layer. The path stays in \(H\) by positive closure. By hypothesis \(I\) is active; consequently every vertex on the path reaches a direct vertex and is active. This is a contradiction. The head is therefore a different variable and persists under substitution, so the skipped application stays good and keeps its default.

For a skipped nonproduct Read, goodness supplies \(\{s\}\in S\) and a variable head. If that head were \(x\), the same spine argument would start at \(\operatorname{Ax}(s)\). This is nonempty because a neutral typed at \(s\) has sorted \(s\), and it is a seed in \(H\). It would reach the active vertex \(I\), forcing \(\operatorname{Ax}(s)\) active, contrary to this being a skipped Read. Thus that head also persists. In the active case use the all-shape base projection of Lemma 30 and the Val induction already proved, even if substitution changes the root shape. Read outside actual profile \(S\) stays the same default. This exhausts the clauses. ◻

Proof. Construct the transported tree independently of its environment. At contextual steps transport the changed child. A change in a product domain context-converts its open codomain tree. A change in a lambda annotation also transports the supporting product typing by subject reduction and context-converts the open body. A change in an application argument changes its core result type to a convertible one; subject reduction retains the root expectation.

Induct on the reduction position, simultaneously for Val and Read. At evaluated children use the induction hypothesis. At binders apply it under every typed raw extension required by goodness; structural invariance handles the context-converted unchanged children. Actual types, gates, and argument keys are unchanged. At a skipped variable-headed spine, a reduction can only be inside its arguments; the head and skipped condition persist. Ignored children need no semantic property, only the transported typing. For a remaining Read with active base projection, apply the Val statement already proved at the same root. A Read outside actual profile \(S\) remains default.

At a root contraction \((\lambda x:D.P)N\longrightarrow P[N/x]\), generation and product compatibility align the lambda annotation and body type with the application’s stored product. Retarget the argument to the annotation type, substitute its tree in the body, and retarget the result to the old expectation.

Consider a good active Val. The application cannot have been skipped, since its syntactic head is a lambda. Let \(K,L\) be the actual function and result layers, respectively. They are active. By Lemma 26, the actual domain layer \(I\) is active whenever it belongs to \(H\). The argument is good if \(I\) is active. Evaluation uses the valid normal key \((N\xi)^\#\) and, when required, the payload Val\((N)\). The lambda equation gives its body value with this key, including at an exit where the lambda supplied the correct tag. The raw image \(N\xi\) is convertible to its normal form. Structural invariance therefore identifies this body value with the one at the raw image, with the same payload. Lambda goodness supplies body goodness for both typed extensions. Lemma 31 now identifies that value with the beta contractum and proves its goodness. No strong normalization of \(N\xi\) was used.

For a Read with actual profile in \(S\), a skipped clause at the root is impossible because the head is a lambda. Its goodness therefore provides the active all-shape base projection, and the preceding Val argument applies. This proves the root case and the lemma. ◻

Proof. Induct in the Val/Read syntax order, comparing the same environments. Variables use the same declaration parameter and sorts use defaults. For product Val, convertible expected types force its two literal core sorts to agree. The override condition is therefore identical. For product Read, the product candidate compares the child Reads independently of their sort choices, by induction. Its raw extensions and actual indices agree, so the candidates are equal.

For a lambda, product compatibility aligns the body expectations up to conversion. The annotation is fixed syntax. The body Val induction therefore compares every frame and observation. In a normal application the function is variable-headed, so its generic type is unique up to conversion. Product compatibility aligns the domains and codomains in the two application trees. The function and argument Val induction hypotheses give the same keys, payloads, and selected outputs. Finally, a normal nonsort, nonproduct expression is neutral and has a unique literal sort. Thus any nondefault Read uses the same Val base. These are all normal syntactic shapes. Only neutral type uniqueness has been used; functionality of the specification is not assumed. ◻

Proof. Candidate membership and the product clause are the Read construction and the candidate test lemma. The interpretation’s invariances follow from structural invariance and normal-tree independence. Every active space has its distinguished member, so arbitrary context extensions can always be supplied with parameters.

For specialization, if the actual product profile is in \(U\), its candidate is the top and hence equals \(G\). The domain tester is strongly normalizing. Propagation of \(G\) along this typed argument gives the required typed strong normalization at the instantiated profile, which also lies in \(U\). We may therefore suppose the actual product profile \(K\) is in \(S\). First suppose that the actual instantiated codomain profile \(L\) is in \(S\), and let \(I\) be the actual domain profile. Lemma 26 places the open codomain profile in \(S\). Thus if \(I\in H\), the definition makes \(I\) direct and hence active; in particular, every active \(I\) is direct. Normalize the generic argument \(N\) to \(N^\#\), retaining its type \(D\) by subject reduction. If \(I\) is active, choose as binder payload \[v=\operatorname{Val}(N^\#:D;\xi,\theta).\] This exists and is good by normal-syntax goodness. The product test quantifies over every payload and therefore includes this choice.

Its open codomain \(E\) is normal, with generic profile in \(U\cup S\), so its Read is good. Apply Lemma 31 to substitute \(N^\#\) there, using the raw image \(N\xi\). This image is convertible to \(N^\#\xi\), as required. The lemma identifies the tested open codomain Read with the good Read of the generic expression \(E[N^\#/x]\). This expression is typed by substitution and hence weakly normalizing by the system hypothesis. Transport its tree along a normalizing sequence using Lemma 32. Its normal form is precisely \((E[N/x])^\#\), because \(N\) and \(N^\#\) are convertible. Normal-tree independence identifies the final Read with (30) at that type.

For completeness, its generic profile belongs to \(U\cup S\): it has a positive ascent to the original product profile. It cannot belong to \(U\) when its actual profile is \(L\in S\), because profile growth from \(U\) stays in \(U\). Thus (30) is indeed the appropriate generic \(S\) entry. If the actual instantiated profile is in \(U\), the test demands typed strong normalization and the processed component identity identifies this with the required top candidate. These are the only actual profiles reached from the current component. ◻

Proof. Substitution preserves modes by induction on syntax. A data expression has no free proof variable, so substitution for a proof variable cannot introduce proof syntax into a data expression. Substitution for a data variable uses a data term. At binders, choose fresh names in the same mode class.

Context validity follows by rule induction, retaining the sort typing of each declaration from its introduction premise. The proofs of weakening and typed substitution are inductions on typing derivations. Each binder retains its label, and each substituted term has the mode required by that binder or declaration. Context conversion follows by the identity substitution, typing the changed variable at its old type by conversion. Generation follows by removing final conversions and weakenings. None of these arguments compares distinct possible sort assignments.

Correctness of types is another rule induction: an expected type is a literal sort or is itself sorted. At application, the function’s product type is sorted by induction; generation on that product and typed substitution sort the application’s result type. This remains true through conversion and weakening.

For confluence, use parallel reduction with homomorphic clauses at every constructor, including annotation children, and a contracting clause only when the application and lambda labels match. Parallel substitution is proved by syntax induction. Every parallel reduct of a term parallel-reduces to its complete development: contract the matching redexes already present in the original term and develop all children. At an unmatched lambda–application pair only the homomorphic clause applies. This proves the triangle property, hence confluence. The reflexive transitive closures of parallel and ordinary reduction agree, since parallel contractions can be performed from the children upwards. Reduction never changes a product’s outer constructor or labels. Common reducts therefore give labelled product compatibility, and a product cannot be convertible to a sort.

Subject reduction now follows by induction on a typing derivation. At a root beta step, generation and product compatibility identify the lambda’s annotation with the application’s domain up to conversion. Convert the argument to the annotation type, substitute in the body, and convert the result to the original expected type. A reduction of an application argument changes its substituted result type by conversion. A reduction of a product domain is handled by context conversion in the codomain premise. For a lambda annotation step, reduce the corresponding domain in its supporting product judgment, context-convert its body premise, re-form the lambda, and convert back to the original sorted product type. The other positions, including positions inside annotations, follow by induction. These constructions keep every label. Erasure of typing follows directly by induction on the labelled derivation.

It remains to check that an erased redex can be contracted with the labels present. Every syntactic subterm of a typable term has a typing in the appropriate binder context; for an annotation this follows from context validity. Consider the subterm at the erased redex. Its shape is \[(\lambda^{i,j}x:D.P)\mathbin{@^{i',j}}Q.\] The result modes already force the displayed common \(j\). Lambda generation gives a product type with labels \((i,j)\); application generation gives a convertible product type with labels \((i',j)\). Product compatibility forces \(i=i'\). Thus this is a matching labelled redex. Contract it at the same position. Capture-free substitution commutes with erasure, so its erasure is \(N\); subject reduction gives the asserted judgment and substitution preserves its mode. This applies to any position, including one in a lambda or product annotation. Induction on a finite erased reduction proves the remaining assertions. ◻

Proof. Associate each terminal with a negative edge producing it. Lift the input terminal along the positive edge of its associated triple, reaching \(S\). Choose a path in \(S\) to the domain vertex of an edge producing the target terminal, and append that negative edge. Carry a proof along this route. At a positive edge use the lift above. At a negative edge \((I,J,K)\), if the currently carried type is \(T\), introduce a fresh proof variable \(c:\Pi^{\mathsf p,\mathsf p}u:T.F_J\) and replace the carried proof \(t\) by \(c\,t:F_J\). Unless this is the last edge, lift \(c\,t\) along the positive edge \(J\longrightarrow K\) of this same triple before continuing. The product type of \(c\) is sorted at \(K\), so the declaration is valid.

Initially the carried type is a terminal. Positive edges add constant \((\mathsf d,\mathsf p)\) prefixes, and negative edges reset the carried type to a terminal before the prescribed lift. Thus every converter domain has precisely the asserted form. Its normality and the sorting of each suffix follow from its construction. The types depend on chosen types and paths, not on the input proof. Choose the finitely many pairwise routes first and predeclare all their converters in \(\Delta_{\mathsf p}\); weakening makes every resulting transformation available in the same context. Types use data only, so the converter declarations do not depend on one another. ◻

Proof. List the finitely many atoms and nest cases on their terms \(\operatorname{em}\). Each resulting branch supplies either the atom or its negation. Recursively build a proof of every true parsed formula and a proof of the negation of every false parsed formula. For \(\bot\) the required negation is the identity term. For conjunction, a true case uses pairing, and a false case contradicts the false conjunct’s projection. For disjunction, a true case uses its true injection, and a false case uses case analysis to contradict either disjunct. For implication, a true case either returns a proof of the consequent or derives it by \(\operatorname{abs}\) from the false antecedent; a false case contradicts the application of an assumed implication to the already proved antecedent. Negation is implication to \(\bot\), and biconditional is its displayed conjunction. If some premise is false, apply its constructed negation to the given proof and use \(\operatorname{abs}_R\). Otherwise the assumed truth-table entailment makes \(R\) true, so use its constructed proof. The recursively typed case terms discharge all branch assumptions. ◻

Proof. Induct on the path. The empty-path equivalence is propositional reflexivity. A positive extension beta-reduces its projection of a lift, so conversion reduces its assertion to the preceding one. For a negative extension, the displayed lambda beta-reduces the left side to \(\operatorname{read}_J(\operatorname{send}_J(\Psi))\), where \(\Psi\) is the left side of the previous cancellation assertion. Apply (32), the induction hypothesis, and \(\mathsf{pl}\) for transitivity of equivalence. The expansions commute with capture-free substitution because all paths, tails and names are fixed hygienically. Consequently the final callback is exactly \(\Phi[x:=t]\) up to labelled conversion, with no extensional substitution inside data. ◻

Proof. If \(C\) has an odd closed walk, between any two of its vertices there are paths of both parities: choose paths to and from the base of that walk, and insert the walk once to change parity. Choose any internal retained negative \((p,n,g)\) and then choose the three required parities for \(\alpha\), \(\beta\), and \(\kappa\).

Suppose instead that every closed walk in \(C\) is even. Color its vertices by the parity of a path from a fixed vertex. The color is well defined: appending a fixed return path to two such paths shows that their parities are equal. A positive edge preserves color and a negative edge changes it. The positive edge \(J\longrightarrow k\) of the triple in (34) is retained, since \(J,k\in C\subseteq H\); hence \(J\) and \(k\) have the same color. There is a negative edge entering this color. Indeed, take any internal negative. If it enters the other color, follow a directed return path to its source; that path must contain a negative edge entering the color of \(k\). Choose such an edge \(p\longrightarrow g\), with its retained triple \((p,n,g)\). Thus \(g\) has the color of \(J,k\), and \(p\) has the opposite color. Connectivity now gives \(\kappa\) even and \(\alpha,\beta\) odd.

Finally, \(k\) is plain. By the definition of plainness it has an odd path to a direct vertex \(j\) and an even path to a direct vertex \(h\). They need not have the same endpoint and need not stay inside \(C\). Choose them as \(\lambda\) and \(\theta\). Concatenating \(\beta\) with \(\theta\) gives the claimed odd path \(\eta\). ◻

Proof. For (36), cancellation for \(\operatorname{Log}\) gives the comparison with \(\langle\operatorname{Raw}(y),t\rangle_{L_c}\), and cancellation for \(\operatorname{Raw}\) compares this with \(\langle y,t\rangle_L\). Apply \(\mathsf{pl}\) to these two biconditionals. For (37), expand \(@\) and cancel \(\operatorname{mk}_{\mathsf P_L}\) at the exact argument \(c=\operatorname{Raw}(w)\). Its callback becomes \(\Phi[x:=\operatorname{Log}(\operatorname{Raw}(w))]\), which is the displayed formula by definition. ◻

Proof. Cancel the second wrapper, then the first. Evaluation of \(\operatorname{emb}_1(t)\) against \(\operatorname{mk}_1(u.\Phi)\) is biconditional to \(\Phi[u:=t]\); evaluation of \(\operatorname{emb}_0(t)\) against the same value is biconditional to \(\neg\Phi[u:=t]\). Each comparison follows by \(\mathsf{pl}\) from the two cancellation proofs. With \(\Phi=\top\), the proof of \(\top\) and these comparisons give the signed bits. If \(\epsilon=1\), the definition of \(\operatorname{rec}\) then selects the positive comparison. If \(\epsilon=0\), it selects the negation of the negative comparison. The propositional double-negation equivalence is available from \(\mathsf{pl}\) by Lemma 37, since the logical constructors and classical proof builders have already been derived in the labelled fragment. Thus \(\mathsf{pl}\) gives the recovery biconditional in both cases. ◻

Proof. For a marker, cancel (39) at \(E_u(c_\top)\). The data-string test is false by the signed-bit proofs. The remaining marker-string test holds exactly when \(u=t\), again by those proofs. Apply \(\mathsf{pl}\) to obtain the asserted signed mark.

For the decoder, first cancel its \(\mathsf P_L\) constructor at the exact input \(c\), then cancel (39) at \(E_{\mathrm{data}}(c)\). Here the data-string test holds, the marker-string test fails, and (38) compares the remaining recovery formula with \(\langle P,c\rangle_{\mathsf P_L}\). Combine these proofs with \(\mathsf{pl}\). To obtain (40), use this result at \(c=\operatorname{Raw}(y)\) and expand the definition of \(@\). Thus this calculation inserts neither \(\operatorname{Round}(y)\) nor an additional rounding of its raw value. ◻

Proof. Cancellation compares \(D(\operatorname{dummy})\) with \(\top\), which has its derived proof. It compares every marker of \(bp_\bot\) with \(\bot\), giving the asserted negations by \(\mathsf{pl}\). Cancellation at \(bp_\bot\) compares \(D(\operatorname{point}(y))\) with a conjunction having \(\operatorname{Mark}_{\operatorname{pt}}(bp_\bot)\) as its first conjunct, and hence gives its negation. Finally, cancellation compares the left side of (42) with \[\operatorname{Mark}_{\operatorname{pt}} (\operatorname{Enc}_{\operatorname{pt}}(P)) \land \bigl(\operatorname{Dec}(\operatorname{Enc}_{\operatorname{pt}}(P))@y\bigr).\] The marker proof and (40) prove the required biconditional by \(\mathsf{pl}\). ◻

Proof. Throughout this proof \(w\) abbreviates the exact data expression \(\operatorname{Bundle}(m,y)\); it is not a fresh datum with an assumed property. For any \(f:F(A)\), cancellation of the bundle gives a proof of \[ \langle w,f\rangle_{\operatorname{Single}} \leftrightarrow \operatorname{if}\bigl( \langle f,\operatorname{dummy}\rangle_F; \langle f,m\rangle_F, \langle f,\operatorname{point}(y)\rangle_F\bigr). \tag{46}\]

First apply cancellation to \(f_e(w)\) at \(\operatorname{dummy}:M(A)\). It gives \[\langle f_e(w),\operatorname{dummy}\rangle_F \leftrightarrow \operatorname{if}\bigl(D(\operatorname{dummy});\top, \langle w,f_i(\operatorname{dummy})\rangle_{\operatorname{Single}}\bigr).\] Together with \(D(\operatorname{dummy})\) from Lemma 43 and the proof of \(\top\), this gives, by \(\mathsf{pl}\), a proof of \(\langle f_e(w),\operatorname{dummy}\rangle_F\). Cancellation at the exact input \(m\) gives \[\langle f_e(w),m\rangle_F \leftrightarrow \operatorname{if}\bigl(D(m);\top, \langle w,f_i(m)\rangle_{\operatorname{Single}}\bigr).\] Use \(d_m\) and \(\mathsf{pl}\) to obtain \[\langle f_e(w),m\rangle_F \leftrightarrow\langle w,f_i(m)\rangle_{\operatorname{Single}}.\] Now use (46) with \(f=f_e(w)\). Its condition has the positive proof just constructed, so \(\mathsf{pl}\) selects its first branch and gives \[ \operatorname{Access}(w;o,x.\Psi) \leftrightarrow\langle w,f_i(m)\rangle_{\operatorname{Single}}. \tag{47}\] This is where the first occurrence of the callback parameter is fixed: it is the original \(m\) by the exact substitution in cancellation.

For the second selection, cancellation of \(f_i(m)\) at \(\operatorname{dummy}\) gives \[\langle f_i(m),\operatorname{dummy}\rangle_F \leftrightarrow \operatorname{if}\bigl(D(\operatorname{dummy});\bot, \operatorname{qry}_{\operatorname{pt}} (\operatorname{dummy},\operatorname{pred}(x.\Psi(m,x)))\bigr).\] The proof of \(D(\operatorname{dummy})\) therefore gives a proof of \(\neg\langle f_i(m),\operatorname{dummy}\rangle_F\) by \(\mathsf{pl}\). Cancellation of \(f_i(m)\) at \(\operatorname{point}(y)\), followed by \(\neg D(\operatorname{point}(y))\), gives \[\langle f_i(m),\operatorname{point}(y)\rangle_F \leftrightarrow \operatorname{qry}_{\operatorname{pt}} (\operatorname{point}(y),\operatorname{pred}(x.\Psi(m,x))).\] The point-query proof (42), at the exact predicate \(\operatorname{pred}(x.\Psi(m,x))\), compares this right side with \(\operatorname{pred}(x.\Psi(m,x))@y\). In turn, (37) compares that formula with \(\Psi(m,\operatorname{Round}(y))\). Combining these proofs gives \[\langle f_i(m),\operatorname{point}(y)\rangle_F \leftrightarrow\Psi(m,\operatorname{Round}(y)).\] Use (46) once more, now with \(f=f_i(m)\). Its condition has the negative proof above, so \(\mathsf{pl}\) selects its second branch and yields \[\langle w,f_i(m)\rangle_{\operatorname{Single}} \leftrightarrow\Psi(m,\operatorname{Round}(y)).\] Finally combine this with (47) by \(\mathsf{pl}\). Only predicate evaluation rounded an argument, and that argument was \(y\). Every occurrence of \(m\) in this derivation comes from exact data substitution, without a logical replacement of data. ◻

Proof. Reflexivity is \(\Lambda P.\lambda^*h.\mathsf{pl}_{P@y\leftrightarrow P@y}()\). For symmetry, under \(e:y\sim z\), introduce \(P,h\), instantiate \(e[P]\cdot h\), and apply \(\mathsf{pl}\) to reverse its biconditional. For transitivity, under \(e:y\sim z\) and \(f:z\sim w\), introduce \(P,h\) and apply \(\mathsf{pl}_{P@y\leftrightarrow P@w}\) to \(e[P]\cdot h,f[P]\cdot h\). For rounding introduce \(P,h\), project \(\forall w.(P@w\leftrightarrow P@\operatorname{Round}w)\) from \(h:\operatorname{Good}(P)\), and instantiate it at \(y\). Write these builders as \(\operatorname{refl}\), \(\operatorname{sym}\), and \(\operatorname{trans}\). The two components of the last biconditional are \[\begin{aligned} &\lambda^*u.\operatorname{trans} (\operatorname{sym}(e),\operatorname{trans}(u,f)),\\ &\lambda^*u.\operatorname{trans} (e,\operatorname{trans}(u,\operatorname{sym}(f))). \end{aligned}\] In the first line \(u:a\sim c\), and in the second \(u:a'\sim c'\), so the endpoints are respectively \(a'\sim c'\) and \(a\sim c\). ◻

Proof. Predicate evaluation first gives \[c_y@w\leftrightarrow(\operatorname{Round}w\sim y).\] Apply relation congruence with \(\operatorname{RoundRel}(w)\) and \(\operatorname{refl}(y)\); propositional chaining gives the first displayed evaluation. For the union do this separately for \(y\) and \(z\), then chain their disjunctions. For \(e:y\sim y'\), congruence with \(\operatorname{refl}(w),e\), together with the two class evaluations, gives \(c_y@w\leftrightarrow c_{y'}@w\). Introduce \(w\) to obtain the class comparison. For the union use the two parameter congruences inside the disjunction before introducing \(w\).

Apply \(\operatorname{qr}_{C_t}\) to the class comparison to obtain the \(\operatorname{Is}_t\) comparison. For \(T_t\), combine the two resulting \(\operatorname{Is}\) comparisons and \(\operatorname{qr}_{E_t}\) applied to the union comparison. For \(\operatorname{form}\), fix \(y\). The \(T_\ell\) comparison with its first argument unchanged, together with \((P\approx P')[y]\), gives \[(T_\ell(y,z)\land P@y)\leftrightarrow (T_\ell(y,z')\land P'@y).\] Apply \(\mathsf{Ex}_y\), then combine its result with the \(T_r(a,z)\leftrightarrow T_r(a',z')\) comparison by \(\mathsf{pl}\). Predicate evaluation for \(\operatorname{Pair}\) has right side \(\operatorname{form}(P,a,\operatorname{Round}z)\). The just-proved form congruence, with \(P,a\) unchanged and \(\operatorname{RoundRel}(z)\), gives \(\operatorname{pv}\). Finally fix \(z\), combine both \(\operatorname{pv}\) proofs with form congruence at unchanged \(z\), and introduce \(z\). ◻

Proof. For \(\simeq\), introduce \(i\) and use propositional reflexivity, symmetry, or transitivity of the instantiated biconditionals. Its congruence builder is the pair displayed in Lemma 45, with the relation replaced by \(\simeq\). Primitive \(X\)-evaluation is preserved by \(\operatorname{Round}_X\). Apply this preservation at \(z_i\) and introduce \(i\) to obtain \(\operatorname{RoundRel}_X\). Cancellation of \(\operatorname{mk}_X\) gives \(\operatorname{LP}\) at the exact input \(z_i\).

For (54), the application \(z_iA^\uparrow\) beta-reduces to the same pack and data lambda at \(A\), since \((A^\uparrow)^\downarrow=_\beta A\) and the wrapper choices are fixed. The pack/use cancellation leaves the read of that function applied to \(\operatorname{Bundle}(m,y)\). After its raw beta contraction, read/send cancellation leaves \[\operatorname{Access} (\operatorname{Bundle}(m,y);o,w.i@\operatorname{lift}_o(w)).\] The Access builder, applied to \(d_m\), compares this with \(i@\operatorname{lift}_m(\operatorname{Round}y)\). Chain these three biconditionals by \(\mathsf{pl}\).

To obtain \(\operatorname{LC}(e)\), introduce \(i\). Pair congruence applied to the reflexive comparison of \(\operatorname{Part}(z_i)\) and to \(e\), followed by \(\operatorname{qr}_R\), compares \(\operatorname{sb}(z_i,m,a)\) and \(\operatorname{sb}(z_i,m,a')\). Combine it with the two \(\operatorname{LP}\) proofs and introduce \(i\).

For validity introduce \(i,i'\) and \(e:i\approx i'\). There is a comparison \(\operatorname{Part}(z_i)\approx\operatorname{Part}(z_{i'})\): at \(y\), predicate evaluation gives the two expressions \(z_i\diamond_m\operatorname{Round}y\) and \(z_{i'}\diamond_m\operatorname{Round}y\). Apply (54) at precisely \(\operatorname{Round}y\), and use \[e[\operatorname{lift}_m (\operatorname{Round}(\operatorname{Round}y))].\] These proofs propositionally entail the required evaluation comparison; introduce \(y\). Apply Pair congruence with \(a\) unchanged, then \(\operatorname{qr}_R\), and finally the two \(\operatorname{LP}\) proofs. Introducing \(i,i',e\) proves (56).

For (57), apply \(ex\) at \(\operatorname{lift}_m y,\operatorname{lift}_m(\operatorname{Round}y)\) to \(\operatorname{LC}(\operatorname{RoundRel}(y))\). Combine its result with (54). Under \(e:y\sim z\), apply \(ex\) at the two lifts to \(\operatorname{LC}(e)\), and combine this with the exact probe evaluations at \(y,z\). Introducing \(y,z,e\) proves \(\operatorname{Resp}(z_i)\). Finally predicate evaluation gives \(\operatorname{Part}(v)@y\leftrightarrow v\diamond_m\operatorname{Round}y\). Combine it with \(h[y][\operatorname{Round}y]\cdot \operatorname{RoundRel}(y)\) to obtain (58). ◻

Proof. The two double-embedding builders give their signed bits and recover each callback at its exact input. Apply them successively to \(B_1\) and to \(u\mapsto\langle u,z_i\rangle_{\rho_1}\). For the latter, first-wrapper cancellation gives \(\langle y_1(x),z_i\rangle_{\rho_1}\leftrightarrow[xz_i]\). Propositional chaining gives all the asserted canonical evaluations. For a general \(y\), the outer bit and every outer recovery are Boolean combinations of primitive \(L\)-evaluations at arguments independent of \(y\). Primitive Round preservation at those arguments, followed by \(\mathsf{pl}\), therefore gives each invariance proof.

Reflexivity of \(\operatorname{Ae}\) pairs the propositional bit reflexivities with \(\Lambda i.\mathsf{pl}_{O_i(y)\leftrightarrow O_i(y)}()\). For symmetry, project both bit comparisons and the observation universal, reverse the former by \(\mathsf{pl}\), instantiate the latter at \(i\), reverse it, and introduce \(i\). For transitivity perform these projections on both premises, compose the bit comparisons, and at each \(i\) compose the two observation comparisons before introducing \(i\). Reassemble the conjunctions by \(\mathsf{pl}\). The invariance proofs supply the two bit components of \(\operatorname{AeRound}\) and, after introduction of \(i\), its observation component. The congruence builder for \(\operatorname{Ae}\) is the explicit two-component transitivity construction of Lemma 45.

Given \(e:x\simeq x'\), the canonical signed bits imply the two same-tag bit comparisons. At \(i\), combine \(e[i]\) with both canonical \(O_i\) evaluations, then introduce \(i\). This proves \(\operatorname{Ae}(x^t,x'^{\,t})\). Conversely project its observation universal, instantiate at \(i\), and chain the two canonical evaluations to obtain \(\operatorname{le}(i,x)\leftrightarrow \operatorname{le}(i,x')\); introduce \(i\). For \(t\ne u\), choose a coordinate where their fixed strings differ. The two signed-bit proofs contradict the comparison at that coordinate projected from an assumed \(\operatorname{Ae}(x^t,x'^{\,u})\). Abstract that assumption to obtain the negation. ◻

Proof. Under \(x,x'\), the evaluations \(d[x],d[x']\) propositionally entail \[(x\simeq x'\Rightarrow(i@x\leftrightarrow i@x')) \leftrightarrow (x\simeq x'\Rightarrow(i'@x\leftrightarrow i'@x')).\] Apply \(\mathsf{All}_{x,x'}\) to obtain \(\operatorname{ExtC}(d)\).

For \(G\), under \(y,z\), apply \(\mathsf{pl}\) to \(e[y],e[z]\) with target the comparison of the two implications whose common antecedent is \(\operatorname{Ae}(y,z)\); then apply \(\mathsf{All}_{y,z}\). For \(C_t\), under \(x,w\), the proof \(e[w]\) compares \[P@w\leftrightarrow\operatorname{Ae}(w,x^t) \quad\hbox{with}\quad P'@w\leftrightarrow\operatorname{Ae}(w,x^t).\] Apply \(\mathsf{All}_w\) and then \(\mathsf{Ex}_x\). For \(E_t\), use exactly the same two typed operations, with their common right side now \(\operatorname{Ae}(w,x^0)\lor\operatorname{Ae}(w,x^t)\).

For \(R\), predicate evaluation at \(x\) for \(i_P,i_{P'}\) has right sides \[P@((\operatorname{Round}_Xx)^\ell) \quad\hbox{and}\quad P'@((\operatorname{Round}_Xx)^\ell).\] Combine these evaluations with \(e[(\operatorname{Round}_Xx)^\ell]\) and introduce \(x\), obtaining \(d:i_P\approx i_{P'}\). The proof \(\operatorname{ExtC}(d)\) compares the two antecedents of \(\mathcal P_R\). Under \(x,v:\operatorname{Valid}(x)\), combine \[e[x^r],\qquad v[i_P][i_{P'}]\cdot d\] with target \[(P@(x^r)\Rightarrow \operatorname{le}(i_P,x)) \leftrightarrow(P'@(x^r)\Rightarrow \operatorname{le}(i_{P'},x)).\] Apply \(\mathsf{Gd}_{v:\operatorname{Valid}(x)}\), then \(\mathsf{All}_x\). This compares the consequents of \(\mathcal P_R\). Combine it propositionally with \(\operatorname{ExtC}(d)\). In particular, the change of predicate in \(le\) has used its explicit validity guard.

Data cancellation at \(\operatorname{Enc}_t(P)\) compares \(\operatorname{qry}_t(m_0,P)\) with the defining disjunction evaluated there. The signed marker proofs eliminate every disjunct except \(t\), and give a comparison with \(\mathcal P_t(\operatorname{Dec}(\operatorname{Enc}_t(P)))\). Introduce \(y\) in the decoder evaluation comparison to get \[\operatorname{Dec}(\operatorname{Enc}_t(P))\approx P.\] Use the property-respect builder just proved and chain to obtain \(q_t(P)\). Cancellation at \(bp_\bot\) and the negations of all its structural markers give \(\neg D(m_0)\). For each structural \(t\), form \[\Lambda P,P'.\lambda^*e.\, \mathsf{pl}\bigl(q_t(P),q_t(P'), \text{property-respect}_t(e)\bigr)\] with target \(\operatorname{qry}_t(m_0,P)\leftrightarrow \operatorname{qry}_t(m_0,P')\). Together with \(\neg D(m_0)\), these are exactly the conjuncts of the displayed admissibility formula. ◻

Proof. The proof \(q_G(P)\) identifies the second conjunct of \(\operatorname{Good}(P)\). Its property implies the first: the builder \[\lambda^*g.\Lambda y.\, g[y][\operatorname{Round}y]\cdot\operatorname{AeRound}(y)\] has that implication as type. Combining these by \(\mathsf{pl}\) gives \(\operatorname{GA}(P)\).

For an observation \(\Phi\) equal to \(H_1,H_2\), or \(O_i\) with \(i\) temporarily free, put \(P_\Phi=\operatorname{pred}(w.\Phi(w))\). Predicate evaluation and Round invariance give, at every \(u\), an evaluation proof \(P_\Phi@u\leftrightarrow\Phi(u)\). Under \(a:\operatorname{Ae}(u,w)\), project the relevant bit comparison, or project and instantiate its observation universal at the free \(i\). Combine it with the two evaluations to get \(P_\Phi@u\leftrightarrow P_\Phi@w\). Introducing \(u,w,a\) proves \(\mathcal P_G(P_\Phi)\); apply \(\operatorname{back}(\operatorname{GA}(P_\Phi),-)\) to get \(\operatorname{Good}(P_\Phi)\).

Under \(e:y\sim z\), the proof \(e[P_\Phi]\cdot\operatorname{Good}(P_\Phi)\), combined with the two evaluations, gives \(\Phi(y)\leftrightarrow\Phi(z)\). Take the two bit instances. For \(O_i\), introduce \(i\) after obtaining this comparison. Their conjunction proves \(\operatorname{Ae}(y,z)\). Conversely, under \(a:\operatorname{Ae}(y,z)\), the term \[\Lambda P.\lambda^*g.\, \bigl(\operatorname{to}(\operatorname{GA}(P),g)\bigr) [y][z]\cdot a\] proves \(y\sim z\). Abstract the two premises and pair the directions to obtain \(\operatorname{SA}\).

Given \(e:x\simeq x'\), use the same-tag direction of Lemma 48, then \(\operatorname{back}(\operatorname{SA},-)\). Given \(f:x^t\sim x'^{\,t}\), use \(\operatorname{to}(\operatorname{SA},f)\) and the reverse same-tag direction. For distinct tags, introduce \(f:x^t\sim x'^{\,u}\), map it forward through \(\operatorname{SA}\), and apply the negation from Lemma 48. These define the three asserted builders. ◻

Proof. For the first forward implication, take \(h:\operatorname{Is}_t(y)\), apply \(\operatorname{to}(q_{C_t}(c_y),h)\), and open the result as \(x,p\), where \[p:\forall w.\,(c_y@w\leftrightarrow\operatorname{Ae}(w,x^t)).\] The class evaluation and reflexivity prove \(c_y@y\). Apply \(p[y]\) forward and \(\operatorname{SA}(y,x^t)\) backward to obtain \(y\sim x^t\). Witness the opened \(x\) in the target existential. The target contains no free occurrence of either local witness. For the reverse, open \(x,e:y\sim x^t\). At \(w\), the class evaluation, congruence with \(\operatorname{refl}(w),e\), and \(\operatorname{SA}(w,x^t)\) yield \(c_y@w\leftrightarrow\operatorname{Ae}(w,x^t)\). Introduce \(w\), witness \(x\) in \(\mathcal P_{C_t}(c_y)\), and apply \(q_{C_t}(c_y)\) backward.

For the edge forward implication, take \(h:T_t(y,z)\). Project both \(\operatorname{Is}\) conjuncts and its query. Use the first equivalence and open their witnesses as \[a,e_a:y\sim a^0,\qquad b',e_{b'}:z\sim b'^{\,t}.\] Map the query forward through \(q_{E_t}(u_{yz})\) and open its witness as \(x,p\), with \[p:\forall w.\, \bigl(u_{yz}@w\leftrightarrow (\operatorname{Ae}(w,x^0)\lor\operatorname{Ae}(w,x^t))\bigr).\] The union evaluation and reflexivity prove \(u_{yz}@y\) and \(u_{yz}@z\). Apply \(p\) at each of these points and the comparisons \(\operatorname{SA}\); the resulting proofs have types \[(y\sim x^0)\lor(y\sim x^t),\qquad (z\sim x^0)\lor(z\sim x^t).\] The term \[\lambda^*f.\operatorname{diff}_{0,t}\cdot \operatorname{trans}(\operatorname{sym}(e_a),f)\] negates \(y\sim x^t\). The corresponding term \[\lambda^*f.\operatorname{diff}_{t,0}\cdot \operatorname{trans}(\operatorname{sym}(e_{b'}),f)\] negates \(z\sim x^0\). Propositional elimination gives \(y\sim x^0\) and \(z\sim x^t\); pair them and witness \(x\). All three openings have the original target existential.

For the reverse, open \(x,e\) and project \(e_0:y\sim x^0\), \(e_t:z\sim x^t\). Witness \(x\) with \(e_0\) or \(e_t\) in the first equivalence backward to obtain the two \(\operatorname{Is}\) conjuncts. At \(w\), the union evaluation and congruences along \(e_0,e_t\) compare \(u_{yz}@w\) with \((w\sim x^0)\lor(w\sim x^t)\). Use the two \(\operatorname{SA}\) proofs and introduce \(w\), obtaining the property required for the witness \(x\) in \(\mathcal P_{E_t}(u_{yz})\). Apply \(q_{E_t}(u_{yz})\) backward and conjoin the three results. ◻

Proof. For (60) forward, first negate \(T_r(x^0,x'^{\,\ell})\). Given such a proof, map it forward through Lemma 51 and open its witness \(u\) into \(\bot\). Its second conjunct is \(x'^{\,\ell}\sim u^r\), contradicted by \(\operatorname{diff}_{\ell,r}\). Given \(p:P_x@(x'^{\,\ell})\), use \(\operatorname{pv}\) and this negation to extract \[\exists y.\, (T_\ell(y,x'^{\,\ell})\land\operatorname{Part}(v)@y).\] Open it as \(y,q\), and open the edge witness from the first conjunct as \(u,q_0,q_\ell\), where \[q_0:y\sim u^0,\qquad q_\ell:x'^{\,\ell}\sim u^\ell.\] The proof \(\operatorname{TagBack}_\ell(q_\ell)\) is \(x'\simeq u\). Symmetrize it and apply \(\operatorname{Tag}_0\), then compose with \(q_0\), to get \(e:y\sim x'^{\,0}\). From the second conjunct of \(q\), the unrounded Part evaluation gives \(v\diamond_m y\). Apply \(h[y][x'^{\,0}]\cdot e\) forward to obtain the target \(v\diamond_m(x'^{\,0})\). Each opening uses this fixed target.

For the left reverse implication, a proof of \(v\diamond_m(x'^{\,0})\) gives \(\operatorname{Part}(v)@(x'^{\,0})\) by (58) backward. Witness \(x'\) with the two reflexivities in the edge equivalence backward to get \(T_\ell(x'^{\,0},x'^{\,\ell})\). Pair these, witness \(y=x'^{\,0}\), inject the resulting existential into \(\operatorname{form}\), and apply \(\operatorname{pv}\) backward.

For (61) forward, negate \(\exists y.(T_\ell(y,x'^{\,r})\land\operatorname{Part}(v)@y)\). Open an assumed existential into \(\bot\), open its \(T_\ell\) witness, and contradict its second conjunct \(x'^{\,r}\sim u^\ell\) with \(\operatorname{diff}_{r,\ell}\). Thus \(\operatorname{pv}\) maps a proof of \(P_x@(x'^{\,r})\) to \(T_r(x^0,x'^{\,r})\). Open its witness \(u\), with \(x^0\sim u^0\) and \(x'^{\,r}\sim u^r\). The two same-tag converses give \(x\simeq u\) and \(x'\simeq u\). Compose the first with the symmetry of the second to prove \(x\simeq x'\). For the reverse, given \(e:x\simeq x'\), witness \(x\) in the edge equivalence with reflexivity at \(x^0\) and \(\operatorname{Tag}_r(\operatorname{sym}(e)): x'^{\,r}\sim x^r\). This gives \(T_r(x^0,x'^{\,r})\); inject it into \(\operatorname{form}\), then apply \(\operatorname{pv}\) backward. Abstract each input proof and pair the two directions. ◻

Proof. Choose a counterexample of least syntax size, allowing all such data extensions and all targets in \(\mathcal T\). A proof-mode term is neither a sort nor a product.

Suppose first that \(P\) is a lambda. Its body and result have proof mode. Its generated type is therefore a product with result label \(\mathsf p\). This type cannot convert to a terminal: a normal terminal is either not a product, or has outer product labels \((\mathsf d,\mathsf d)\). Consequently \(T\) has a nonempty positive prefix. Product compatibility forces the lambda’s labels to be \((\mathsf d,\mathsf p)\), with annotation convertible to the first telescope domain. Its binder is a data variable. Generation gives a body typing whose expected type converts to the remaining suffix. The suffix’s recorded sort typing, transported by context conversion to the lambda annotation and weakened as necessary, permits conversion of the body to that suffix. The body has normal erasure and is strictly smaller than \(P\), in an allowed extension by one more data declaration. This contradicts minimality.

Otherwise \(P\) is a variable or an application spine. Every function position of a proof-mode spine has proof mode. Its head cannot be a sort or product, and a lambda head with a nonempty spine would create a redex in its erasure. Thus its head is a proof variable, hence one of the converters \(c\).

If the spine is empty, variable generation says that \(T\) converts to \(\Pi^{\mathsf p,\mathsf p}u:T_c.F_c\). Both are normal. The latter has outer labels \((\mathsf p,\mathsf p)\), whereas \(T\) either has a \((\mathsf d,\mathsf p)\) prefix or is an all-data terminal. This is impossible by confluence and product compatibility.

If the spine is nonempty, let \(Q\) be its first argument. Generation at the first application and at \(c\), followed by product compatibility, forces that application to have labels \((\mathsf p,\mathsf p)\) and its domain to convert to \(T_c\). Thus \(Q\) is a proof-mode term. The recorded sort typing of \(T_c\), weakened to the current context, converts its generated argument typing to \(Q:T_c\). Its erasure is normal because it is a subterm of the normal erasure of \(P\), and its syntax size is strictly smaller. This is another counterexample to minimality. ◻

Proof. If the configuration prohibited in (7) occurred, Sections 6–9, culminating in Proposition 57, would give a finite legal labelled context \(\Delta\) of the form above and a proof-mode term \[\Delta\vdash P:F_b.\] Every other temporary assumption in the construction has been discharged or instantiated. Erasure gives an ordinary typing derivation \(|\Delta|\vdash |P|:|F_b|\) using only the original specification. The system-wide hypothesis therefore applies to this particular open legal term \(|P|\). Choose a finite reduction to a full beta-normal form. Lemma 35 lifts that reduction to a labelled reduct \(P'\) with the same exact type \(F_b\), the same proof mode, and normal erasure. Lemma 58 rules out \(P'\). ◻

Proof of Theorem 1. By Lemma 12, it suffices to treat a finite specification. Process the finitely many primary components in dependency order. For a component without an odd closed walk use Proposition 22. For one with no profile triple entirely inside it use Proposition 25. Every remaining component satisfies the hypotheses of Proposition 59; hence Proposition 34 supplies its candidate interface. Proposition 20 therefore advances the processed invariant at every stage. Once all components are processed, Proposition 21 gives strong normalization of every legal expression. This includes expressions in arbitrary valid open contexts and every reduction position in their annotations. ◻