HW17.2

CalcCheckWeb — Homework Notebook 17.2: Relations via Set Theory: Properties of Relations
Your latest 3 submissions:
salehh6__Hishmat+Salehi__2019-11-18_23:17:10.827571_EST.calcnb
salehh6__Hishmat+Salehi__2019-11-18_23:36:14.237315_EST.calcnb
salehh6__Hishmat+Salehi__2019-11-18_23:54:38.609777_EST.calcnb
[1]
Building on the relation operations and properties from Homeworks 15, 16, and 17.1, this notebook explores properties of relation.

Several proofs here require you to just replace “?₁” with a single hint item; in those cases you are not allowed to edit the proof in any other way.

[2]
Reflexivity
[3]
We define the reflexivity predicate for relations using the predicate-logic formulation:

[4]
Declaration: is-reflexive : A ↔ A  →  𝔹
Axiom “Definition of reflexivity”:  is-reflexive R  ≡  ∀ x • x ⦗ R ⦘ x

Declaration: is-reflexive : A ↔ A → 𝔹
Axiom “Definition of reflexivity”: is-reflexive R ≡ (∀ x • x ⦗ R ⦘ x )
— CalcCheck: Metavariables: R = R〖 〗
— CalcCheck: Proviso: ¬occurs(`x`, `R`)
[5]
Proving a goal of shape “is-reflexive R” using this axiom can just proceed via an equivalence calculation:

[6]
Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
    is-reflexive Id
  ≡⟨ “Definition of reflexivity” ⟩
    ∀ x • x ⦗ Id ⦘ x
  ≡⟨ Subproof:
        For any `x`:
            x ⦗ Id ⦘ x
          ≡⟨ “Identity relation” ⟩
            x = x  — This is 【 “Reflexivity of =” 】
    ⟩
    true

Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
        Proving    `is-reflexive Id`:
            is-reflexive Id
        ≡ ⟨ “Definition of reflexivity” ⟩
                — CalcCheck: Found “Definition of reflexivity”
                — CalcCheck: ─ OK
            (∀ x • x ⦗ Id ⦘ x )
        ≡ ⟨ Subproof for `(∀ x • x ⦗ Id ⦘ x )`:
            For any ` x`:
                    Proving    `x ⦗ Id ⦘ x`:
                        x ⦗ Id ⦘ x
                    ≡ ⟨ “Identity relation” ⟩
                            — CalcCheck: Found “Identity relation”
                            — CalcCheck: ─ OK
                        x = x     — This is 【 “Reflexivity of =” 】
                — CalcCheck: Final “This is”: OK (no change)
                — CalcCheck: Found (1.2) “Reflexivity of =”
                — CalcCheck: All steps OK
                — CalcCheck: Calculation matches goal ─ OK
            ⟩
                — CalcCheck: ─ OK
            true
    — CalcCheck: All steps OK
    — CalcCheck: Calculation matches goal ─ OK
[7]
This has the disadvantage that it produces after the first calculation step a universal quantification that, in the current setting, is most naturally approached via a “For any” proof either in a “Proof for this” construct or inside a Subproof hint which contains the whole remainder of the proof. In either case, that the initial calculation only really has one nice calculation step.

Such proofs can be presented more nicely via Using:

[8]
Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
  Using “Definition of reflexivity”:
    Subproof for `∀ x • x ⦗ Id ⦘ x`:
      For any `x`:
          x ⦗ Id ⦘ x
        ≡⟨ “Identity relation” ⟩
          x = x  — This is “Reflexivity of =”

Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
    Using “Definition of reflexivity”:
        Subproof for `(∀ x • x ⦗ Id ⦘ x )`:
            For any ` x`:
                    Proving    `x ⦗ Id ⦘ x`:
                        x ⦗ Id ⦘ x
                    ≡ ⟨ “Identity relation” ⟩
                            — CalcCheck: Found “Identity relation”
                            — CalcCheck: ─ OK
                        x = x     — This is “Reflexivity of =”
                — CalcCheck: Final “This is”: OK (no change)
                — CalcCheck: Found (1.2) “Reflexivity of =”
                — CalcCheck: All steps OK
                — CalcCheck: Calculation matches goal ─ OK
    — CalcCheck: Found “Definition of reflexivity”
[9]
Where the proof inside a Subproof is of a shape for which CalcCheck can infer the goal, the subproof goal (after “for”) can be omitted:

[10]
Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
  Using “Definition of reflexivity”:
    Subproof:
      For any `x`:
          x ⦗ Id ⦘ x
        ≡⟨ “Identity relation” ⟩
          x = x  — This is “Reflexivity of =”

Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
    Using “Definition of reflexivity”:
        Subproof for `(∀ x • x ⦗ Id ⦘ x )`:
            For any ` x`:
                    Proving    `x ⦗ Id ⦘ x`:
                        x ⦗ Id ⦘ x
                    ≡ ⟨ “Identity relation” ⟩
                            — CalcCheck: Found “Identity relation”
                            — CalcCheck: ─ OK
                        x = x     — This is “Reflexivity of =”
                — CalcCheck: Final “This is”: OK (no change)
                — CalcCheck: Found (1.2) “Reflexivity of =”
                — CalcCheck: All steps OK
                — CalcCheck: Calculation matches goal ─ OK
    — CalcCheck: Found “Definition of reflexivity”
[11]
And where a Using takes only one subproof, and that subproof does not need its goal explicit, the whole subproof line can be omitted:

