- scc_lemma_1_4_2_1_2_2
-
|- ∀R R' P x. (∀y. P y ∧ ¬R x y ⇒ ¬R' x y) ∧ (∀y. ¬R x y) ⇒ ∀y. R' x y ⇒ ¬P y
- scc_lemma_1_4_2_1_3_1_3_1
-
|- ∀R s x.
(∀x y. x ∈ s ∧ R x y ⇒ y ∈ s) ⇒
∀y. R⁺ x y ⇒ (λx y. R x y ∧ y ∈ s)⁺ x y ∨ ∃y. R x y ∧ y ∉ s
- scc_lemma_1_4_2_1_3_1_3
-
|- ∀R s x.
(∀y. R x y ⇒ y ∈ s) ∧ (∀x y. x ∈ s ∧ R x y ⇒ y ∈ s) ⇒
∀y. R⁺ x y ⇒ (λx y. R x y ∧ y ∈ s)⁺ x y
- scc_lemma_1_4_2_1_3_1_4_2_1
-
|- ∀R x y. R⁺ x y ⇒ (λx y. R x y ∧ x ≠ y)⁺ x y ∨ (x = y)
- scc_lemma_1_4_2_1_3_1
-
|- ∀R x y. (∀z. ¬R y z) ⇒ ∀z. R⁺ x z ⇒ (z = y) ∨ ¬∀a. R x a ⇒ (a = y)
- scc_lemma_1_4_2_1_3
-
|- ∀R x y. (∀z. R x z ⇒ (z = y)) ∧ (∀z. ¬R y z) ⇒ ∀z. R⁺ x z ⇒ (z = y)
- scc_lemma_x
-
|- ∀R x z. R x z ∨ (∃y. R x y ∧ R⁺ y z) ⇒ R⁺ x z
- TC_CASES1_RW
-
|- ∀R x z. R x z ∨ (∃y. R x y ∧ R⁺ y z) ⇔ R⁺ x z
- scc_lemma_xx
-
|- ∀R R' P P'.
(∀x y. P x ∧ P' y ⇒ (R x y ⇒ R' x y) ∧ (λx y. R x y ∧ P x ∧ P' y)⁺ x y) ⇒
∀x y. P x ∧ P' y ⇒ R'⁺ x y
- scc_lemma_xxx
-
|- ∀R x z. R x z ∨ (∃y. R⁺ x y ∧ R y z) ⇒ R⁺ x z
- TC_CASES2_RW
-
|- ∀R x z. R x z ∨ (∃y. R⁺ x y ∧ R y z) ⇔ R⁺ x z
- scc_lemma_1_4_2_1_1_1_3_2_1_1
-
|- ∀R P x y. ¬R⁺ x y ⇒ ¬(λx y. R x y ∧ P x y)⁺ x y
- scc_lemma_1_4_2_1_1_1_3_2_1
-
|- ∀R R' P x y.
(∀x y. P x y ⇒ R' x y ⇒ R x y) ∧ ¬R⁺ x y ⇒ ¬(λx y. R' x y ∧ P x y)⁺ x y
- scc_lemma_1_4_1_1_2_1_3
-
|- ∀R R' P.
(∀x y. P x ∧ P y ⇒ (R x y ⇒ R' x y) ∧ (λx y. R x y ∧ P x ∧ P y)⁺ x y) ⇒
∀x y. P x ∧ P y ⇒ R'⁺ x y
- scc_lemma_1_4_2_1_1_1_3_2_2_1
-
|- ∀R P x y. (λx y. R x y ∧ P x y)⁺ x y ⇒ R⁺ x y
- scc_lemma_1_4_2_1_1_1_3_2_2
-
|- ∀R'.
reflexive R' ⇒
∀P x y.
R'⁺ x y ⇒
(λx y. R' x y ∧ P x ∧ P y)⁺ x y ∨ ∃z. ¬P z ∧ R'⁺ x z ∧ R'⁺ z y
- scc_lemma_1_4_2_1_1_1_3_2
-
|- ∀R R' P x y.
reflexive R' ∧ (∀x y. P x ∧ P y ⇒ R' x y ⇒ R x y) ∧ ¬R⁺ x y ⇒
¬R'⁺ x y ∨ ∃z. ¬P z ∧ R'⁺ x z ∧ R'⁺ z y
- TC_CASES1_NEQ
-
|- ∀R x z. R⁺ x z ⇒ R x z ∨ ∃y. x ≠ y ∧ y ≠ z ∧ R x y ∧ R⁺ y z
- TC_CASES2_NEQ
-
|- ∀R x z. R⁺ x z ⇒ R x z ∨ ∃y. x ≠ y ∧ y ≠ z ∧ R⁺ x y ∧ R y z