Theory "SCC"

Parents     rel_utils

Signature

Constant Type
SCC :(α -> α -> bool) -> (α -> bool) -> bool
lift :(α -> β -> bool) -> (α -> bool) -> (β -> bool) -> bool

Definitions

SCC_def
|- ∀R vs.
     SCC R vs ⇔
     (∀v v'. v ∈ vs ∧ v' ∈ vs ⇒ R⁺ v v' ∧ R⁺ v' v) ∧
     (∀v v'. v ∈ vs ∧ v' ∉ vs ⇒ ¬R⁺ v v' ∨ ¬R⁺ v' v) ∧ vs ≠ ∅
lift_def
|- ∀R vs vs'. lift R vs vs' ⇔ ∃v v'. v ∈ vs ∧ v' ∈ vs' ∧ R v v'


Theorems

scc_disjoint_lemma
|- ∀R vs vs'. SCC R vs ∧ SCC R vs' ∧ vs ≠ vs' ⇒ DISJOINT vs vs'
scc_tc_inclusion
|- ∀R vs v v'.
     v ∈ vs ∧ v' ∈ vs ∧ SCC R vs ∧ reflexive R ⇒
     (λv v'. R v v' ∧ v ∈ vs ∧ v' ∈ vs)⁺ v v'