[12]
Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
  Using “Definition of reflexivity”:
    For any `x`:
        x ⦗ Id ⦘ x
      ≡⟨ “Identity relation” ⟩
        x = x  — This is “Reflexivity of =”

Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
    Using “Definition of reflexivity”:
        Subproof for `(∀ x • x ⦗ Id ⦘ x )`:
            For any ` x`:
                    Proving    `x ⦗ Id ⦘ x`:
                        x ⦗ Id ⦘ x
                    ≡ ⟨ “Identity relation” ⟩
                            — CalcCheck: Found “Identity relation”
                            — CalcCheck: ─ OK
                        x = x     — This is “Reflexivity of =”
                — CalcCheck: Final “This is”: OK (no change)
                — CalcCheck: Found (1.2) “Reflexivity of =”
                — CalcCheck: All steps OK
                — CalcCheck: Calculation matches goal ─ OK
    — CalcCheck: Found “Definition of reflexivity”
[13]
However, remember that where an attempt to do such a proof does not succeed, you can always revert to the explicit calculation with the “For any” inside a Subproof!

And, when in doubt, always make subproof goals explicit.

[14]
Deriving the relation-algebraic formulation of reflexivity can be done in a straight-forward equivalence calculation — start from the right:

[15]
Theorem “Reflexivity”:  is-reflexive R  ≡  Id ⊆ R
Proof:
    Id ⊆ R
  ≡⟨ “Relation inclusion” ⟩
    ∀ x • ∀ y • x ⦗ Id ⦘ y ⇒ x ⦗ R ⦘ y
  ≡⟨ “Identity relation” ⟩
    ∀ x • ∀ y • x = y ⇒ x ⦗ R ⦘ y
  ≡⟨ “Trading for ∀” ⟩
    ∀ x • ∀ y ❙ x = y • x ⦗ R ⦘ y
  ≡⟨ “One-point rule for ∀” ⟩
    ∀ x • (x ⦗ R ⦘ y)[y ≔ x]
  ≡⟨ Substitution ⟩
    ∀ x • x ⦗ R ⦘ x
  ≡⟨ “Definition of reflexivity” ⟩
    is-reflexive R

Theorem “Reflexivity”: is-reflexive R ≡ Id ⊆ R
Proof:
        Proving    `is-reflexive R ≡ Id ⊆ R`:
            Id ⊆ R
        ≡ ⟨ “Relation inclusion” ⟩
                — CalcCheck: Found “Relation inclusion”, “Relation inclusion”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • x ⦗ Id ⦘ y ⇒ x ⦗ R ⦘ y ) )
        ≡ ⟨ “Identity relation” ⟩
                — CalcCheck: Found “Identity relation”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • x = y ⇒ x ⦗ R ⦘ y ) )
        ≡ ⟨ “Trading for ∀” ⟩
                — CalcCheck: Found (9.2) “Trading for ∀”, (9.3a) “Trading for ∀”, (9.3b) “Trading for ∀”, (9.3c) “Trading for ∀”, (9.4a) “Trading for ∀”, (9.4b) “Trading for ∀”, (9.4c) “Trading for ∀”, (9.4d) “Trading for ∀”
                — CalcCheck: ─ OK
            (∀ x • (∀ y ❙ x = y • x ⦗ R ⦘ y ) )
        ≡ ⟨ “One-point rule for ∀” ⟩
                — CalcCheck: Found (8.14) “One-point rule for ∀”
                — CalcCheck: ─ OK
            (∀ x • (x ⦗ R ⦘ y)[y ≔ x] )
        ≡ ⟨ Substitution ⟩
                — CalcCheck: ─ OK
            (∀ x • x ⦗ R ⦘ x )
        ≡ ⟨ “Definition of reflexivity” ⟩
                — CalcCheck: Found “Definition of reflexivity”
                — CalcCheck: ─ OK
            is-reflexive R
    — CalcCheck: All steps OK
    — CalcCheck: Calculation matches goal ─ OK
[16]
The composition of two reflexive relations is reflexive again — if you start just with “Assuming `is-reflexive R`”, you will need to use this assumption later via

        Assumption `is-reflexive R` with “Definition of reflexivity”
which gives you “∀ x • x ⦗ R ⦘ x” (which at that time you will apply via implicit instantiation of x to some local variable).

[17]
Theorem “Composition of reflexive relations”:
  is-reflexive R ⇒ is-reflexive S ⇒ is-reflexive (R ⨾ S)
Proof:
  Assuming `is-reflexive R`:
    Assuming `is-reflexive S`:
      Using “Definition of reflexivity”:
        For any `x`:
            x ⦗ R ⨾ S ⦘ x
          ≡⟨ “Relation composition” ⟩
            ∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x
          ⇐⟨ “∃-Introduction” ⟩
            (x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x)[b ≔ x]
          ≡⟨ Substitution ⟩
            (x ⦗ R ⦘ x ∧ x ⦗ S ⦘ x)
          ≡⟨ Assumption `is-reflexive R` with “Definition of reflexivity” ⟩
            (true ∧ x ⦗ S ⦘ x)
          ≡⟨ Assumption `is-reflexive S` with “Definition of reflexivity” ⟩
            (true ∧ true)
          ≡⟨ “Idempotency of ∧” ⟩
            true

