Theory "relation"

Signature

Definitions

transitive_def

|- ∀R. transitive R ⇔ ∀x y z. R x y ∧ R y z ⇒ R x z

reflexive_def

|- ∀R. reflexive R ⇔ ∀x. R x x

irreflexive_def

|- ∀R. irreflexive R ⇔ ∀x. ¬R x x

symmetric_def

|- ∀R. symmetric R ⇔ ∀x y. R x y ⇔ R y x

antisymmetric_def

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

equivalence_def

|- ∀R. equivalence R ⇔ reflexive R ∧ symmetric R ∧ transitive R

total_def

|- ∀R. total R ⇔ ∀x y. R x y ∨ R y x

trichotomous

|- ∀R. trichotomous R ⇔ ∀a b. R a b ∨ R b a ∨ (a = b)

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

RTC_DEF

|- ∀R a b. R^* a b ⇔ ∀P. (∀x. P x x) ∧ (∀x y z. R x y ∧ P y z ⇒ P x z) ⇒ P a b

RC_DEF

|- ∀R x y. RC R x y ⇔ (x = y) ∨ R x y

SC_DEF

|- ∀R x y. SC R x y ⇔ R x y ∨ R y x

EQC_DEF

|- ∀R. R^= = RC (SC R)⁺

WF_DEF

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

EMPTY_REL_DEF

|- ∀x y. REMPTY x y ⇔ F

inv_image_def

|- ∀R f. inv_image R f = (λx y. R (f x) (f y))

RESTRICT_DEF

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

approx_def

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

the_fun_def

|- ∀R M x. the_fun R M x = @f. approx R M x f

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)

WFP_DEF

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

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)

inv_DEF

|- ∀R x y. inv R x y ⇔ R y x

INVOL_DEF

|- ∀f. INVOL f ⇔ (f o f = I)

IDEM_DEF

|- ∀f. IDEM f ⇔ (f o f = f)

O_DEF

|- ∀R1 R2 x z. (R1 O R2) x z ⇔ ∃y. R2 x y ∧ R1 y z

RSUBSET

|- ∀R1 R2. R1 RSUBSET R2 ⇔ ∀x y. R1 x y ⇒ R2 x y

RUNION

|- ∀R1 R2 x y. (R1 RUNION R2) x y ⇔ R1 x y ∨ R2 x y

RINTER

|- ∀R1 R2 x y. (R1 RINTER R2) x y ⇔ R1 x y ∧ R2 x y

RCOMPL

|- ∀R x y. RCOMPL R x y ⇔ ¬R x y

PreOrder

|- ∀R. PreOrder R ⇔ reflexive R ∧ transitive R

Order

|- ∀Z. Order Z ⇔ antisymmetric Z ∧ transitive Z

WeakOrder

|- ∀Z. WeakOrder Z ⇔ reflexive Z ∧ antisymmetric Z ∧ transitive Z

StrongOrder

|- ∀Z. StrongOrder Z ⇔ irreflexive Z ∧ transitive Z

STRORD

|- ∀R a b. STRORD R a b ⇔ R a b ∧ a ≠ b

LinearOrder

|- ∀R. LinearOrder R ⇔ Order R ∧ trichotomous R

StrongLinearOrder

|- ∀R. StrongLinearOrder R ⇔ StrongOrder R ∧ trichotomous R

WeakLinearOrder

|- ∀R. WeakLinearOrder R ⇔ WeakOrder R ∧ trichotomous R

diag_def

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

RDOM_DEF

|- ∀R x. RDOM R x ⇔ ∃y. R x y

RRANGE

|- ∀R y. RRANGE R y ⇔ ∃x. R x y

RUNIV

|- ∀x y. RUNIV x y ⇔ T

RRESTRICT_DEF

|- ∀R s x y. RRESTRICT R s x y ⇔ R x y ∧ x ∈ s

RDOM_DELETE_DEF

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

diamond_def

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

rcdiamond_def

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

CR_def

|- ∀R. CR R ⇔ diamond R^*

WCR_def

|- ∀R. WCR R ⇔ ∀x y z. R x y ∧ R x z ⇒ ∃u. R^* y u ∧ R^* z u

SN_def

|- ∀R. SN R ⇔ WF (inv R)

nf_def

|- ∀R x. nf R x ⇔ ∀y. ¬R x y

Theorems

SC_SYMMETRIC

|- ∀R. symmetric (SC R)

TC_TRANSITIVE

|- ∀R. transitive 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

TC_RULES

|- ∀R. (∀x y. R x y ⇒ R⁺ x y) ∧ ∀x y z. R⁺ x y ∧ 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_REFL

|- R^* x x

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_RTC

