Theory "relation"

Signature

Definitions

CR_def

⊢ ∀R. CR R ⇔ diamond R꙳

EMPTY_REL_DEF

⊢ ∀x y. ∅ᵣ x y ⇔ F

EQC_DEF

⊢ ∀R. R^= = RC (SC R)⁺

IDEM_DEF

⊢ ∀f. IDEM f ⇔ (f ∘ f = f)

INDUCTIVE_INVARIANT_DEF

⊢ ∀R P M.
    INDUCTIVE_INVARIANT R P M ⇔ ∀f x. (∀y. R y x ⇒ P y (f y)) ⇒ P x (M f x)

INDUCTIVE_INVARIANT_ON_DEF

⊢ ∀R D P M.
    INDUCTIVE_INVARIANT_ON R D P M ⇔
    ∀f x. D x ∧ (∀y. D y ⇒ R y x ⇒ P y (f y)) ⇒ P x (M f x)

INVOL_DEF

⊢ ∀f. INVOL f ⇔ (f ∘ f = I)

LinearOrder

⊢ ∀R. LinearOrder R ⇔ Order R ∧ trichotomous R

O_DEF

⊢ ∀R1 R2 x z. (R1 ∘ᵣ R2) x z ⇔ ∃y. R2 x y ∧ R1 y z

Order

⊢ ∀Z. Order Z ⇔ antisymmetric Z ∧ transitive Z

PreOrder

⊢ ∀R. PreOrder R ⇔ reflexive R ∧ transitive R

RCOMPL

⊢ ∀R x y. RCOMPL R x y ⇔ ¬R x y

RC_DEF

⊢ ∀R x y. RC R x y ⇔ (x = y) ∨ R x y

RDOM_DEF

⊢ ∀R x. RDOM R x ⇔ ∃y. R x y

RDOM_DELETE_DEF

⊢ ∀R x u v. (R \\ x) u v ⇔ R u v ∧ u ≠ x

RESTRICT_DEF

⊢ ∀f R x. RESTRICT f R x = (λy. if R y x then f y else ARB)

RINTER

⊢ ∀R1 R2 x y. (R1 ∩ᵣ R2) x y ⇔ R1 x y ∧ R2 x y

RRANGE

⊢ ∀R y. RRANGE R y ⇔ ∃x. R x y

RRESTRICT_DEF

⊢ ∀R s x y. RRESTRICT R s x y ⇔ R x y ∧ x ∈ s

RSUBSET

⊢ ∀R1 R2. R1 ⊆ᵣ R2 ⇔ ∀x y. R1 x y ⇒ R2 x y

RTC_def

