Exercise 4

You can now try to write your own proof! It is a quite difficult one, so do not despair if you do not solve it right away.

You will need to use all constructs that you got to know in the previous tasks. You can look at the solutions of the previous tasks below the prover.

Remember the following peculiarities of the Elfe language:

Line , Col
Lemma: R ⊆ S and S ⊆ T implies S ⊆ T. Proof: Assume R ⊆ S and S ⊆ T. Assume R[x,y]. Then S[x,y]. Hence T[x,y]. Hence S ⊆ T. qed.
Lemma: R ∪ (R⁻¹) is symmetric. Proof: Assume (R ∪ (R⁻¹))[x,y]. Then R[x,y] or (R⁻¹)[x,y]. Case R[x,y]: Then (R⁻¹)[y,x]. qed. Case (R⁻¹)[x,y]: Then R[y,x]. qed. Hence (R ∪ (R⁻¹))[y,x]. qed.

Finish the training