Theory set_relation

⊢ ∀R s. RREFL_EXP R s = R ∪ᵣ (λx y. x = y ∧ x ∉ s)

⊢ ∀s. RRUNIV s = (λx y. x ∈ s ∧ y ∈ s)

⊢ ∀r. acyclic r ⇔ ∀x. (x,x) ∉ tc r

⊢ ∀xss.
    all_choices xss =
    {IMAGE choice xss | choice | ∀xs. xs ∈ xss ⇒ choice xs ∈ xs}

⊢ ∀r. antisym r ⇔ ∀x y. (x,y) ∈ r ∧ (y,x) ∈ r ⇒ x = y

⊢ ∀s r. chain s r ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ (x,y) ∈ r ∨ (y,x) ∈ r

⊢ ∀r. domain r = {x | ∃y. (x,y) ∈ r}

⊢ ∀r. fchains r =
      {k |
       chain k r ∧ k ≠ ∅ ∧
       ∀C. chain C r ∧ C ⊆ k ∧ (upper_bounds C r DIFF C) ∩ k ≠ ∅ ⇒
           CHOICE (upper_bounds C r DIFF C) ∈
           minimal_elements ((upper_bounds C r DIFF C) ∩ k) r}

⊢ ∀r s. finite_prefixes r s ⇔ ∀e. e ∈ s ⇒ FINITE {e' | (e',e) ∈ r}

⊢ ∀r' s r.
    get_min r' (s,r) =
    (let
       mins = minimal_elements (minimal_elements s r) r'
     in
       if SING mins then SOME (CHOICE mins) else NONE)

⊢ ∀r s. irreflexive r s ⇔ ∀x. x ∈ s ⇒ (x,x) ∉ r

⊢ ∀r s.
    linear_order r s ⇔
    domain r ⊆ s ∧ range r ⊆ s ∧ transitive r ∧ antisym r ∧
    ∀x y. x ∈ s ∧ y ∈ s ⇒ (x,y) ∈ r ∨ (y,x) ∈ r

