A procedure é chamada '''dual''' (naturalmente) e recebe como argumentos a expressão booleana formada usando as versões inertes dos operadores booleanos.
<pre>dual(false);
dual(true); dual(x &and y); dual(x &or (¬ y &or ¬ x and ¬ (¬ z)));</pre>
A beleza da dualidade é que, uma vez que você provar uma identidade booleana, você pode usar o '''dual''' a vontade!
e formular nossas expressões usando operadores inertes.
<pre>with(logic): # don't forget to define 'bequal'.
left := (x &and ¬ y) &or (y &and ¬ z) &or (z &and ¬ x); right := (¬ x &and y) &or (¬ y &and z) &or (¬ z &and x); bequal(left, right);</pre>
Agora, nos usamos esta afirmação à vontade.
<pre>dual(left);