Constant | Type |
---|---|
SCC | :(α -> α -> bool) -> (α -> bool) -> bool |
lift | :(α -> β -> bool) -> (α -> bool) -> (β -> bool) -> bool |
|- ∀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 ≠ ∅
|- ∀R vs vs'. lift R vs vs' ⇔ ∃v v'. v ∈ vs ∧ v' ∈ vs' ∧ R v v'
|- ∀R vs vs'. SCC R vs ∧ SCC R vs' ∧ vs ≠ vs' ⇒ DISJOINT vs vs'
|- ∀R vs v v'. v ∈ vs ∧ v' ∈ vs ∧ SCC R vs ∧ reflexive R ⇒ (λv v'. R v v' ∧ v ∈ vs ∧ v' ∈ vs)⁺ v v'