Theorem “Composition of reflexive relations”: is-reflexive R ⇒ (is-reflexive S ⇒ is-reflexive (R ⨾ S))
Proof:
    Assuming `is-reflexive R`:
    — CalcCheck: Assumption matches goal
        Assuming `is-reflexive S`:
        — CalcCheck: Assumption matches goal
            Using “Definition of reflexivity”:
                Subproof for `(∀ x • x ⦗ R ⨾ S ⦘ x ⇐ true )`:
                    For any ` x`:
                            Proving    `x ⦗ R ⨾ S ⦘ x ⇐ true`:
                                x ⦗ R ⨾ S ⦘ x
                            ≡ ⟨ “Relation composition” ⟩
                                    — CalcCheck: Found “Relation composition”
                                    — CalcCheck: ─ OK
                                (∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x )
                            ⇐ ⟨ “∃-Introduction” ⟩
                                    — CalcCheck: Found (9.28) “∃-Introduction”
                                    — CalcCheck: ─ OK
                                (x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x)[b ≔ x]
                            ≡ ⟨ Substitution ⟩
                                    — CalcCheck: ─ OK
                                x ⦗ R ⦘ x ∧ x ⦗ S ⦘ x
                            ≡ ⟨ Assumption `is-reflexive R` with “Definition of reflexivity” ⟩
                                    — CalcCheck: Found “Definition of reflexivity”
                                    — CalcCheck: Found assumption `is-reflexive R`
                                    — CalcCheck: ─ OK
                                true ∧ x ⦗ S ⦘ x
                            ≡ ⟨ Assumption `is-reflexive S` with “Definition of reflexivity” ⟩
                                    — CalcCheck: Found “Definition of reflexivity”
                                    — CalcCheck: Found assumption `is-reflexive S`
                                    — CalcCheck: ─ OK
                                true ∧ true
                            ≡ ⟨ “Idempotency of ∧” ⟩
                                    — CalcCheck: Found (3.38) “Idempotency of ∧”
                                    — CalcCheck: ─ OK
                                true
                        — CalcCheck: All steps OK
                        — CalcCheck: Calculation matches goal ─ OK
            — CalcCheck: Found “Definition of reflexivity”
[18]
Especially in cases where such assumptions are used more than once, the “Assuming `...` and using with ...” syntax is useful — in the same proof as above, you now only need to refer to “Assumption `is-reflexive R`”:

[19]
Theorem “Composition of reflexive relations”:
  is-reflexive R ⇒ is-reflexive S ⇒ is-reflexive (R ⨾ S)
Proof:
  Assuming `is-reflexive R` and using with “Definition of reflexivity”:
      is-reflexive S ⇒ is-reflexive (R ⨾ S)
    ≡⟨ “Definition of reflexivity” ⟩
      is-reflexive S ⇒ ∀ x • x ⦗ R ⨾ S ⦘ x
    ≡⟨ “Distributivity of ⇒ over ∀” ⟩
      ∀ x • is-reflexive S ⇒ x ⦗ R ⨾ S ⦘ x
    ≡⟨ “Definition of reflexivity” ⟩
      ∀ x • (∀ y • y ⦗ S ⦘ y) ⇒ x ⦗ R ⨾ S ⦘ x
    ≡⟨ “Relation composition” ⟩
      ∀ x • (∀ y • y ⦗ S ⦘ y) ⇒ ∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x
    ≡⟨ Subproof:
         For any `x`:
           Assuming `∀ y • y ⦗ S ⦘ y`:
               ∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x
             ⇐⟨ “∃-Introduction” ⟩
               (x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x)[b ≔ x]
             ≡⟨ Substitution ⟩
               (x ⦗ R ⦘ x ∧ x ⦗ S ⦘ x)
             ≡⟨ Assumption `is-reflexive R` with “Definition of reflexivity” ⟩
               true ∧ x ⦗ S ⦘ x
             ≡⟨ Assumption `∀ y • y ⦗ S ⦘ y` ⟩
               true ∧ true
             ≡⟨ “Idempotency of ∧” ⟩
               true
      ⟩
      true

Theorem “Composition of reflexive relations”: is-reflexive R ⇒ (is-reflexive S ⇒ is-reflexive (R ⨾ S))
Proof:
    Assuming `is-reflexive R` and using with “Definition of reflexivity”
    — CalcCheck: Found “Definition of reflexivity”:
    — CalcCheck: Assumption matches goal
            Proving    `is-reflexive S ⇒ is-reflexive (R ⨾ S)`:
                is-reflexive S ⇒ is-reflexive (R ⨾ S)
            ≡ ⟨ “Definition of reflexivity” ⟩
                    — CalcCheck: Found “Definition of reflexivity”
                    — CalcCheck: ─ OK
                is-reflexive S ⇒ (∀ x • x ⦗ R ⨾ S ⦘ x )
            ≡ ⟨ “Distributivity of ⇒ over ∀” ⟩
                    — CalcCheck: Found “Distributivity of ⇒ over ∀”
                    — CalcCheck: ─ OK
                (∀ x • is-reflexive S ⇒ x ⦗ R ⨾ S ⦘ x )
            ≡ ⟨ “Definition of reflexivity” ⟩
                    — CalcCheck: Found “Definition of reflexivity”
                    — CalcCheck: ─ OK
                (∀ x • (∀ y • y ⦗ S ⦘ y ) ⇒ x ⦗ R ⨾ S ⦘ x )
            ≡ ⟨ “Relation composition” ⟩
                    — CalcCheck: Found “Relation composition”
                    — CalcCheck: ─ OK
                (∀ x • (∀ y • y ⦗ S ⦘ y ) ⇒ (∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x ) )
            ≡ ⟨ Subproof for `(∀ x • (∀ y • y ⦗ S ⦘ y ) ⇒ (∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x ) )`:
                For any ` x`:
                    Assuming `(∀ y • y ⦗ S ⦘ y )`:
                    — CalcCheck: Assumption matches goal
                            Proving    `(∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x )`:
                                (∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x )
                            ⇐ ⟨ “∃-Introduction” ⟩
                                    — CalcCheck: Found (9.28) “∃-Introduction”
                                    — CalcCheck: ─ OK
                                (x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x)[b ≔ x]
                            ≡ ⟨ Substitution ⟩
                                    — CalcCheck: ─ OK
                                x ⦗ R ⦘ x ∧ x ⦗ S ⦘ x
                            ≡ ⟨ Assumption `is-reflexive R` with “Definition of reflexivity” ⟩
                                    — CalcCheck: Found “Definition of reflexivity”
                                    — CalcCheck: Found assumption `is-reflexive R`
                                    — CalcCheck: ─ OK
                                true ∧ x ⦗ S ⦘ x
                            ≡ ⟨ Assumption `(∀ y • y ⦗ S ⦘ y )` ⟩
                                    — CalcCheck: Found assumption `(∀ y • y ⦗ S ⦘ y )`
                                    — CalcCheck: ─ OK
                                true ∧ true
                            ≡ ⟨ “Idempotency of ∧” ⟩
                                    — CalcCheck: Found (3.38) “Idempotency of ∧”
                                    — CalcCheck: ─ OK
                                true
                        — CalcCheck: All steps OK
                        — CalcCheck: Calculation matches goal ─ OK
                ⟩
                    — CalcCheck: ─ OK
                true
        — CalcCheck: All steps OK
        — CalcCheck: Calculation matches goal ─ OK
