At first, we will get to know the system.

Below you find the user interface of Elfe. Inside is a proof about relations: If a relation is empty, than it is especially symmetric. Take a look at the proof – you do not need to understand it completely yet, as we will dive deeper into the Elfe language in the next exercises.

In order to check the proof, you can click "Verify" in the upper right corner. If the proof is correct, all lines will appear green. You then can inspect the lines of the proofs.

Put the cursor on line 6. Below the input you should find the internal representation of the mathematical statement.

You can press the buttons in the left upper corner to insert special characters.

In order to get to the next exercise, press "Go to next exercise" below the prover interface.

Line , Col

Go to next exercise