dedekind::order::detail_cover_witness Namespace Reference

Classes
struct	Walk
	A walk along the cover: where it is, and whether it met b. More...
struct	StepToward
	One successor step of a walk that looks for b. More...
struct	AgreesFrom
	For a fixed a, every b agrees: a < b iff reached. More...
struct	AgreesOn
	Every a in the window agrees with every b. More...

Functions
constexpr bool	reaches (int a, int b, int k)
	Whether b is reached from a in 1 to k − 1 cover steps.
consteval bool	order_is_cover_star (int k)

Detailed Description

The successor is the cover; the order

is its star. On a discrete chain nothing lies strictly between x and S(x): the bounded meet (x, S(x)) is empty and (x, S(S(x))) is the point S(x), both read off the one bounded law. And the order is the Kleene star of the cover relation \(\Gamma_S = \mathrm{graph}(S)\): \(a < b \iff (a, b) \in \Gamma_S^{+}\) — the one relation whose star is point-free here, because the chain's own < decides it.