Equivalence (<->) in Sequent Calculus

Question

In the solution for the VRS exam 08/2018 in task 1 b)

it seems like a rule for <-> was used to split !d<->a&c, but we had no such rule in the slides. Would it be allowed in the exam to write it down like this? So are we allowed to use such "intuitive" rules?

Or do we have to write down all intermediate steps, so for example first rewriting a<->b = (a->b)&(b->a), second rewriting (a->b)&(b->a) = (!a | b) & (!b | a) and then using and/or/negation rules, since we just had these rules in the slides? Would cost more time that's why I am asking..

Answer 1

You can directly use a rule for eliminating xor or equivalence that you worked out aside. That will be fine! (Just make sure that it is correct). There are also at least two versions.

There was already a related question; please refer to that ones answer: https://q2a.cs.uni-kl.de/1214/sequent-calculus