[20]
The same proof structure can be used to show that converse preserves reflexivity:

[21]
Theorem “Converse of reflexive relations”:
  is-reflexive R ⇒ is-reflexive (R ˘)
Proof:
  Assuming `is-reflexive R` and using with “Definition of reflexivity”:
      is-reflexive (R ˘)
    ≡⟨ “Definition of reflexivity” ⟩
      ∀ x • x ⦗ R ˘ ⦘ x
    ≡⟨ “Relation converse” ⟩
      ∀ x • x ⦗ R ⦘ x
    ≡⟨ Assumption `is-reflexive R` with “Definition of reflexivity” ⟩
      ∀ x • true
    ≡⟨ “True ∀ body” ⟩
      true

Theorem “Converse of reflexive relations”: is-reflexive R ⇒ is-reflexive (R ˘)
Proof:
    Assuming `is-reflexive R` and using with “Definition of reflexivity”
    — CalcCheck: Found “Definition of reflexivity”:
    — CalcCheck: Assumption matches goal
            Proving    `is-reflexive (R ˘)`:
                is-reflexive (R ˘)
            ≡ ⟨ “Definition of reflexivity” ⟩
                    — CalcCheck: Found “Definition of reflexivity”
                    — CalcCheck: ─ OK
                (∀ x • x ⦗ R ˘ ⦘ x )
            ≡ ⟨ “Relation converse” ⟩
                    — CalcCheck: Found “Relation converse”
                    — CalcCheck: ─ OK
                (∀ x • x ⦗ R ⦘ x )
            ≡ ⟨ Assumption `is-reflexive R` with “Definition of reflexivity” ⟩
                    — CalcCheck: Found “Definition of reflexivity”
                    — CalcCheck: Found assumption `is-reflexive R`
                    — CalcCheck: ─ OK
                (∀ x • true )
            ≡ ⟨ “True ∀ body” ⟩
                    — CalcCheck: Found (9.8) “True ∀ body”
                    — CalcCheck: ─ OK
                true
        — CalcCheck: All steps OK
        — CalcCheck: Calculation matches goal ─ OK
[22]
That same proof structure could also be used to show that converse reflects reflexivity — but you also can prove this at a higher level if you remember that you proved

Theorem “Self-inverse of ˘”: R ˘ ˘      =  R
in Homework 16:

[23]
Theorem “Converse reflects reflectivity”:
  is-reflexive (R ˘) ⇒ is-reflexive R
Proof:
  Assuming `is-reflexive (R ˘)` and using with “Definition of reflexivity”:
      is-reflexive R
    ≡⟨ “Definition of reflexivity” ⟩
      ∀ x • x ⦗ R ⦘ x
    ≡⟨ “Relation converse” ⟩
      ∀ x • x ⦗ R ˘ ⦘ x
    ≡⟨ Assumption `is-reflexive (R ˘)` with “Definition of reflexivity” ⟩
      ∀ x • true
    ≡⟨ “True ∀ body” ⟩
      true

Theorem “Converse reflects reflectivity”: is-reflexive (R ˘) ⇒ is-reflexive R
Proof:
    Assuming `is-reflexive (R ˘)` and using with “Definition of reflexivity”
    — CalcCheck: Found “Definition of reflexivity”:
    — CalcCheck: Assumption matches goal
            Proving    `is-reflexive R`:
                is-reflexive R
            ≡ ⟨ “Definition of reflexivity” ⟩
                    — CalcCheck: Found “Definition of reflexivity”
                    — CalcCheck: ─ OK
                (∀ x • x ⦗ R ⦘ x )
            ≡ ⟨ “Relation converse” ⟩
                    — CalcCheck: Found “Relation converse”
                    — CalcCheck: ─ OK
                (∀ x • x ⦗ R ˘ ⦘ x )
            ≡ ⟨ Assumption `is-reflexive (R ˘)` with “Definition of reflexivity” ⟩
                    — CalcCheck: Found “Definition of reflexivity”
                    — CalcCheck: Found assumption `is-reflexive (R ˘)`
                    — CalcCheck: ─ OK
                (∀ x • true )
            ≡ ⟨ “True ∀ body” ⟩
                    — CalcCheck: Found (9.8) “True ∀ body”
                    — CalcCheck: ─ OK
                true
        — CalcCheck: All steps OK
        — CalcCheck: Calculation matches goal ─ OK