|- ∀R x y. R^* x y ⇒ ∀z. R^* y z ⇒ R^* x z

RTC_TRANSITIVE

|- ∀R. transitive R^*

transitive_RTC

|- ∀R. transitive R^*

RTC_REFLEXIVE

|- ∀R. reflexive R^*

reflexive_RTC

|- ∀R. reflexive R^*

RC_REFLEXIVE

|- ∀R. reflexive (RC R)

reflexive_RC

|- ∀R. reflexive (RC R)

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)

RC_MONOTONE

|- (∀x y. R x y ⇒ Q x y) ⇒ RC R x y ⇒ RC Q x 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_equalities

|- (∀x y. R x y ⇒ (f x = f y)) ⇒ ∀x y. RC 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)

SC_lifts_equalities

|- (∀x y. R x y ⇒ (f x = f y)) ⇒ ∀x y. SC R x y ⇒ (f x = f y)

SC_MONOTONE

|- (∀x y. R x y ⇒ Q x y) ⇒ SC R x y ⇒ SC Q x y

symmetric_RC

|- ∀R. symmetric (RC R) ⇔ symmetric R

antisymmetric_RC

|- ∀R. antisymmetric (RC R) ⇔ antisymmetric R

transitive_RC

|- ∀R. transitive R ⇒ transitive (RC R)

TC_SUBSET

|- ∀R x y. R x y ⇒ R⁺ x y

RTC_SUBSET

|- ∀R x y. R x y ⇒ R^* x y

RC_SUBSET

|- ∀R x y. R x y ⇒ RC R x y

RC_RTC

|- ∀R x y. RC R x y ⇒ R^* x y

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_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_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_lifts_monotonicities

