Variations in HYP, CNTR and GenMP
From Event-B
This page explains how the variants array in Inference Rules have been generated.
The reasoners implementing the inference rules HYP, HYP_OR, CNTR and GENMP take into account such variants of and
. These variants correspond to a predicate equivalent or a sufficient conditon for apply the rule. The variants are only relational predicates. We consider
and
. Moreover, the default value of
is
and this of
is
.
Only the negative predicate "¬ a = b" is allowed, the others are rewritten because the reasoners implementing those inference rules are applied after such normalization of relational predicates.