Theory "dirGraph"

Parents     indexedLists   patternMatches

Signature

Constant Type
EXCLUDE :(β -> α list) -> (β -> bool) -> β -> α list
Parents :(α -> β list) -> α -> bool
REACH :(α -> α list) -> α -> α -> bool
REACH_LIST :(α -> α list) -> α list -> α -> bool

Definitions

EXCLUDE_def 
⊢ ∀G ex node. EXCLUDE G ex node = if node ∈ ex then [] else G node
Parents_def 
⊢ ∀G. Parents G = {x | G x ≠ []}
REACH_LIST_def 
⊢ ∀G nodes y. REACH_LIST G nodes y ⇔ ∃x. MEM x nodes ∧ y ∈ REACH G x
REACH_def 
⊢ ∀G. REACH G = (λx y. MEM y (G x))꙳

Theorems

EXCLUDE_LEM 
⊢ ∀G x l. EXCLUDE G (x INSERT l) = EXCLUDE (EXCLUDE G l) {x}
REACH_EXCLUDE 
⊢ ∀G x. REACH (EXCLUDE G x) = (λx' y. x' ∉ x ∧ MEM y (G x'))꙳
REACH_LEM1 
⊢ ∀p G seen.
    p ∉ seen ⇒
    (REACH (EXCLUDE G seen) p =
     p INSERT REACH_LIST (EXCLUDE G (p INSERT seen)) (G p))
REACH_LEM2 
⊢ ∀G x y. REACH G x y ⇒ ∀z. ¬REACH G z y ⇒ REACH (EXCLUDE G {z}) x y