|- (∀x y. R x y ⇒ R (f x) (f y)) ⇒ ∀x y. R⁺ x y ⇒ R⁺ (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_equalities

|- (∀x y. R x y ⇒ (f x = f y)) ⇒ ∀x y. R⁺ x y ⇒ (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)

TC_implies_one_step

|- ∀x y. R⁺ x y ∧ x ≠ y ⇒ ∃z. R x z ∧ x ≠ z

TC_RTC

|- ∀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

TC_RC_EQNS

|- ∀R. (RC R⁺ = R^* ) ∧ ((RC R)⁺ = R^* )

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_RULES_RIGHT1

|- ∀R. (∀x. R^* x x) ∧ ∀x y z. R^* x y ∧ R y z ⇒ R^* x z

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

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

reflexive_RC_identity

|- ∀R. reflexive R ⇒ (RC R = R)

symmetric_SC_identity

|- ∀R. symmetric R ⇒ (SC R = R)

transitive_TC_identity

|- ∀R. transitive R ⇒ (R⁺ = R)

RC_IDEM

|- ∀R. RC (RC R) = RC R

SC_IDEM

|- ∀R. SC (SC R) = SC R

TC_IDEM

|- ∀R. R⁺ ⁺ = R⁺

RC_MOVES_OUT

|- ∀R. (SC (RC R) = RC (SC R)) ∧ (RC (RC R) = RC R) ∧ ((RC R)⁺ = RC R⁺)

symmetric_TC

|- ∀R. symmetric R ⇒ symmetric R⁺

reflexive_TC

|- ∀R. reflexive R ⇒ reflexive R⁺

EQC_EQUIVALENCE

|- ∀R. equivalence R^=

EQC_IDEM

|- ∀R. R^= ^= = R^=

RTC_IDEM

|- ∀R. R^* ^* = R^*

RTC_CASES1

|- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R x u ∧ R^* u y

RTC_CASES_TC

|- ∀R x y. R^* x y ⇔ (x = y) ∨ R⁺ x 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

TC_CASES1_E

|- ∀R x z. R⁺ x z ⇒ R x z ∨ ∃y. R x y ∧ R⁺ y z

TC_CASES1

|- 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_CASES2

|- R⁺ x z ⇔ R x z ∨ ∃y. R⁺ x y ∧ R y z

TC_MONOTONE

|- (∀x y. R x y ⇒ Q x y) ⇒ R⁺ x y ⇒ Q⁺ x y

RTC_MONOTONE

|- (∀x y. R x y ⇒ Q x y) ⇒ R^* x y ⇒ Q^* x y

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_REFL

|- ∀R x. R^= x x

EQC_R

|- ∀R x y. R x y ⇒ R^= x y

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

transitive_EQC

|- transitive R^=

symmetric_EQC

|- symmetric R^=

reflexive_EQC

|- reflexive R^=

EQC_MOVES_IN

|- ∀R. ((RC R)^= = R^=) ∧ ((SC R)^= = R^=) ∧ (R⁺ ^= = R^=)

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

ALT_equivalence

|- ∀R. equivalence R ⇔ ∀x y. R x y ⇔ (R x = R y)

EQC_MONOTONE

|- (∀x y. R x y ⇒ R' x y) ⇒ R^= x y ⇒ R'^= x y

RTC_EQC

|- ∀x y. R^* x y ⇒ R^= x 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_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

WF_INDUCTION_THM

|- ∀R. WF R ⇒ ∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x

INDUCTION_WF_THM

|- ∀R. (∀P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. P x) ⇒ WF R

WF_EQ_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_irreflexive

|- WF R ⇒ irreflexive R

WF_EMPTY_REL

|- WF REMPTY

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_noloops

|- WF R ⇒ R⁺ x y ⇒ x ≠ y

WF_antisymmetric

|- WF R ⇒ antisymmetric R

inv_image_thm

|- ∀R f x y. inv_image R f x y ⇔ R (f x) (f y)

WF_inv_image

|- ∀R f. WF R ⇒ WF (inv_image R f)

total_inv_image

|- ∀R f. total R ⇒ total (inv_image R f)

reflexive_inv_image

|- ∀R f. reflexive R ⇒ reflexive (inv_image R f)

symmetric_inv_image

|- ∀R f. symmetric R ⇒ symmetric (inv_image R f)

transitive_inv_image

|- ∀R f. transitive R ⇒ transitive (inv_image R f)

RESTRICT_LEMMA

|- ∀f R y z. R y z ⇒ (RESTRICT f R z y = f y)

WFREC_THM

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

WFREC_COROLLARY

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

WF_RECURSION_THM

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

WFP_RULES

|- ∀R x. (∀y. R y x ⇒ WFP R y) ⇒ WFP R x

WFP_INDUCT

|- ∀R P. (∀x. (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. WFP R x ⇒ P x

WFP_CASES

|- ∀R x. WFP R x ⇔ ∀y. R y x ⇒ WFP R y

WFP_STRONG_INDUCT

|- ∀R. (∀x. WFP R x ∧ (∀y. R y x ⇒ P y) ⇒ P x) ⇒ ∀x. WFP R x ⇒ P x

WF_EQ_WFP

|- ∀R. WF R ⇔ ∀x. WFP R x

INDUCTIVE_INVARIANT_WFREC

|- ∀R P M. WF R ∧ INDUCTIVE_INVARIANT R P M ⇒ ∀x. P x (WFREC R M 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)

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)

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)

inv_inv

|- ∀R. inv (inv R) = R

inv_RC

|- ∀R. inv (RC R) = RC (inv R)

inv_SC

|- ∀R. (inv (SC R) = SC R) ∧ (SC (inv R) = SC R)

inv_TC

|- ∀R. inv R⁺ = (inv R)⁺

inv_EQC

|- ∀R. (inv R^= = R^=) ∧ ((inv R)^= = R^=)

inv_MOVES_OUT

|- ∀R.
     (inv (inv R) = R) ∧ (SC (inv R) = SC R) ∧ (RC (inv R) = inv (RC R)) ∧
     ((inv R)⁺ = inv R⁺) ∧ ((inv R)^* = inv R^* ) ∧ ((inv R)^= = R^=)

reflexive_inv

|- ∀R. reflexive (inv R) ⇔ reflexive R

irreflexive_inv

|- ∀R. irreflexive (inv R) ⇔ irreflexive R

symmetric_inv

|- ∀R. symmetric (inv R) ⇔ symmetric R

antisymmetric_inv

|- ∀R. antisymmetric (inv R) ⇔ antisymmetric R

transitive_inv

|- ∀R. transitive (inv R) ⇔ transitive R

symmetric_inv_identity

|- ∀R. symmetric R ⇒ (inv R = R)

equivalence_inv_identity

|- ∀R. equivalence R ⇒ (inv R = R)

INVOL

|- ∀f. INVOL f ⇔ ∀x. f (f x) = x

INVOL_ONE_ONE

|- ∀f. INVOL f ⇒ ∀a b. (f a = f b) ⇔ (a = b)

INVOL_ONE_ENO

|- ∀f. INVOL f ⇒ ∀a b. (f a = b) ⇔ (a = f b)

NOT_INVOL

|- INVOL $~

IDEM

|- ∀f. IDEM f ⇔ ∀x. f (f x) = f x

inv_INVOL

|- INVOL inv

inv_O

|- ∀R R'. inv (R O R') = inv R' O inv R

irreflexive_RSUBSET

|- ∀R1 R2. irreflexive R2 ∧ R1 RSUBSET R2 ⇒ irreflexive R1

RUNION_COMM

|- R1 RUNION R2 = R2 RUNION R1

RUNION_ASSOC

|- R1 RUNION (R2 RUNION R3) = R1 RUNION R2 RUNION R3

RINTER_COMM

|- R1 RINTER R2 = R2 RINTER R1

RINTER_ASSOC

|- R1 RINTER (R2 RINTER R3) = R1 RINTER R2 RINTER R3

antisymmetric_RINTER

|- (antisymmetric R1 ⇒ antisymmetric (R1 RINTER R2)) ∧
   (antisymmetric R2 ⇒ antisymmetric (R1 RINTER R2))

transitive_RINTER

|- transitive R1 ∧ transitive R2 ⇒ transitive (R1 RINTER R2)

reflexive_Id_RSUBSET

|- ∀R. reflexive R ⇔ $= RSUBSET R

symmetric_inv_RSUBSET

|- symmetric R ⇔ inv R RSUBSET R

transitive_O_RSUBSET

|- transitive R ⇔ R O R RSUBSET R

irrefl_trans_implies_antisym

|- ∀R. irreflexive R ∧ transitive R ⇒ antisymmetric R

StrongOrd_Ord

|- ∀R. StrongOrder R ⇒ Order R

WeakOrd_Ord

|- ∀R. WeakOrder R ⇒ Order R

WeakOrder_EQ

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

RSUBSET_ANTISYM

|- ∀R1 R2. R1 RSUBSET R2 ∧ R2 RSUBSET R1 ⇒ (R1 = R2)

RSUBSET_antisymmetric

|- antisymmetric $RSUBSET

RSUBSET_WeakOrder

|- WeakOrder $RSUBSET

EqIsBothRSUBSET

|- ∀y z. (y = z) ⇔ y RSUBSET z ∧ z RSUBSET y

STRORD_AND_NOT_Id

|- STRORD R = R RINTER RCOMPL $=

RC_OR_Id

|- RC R = R RUNION $=

RC_Weak

|- Order R ⇔ WeakOrder (RC R)

STRORD_Strong

|- ∀R. Order R ⇔ StrongOrder (STRORD R)

STRORD_RC

|- ∀R. StrongOrder R ⇒ (STRORD (RC R) = R)

RC_STRORD

|- ∀R. WeakOrder R ⇒ (RC (STRORD R) = R)

IDEM_STRORD

|- IDEM STRORD

IDEM_RC

|- IDEM RC

IDEM_SC

|- IDEM SC

IDEM_TC

|- IDEM TC

IDEM_RTC

|- IDEM RTC

trichotomous_STRORD

|- trichotomous (STRORD R) ⇔ trichotomous R

trichotomous_RC

|- trichotomous (RC R) ⇔ trichotomous R

WeakLinearOrder_dichotomy

|- ∀R. WeakLinearOrder R ⇔ WeakOrder R ∧ ∀a b. R a b ∨ R b a

O_ASSOC

|- R1 O R2 O R3 = (R1 O R2) O R3

Id_O

|- $= O R = R

O_Id

|- R O $= = R

O_MONO

|- R1 RSUBSET R2 ∧ S1 RSUBSET S2 ⇒ R1 O S1 RSUBSET R2 O S2

inv_Id

|- inv $= = $=

inv_diag

|- inv (diag A) = diag A

IN_RDOM

|- x ∈ RDOM R ⇔ ∃y. R x y

IN_RRANGE

|- y ∈ RRANGE R ⇔ ∃x. R x y

IN_RDOM_RUNION

|- x ∈ RDOM (R1 RUNION R2) ⇔ x ∈ RDOM R1 ∨ x ∈ RDOM R2

RUNIV_SUBSET

|- (RUNIV RSUBSET R ⇔ (R = RUNIV)) ∧ R RSUBSET RUNIV

REMPTY_SUBSET

|- REMPTY RSUBSET R ∧ (R RSUBSET REMPTY ⇔ (R = REMPTY))

IN_RDOM_RRESTRICT

|- x ∈ RDOM (RRESTRICT R s) ⇔ x ∈ RDOM R ∧ x ∈ s

IN_RDOM_DELETE

|- x ∈ RDOM (R \\ k) ⇔ x ∈ RDOM R ∧ x ≠ k

rcdiamond_diamond

|- ∀R. rcdiamond R ⇔ diamond (RC R)

diamond_RC_diamond

|- ∀R. diamond R ⇒ diamond (RC R)

diamond_TC_diamond

|- ∀R. diamond R ⇒ diamond R⁺

establish_CR

|- ∀R. (rcdiamond R ⇒ CR R) ∧ (diamond R ⇒ CR R)

Newmans_lemma

|- ∀R. WCR R ∧ SN R ⇒ CR R