[24]
Transitivity
[25]
We define the transitivity predicate for relations using the predicate-logic formulation:

[26]
Declaration: is-transitive : A ↔ A  →  𝔹
Axiom “Definition of transitivity”:    is-transitive R   ≡  ∀ x • ∀ y • ∀ z •
                        x ⦗ R ⦘ y ⦗ R ⦘ z  ⇒  x ⦗ R ⦘ z

Declaration: is-transitive : A ↔ A → 𝔹
Axiom “Definition of transitivity”: is-transitive R ≡ (∀ x • (∀ y • (∀ z • x ⦗ R ⦘ y ⦗ R ⦘ z ⇒ x ⦗ R ⦘ z ) ) )
— CalcCheck: Metavariables: R = R〖 〗
— CalcCheck: Proviso: ¬occurs(`x, y, z`, `R`)
[27]
Converse also preserves transitivity:

[28]
Theorem “Converse of transitive relations”:
    is-transitive R ⇒ is-transitive (R ˘)
Proof:
  Assuming `is-transitive R` and using with “Definition of transitivity”:
      is-transitive (R ˘)
    ≡⟨ “Definition of transitivity” ⟩
      ∀ x • ∀ y • ∀ z • x ⦗ R ˘ ⦘ y ⦗ R ˘ ⦘ z  ⇒  x ⦗ R ˘ ⦘ z
    ≡⟨ “Relation converse” ⟩
      ∀ x • ∀ y • ∀ z • x ⦗ R ˘ ⦘ y ⦗ R ˘ ⦘ z  ⇒  z ⦗ R ⦘ x
    ≡⟨ “Reflexivity of ≡” ⟩
      ∀ x • ∀ y • ∀ z • x ⦗ R ˘ ⦘ y ∧ y ⦗ R ˘ ⦘ z  ⇒  z ⦗ R ⦘ x
    ≡⟨ “Relation converse” ⟩
      ∀ x • ∀ y • ∀ z • y ⦗ R ⦘ x ∧ z ⦗ R ⦘ y  ⇒  z ⦗ R ⦘ x
    ≡⟨ “Symmetry of ∧” ⟩
      ∀ x • ∀ y • ∀ z • z ⦗ R ⦘ y ∧ y ⦗ R ⦘ x ⇒  z ⦗ R ⦘ x
    ≡⟨ “Interchange of dummies for ∀” ⟩
      ∀ z • ∀ y • ∀ x • z ⦗ R ⦘ y ∧ y ⦗ R ⦘ x ⇒  z ⦗ R ⦘ x
    ≡⟨ Assumption  `is-transitive R` with “Definition of transitivity” ⟩
      true

Theorem “Converse of transitive relations”: is-transitive R ⇒ is-transitive (R ˘)
Proof:
    Assuming `is-transitive R` and using with “Definition of transitivity”
    — CalcCheck: Found “Definition of transitivity”:
    — CalcCheck: Assumption matches goal
            Proving    `is-transitive (R ˘)`:
                is-transitive (R ˘)
            ≡ ⟨ “Definition of transitivity” ⟩
                    — CalcCheck: Found “Definition of transitivity”
                    — CalcCheck: ─ OK
                (∀ x • (∀ y • (∀ z • x ⦗ R ˘ ⦘ y ⦗ R ˘ ⦘ z ⇒ x ⦗ R ˘ ⦘ z ) ) )
            ≡ ⟨ “Relation converse” ⟩
                    — CalcCheck: Found “Relation converse”
                    — CalcCheck: ─ OK
                (∀ x • (∀ y • (∀ z • x ⦗ R ˘ ⦘ y ⦗ R ˘ ⦘ z ⇒ z ⦗ R ⦘ x ) ) )
            ≡ ⟨ “Reflexivity of ≡” ⟩
                    — CalcCheck: Found (3.5) “Reflexivity of ≡”
                    — CalcCheck: OK (no change)
                    — CalcCheck: ─ OK
                (∀ x • (∀ y • (∀ z • x ⦗ R ˘ ⦘ y ∧ y ⦗ R ˘ ⦘ z ⇒ z ⦗ R ⦘ x ) ) )
            ≡ ⟨ “Relation converse” ⟩
                    — CalcCheck: Found “Relation converse”
                    — CalcCheck: ─ OK
                (∀ x • (∀ y • (∀ z • y ⦗ R ⦘ x ∧ z ⦗ R ⦘ y ⇒ z ⦗ R ⦘ x ) ) )
            ≡ ⟨ “Symmetry of ∧” ⟩
                    — CalcCheck: Found (3.36) “Symmetry of ∧”
                    — CalcCheck: OK (no change)
                    — CalcCheck: ─ OK
                (∀ x • (∀ y • (∀ z • z ⦗ R ⦘ y ∧ y ⦗ R ⦘ x ⇒ z ⦗ R ⦘ x ) ) )
            ≡ ⟨ “Interchange of dummies for ∀” ⟩
                    — CalcCheck: Found (8.19) “Interchange of dummies for ∀”
                    — CalcCheck: ─ OK
                (∀ z • (∀ y • (∀ x • z ⦗ R ⦘ y ∧ y ⦗ R ⦘ x ⇒ z ⦗ R ⦘ x ) ) )
            ≡ ⟨ Assumption `is-transitive R` with “Definition of transitivity” ⟩
                    — CalcCheck: Found “Definition of transitivity”
                    — CalcCheck: Found assumption `is-transitive R`
                    — CalcCheck: ─ OK
                true
        — CalcCheck: All steps OK
        — CalcCheck: Calculation matches goal ─ OK
[29]
The relation-algebraic formulation of transitivity can again be shown via a relatively straight-forward equivalence calculation — you may need some advance quantifier theorems, e.g.:

