Theory dirGraph

⊢ ∀G ex node. EXCLUDE G ex node = if node ∈ ex then [] else G node

⊢ ∀G. Parents G = {x | G x ≠ []}

⊢ ∀G nodes y. REACH_LIST G nodes y ⇔ ∃x. MEM x nodes ∧ y ∈ REACH G x

⊢ ∀G. REACH G = (λx y. MEM y (G x))꙳

⊢ ∀G x l. EXCLUDE G (x INSERT l) = EXCLUDE (EXCLUDE G l) {x}

⊢ ∀G x. REACH (EXCLUDE G x) = (λx' y. x' ∉ x ∧ MEM y (G x'))꙳

⊢ ∀p G seen.
    p ∉ seen ⇒
    REACH (EXCLUDE G seen) p =
    p INSERT REACH_LIST (EXCLUDE G (p INSERT seen)) (G p)

⊢ ∀G x y. REACH G x y ⇒ ∀z. ¬REACH G z y ⇒ REACH (EXCLUDE G {z}) x y