The using...prove declaration

This declaration has the form form

        using
          p_1, p_2, ..., p_k
        prove
          q_1, q_2, ..., q_m
        ;

where p_1, p_2, ..., p_k and q_1, q_2, ..., q_m are properties. The meaning of the declaration is that properties p_1, p_2, ..., p_k are to be taken as assumptions when proving the properties q_1, q_2, ..., q_m.

If assumptions are not declared for a given property, then that property inherits the assumptions of its parent. For example, if we wish to assume property foo when proving bar.a, bar.b and bar.c, it is sufficient to declare

        using foo prove bar;

If there is no declaration of assumptions for bar.a, then it will inherit the assumption of foo from its parent, bar. Note, however, that if we include the declaration

        using baz prove bar.a;

then only property baz is used to prove bar.a.

Similarly, if we wish to assume a collection of properties foo.a, foo.b and foo.c when proving a property bar, it is sufficient to declare:

        using bar prove foo;

It is allowed to use several assignments to the same signal as assumptions. For example:

        using x//P1, x//P2 prove y//P

In this case, the conjunction of the two assumptions is used.