Axiom (8.20) “Nesting for ∀”:                        (∀ x, y ❙ R ∧ S • P)  ≡  (∀ x ❙ R • (∀ y ❙ S • P))
Theorem (8.20a) “Nesting for ∀”:                         (∀ x, y ❙ S • P)  ≡  (∀ x • (∀ y ❙ S • P))
Axiom “Dummy list permutation for ∀”                     (∀ x, y ❙ R • P)  ≡  (∀ y, x ❙ R • P)
Theorem (8.19) “Interchange of dummies for ∀”:  (∀ x ❙ R • (∀ y ❙ S • P))  ≡  (∀ y ❙ S • (∀ x ❙ R • P))
Axiom (9.5) “Distributivity of ∨ over ∀”:               P ∨ (∀ x ❙ R • Q)  ≡  (∀ x ❙ R • P ∨ Q)
Theorem “Distributivity of ⇒ over ∀”:                 (P ⇒ (∀ x ❙ R • Q))  ≡  (∀ x ❙ R • P ⇒ Q)
Theorem (9.30a) “Witness”:                             ((∃ x ❙ R • P) ⇒ Q)  ≡  (∀ x • R ∧ P ⇒ Q)
[30]
Theorem “Transitivity”:
  is-transitive R   ≡   R ⨾ R ⊆ R
Proof:
    R ⨾ R ⊆ R
  ≡⟨ “Relation inclusion” ⟩
    ∀ x • ∀ y • x ⦗ R ⨾ R ⦘ y ⇒ x ⦗ R ⦘ y
  ≡⟨ “Relation composition” ⟩
    ∀ x • ∀ y • (∃ b • x ⦗ R ⦘ b ∧ b ⦗ R ⦘ y) ⇒ x ⦗ R ⦘ y
  ≡⟨ “Definition of ⇒” ⟩
    ∀ x • ∀ y • ¬ (∃ b • x ⦗ R ⦘ b ∧ b ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y
  ≡⟨ “Generalised De Morgan” ⟩
    ∀ x • ∀ y • (∀ b • ¬ (x ⦗ R ⦘ b ∧ b ⦗ R ⦘ y)) ∨ x ⦗ R ⦘ y
  ≡⟨ “De Morgan” ⟩
    ∀ x • ∀ y • (∀ b • ¬ (x ⦗ R ⦘ b) ∨ ¬ (b ⦗ R ⦘ y)) ∨ x ⦗ R ⦘ y
  ≡⟨ “Definition of ⇒” ⟩
    ∀ x • ∀ y • (∀ b • (x ⦗ R ⦘ b) ⇒ ¬ (b ⦗ R ⦘ y)) ∨ x ⦗ R ⦘ y
  ≡⟨ “Trading for ∀” ⟩
    ∀ x • ∀ y • (∀ b ❙ (x ⦗ R ⦘ b) • ¬ (b ⦗ R ⦘ y)) ∨ x ⦗ R ⦘ y
  ≡⟨ “Distributivity of ∨ over ∀” ⟩
    ∀ x • ∀ y • (∀ b ❙ (x ⦗ R ⦘ b) • ¬ (b ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y)
  ≡⟨ “Trading for ∀” ⟩
    ∀ x • ∀ y • (∀ b • ¬ (x ⦗ R ⦘ b) ∨ ¬ (b ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y)
  ≡⟨ “Distributivity of ∨ over ∨”, “De Morgan” ⟩
    ∀ x • ∀ y • ∀ b • ¬ ((x ⦗ R ⦘ b ⦗ R ⦘ y) ∧ (x ⦗ R ⦘ b)) ∨  x ⦗ R ⦘ y
  ≡⟨ “Idempotency of ∧” ⟩
    ∀ x • ∀ y • ∀ b • ¬ (x ⦗ R ⦘ b ⦗ R ⦘ y) ∨  x ⦗ R ⦘ y
  ≡⟨ “Definition of ⇒”, “Interchange of dummies for ∀” ⟩
    ∀ x • ∀ b • ∀ y • (x ⦗ R ⦘ b ⦗ R ⦘ y) ⇒  x ⦗ R ⦘ y
  ≡⟨ “Definition of transitivity” ⟩
    is-transitive R

Theorem “Transitivity”: is-transitive R ≡ R ⨾ R ⊆ R
Proof:
        Proving    `is-transitive R ≡ R ⨾ R ⊆ R`:
            R ⨾ R ⊆ R
        ≡ ⟨ “Relation inclusion” ⟩
                — CalcCheck: Found “Relation inclusion”, “Relation inclusion”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • x ⦗ R ⨾ R ⦘ y ⇒ x ⦗ R ⦘ y ) )
        ≡ ⟨ “Relation composition” ⟩
                — CalcCheck: Found “Relation composition”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∃ b • x ⦗ R ⦘ b ∧ b ⦗ R ⦘ y ) ⇒ x ⦗ R ⦘ y ) )
        ≡ ⟨ “Definition of ⇒” ⟩
                — CalcCheck: Found (3.57) “Definition of ⇒”, (3.59) “Definition of ⇒”, (3.60) “Definition of ⇒”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • ¬ (∃ b • x ⦗ R ⦘ b ∧ b ⦗ R ⦘ y ) ∨ x ⦗ R ⦘ y ) )
        ≡ ⟨ “Generalised De Morgan” ⟩
                — CalcCheck: Found (9.17) “Generalised De Morgan”, (9.18a) “Generalised De Morgan”, (9.18b) “Generalised De Morgan”, (9.18c) “Generalised De Morgan”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∀ b • ¬ (x ⦗ R ⦘ b ∧ b ⦗ R ⦘ y) ) ∨ x ⦗ R ⦘ y ) )
        ≡ ⟨ “De Morgan” ⟩
                — CalcCheck: Found (3.47a) “De Morgan”, (3.47b) “De Morgan”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∀ b • ¬ (x ⦗ R ⦘ b) ∨ ¬ (b ⦗ R ⦘ y) ) ∨ x ⦗ R ⦘ y ) )
        ≡ ⟨ “Definition of ⇒” ⟩
                — CalcCheck: Found (3.57) “Definition of ⇒”, (3.59) “Definition of ⇒”, (3.60) “Definition of ⇒”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∀ b • x ⦗ R ⦘ b ⇒ ¬ (b ⦗ R ⦘ y) ) ∨ x ⦗ R ⦘ y ) )
        ≡ ⟨ “Trading for ∀” ⟩
                — CalcCheck: Found (9.2) “Trading for ∀”, (9.3a) “Trading for ∀”, (9.3b) “Trading for ∀”, (9.3c) “Trading for ∀”, (9.4a) “Trading for ∀”, (9.4b) “Trading for ∀”, (9.4c) “Trading for ∀”, (9.4d) “Trading for ∀”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∀ b ❙ x ⦗ R ⦘ b • ¬ (b ⦗ R ⦘ y) ) ∨ x ⦗ R ⦘ y ) )
        ≡ ⟨ “Distributivity of ∨ over ∀” ⟩
                — CalcCheck: Found (9.5) “Distributivity of ∨ over ∀”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∀ b ❙ x ⦗ R ⦘ b • ¬ (b ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y ) ) )
        ≡ ⟨ “Trading for ∀” ⟩
                — CalcCheck: Found (9.2) “Trading for ∀”, (9.3a) “Trading for ∀”, (9.3b) “Trading for ∀”, (9.3c) “Trading for ∀”, (9.4a) “Trading for ∀”, (9.4b) “Trading for ∀”, (9.4c) “Trading for ∀”, (9.4d) “Trading for ∀”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∀ b • ¬ (x ⦗ R ⦘ b) ∨ (¬ (b ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y) ) ) )
        ≡ ⟨ “Distributivity of ∨ over ∨”, “De Morgan” ⟩
                — CalcCheck: Found (3.31) “Distributivity of ∨ over ∨”
                — CalcCheck: Found (3.47a) “De Morgan”, (3.47b) “De Morgan”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∀ b • ¬ (x ⦗ R ⦘ b ⦗ R ⦘ y ∧ x ⦗ R ⦘ b) ∨ x ⦗ R ⦘ y ) ) )
        ≡ ⟨ “Idempotency of ∧” ⟩
                — CalcCheck: Found (3.38) “Idempotency of ∧”
                — CalcCheck: ─ OK
            (∀ x • (∀ y • (∀ b • ¬ (x ⦗ R ⦘ b ⦗ R ⦘ y) ∨ x ⦗ R ⦘ y ) ) )
        ≡ ⟨ “Definition of ⇒”, “Interchange of dummies for ∀” ⟩
                — CalcCheck: Found (3.57) “Definition of ⇒”, (3.59) “Definition of ⇒”, (3.60) “Definition of ⇒”
                — CalcCheck: Found (8.19) “Interchange of dummies for ∀”
                — CalcCheck: ─ OK
            (∀ x • (∀ b • (∀ y • x ⦗ R ⦘ b ⦗ R ⦘ y ⇒ x ⦗ R ⦘ y ) ) )
        ≡ ⟨ “Definition of transitivity” ⟩
                — CalcCheck: Found “Definition of transitivity”
                — CalcCheck: ─ OK
            is-transitive R
    — CalcCheck: All steps OK
    — CalcCheck: Calculation matches goal ─ OK
