Justified Algebraic Manipulation
When algebra is used to manipulate constants, it comes with a cost. By default, any algebraic manipulation is permitted. This means that arbitrary jumps towards proof objectives are permitted. In strict mode, algebraic manipulation must be justified.
Algebra in Strict Mode
By default arbitrary algebra is permitted.
[if a%2==0 then 1 else 2]\[a%2|1] : [if 1==0 then 1 else 2] : [2]
In strict mode, the algebraic substitution operator \ is only permitted when the rule applied appears in an attached invariant.
(x:Odd) \ [self%2|1]
This restriction is necessary to construct sound proof objects. Without the restriction, it would be easy to jump to arbitrary conclusions.