⊢ ∀xs r.
    maximal_elements xs r =
    {x | x ∈ xs ∧ ∀x'. x' ∈ xs ∧ (x,x') ∈ r ⇒ x = x'}

⊢ ∀xs r.
    minimal_elements xs r =
    {x | x ∈ xs ∧ ∀x'. x' ∈ xs ∧ (x',x) ∈ r ⇒ x = x'}

⊢ ∀f s. num_order f s = {(x,y) | x ∈ s ∧ y ∈ s ∧ f x ≤ f y}

⊢ ∀r s.
    partial_order r s ⇔
    domain r ⊆ s ∧ range r ⊆ s ∧ transitive r ∧ reflexive r s ∧ antisym r

⊢ ∀xs xss.
    per xs xss ⇔
    BIGUNION xss ⊆ xs ∧ ∅ ∉ xss ∧
    ∀xs1 xs2. xs1 ∈ xss ∧ xs2 ∈ xss ∧ xs1 ≠ xs2 ⇒ DISJOINT xs1 xs2

⊢ ∀xss xs. per_restrict xss xs = {xs' ∩ xs | xs' ∈ xss} DELETE ∅

⊢ ∀r. range r = {y | ∃x. (x,y) ∈ r}

⊢ ∀r1 r2. r1 OO r2 = {(x,y) | ∃z. (x,z) ∈ r1 ∧ (z,y) ∈ r2}

⊢ ∀r s. reflexive r s ⇔ ∀x. x ∈ s ⇒ (x,x) ∈ r

⊢ ∀R. rel_to_reln R = {(x,y) | R x y}

⊢ ∀r. reln_to_rel r = (λx y. (x,y) ∈ r)

⊢ ∀r s. rrestrict r s = {(x,y) | (x,y) ∈ r ∧ x ∈ s ∧ y ∈ s}

⊢ ∀r. strict r = {(x,y) | (x,y) ∈ r ∧ x ≠ y}

⊢ ∀r s.
    strict_linear_order r s ⇔
    domain r ⊆ s ∧ range r ⊆ s ∧ transitive r ∧ (∀x. (x,x) ∉ r) ∧
    ∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ⇒ (x,y) ∈ r ∨ (y,x) ∈ r

⊢ ∀r s. symmetric r s ⇔ ∀x y. x ∈ s ∧ y ∈ s ⇒ ((x,y) ∈ r ⇔ (y,x) ∈ r)

⊢ ∀r. transitive r ⇔ ∀x y z. (x,y) ∈ r ∧ (y,z) ∈ r ⇒ (x,z) ∈ r

⊢ ∀xs. univ_reln xs = {(x1,x2) | x1 ∈ xs ∧ x2 ∈ xs}

⊢ ∀s r. upper_bounds s r = {x | x ∈ range r ∧ ∀y. y ∈ s ⇒ (y,x) ∈ r}

⊢ x ∈ X ⇒ linear_order lo X ⇒ y ∈ minimal_elements X lo ⇒ (y,x) ∈ lo

⊢ REL_RESTRICT R 𝕌(:α) = R

⊢ R ⊆ᵣ RREFL_EXP R s

⊢ RREFL_EXP R 𝕌(:α) = R

⊢ ∀R1. StrongOrder R1 ⇒ ∃R2. R1 ⊆ᵣ R2 ∧ StrongLinearOrder R2

⊢ ∀r. WF (reln_to_rel r) ⇒ acyclic r

⊢ WF (reln_to_rel r) ⇒
  x ∈ s ⇒
  ∃y. y ∈ minimal_elements s r ∧ ((y,x) ∈ tc r ∨ y = x)

⊢ acyclic (IMAGE SWAP r) ⇔ acyclic r

⊢ FINITE s ∧ acyclic r ∧ domain r ⊆ s ∧ range r ⊆ s ⇒ WF (reln_to_rel r)

⊢ ∀rs.
    (∀r r'.
       r ∈ rs ∧ r' ∈ rs ∧ r ≠ r' ⇒
       DISJOINT (domain r ∪ range r) (domain r' ∪ range r')) ∧
    (∀r. r ∈ rs ⇒ acyclic r) ⇒
    acyclic (BIGUNION rs)

⊢ ∀r x. acyclic r ⇒ (x,x) ∉ r

⊢ acyclic r ⇔ irreflexive (reln_to_rel r)⁺

⊢ ∀r s. acyclic r ⇒ acyclic (rrestrict r s)

⊢ ∀r1 r2. acyclic r1 ∧ r2 ⊆ r1 ⇒ acyclic r2

⊢ ∀r1 r2. acyclic (r1 ∪ r2) ⇒ acyclic r1 ∧ acyclic r2

⊢ ∀r r'.
    DISJOINT (domain r ∪ range r) (domain r' ∪ range r') ∧ acyclic r ∧
    acyclic r' ⇒
    acyclic (r ∪ r')

⊢ ∀x s y. x ∈ all_choices s ∧ y ∈ x ⇒ ∃z. z ∈ s ∧ y ∈ z

⊢ antisym r ⇔ antisymmetric (reln_to_rel r)

⊢ antisym t ⇒ s ⊆ t ⇒ antisym s

⊢ ∀xs xss. countable xs ∧ per xs xss ⇒ countable xss

⊢ r ⊆ r' ⇒ domain r ⊆ domain r'

⊢ domain (rrestrict r s) ⊆ s

⊢ domain r = RDOM (reln_to_rel r)

⊢ ∀r. linear_order r ∅ ⇔ r = ∅

⊢ ∀r. strict_linear_order r ∅ ⇔ r = ∅

⊢ ∀r s x.
    x ∉ s ∧ linear_order r s ⇒
    linear_order (r ∪ {(y,x) | y | y ∈ s ∪ {x}}) (s ∪ {x})

⊢ ∀s. FINITE s ⇒ s ≠ ∅ ⇒ ∀r. acyclic r ⇒ ∃x. x ∈ maximal_elements s r

⊢ ∀s r x.
    FINITE s ∧ acyclic r ∧ x ∈ s ∧ x ∉ maximal_elements s r ⇒
    ∃y. y ∈ maximal_elements s r ∧ (x,y) ∈ tc r

⊢ ∀s. FINITE s ⇒ s ≠ ∅ ⇒ ∀r. acyclic r ⇒ ∃x. x ∈ minimal_elements s r

⊢ ∀s r x.
    FINITE s ∧ acyclic r ∧ x ∈ s ∧ x ∉ minimal_elements s r ⇒
    ∃y. y ∈ minimal_elements s r ∧ (y,x) ∈ tc r

⊢ ∀s r. FINITE s ∧ linear_order r s ∧ s ≠ ∅ ⇒ ∃x. x ∈ maximal_elements s r

⊢ ∀s r. FINITE s ∧ linear_order r s ∧ s ≠ ∅ ⇒ ∃x. x ∈ minimal_elements s r

⊢ ∀r s s'.
    linear_order r s ∧ finite_prefixes r s ∧ x ∈ s' ∧ s' ⊆ s ⇒
    SING (minimal_elements s' r)

⊢ ∀r s x s'.
    partial_order r s ∧ finite_prefixes r s ∧ x ∉ minimal_elements s' r ∧
    x ∈ s' ∧ s' ⊆ s ⇒
    ∃x'. x' ∈ minimal_elements s' r ∧ (x',x) ∈ r

⊢ ∀r1 r2 s1 s2.
    finite_prefixes r1 s1 ∧ finite_prefixes r2 s2 ∧
    {x | ∃y. y ∈ s2 ∧ (x,y) ∈ r2} ⊆ s1 ⇒
    finite_prefixes (r1 OO r2) s2

⊢ ∀f r s.
    (∀x y. f x = f y ⇒ x = y) ∧ finite_prefixes r s ⇒
    finite_prefixes {(f x,f y) | (x,y) ∈ r} (IMAGE f s)

⊢ ∀r s t.
    finite_prefixes r s ∧ DISJOINT t (range r) ⇒ finite_prefixes r (s ∪ t)

⊢ ∀r s s'.
    finite_prefixes r s ∧ s' ⊆ s ⇒
    finite_prefixes r s' ∧ finite_prefixes (rrestrict r s') s'

⊢ ∀r r' s. finite_prefixes r s ∧ r' ⊆ r ⇒ finite_prefixes r' s

⊢ ∀r s r' s'. finite_prefixes r s ⇒ r' ⊆ r ⇒ s' ⊆ s ⇒ finite_prefixes r' s'

⊢ ∀r s s'. finite_prefixes r s ∧ s' ⊆ s ⇒ finite_prefixes r s'

⊢ ∀r1 r2 s1 s2.
    finite_prefixes r1 s1 ∧ finite_prefixes r2 s2 ⇒
    finite_prefixes (r1 ∪ r2) (s1 ∩ s2)

⊢ ∀r. FINITE r ⇒ FINITE (sc r)

⊢ ∀s r.
    FINITE s ∧ strict_linear_order r s ∧ s ≠ ∅ ⇒
    ∃x. x ∈ maximal_elements s r

⊢ ∀s r.
    FINITE s ∧ strict_linear_order r s ∧ s ≠ ∅ ⇒
    ∃x. x ∈ minimal_elements s r

⊢ (x,y) ∈ r ⇒ x ∈ domain r ∧ y ∈ range r

⊢ ∀x r. x ∈ domain r ⇔ ∃y. (x,y) ∈ r

⊢ ∀y r. y ∈ range r ⇔ ∃x. (x,y) ∈ r

⊢ xy ∈ rel_to_reln R ⇔ R (FST xy) (SND xy)

⊢ ∀x y r s. (x,y) ∈ rrestrict r s ⇔ (x,y) ∈ r ∧ x ∈ s ∧ y ∈ s

⊢ x ∈ rrestrict r s ⇔ x ∈ r ∧ FST x ∈ s ∧ SND x ∈ s

⊢ irreflexive r s ⇔ irreflexive (REL_RESTRICT (reln_to_rel r) s)

⊢ irreflexive r 𝕌(:α) ⇔ irreflexive (reln_to_rel r)

⊢ ∀r1 r2 s. irreflexive r1 s ∧ irreflexive r2 s ⇒ irreflexive (r1 ∪ r2) s

⊢ ∀r s. strict_linear_order r s ⇒ linear_order (r ∪ {(x,x) | x ∈ s}) s

⊢ linear_order lo X ⇒ domain lo ∪ range lo = X

⊢ ∀r s x y. (x,y) ∈ r ∧ linear_order r s ⇒ x ∈ s ∧ y ∈ s

⊢ linear_order lo X ⇒ (x,y) ∈ lo ⇒ x ∈ X ∧ y ∈ X

⊢ ∀f s t. INJ f s t ⇒ linear_order (num_order f s) s

⊢ ∀r s.
    countable s ∧ partial_order r s ∧ finite_prefixes r s ⇒
    ∃r'. linear_order r' s ∧ finite_prefixes r' s ∧ r ⊆ r'

⊢ linear_order lo X ⇒ x ∈ X ⇒ (x,x) ∈ lo

⊢ linear_order r 𝕌(:α) ⇔ WeakLinearOrder (reln_to_rel r)

⊢ ∀s r s'. linear_order r s ⇒ linear_order (rrestrict r s') (s ∩ s')

⊢ ∀r s s'. linear_order r s ∧ s' ⊆ s ⇒ linear_order (rrestrict r s') s'

⊢ ∀s r.
    domain r ⊆ s ∧ range r ⊆ s ⇒
    maximal_elements s (tc r) = maximal_elements s r

⊢ ∀s r x y. y ∈ s ∧ linear_order r s ∧ x ∈ maximal_elements s r ⇒ (y,x) ∈ r

⊢ ∀e s r1 r2.
    e ∈ maximal_elements s (r1 ∪ r2) ⇒
    e ∈ maximal_elements s r1 ∧ e ∈ maximal_elements s r2

⊢ ∀s r.
    domain r ⊆ s ∧ range r ⊆ s ⇒
    minimal_elements s (tc r) = minimal_elements s r

⊢ minimal_elements xs (IMAGE SWAP r) = maximal_elements xs r

⊢ r ⊆ r' ⇒ minimal_elements xs r' ⊆ minimal_elements xs r

⊢ minimal_elements xs (rrestrict r xs) = minimal_elements xs r

⊢ minimal_elements s lo ⊆ s

⊢ ∀s r x y. y ∈ s ∧ linear_order r s ∧ x ∈ minimal_elements s r ⇒ (x,y) ∈ r

⊢ ∀r s s' x y.
    linear_order r s ∧ x ∈ minimal_elements s' r ∧
    y ∈ minimal_elements s' r ∧ s' ⊆ s ⇒
    x = y

⊢ ∀e s r1 r2.
    e ∈ minimal_elements s (r1 ∪ r2) ⇒
    e ∈ minimal_elements s r1 ∧ e ∈ minimal_elements s r2

⊢ ∀f s.
    (∀n m. f m = f n ∧ f m ≠ NONE ⇒ m = n) ∧
    (∀x. x ∈ s ⇒ ∃m. f m = SOME x) ∧ (∀m x. f m = SOME x ⇒ x ∈ s) ⇒
    linear_order {(x,y) | (∃m n. m ≤ n ∧ f m = SOME x ∧ f n = SOME y)} s ∧
    finite_prefixes {(x,y) | (∃m n. m ≤ n ∧ f m = SOME x ∧ f n = SOME y)} s

⊢ (∀s r' r. nth_min r' (s,r) 0 = get_min r' (s,r)) ∧
  (∀s r' r n.
     nth_min r' (s,r) <..num comp'n..> =
     (let
        min = get_min r' (s,r)
      in
        if min = NONE then NONE
        else nth_min r' (s DELETE THE min,r) (<..num comp'n..> − 1))) ∧
  ∀s r' r n.
    nth_min r' (s,r) <..num comp'n..> =
    (let
       min = get_min r' (s,r)
     in
       if min = NONE then NONE
       else nth_min r' (s DELETE THE min,r) <..num comp'n..> )

⊢ (∀s r' r. nth_min r' (s,r) 0 = get_min r' (s,r)) ∧
  ∀s r' r n.
    nth_min r' (s,r) (SUC n) =
    (let
       min = get_min r' (s,r)
     in
       if min = NONE then NONE else nth_min r' (s DELETE THE min,r) n)

⊢ ∀P. (∀r' s r. P r' (s,r) 0) ∧
      (∀r' s r n.
         (∀min.
            min = get_min r' (s,r) ∧ min ≠ NONE ⇒
            P r' (s DELETE THE min,r) n) ⇒
         P r' (s,r) (SUC n)) ⇒
      ∀v v1 v2 v3. P v (v1,v2) v3

⊢ ∀f s t. INJ f s t ⇒ finite_prefixes (num_order f s) s

⊢ ∀r s x y. (x,y) ∈ r ∧ partial_order r s ⇒ x ∈ s ∧ y ∈ s

⊢ ∀r s. linear_order r s ⇒ partial_order r s

⊢ partial_order r s ⇔
  reln_to_rel r ⊆ᵣ RRUNIV s ∧ WeakOrder (RREFL_EXP (reln_to_rel r) s)

⊢ partial_order r 𝕌(:α) ⇔ WeakOrder (reln_to_rel r)

⊢ ∀r s s'. partial_order r s ∧ s' ⊆ s ⇒ partial_order (rrestrict r s') s'

⊢ ∀xs xss e.
    per xs xss ⇒
    per (xs DELETE e) {es | es ∈ IMAGE (λes. es DELETE e) xss ∧ es ≠ ∅}

⊢ ∀r s s'. per s r ⇒ per s' (per_restrict r s')

⊢ r ⊆ r' ⇒ range r ⊆ range r'

⊢ range (rrestrict r s) ⊆ s

⊢ range r = RRANGE (reln_to_rel r)

⊢ r1 OO r2 = rel_to_reln (reln_to_rel r2 ∘ᵣ reln_to_rel r1)

⊢ reflexive r s ⇔ reflexive (RREFL_EXP (reln_to_rel r) s)

⊢ reflexive r 𝕌(:α) ⇔ reflexive (reln_to_rel r)

⊢ rel_to_reln R1 = rel_to_reln R2 ⇔ R1 = R2

⊢ rel_to_reln = UNCURRY

⊢ reln_to_rel (rel_to_reln R) = R

⊢ r = rel_to_reln R ⇔ reln_to_rel r = R

⊢ ((xy ∈ rel_to_reln R ⇔ R (FST xy) (SND xy)) ∧
   (reln_to_rel r x y ⇔ (x,y) ∈ r) ∧ reln_to_rel (rel_to_reln R) = R ∧
   rel_to_reln (reln_to_rel r) = r ∧
   (reln_to_rel r1 = reln_to_rel r2 ⇔ r1 = r2) ∧
   (rel_to_reln R1 = rel_to_reln R2 ⇔ R1 = R2)) ∧ RREFL_EXP R 𝕌(:α) = R ∧
  REL_RESTRICT R 𝕌(:α) = R ∧ domain r = RDOM (reln_to_rel r) ∧
  range r = RRANGE (reln_to_rel r) ∧
  strict r = rel_to_reln (STRORD (reln_to_rel r)) ∧
  rrestrict r s = rel_to_reln (REL_RESTRICT (reln_to_rel r) s) ∧
  r1 OO r2 = rel_to_reln (reln_to_rel r2 ∘ᵣ reln_to_rel r1) ∧
  univ_reln s = rel_to_reln (RRUNIV s) ∧
  tc r = rel_to_reln (reln_to_rel r)⁺ ∧
  (acyclic r ⇔ irreflexive (reln_to_rel r)⁺) ∧
  (irreflexive r s ⇔ irreflexive (REL_RESTRICT (reln_to_rel r) s)) ∧
  (reflexive r s ⇔ reflexive (RREFL_EXP (reln_to_rel r) s)) ∧
  (transitive r ⇔ transitive (reln_to_rel r)) ∧
  (antisym r ⇔ antisymmetric (reln_to_rel r)) ∧
  (partial_order r 𝕌(:α) ⇔ WeakOrder (reln_to_rel r)) ∧
  (linear_order r 𝕌(:α) ⇔ WeakLinearOrder (reln_to_rel r)) ∧
  (strict_linear_order r 𝕌(:α) ⇔ StrongLinearOrder (reln_to_rel r))

⊢ reln_to_rel r1 = reln_to_rel r2 ⇔ r1 = r2

⊢ reln_to_rel = CURRY

⊢ reln_to_rel r x y ⇔ (x,y) ∈ r

⊢ rel_to_reln (reln_to_rel r) = r

⊢ ∀s t. s = t ⇔ ∀x y. (x,y) ∈ s ⇔ (x,y) ∈ t

⊢ rrestrict r s ⊆ r

⊢ ∀r x y. rrestrict (rrestrict r x) y = rrestrict r (x ∩ y)

⊢ ∀e e'. (e,e') ∈ tc (rrestrict r x) ⇒ (e,e') ∈ tc r

⊢ rrestrict r s = rel_to_reln (REL_RESTRICT (reln_to_rel r) s)

⊢ ∀r1 r2 s. rrestrict (r1 ∪ r2) s = rrestrict r1 s ∪ rrestrict r2 s

⊢ ∀r tc'.
    (∀x. x ∈ domain r ∨ x ∈ range r ⇒ tc' x x) ∧
    (∀x y. (∃z. tc' x z ∧ (z,y) ∈ r) ⇒ tc' x y) ⇒
    ∀x y. (x,y) ∈ tc r ⇒ tc' x y

⊢ ∀r x y. (x,y) ∈ sc r ⇔ (x,y) ∈ r ∨ (y,x) ∈ sc r

⊢ ∀r. sc r = {(x,y) | (x,y) ∈ r ∨ (y,x) ∈ r}

⊢ sc ∅ = ∅

⊢ ∀r sc'.
    (∀x y. (x,y) ∈ r ⇒ sc' x y) ∧ (∀x y. sc' x y ⇒ sc' y x) ⇒
    ∀x y. (x,y) ∈ sc r ⇒ sc' x y

⊢ ∀r s. irreflexive r s ⇒ irreflexive (sc r) s

⊢ ∀r. (∀x y. (x,y) ∈ r ⇒ (x,y) ∈ sc r) ∧ ∀x y. (x,y) ∈ sc r ⇒ (y,x) ∈ sc r

⊢ ∀r sc'.
    (∀x y. (x,y) ∈ r ⇒ sc' x y) ∧ (∀x y. (x,y) ∈ sc r ∧ sc' x y ⇒ sc' y x) ⇒
    ∀x y. (x,y) ∈ sc r ⇒ sc' x y

⊢ ∀x y r. (x,y) ∈ sc r ⇔ (y,x) ∈ sc r

⊢ symmetric (sc r) s

⊢ ∀r s. linear_order r s ⇒ strict_linear_order (strict r) s

⊢ ∀r s. strict_linear_order r s ⇒ acyclic r

⊢ ∀r s x y. (x,y) ∈ r ∧ strict_linear_order r s ⇒ x ∈ s ∧ y ∈ s

⊢ strict_linear_order r 𝕌(:α) ⇔ StrongLinearOrder (reln_to_rel r)

⊢ ∀s r s'.
    strict_linear_order r s ⇒ strict_linear_order (rrestrict r s') (s ∩ s')

⊢ ∀r1 r2 s.
    strict_linear_order r1 s ∧ domain r2 ∪ range r2 ⊆ s ⇒
    (acyclic (r1 ∪ r2) ⇔ r2 ⊆ r1)

⊢ ∀r s.
    partial_order r s ⇒
    domain (strict r) ⊆ s ∧ range (strict r) ⊆ s ∧ transitive (strict r) ∧
    antisym (strict r)

⊢ ∀r s. partial_order r s ⇒ acyclic (strict r)

⊢ ∀r s. strict (rrestrict r s) = rrestrict (strict r) s

⊢ strict r = rel_to_reln (STRORD (reln_to_rel r))

⊢ r ⊆ tc r

⊢ ∀r1 r2 s. symmetric r1 s ∧ symmetric r2 s ⇒ symmetric (r1 ∪ r2) s

⊢ tc (IMAGE SWAP r) = IMAGE SWAP (tc r)

⊢ ∀r x y. (x,y) ∈ tc r ⇔ (x,y) ∈ r ∨ ∃z. (x,z) ∈ tc r ∧ (z,y) ∈ tc r

⊢ ∀r x y. (x,y) ∈ tc r ⇔ (x,y) ∈ r ∨ ∃z. (x,z) ∈ r ∧ (z,y) ∈ tc r

⊢ ∀r x y. (x,y) ∈ tc r ⇔ (x,y) ∈ r ∨ ∃z. (x,z) ∈ tc r ∧ (z,y) ∈ r

⊢ r ⊆ tc s ⇒ tc r ⊆ tc s

⊢ ∀x y. (x,y) ∈ tc r ⇒ x ∈ domain r ∧ y ∈ range r

⊢ ∀x y. (x,y) ∉ tc ∅

⊢ tc ∅ = ∅

⊢ tc (tc r) = tc r

⊢ ∀r1 r2.
    (∀x y. (x,y) ∈ r1 ⇒ (x,y) ∈ r2) ⇒ ∀x y. (x,y) ∈ tc r1 ⇒ (x,y) ∈ tc r2

⊢ ∀r tc'.
    (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧ (∀x y. (∃z. tc' x z ∧ tc' z y) ⇒ tc' x y) ⇒
    ∀x y. (x,y) ∈ tc r ⇒ tc' x y

⊢ ∀r tc'.
    (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
    (∀x y. (∃z. (x,z) ∈ r ∧ tc' z y) ⇒ tc' x y) ⇒
    ∀x y. (x,y) ∈ tc r ⇒ tc' x y

⊢ ∀r tc'.
    (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
    (∀x y. (∃z. tc' x z ∧ (z,y) ∈ r) ⇒ tc' x y) ⇒
    ∀x y. (x,y) ∈ tc r ⇒ tc' x y

⊢ r ⊆ s ⇒ tc r ⊆ tc s

⊢ ∀r. (∀x y. (x,y) ∈ r ⇒ (x,y) ∈ tc r) ∧
      ∀x y. (∃z. (x,z) ∈ tc r ∧ (z,y) ∈ tc r) ⇒ (x,y) ∈ tc r

⊢ ∀r tc'.
    (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
    (∀x y. (∃z. (x,z) ∈ tc r ∧ tc' x z ∧ (z,y) ∈ tc r ∧ tc' z y) ⇒ tc' x y) ⇒
    ∀x y. (x,y) ∈ tc r ⇒ tc' x y

⊢ ∀r tc'.
    (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
    (∀x y. (∃z. (x,z) ∈ r ∧ (z,y) ∈ tc r ∧ tc' z y) ⇒ tc' x y) ⇒
    ∀x y. (x,y) ∈ tc r ⇒ tc' x y

⊢ ∀r tc'.
    (∀x y. (x,y) ∈ r ⇒ tc' x y) ∧
    (∀x y. (∃z. (x,z) ∈ tc r ∧ tc' x z ∧ (z,y) ∈ r) ⇒ tc' x y) ⇒
    ∀x y. (x,y) ∈ tc r ⇒ tc' x y

⊢ tc r = rel_to_reln (reln_to_rel r)⁺

⊢ ∀r. transitive (tc r)

⊢ ∀x y. (x,y) ∈ tc r1 ⇒ ∀r2. (x,y) ∈ tc (r1 ∪ r2)

⊢ transitive r ⇔ transitive (reln_to_rel r)

⊢ ∀r. transitive r ⇒ tc r = r

⊢ univ_reln s = rel_to_reln (RRUNIV s)

⊢ ∀r s x1 x2.
    transitive r ∧ x1 ∈ upper_bounds s r ∧ (x1,x2) ∈ r ⇒
    x2 ∈ upper_bounds s r

⊢ ∀r s.
    s ≠ ∅ ∧ partial_order r s ∧ (∀t. chain t r ⇒ upper_bounds t r ≠ ∅) ⇒
    ∃x. x ∈ maximal_elements s r