Az egyenlőtlenség kezelése, az univerzális kvantálás, az implikáció és a logikai ekvivalencia használata kettős negációk megjelenését okozhatja, ami az egyébként jól-formált kódot nem mód-helyessé tehet. E probléma elkerülésére a nyelv előírja, hogy a szintaktikus elemzés és az implicit kvantálás után, de a mód-elemzés előtt az implementációnak el kell távolítania a kettős negációkat, valamint negációk konjunkciójának negációját helyettesíteni kell diszjunkciókkal. (Mindkét transzformáció megtartja a kód logikai jelentését és típus-helyességét, valamint megtartják vagy javítják a mód-helyességet: soha nem alakítanak át egyébként mód-helyes kód részleteket nem mód-helyessé.)