[31]
Calling all brothers…
[32]
The free variables of the following two theorem statements are intended to have the following types:

    R : A ↔ B
    S : A ↔ C
(I could have put those into additional explicit universal quantifiers…)

All bound variables are named accordingly.

Once you can calculate, start from the right…

[33]
Theorem (R1): ∀ b : B • ∀ c : C •
  (∀ a : A ❙ a ⦗ R ⦘ b • a ⦗ S ⦘ c)  ≡  b ⦗ ~ (R ˘ ⨾ ~ S) ⦘ c
Proof:
  For any `b`, `c`:
      b ⦗ ~ (R ˘ ⨾ ~ S) ⦘ c
    ≡⟨ “Relation complement” ⟩
      ¬ (b ⦗ (R ˘ ⨾ ~ S) ⦘ c)
    ≡⟨ “Relation composition” ⟩
      ¬ (∃ a : A • (b ⦗ R ˘ ⦘ a ∧ a ⦗ ~ S ⦘ c))
    ≡⟨ “Relation converse” ⟩
      ¬ (∃ a • (a ⦗ R ⦘ b ∧ a ⦗ ~ S ⦘ c))
    ≡⟨ “Relation complement” ⟩
      ¬ (∃ a • a ⦗ R ⦘ b ∧ ¬ (a ⦗ S ⦘ c))
    ≡⟨ “Double negation” ⟩
      ¬ (∃ a • ¬ ¬ (a ⦗ R ⦘ b) ∧ ¬ (a ⦗ S ⦘ c))
    ≡⟨ “De Morgan” ⟩
      ¬ (∃ a • ¬ (¬ (a ⦗ R ⦘ b) ∨ (a ⦗ S ⦘ c)))
    ≡⟨ “Generalised De Morgan” ⟩
      (∀ a • (¬ (a ⦗ R ⦘ b) ∨ (a ⦗ S ⦘ c)))
    ≡⟨ “Definition of ⇒” ⟩
      (∀ a • (a ⦗ R ⦘ b) ⇒ (a ⦗ S ⦘ c))
    ≡⟨ “Trading for ∀” ⟩
      (∀ a : A ❙ a ⦗ R ⦘ b • a ⦗ S ⦘ c)

