Manuscript En08-A@1 · En08-A.tex · theorem · c688d76d
Theorem: Exact availability criterion
Causal typing as an explicit refinement › An affine first-order interface · lines 1867–1892 · proof included or linked
En08-A@1#thm:typing
One has if and only if
Consequently, an unavailable context entry may occur only if its name is unused.
Proof. Erasing an annotated derivation gives an affine derivation. Induction proves the origin condition: it is the variable side condition, is inherited through operations, and is unaffected by weakening.
Conversely, restore each context entry's origin in an affine derivation. Every variable leaf is a free occurrence in the enclosing first-order term, so the assumed origin condition validates its annotated variable rule. Disjointness of contexts is unchanged, and weakening places no condition on an unused entry. Induction reconstructs the annotated derivation.
Displayed formulas in this passage
unlabeled · line 1870