⊢ RTC =
  (λR a0 a1.
       ∀RTC'.
         (∀a0 a1. (a1 = a0) ∨ (∃y. R a0 y ∧ RTC' y a1) ⇒ RTC' a0 a1) ⇒
         RTC' a0 a1)

RUNION

⊢ ∀R1 R2 x y. (R1 ∪ᵣ R2) x y ⇔ R1 x y ∨ R2 x y

RUNIV

⊢ ∀x y. 𝕌ᵣ x y ⇔ T

SC_DEF

⊢ ∀R x y. SC R x y ⇔ R x y ∨ R y x

SN_def

⊢ ∀R. SN R ⇔ WF Rᵀ

STRORD

⊢ ∀R a b. STRORD R a b ⇔ R a b ∧ a ≠ b

StrongLinearOrder

⊢ ∀R. StrongLinearOrder R ⇔ StrongOrder R ∧ trichotomous R

StrongOrder

⊢ ∀Z. StrongOrder Z ⇔ irreflexive Z ∧ transitive Z

TC_DEF

⊢ ∀R a b.
    R⁺ a b ⇔
    ∀P. (∀x y. R x y ⇒ P x y) ∧ (∀x y z. P x y ∧ P y z ⇒ P x z) ⇒ P a b

WCR_def

⊢ ∀R. WCR R ⇔ ∀x y z. R x y ∧ R x z ⇒ ∃u. R꙳ y u ∧ R꙳ z u

WFP_DEF

⊢ ∀R a. WFP R a ⇔ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ P a

WFREC_DEF

⊢ ∀R M.
    WFREC R M =
    (λx. M (RESTRICT (the_fun R⁺ (λf v. M (RESTRICT f R v) v) x) R x) x)

WF_DEF

⊢ ∀R. WF R ⇔ ∀B. (∃w. B w) ⇒ ∃min. B min ∧ ∀b. R b min ⇒ ¬B b

WeakLinearOrder

⊢ ∀R. WeakLinearOrder R ⇔ WeakOrder R ∧ trichotomous R

WeakOrder

⊢ ∀Z. WeakOrder Z ⇔ reflexive Z ∧ antisymmetric Z ∧ transitive Z

antisymmetric_def

⊢ ∀R. antisymmetric R ⇔ ∀x y. R x y ∧ R y x ⇒ (x = y)

approx_def

⊢ ∀R M x f. approx R M x f ⇔ (f = RESTRICT (λy. M (RESTRICT f R y) y) R x)

diag_def

⊢ ∀A x y. diag A x y ⇔ (x = y) ∧ x ∈ A

diamond_def

⊢ ∀R. diamond R ⇔ ∀x y z. R x y ∧ R x z ⇒ ∃u. R y u ∧ R z u

equivalence_def

⊢ ∀R. equivalence R ⇔ reflexive R ∧ symmetric R ∧ transitive R

inv_DEF

⊢ ∀R x y. Rᵀ x y ⇔ R y x

inv_image_def

⊢ ∀R f. inv_image R f = (λx y. R (f x) (f y))

irreflexive_def

⊢ ∀R. irreflexive R ⇔ ∀x. ¬R x x

nf_def

⊢ ∀R x. nf R x ⇔ ∀y. ¬R x y

rcdiamond_def

⊢ ∀R. rcdiamond R ⇔ ∀x y z. R x y ∧ R x z ⇒ ∃u. RC R y u ∧ RC R z u

reflexive_def

⊢ ∀R. reflexive R ⇔ ∀x. R x x

symmetric_def

⊢ ∀R. symmetric R ⇔ ∀x y. R x y ⇔ R y x

the_fun_def

⊢ ∀R M x. the_fun R M x = @f. approx R M x f

total_def

⊢ ∀R. total R ⇔ ∀x y. R x y ∨ R y x

transitive_def

⊢ ∀R. transitive R ⇔ ∀x y z. R x y ∧ R y z ⇒ R x z

trichotomous

⊢ ∀R. trichotomous R ⇔ ∀a b. R a b ∨ R b a ∨ (a = b)

Theorems

ALT_equivalence

⊢ ∀R. equivalence R ⇔ ∀x y. R x y ⇔ (R x = R y)

EQC_EQUIVALENCE

⊢ ∀R. equivalence R^=

EQC_IDEM

⊢ ∀R. R^= ^= = R^=

EQC_INDUCTION

⊢ ∀R P.
    (∀x y. R x y ⇒ P x y) ∧ (∀x. P x x) ∧ (∀x y. P x y ⇒ P y x) ∧
    (∀x y z. P x y ∧ P y z ⇒ P x z) ⇒
    ∀x y. R^= x y ⇒ P x y

EQC_MONOTONE

⊢ (∀x y. R x y ⇒ R' x y) ⇒ R^= x y ⇒ R'^= x y

EQC_MOVES_IN

⊢ ∀R. ((RC R)^= = R^=) ∧ ((SC R)^= = R^=) ∧ (R⁺ ^= = R^=)

EQC_R

⊢ ∀R x y. R x y ⇒ R^= x y

EQC_REFL

⊢ ∀R x. R^= x x

EQC_SYM

⊢ ∀R x y. R^= x y ⇒ R^= y x

EQC_TRANS

⊢ ∀R x y z. R^= x y ∧ R^= y z ⇒ R^= x z

EXTEND_RTC_TC

⊢ ∀R x y z. R x y ∧ R꙳ y z ⇒ R⁺ x z

EXTEND_RTC_TC_EQN

⊢ ∀R x z. R⁺ x z ⇔ ∃y. R x y ∧ R꙳ y z

EXTEND_RTC_TC_RIGHT1

⊢ ∀R x y z. R꙳ x y ∧ R y z ⇒ R⁺ x z

EXTEND_RTC_TC_RIGHT1_EQN

⊢ ∀R x z. R⁺ x z ⇔ ∃y. R꙳ x y ∧ R y z

EqIsBothRSUBSET

⊢ ∀y z. (y = z) ⇔ y ⊆ᵣ z ∧ z ⊆ᵣ y

IDEM

⊢ ∀f. IDEM f ⇔ ∀x. f (f x) = f x

IDEM_RC

⊢ IDEM RC

IDEM_RTC

⊢ IDEM RTC

IDEM_SC

⊢ IDEM SC

IDEM_STRORD

⊢ IDEM STRORD

IDEM_TC

⊢ IDEM TC

INDUCTION_WF_THM

⊢ ∀R. (∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x) ⇒ WF R

INDUCTIVE_INVARIANT_ON_WFREC

⊢ ∀R P M D x. WF R ∧ INDUCTIVE_INVARIANT_ON R D P M ∧ D x ⇒ P x (WFREC R M x)

INDUCTIVE_INVARIANT_WFREC

⊢ ∀R P M. WF R ∧ INDUCTIVE_INVARIANT R P M ⇒ ∀x. P x (WFREC R M x)

INVOL

⊢ ∀f. INVOL f ⇔ ∀x. f (f x) = x

INVOL_ONE_ENO

⊢ ∀f. INVOL f ⇒ ∀a b. (f a = b) ⇔ (a = f b)

INVOL_ONE_ONE

⊢ ∀f. INVOL f ⇒ ∀a b. (f a = f b) ⇔ (a = b)

IN_RDOM

⊢ x ∈ RDOM R ⇔ ∃y. R x y

IN_RDOM_DELETE

⊢ x ∈ RDOM (R \\ k) ⇔ x ∈ RDOM R ∧ x ≠ k

IN_RDOM_RRESTRICT

⊢ x ∈ RDOM (RRESTRICT R s) ⇔ x ∈ RDOM R ∧ x ∈ s

IN_RDOM_RUNION

⊢ x ∈ RDOM (R1 ∪ᵣ R2) ⇔ x ∈ RDOM R1 ∨ x ∈ RDOM R2

IN_RRANGE

⊢ y ∈ RRANGE R ⇔ ∃x. R x y

Id_O

⊢ $= ∘ᵣ R = R

NOT_INVOL

⊢ INVOL $¬

Newmans_lemma

⊢ ∀R. WCR R ∧ SN R ⇒ CR R

O_ASSOC

⊢ R1 ∘ᵣ R2 ∘ᵣ R3 = (R1 ∘ᵣ R2) ∘ᵣ R3

O_Id

⊢ R ∘ᵣ $= = R

O_MONO

⊢ R1 ⊆ᵣ R2 ∧ S1 ⊆ᵣ S2 ⇒ R1 ∘ᵣ S1 ⊆ᵣ R2 ∘ᵣ S2

RC_IDEM

⊢ ∀R. RC (RC R) = RC R

RC_MONOTONE

⊢ (∀x y. R x y ⇒ Q x y) ⇒ RC R x y ⇒ RC Q x y

RC_MOVES_OUT

⊢ ∀R. (SC (RC R) = RC (SC R)) ∧ (RC (RC R) = RC R) ∧ ((RC R)⁺ = RC R⁺)

RC_OR_Id

⊢ RC R = R ∪ᵣ $=

RC_REFL

⊢ RC R x x

RC_REFLEXIVE

⊢ ∀R. reflexive (RC R)

RC_RTC

⊢ ∀R x y. RC R x y ⇒ R꙳ x y

RC_STRORD

⊢ ∀R. WeakOrder R ⇒ (RC (STRORD R) = R)

RC_SUBSET

⊢ ∀R x y. R x y ⇒ RC R x y

RC_Weak

⊢ Order R ⇔ WeakOrder (RC R)

RC_lifts_equalities

⊢ (∀x y. R x y ⇒ (f x = f y)) ⇒ ∀x y. RC R x y ⇒ (f x = f y)

RC_lifts_invariants

⊢ (∀x y. P x ∧ R x y ⇒ P y) ⇒ ∀x y. P x ∧ RC R x y ⇒ P y

RC_lifts_monotonicities

⊢ (∀x y. R x y ⇒ R (f x) (f y)) ⇒ ∀x y. RC R x y ⇒ RC R (f x) (f y)

REMPTY_SUBSET

⊢ ∅ᵣ ⊆ᵣ R ∧ (R ⊆ᵣ ∅ᵣ ⇔ (R = ∅ᵣ))

RESTRICT_LEMMA

⊢ ∀f R y z. R y z ⇒ (RESTRICT f R z y = f y)

RINTER_ASSOC

⊢ R1 ∩ᵣ (R2 ∩ᵣ R3) = R1 ∩ᵣ R2 ∩ᵣ R3

RINTER_COMM

⊢ R1 ∩ᵣ R2 = R2 ∩ᵣ R1

RSUBSET_ANTISYM

⊢ ∀R1 R2. R1 ⊆ᵣ R2 ∧ R2 ⊆ᵣ R1 ⇒ (R1 = R2)

RSUBSET_WeakOrder

⊢ WeakOrder $RSUBSET

RSUBSET_antisymmetric

⊢ antisymmetric $RSUBSET

RTC_ALT_DEF

⊢ ∀R a b. R꙳ a b ⇔ ∀Q. Q b ∧ (∀x y. R x y ∧ Q y ⇒ Q x) ⇒ Q a

RTC_ALT_INDUCT

⊢ ∀R Q b. Q b ∧ (∀x y. R x y ∧ Q y ⇒ Q x) ⇒ ∀x. R꙳ x b ⇒ Q x

RTC_ALT_RIGHT_DEF

⊢ ∀R a b. R꙳ a b ⇔ ∀Q. Q a ∧ (∀y z. Q y ∧ R y z ⇒ Q z) ⇒ Q b

RTC_ALT_RIGHT_INDUCT

⊢ ∀R Q a. Q a ∧ (∀y z. Q y ∧ R y z ⇒ Q z) ⇒ ∀z. R꙳ a z ⇒ Q z

RTC_CASES1

⊢ ∀R x y. R꙳ x y ⇔ (x = y) ∨ ∃u. R x u ∧ R꙳ u y

RTC_CASES2

⊢ ∀R x y. R꙳ x y ⇔ (x = y) ∨ ∃u. R꙳ x u ∧ R u y

RTC_CASES_RTC_TWICE

⊢ ∀R x y. R꙳ x y ⇔ ∃u. R꙳ x u ∧ R꙳ u y

RTC_CASES_TC

⊢ ∀R x y. R꙳ x y ⇔ (x = y) ∨ R⁺ x y

RTC_EQC

⊢ ∀x y. R꙳ x y ⇒ R^= x y

RTC_IDEM

⊢ ∀R. R꙳ ꙳ = R꙳

RTC_INDUCT

⊢ ∀R P. (∀x. P x x) ∧ (∀x y z. R x y ∧ P y z ⇒ P x z) ⇒ ∀x y. R꙳ x y ⇒ P x y

RTC_INDUCT_RIGHT1

⊢ ∀R P. (∀x. P x x) ∧ (∀x y z. P x y ∧ R y z ⇒ P x z) ⇒ ∀x y. R꙳ x y ⇒ P x y

RTC_MONOTONE

⊢ (∀x y. R x y ⇒ Q x y) ⇒ R꙳ x y ⇒ Q꙳ x y

RTC_REFL

⊢ R꙳ x x

RTC_REFLEXIVE

⊢ ∀R. reflexive R꙳

RTC_RINTER

⊢ ∀R1 R2 x y. (R1 ∩ᵣ R2)꙳ x y ⇒ (R1꙳ ∩ᵣ R2꙳) x y

RTC_RTC

⊢ ∀R x y. R꙳ x y ⇒ ∀z. R꙳ y z ⇒ R꙳ x z

RTC_RULES

⊢ ∀R. (∀x. R꙳ x x) ∧ ∀x y z. R x y ∧ R꙳ y z ⇒ R꙳ x z

RTC_RULES_RIGHT1

⊢ ∀R. (∀x. R꙳ x x) ∧ ∀x y z. R꙳ x y ∧ R y z ⇒ R꙳ x z

RTC_SINGLE

⊢ ∀R x y. R x y ⇒ R꙳ x y

RTC_STRONG_INDUCT

⊢ ∀R P.
    (∀x. P x x) ∧ (∀x y z. R x y ∧ R꙳ y z ∧ P y z ⇒ P x z) ⇒
    ∀x y. R꙳ x y ⇒ P x y

RTC_STRONG_INDUCT_RIGHT1

⊢ ∀R P.
    (∀x. P x x) ∧ (∀x y z. P x y ∧ R꙳ x y ∧ R y z ⇒ P x z) ⇒
    ∀x y. R꙳ x y ⇒ P x y

RTC_SUBSET

⊢ ∀R x y. R x y ⇒ R꙳ x y

RTC_TC_RC

⊢ ∀R x y. R꙳ x y ⇒ RC R x y ∨ R⁺ x y

RTC_TRANSITIVE

⊢ ∀R. transitive R꙳

RTC_cases

⊢ ∀R a0 a1. R꙳ a0 a1 ⇔ (a1 = a0) ∨ ∃y. R a0 y ∧ R꙳ y a1

RTC_ind

⊢ ∀R RTC'.
    (∀x. RTC' x x) ∧ (∀x y z. R x y ∧ RTC' y z ⇒ RTC' x z) ⇒
    ∀a0 a1. R꙳ a0 a1 ⇒ RTC' a0 a1

RTC_lifts_equalities

⊢ (∀x y. R x y ⇒ (f x = f y)) ⇒ ∀x y. R꙳ x y ⇒ (f x = f y)

RTC_lifts_invariants

⊢ (∀x y. P x ∧ R x y ⇒ P y) ⇒ ∀x y. P x ∧ R꙳ x y ⇒ P y

RTC_lifts_monotonicities

⊢ (∀x y. R x y ⇒ R (f x) (f y)) ⇒ ∀x y. R꙳ x y ⇒ R꙳ (f x) (f y)

RTC_lifts_reflexive_transitive_relations

⊢ (∀x y. R x y ⇒ Q (f x) (f y)) ∧ reflexive Q ∧ transitive Q ⇒
  ∀x y. R꙳ x y ⇒ Q (f x) (f y)

RTC_rules

⊢ ∀R. (∀x. R꙳ x x) ∧ ∀x y z. R x y ∧ R꙳ y z ⇒ R꙳ x z

RTC_strongind

⊢ ∀R RTC'.
    (∀x. RTC' x x) ∧ (∀x y z. R x y ∧ R꙳ y z ∧ RTC' y z ⇒ RTC' x z) ⇒
    ∀a0 a1. R꙳ a0 a1 ⇒ RTC' a0 a1

RUNION_ASSOC

⊢ R1 ∪ᵣ (R2 ∪ᵣ R3) = R1 ∪ᵣ R2 ∪ᵣ R3

RUNION_COMM

⊢ R1 ∪ᵣ R2 = R2 ∪ᵣ R1

RUNIV_SUBSET

⊢ (𝕌ᵣ ⊆ᵣ R ⇔ (R = 𝕌ᵣ)) ∧ R ⊆ᵣ 𝕌ᵣ

SC_IDEM

⊢ ∀R. SC (SC R) = SC R

SC_MONOTONE

⊢ (∀x y. R x y ⇒ Q x y) ⇒ SC R x y ⇒ SC Q x y

SC_SYMMETRIC

⊢ ∀R. symmetric (SC R)

SC_lifts_equalities

⊢ (∀x y. R x y ⇒ (f x = f y)) ⇒ ∀x y. SC R x y ⇒ (f x = f y)

SC_lifts_monotonicities

⊢ (∀x y. R x y ⇒ R (f x) (f y)) ⇒ ∀x y. SC R x y ⇒ SC R (f x) (f y)

STRONG_EQC_INDUCTION

⊢ ∀R P.
    (∀x y. R x y ⇒ P x y) ∧ (∀x. P x x) ∧ (∀x y. R^= x y ∧ P x y ⇒ P y x) ∧
    (∀x y z. P x y ∧ P y z ∧ R^= x y ∧ R^= y z ⇒ P x z) ⇒
    ∀x y. R^= x y ⇒ P x y

STRORD_AND_NOT_Id

⊢ STRORD R = R ∩ᵣ RCOMPL $=

STRORD_RC

⊢ ∀R. StrongOrder R ⇒ (STRORD (RC R) = R)

STRORD_Strong

⊢ ∀R. Order R ⇔ StrongOrder (STRORD R)

StrongOrd_Ord

⊢ ∀R. StrongOrder R ⇒ Order R

TC_CASES1

⊢ R⁺ x z ⇔ R x z ∨ ∃y. R x y ∧ R⁺ y z

TC_CASES1_E

⊢ ∀R x z. R⁺ x z ⇒ R x z ∨ ∃y. R x y ∧ R⁺ y z

TC_CASES2

⊢ R⁺ x z ⇔ R x z ∨ ∃y. R⁺ x y ∧ R y z

TC_CASES2_E

⊢ ∀R x z. R⁺ x z ⇒ R x z ∨ ∃y. R⁺ x y ∧ R y z

TC_IDEM

⊢ ∀R. R⁺ ⁺ = R⁺

TC_INDUCT

⊢ ∀R P.
    (∀x y. R x y ⇒ P x y) ∧ (∀x y z. P x y ∧ P y z ⇒ P x z) ⇒
    ∀u v. R⁺ u v ⇒ P u v

TC_INDUCT_ALT_LEFT

⊢ ∀R Q. (∀x. R x b ⇒ Q x) ∧ (∀x y. R x y ∧ Q y ⇒ Q x) ⇒ ∀a. R⁺ a b ⇒ Q a

TC_INDUCT_ALT_RIGHT

⊢ ∀R Q. (∀y. R a y ⇒ Q y) ∧ (∀x y. Q x ∧ R x y ⇒ Q y) ⇒ ∀b. R⁺ a b ⇒ Q b

TC_INDUCT_LEFT1

⊢ ∀R P.
    (∀x y. R x y ⇒ P x y) ∧ (∀x y z. R x y ∧ P y z ⇒ P x z) ⇒
    ∀x y. R⁺ x y ⇒ P x y

TC_INDUCT_RIGHT1

⊢ ∀R P.
    (∀x y. R x y ⇒ P x y) ∧ (∀x y z. P x y ∧ R y z ⇒ P x z) ⇒
    ∀x y. R⁺ x y ⇒ P x y

TC_MONOTONE

⊢ (∀x y. R x y ⇒ Q x y) ⇒ R⁺ x y ⇒ Q⁺ x y

TC_RC_EQNS

⊢ ∀R. (RC R⁺ = R꙳) ∧ ((RC R)⁺ = R꙳)

TC_RTC

⊢ ∀R x y. R⁺ x y ⇒ R꙳ x y

TC_RULES

⊢ ∀R. (∀x y. R x y ⇒ R⁺ x y) ∧ ∀x y z. R⁺ x y ∧ R⁺ y z ⇒ R⁺ x z

TC_STRONG_INDUCT

⊢ ∀R P.
    (∀x y. R x y ⇒ P x y) ∧ (∀x y z. P x y ∧ P y z ∧ R⁺ x y ∧ R⁺ y z ⇒ P x z) ⇒
    ∀u v. R⁺ u v ⇒ P u v

TC_STRONG_INDUCT_LEFT1

⊢ ∀R P.
    (∀x y. R x y ⇒ P x y) ∧ (∀x y z. R x y ∧ P y z ∧ R⁺ y z ⇒ P x z) ⇒
    ∀u v. R⁺ u v ⇒ P u v

TC_STRONG_INDUCT_RIGHT1

⊢ ∀R P.
    (∀x y. R x y ⇒ P x y) ∧ (∀x y z. P x y ∧ R⁺ x y ∧ R y z ⇒ P x z) ⇒
    ∀u v. R⁺ u v ⇒ P u v

TC_SUBSET

⊢ ∀R x y. R x y ⇒ R⁺ x y

TC_TRANSITIVE

⊢ ∀R. transitive R⁺

TC_implies_one_step

⊢ ∀x y. R⁺ x y ∧ x ≠ y ⇒ ∃z. R x z ∧ x ≠ z

TC_lifts_equalities

⊢ (∀x y. R x y ⇒ (f x = f y)) ⇒ ∀x y. R⁺ x y ⇒ (f x = f y)

TC_lifts_invariants

⊢ (∀x y. P x ∧ R x y ⇒ P y) ⇒ ∀x y. P x ∧ R⁺ x y ⇒ P y

TC_lifts_monotonicities

⊢ (∀x y. R x y ⇒ R (f x) (f y)) ⇒ ∀x y. R⁺ x y ⇒ R⁺ (f x) (f y)

TC_lifts_transitive_relations

⊢ (∀x y. R x y ⇒ Q (f x) (f y)) ∧ transitive Q ⇒ ∀x y. R⁺ x y ⇒ Q (f x) (f y)

TFL_INDUCTIVE_INVARIANT_ON_WFREC

⊢ ∀f R D P M x.
    (f = WFREC R M) ∧ WF R ∧ INDUCTIVE_INVARIANT_ON R D P M ∧ D x ⇒ P x (f x)

TFL_INDUCTIVE_INVARIANT_WFREC

⊢ ∀f R P M x. (f = WFREC R M) ∧ WF R ∧ INDUCTIVE_INVARIANT R P M ⇒ P x (f x)

WFP_CASES

⊢ ∀R x. WFP R x ⇔ ∀y. R y x ⇒ WFP R y

WFP_INDUCT

⊢ ∀R P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. WFP R x ⇒ P x

WFP_RULES

⊢ ∀R x. (∀y. R y x ⇒ WFP R y) ⇒ WFP R x

WFP_STRONG_INDUCT

⊢ ∀R. (∀x. WFP R x ∧ (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. WFP R x ⇒ P x

WFREC_COROLLARY

⊢ ∀M R f. (f = WFREC R M) ⇒ WF R ⇒ ∀x. f x = M (RESTRICT f R x) x

WFREC_THM

⊢ ∀R M. WF R ⇒ ∀x. WFREC R M x = M (RESTRICT (WFREC R M) R x) x

WF_EMPTY_REL

⊢ WF ∅ᵣ

WF_EQ_INDUCTION_THM

⊢ ∀R. WF R ⇔ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x

WF_EQ_WFP

⊢ ∀R. WF R ⇔ ∀x. WFP R x

WF_INDUCTION_THM

⊢ ∀R. WF R ⇒ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x

WF_NOT_REFL

⊢ ∀R x y. WF R ⇒ R x y ⇒ x ≠ y

WF_RECURSION_THM

⊢ ∀R. WF R ⇒ ∀M. ∃!f. ∀x. f x = M (RESTRICT f R x) x

WF_SUBSET

⊢ ∀R P. WF R ∧ (∀x y. P x y ⇒ R x y) ⇒ WF P

WF_TC

⊢ ∀R. WF R ⇒ WF R⁺

WF_TC_EQN

⊢ WF R⁺ ⇔ WF R

WF_antisymmetric

⊢ WF R ⇒ antisymmetric R

WF_inv_image

⊢ ∀R f. WF R ⇒ WF (inv_image R f)

WF_irreflexive

⊢ WF R ⇒ irreflexive R

WF_noloops

⊢ WF R ⇒ R⁺ x y ⇒ x ≠ y

WeakLinearOrder_dichotomy

⊢ ∀R. WeakLinearOrder R ⇔ WeakOrder R ∧ ∀a b. R a b ∨ R b a

WeakOrd_Ord

⊢ ∀R. WeakOrder R ⇒ Order R

WeakOrder_EQ

⊢ ∀R. WeakOrder R ⇒ ∀y z. (y = z) ⇔ R y z ∧ R z y

antisymmetric_RC

⊢ ∀R. antisymmetric (RC R) ⇔ antisymmetric R

antisymmetric_RINTER

⊢ (antisymmetric R1 ⇒ antisymmetric (R1 ∩ᵣ R2)) ∧
  (antisymmetric R2 ⇒ antisymmetric (R1 ∩ᵣ R2))

antisymmetric_inv

⊢ ∀R. antisymmetric Rᵀ ⇔ antisymmetric R

diamond_RC_diamond

⊢ ∀R. diamond R ⇒ diamond (RC R)

diamond_TC_diamond

⊢ ∀R. diamond R ⇒ diamond R⁺

equivalence_inv_identity

⊢ ∀R. equivalence R ⇒ (Rᵀ = R)

establish_CR

⊢ ∀R. (rcdiamond R ⇒ CR R) ∧ (diamond R ⇒ CR R)

inv_EQC

⊢ ∀R. (R^= ᵀ = R^=) ∧ (Rᵀ ^= = R^=)

inv_INVOL

⊢ INVOL relinv

inv_Id

⊢ $= ᵀ = $=

inv_MOVES_OUT

⊢ ∀R. (Rᵀ ᵀ = R) ∧ (SC Rᵀ = SC R) ∧ (RC Rᵀ = (RC R)ᵀ) ∧ (Rᵀ ⁺ = R⁺ ᵀ) ∧
      (Rᵀ ꙳ = R꙳ ᵀ) ∧ (Rᵀ ^= = R^=)

inv_O

⊢ ∀R R'. (R ∘ᵣ R')ᵀ = R'ᵀ ∘ᵣ Rᵀ

inv_RC

⊢ ∀R. (RC R)ᵀ = RC Rᵀ

inv_SC

⊢ ∀R. ((SC R)ᵀ = SC R) ∧ (SC Rᵀ = SC R)

inv_TC

⊢ ∀R. R⁺ ᵀ = Rᵀ ⁺

inv_diag

⊢ (diag A)ᵀ = diag A

inv_image_thm

⊢ ∀R f x y. inv_image R f x y ⇔ R (f x) (f y)

inv_inv

⊢ ∀R. Rᵀ ᵀ = R

irrefl_trans_implies_antisym

⊢ ∀R. irreflexive R ∧ transitive R ⇒ antisymmetric R

irreflexive_RSUBSET

⊢ ∀R1 R2. irreflexive R2 ∧ R1 ⊆ᵣ R2 ⇒ irreflexive R1

irreflexive_inv

⊢ ∀R. irreflexive Rᵀ ⇔ irreflexive R

rcdiamond_diamond

⊢ ∀R. rcdiamond R ⇔ diamond (RC R)

reflexive_EQC

⊢ reflexive R^=

reflexive_Id_RSUBSET

⊢ ∀R. reflexive R ⇔ $= ⊆ᵣ R

reflexive_RC

⊢ ∀R. reflexive (RC R)

reflexive_RC_identity

⊢ ∀R. reflexive R ⇒ (RC R = R)

reflexive_RTC

⊢ ∀R. reflexive R꙳

reflexive_TC

⊢ ∀R. reflexive R ⇒ reflexive R⁺

reflexive_inv

⊢ ∀R. reflexive Rᵀ ⇔ reflexive R

reflexive_inv_image

⊢ ∀R f. reflexive R ⇒ reflexive (inv_image R f)

symmetric_EQC

⊢ symmetric R^=

symmetric_RC

⊢ ∀R. symmetric (RC R) ⇔ symmetric R

symmetric_SC_identity

⊢ ∀R. symmetric R ⇒ (SC R = R)

symmetric_TC

⊢ ∀R. symmetric R ⇒ symmetric R⁺

symmetric_inv

⊢ ∀R. symmetric Rᵀ ⇔ symmetric R

symmetric_inv_RSUBSET

⊢ symmetric R ⇔ Rᵀ ⊆ᵣ R

symmetric_inv_identity

⊢ ∀R. symmetric R ⇒ (Rᵀ = R)

symmetric_inv_image

⊢ ∀R f. symmetric R ⇒ symmetric (inv_image R f)

total_inv_image

⊢ ∀R f. total R ⇒ total (inv_image R f)

transitive_EQC

⊢ transitive R^=

transitive_O_RSUBSET

⊢ transitive R ⇔ R ∘ᵣ R ⊆ᵣ R

transitive_RC

⊢ ∀R. transitive R ⇒ transitive (RC R)

transitive_RINTER

⊢ transitive R1 ∧ transitive R2 ⇒ transitive (R1 ∩ᵣ R2)

transitive_RTC

⊢ ∀R. transitive R꙳

transitive_TC_identity

⊢ ∀R. transitive R ⇒ (R⁺ = R)

transitive_inv

⊢ ∀R. transitive Rᵀ ⇔ transitive R

transitive_inv_image

⊢ ∀R f. transitive R ⇒ transitive (inv_image R f)

trichotomous_RC

⊢ trichotomous (RC R) ⇔ trichotomous R

trichotomous_STRORD

⊢ trichotomous (STRORD R) ⇔ trichotomous R