Theorem (R1): (∀ b : B • (∀ c : C • (∀ a : A ❙ a ⦗ R ⦘ b • a ⦗ S ⦘ c ) ≡ b ⦗ ~ (R ˘ ⨾ ~ S) ⦘ c ) )
— CalcCheck: Metavariables: A = A〖b, c 〗, C = C〖b 〗, R = R〖b, c 〗, S = S〖b, c 〗
— CalcCheck: Proviso: ¬occurs(`a`, `R, S`)
Proof:
    For any ` b`:
        For any ` c`:
                Proving    `(∀ a : A ❙ a ⦗ R ⦘ b • a ⦗ S ⦘ c ) ≡ b ⦗ ~ (R ˘ ⨾ ~ S) ⦘ c`:
                    b ⦗ ~ (R ˘ ⨾ ~ S) ⦘ c
                ≡ ⟨ “Relation complement” ⟩
                        — CalcCheck: Found “Relation complement”
                        — CalcCheck: ─ OK
                    ¬ (b ⦗ R ˘ ⨾ ~ S ⦘ c)
                ≡ ⟨ “Relation composition” ⟩
                        — CalcCheck: Found “Relation composition”
                        — CalcCheck: ─ OK
                    ¬ (∃ a : A • b ⦗ R ˘ ⦘ a ∧ a ⦗ ~ S ⦘ c )
                ≡ ⟨ “Relation converse” ⟩
                        — CalcCheck: Found “Relation converse”
                        — CalcCheck: ─ OK
                    ¬ (∃ a • a ⦗ R ⦘ b ∧ a ⦗ ~ S ⦘ c )
                ≡ ⟨ “Relation complement” ⟩
                        — CalcCheck: Found “Relation complement”
                        — CalcCheck: ─ OK
                    ¬ (∃ a • a ⦗ R ⦘ b ∧ ¬ (a ⦗ S ⦘ c) )
                ≡ ⟨ “Double negation” ⟩
                        — CalcCheck: Found (3.12) “Double negation”
                        — CalcCheck: ─ OK
                    ¬ (∃ a • ¬ (¬ (a ⦗ R ⦘ b)) ∧ ¬ (a ⦗ S ⦘ c) )
                ≡ ⟨ “De Morgan” ⟩
                        — CalcCheck: Found (3.47a) “De Morgan”, (3.47b) “De Morgan”
                        — CalcCheck: ─ OK
                    ¬ (∃ a • ¬ (¬ (a ⦗ R ⦘ b) ∨ a ⦗ S ⦘ c) )
                ≡ ⟨ “Generalised De Morgan” ⟩
                        — CalcCheck: Found (9.17) “Generalised De Morgan”, (9.18a) “Generalised De Morgan”, (9.18b) “Generalised De Morgan”, (9.18c) “Generalised De Morgan”
                        — CalcCheck: ─ OK
                    (∀ a • ¬ (a ⦗ R ⦘ b) ∨ a ⦗ S ⦘ c )
                ≡ ⟨ “Definition of ⇒” ⟩
                        — CalcCheck: Found (3.57) “Definition of ⇒”, (3.59) “Definition of ⇒”, (3.60) “Definition of ⇒”
                        — CalcCheck: ─ OK
                    (∀ a • a ⦗ R ⦘ b ⇒ a ⦗ S ⦘ c )
                ≡ ⟨ “Trading for ∀” ⟩
                        — CalcCheck: Found (9.2) “Trading for ∀”, (9.3a) “Trading for ∀”, (9.3b) “Trading for ∀”, (9.3c) “Trading for ∀”, (9.4a) “Trading for ∀”, (9.4b) “Trading for ∀”, (9.4c) “Trading for ∀”, (9.4d) “Trading for ∀”
                        — CalcCheck: ─ OK
                    (∀ a : A ❙ a ⦗ R ⦘ b • a ⦗ S ⦘ c )
            — CalcCheck: All steps OK
            — CalcCheck: Calculation matches goal ─ OK
[34]
Prove (R2) by “Relation inclusion” and start calculating from the left — in doubt, make the subproof goal explicit. You will probably need:

(3.66):                                                 p ∧ (p ⇒ q)  ≡  p ∧ q
 “Instantiation”:                                          (∀ x • P)  ⇒  P[x ≔ E]
“Body monotonicity of ∃”:  (∀ x ❙ R • Q ⇒ P)  ⇒     ((∃ x ❙ R • Q)  ⇒  (∃ x ❙ R • P))
 “Distributivity of ∧ over ∃”:                    P ∧ (∃ x ❙ R • Q)  ≡  (∃ x ❙ R • P ∧ Q)
[35]
Theorem (R2): R ⨾ ~ (R ˘ ⨾ ~ S) ⊆ S
Proof:
  Using “Relation inclusion”:
    For any `a`, `c`:

Theorem (R2): R ⨾ ~ (R ˘ ⨾ ~ S) ⊆ S
Proof:
    Using “Relation inclusion”:
        Subproof:
            For any ` a`:
                For any ` c`:
                            ⟪ expecting «expression»! ⟫

                    — CalcCheck: Could not determine the goal for this calculation.
    — CalcCheck: Found “Relation inclusion”, “Relation inclusion”
    — CalcCheck: Could not justify this step!
Check and Save