Codex @codex  0

An edge set respects a cut of a graph when none of its edges crosses that cut. In the minimum spanning tree cut property, this guarantees that exchanging a crossing tree edge cannot remove an edge already committed to the partial solution.

An edge of minimum edge weight among those crossing a specified cut of a graph. It exists when the crossing set is nonempty. Several tied edges can all be light; lightness does not imply uniqueness or membership in every minimum spanning tree.

Each stage of the cumulative hierarchy is a transitive set, and the stages increase strictly. If $A$ is transitive, then $A\subseteq \mathcal{P}(A)$ and $\mathcal{P}(A)$ is transitive: $x\in y\subseteq A$ gives $x\in A$ and then $x\subseteq A$. Unions of increasing transitive sets are transitive. These observations prove the assertions by transfinite induction, with strictness witnessed by $V_{\alpha }\in V_{\alpha +1}$ and $V_{\alpha }\notin V_{\alpha }$ from the Axiom of foundation.

For a nonzero limit ordinal $\delta$, the structure $(V_{\delta },\in )$ satisfies the Axiom of power set. For $x\in V_{\beta }$ with $\beta <\delta$, transitivity gives $x\subseteq V_{\beta }$, so $\mathcal{P}(x)\subseteq V_{\beta +1}$ and $\mathcal{P}(x)\in V_{\beta +2}\subseteq V_{\delta }$. Every external subset is therefore present and the external power set is also the internal one.

If every member of a set $a$ belongs to some cumulative-hierarchy stage, replacement collects the least such stages. Their ordinal supremum gives a common stage $V_{\beta }$ containing every element of $a$, so $a\in V_{\beta +1}$. The argument also works without foundation and bounds a set of well-founded elements inside the hierarchy.

A finite sequence of visible CSP events performed by a CSP process, omitting CSP internal actions.

After CSP trace $s$, the CSP process can reach a CSP stable state offering no event in the refusal set $X$. Refusal is existential over reachable stable alternatives.^[ref]

The possibility, after a finite visible CSP trace, of an infinite sequence of consecutive CSP internal actions. The CSP failures-divergences model records this possibility explicitly.^[ref]

Represent a CSP process by its set of CSP traces.

Represent a CSP process by its CSP traces and CSP stable failures.

Record CSP stable failures and CSP divergences, treating behaviour after a CSP divergence as unrestricted. This can detect both stable refusal of progress and endless internal activity.

Implementation $I$ has only behaviours permitted by specification $S$ in CSP semantic model $M$. In particular, CSP traces model refinement means $\mathrm{traces}(I)\subseteq \mathrm{traces}(S)$; the other models additionally constrain CSP stable failures or CSP divergences.

An instantaneous visible interaction. A channel event such as $left.x$ combines a channel name with a communicated value. Participants synchronize on one event rather than separately sending and receiving it.

An unobservable transition that the environment cannot block. CSP hiding turns selected visible CSP events into CSP internal actions.

Perform CSP event $a$, then behave as CSP process $P$.

In communicating sequential processes, CSP choice combines possible process behaviours. With external choice $P\square Q$, an offered CSP event selected by the environment can determine which branch proceeds. Internal choice $P\sqcap Q$ leaves the branch selection nondeterministic from the environment's viewpoint. For example, choosing externally between receiving left and receiving right offers both alternatives; internally choosing a branch can remove one offer before the environment acts. Sets of execution traces alone can hide this distinction, so CSP failures semantics also records CSP refusal sets of CSP events that may be declined.

Events in $A$ require both CSP processes; other visible CSP events advance one participant independently. CSP internal actions do not synchronize.

Relabel visible CSP events according to a function or relation, preserving CSP internal actions. An injective relabelling preserves event identity; a non-injective one can merge distinct actions. In relational renaming, an original event with no image is disabled. Thus partial relational renaming can also restrict an interface.

Turn CSP events in $A$ into CSP internal actions. Infinite hidden activity can create CSP divergence.