appendix sectionnotation

Symbolic paths and security observations

notation	meaning	owner
notation	meaning	owner
$q ⟶_{c} q^{'}$ , $q ⟶_{c}^{*} q^{'}$	concrete SymImp-DL step and finite closure	chapter 69
$\hat{q} ⟶_{s} {\hat{q}}^{'}$ , $\hat{q} ⟶_{s}^{*} {\hat{q}}^{'}$	symbolic path step and finite closure	chapter 69
$ρ ⊧_{DL} Φ$ , $Φ_{2} ⊧_{DL} Φ_{1}$	difference-logic satisfaction and checked implication	chapter 69
$(ρ, I) R_{sym} ⟨ \hat{q}, q ⟩$	symbolic/concrete state representation	chapter 69
$ℓ_{1} ⊑_{\sec} ℓ_{2}$	permitted security-lattice flow	chapter 70
$s_{1} \approx_{Γ}^{o} s_{2}$	low equivalence at observer $o$ under $Γ$	chapter 70
$Γ ⊢_{p}^{IF} c$ , $⟨ c, s ⟩ ⟶_{IF} ⟨ c^{'}, s^{'} ⟩$ , $⟨ c, s ⟩ ⇓_{IF} s^{'}$	command typing, small-step execution, and terminating evaluation	chapter 70