- (min (*BEGIN*)[[ negate f ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*))
- = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ negate f1 ]]_v(*END*)) by H.
- = (min (*BEGIN*)[[ FNot (dualize f) ]]_v(*END*) (*BEGIN*)[[ FNot (dualize f1) ]]_v(*END*)) by H1.
- = (min (1 - [[ dualize f ]]_v) (1 - [[ dualize f1 ]]_v)).
- = (1 - (max [[ dualize f ]]_v [[ dualize f1 ]]_v)) by min_max.
+ (min (*BEGIN*)[[ negate f ]]v(*END*) (*BEGIN*)[[ negate f1 ]]v(*END*))
+ = (min (*BEGIN*)[[ FNot (dualize f) ]]v(*END*) (*BEGIN*)[[ negate f1 ]]v(*END*)) by H.
+ = (min (*BEGIN*)[[ FNot (dualize f) ]]v(*END*) (*BEGIN*)[[ FNot (dualize f1) ]]v(*END*)) by H1.
+ = (min (1 - [[ dualize f ]]v) (1 - [[ dualize f1 ]]v)).
+ = (1 - (max [[ dualize f ]]v [[ dualize f1 ]]v)) by min_max.