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:

Every assumption needs to be closed with a conclusion: If you open a proof with "Assume ...", later on you will have to close it with "Hence ...".
"Then" can be used to make additional derivations.
You can introduce a case distinction with "Case ...:". Remember to close the proof of the case with "qed."
Take care to always use parentheses around special notations: You need to write "(R ∪ (R⁻¹))[x,y]" instead of R ∪ R⁻¹[x,y].

∈ ∩ ∪ ⊆ ᑦ -> ∘ ⁻¹ [ ] { }

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