def
Hex.GraphIso.Nauty.RelCover
{α : Sort u}
(R : α → α → Prop)
(rank : α → Nat)
(all done live : α → Prop)
:
Each original child is resolved or is related to a no-larger live child. The relation may retain a permutation witness rather than only equality of the children's values.
Equations
Instances For
theorem
Hex.GraphIso.Nauty.RelCover.step
{α : Sort u}
{R : α → α → Prop}
{rank : α → Nat}
{all done live done' live' : α → Prop}
(htrans : ∀ {x y z : α}, R x y → R y z → R x z)
(h : RelCover R rank all done live)
(hs : ∀ (x : α), live x → (∀ (z : α), R z x → done' z) ∨ ∃ (y : α), live' y ∧ R x y ∧ rank y ≤ rank x)
(hd : ∀ (x : α), done x → done' x)
:
RelCover R rank all done' live'
Compose the witnesses through one change of the live set.
theorem
Hex.GraphIso.Nauty.RelCover.resolve
{α : Sort u}
{R : α → α → Prop}
{rank : α → Nat}
{all done live live' : α → Prop}
(hrefl : ∀ (x : α), R x x)
(htrans : ∀ {x y z : α}, R x y → R y z → R x z)
(h : RelCover R rank all done live)
(hdone : ∀ (x y : α), R x y → done y → done x)
(hstep : ∀ (x : α), live x → live' x ∨ ∃ (y : α), all y ∧ R x y ∧ rank y < rank x)
(x : α)
:
Resolve a removed child by strict rank descent, including when the carrier lands outside the set retained by an earlier filter.
theorem
Hex.GraphIso.Nauty.RelCover.filterDesc
{α : Sort u}
{R : α → α → Prop}
{rank : α → Nat}
{all done live live' : α → Prop}
(hrefl : ∀ (x : α), R x x)
(htrans : ∀ {x y z : α}, R x y → R y z → R x z)
(h : RelCover R rank all done live)
(hdone : ∀ (x y : α), R x y → done y → done x)
(hstep : ∀ (x : α), live x → live' x ∨ ∃ (y : α), all y ∧ R x y ∧ rank y < rank x)
:
RelCover R rank all done live'
Apply a descending filter while retaining the relational witnesses.