Theory "dirGraph"

Parents     indexedLists   patternMatches

Signature

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

Definitions

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

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