appendix sectionnotation

Dependent boundaries, stable paths, and controlled dependencies

notation	meaning	owner
notation	meaning	owner
$R <: S$ , $Γ ⊢_{DRef} e \Rightarrow R$ , $Γ ⊢_{DRef} e \Leftarrow R$	certified refinement implication, principal synthesis, and checking in the local difference-constraint calculus	chapter 44
$Γ ⊢_{#} t : T$ , $Γ ⊢_{# #} t : T$	tight and invertible typing in an inert DOT context	chapter 45
$Γ ⊢ p path$ , $Replace (T, p, q, U)$	stable-path formation and one-occurrence path replacement	chapter 46
$p_{N}, c_{N}, e_{N}$ , $μ ⋆ . c_{N}$ , $\hat{tp}$	mutually generated NEF proofs, commands, and contexts; fragment-local control; and the calculus’s distinguished delimiter	chapter 47
$σ ::= ϵ ∣ σ {r ∣ q}$ , $A_{σ}$ , $⊢_{d}$	dependency lists, their formula-compatibility classes, and the dependent context/command mode; regular proof judgments carry no list	definition 109.4