[sv-ac] vacuity

Here is an attempt to define when an assertion pass non-vacuously.
This proposal is also available at mentis (1381).
This is not a proposal, it's a definition for review and discussion.

There are a lot of vacuity definitions, I tried to have a simple definition
that generalizes the implication vacuity that is already being used. The
definition is on the structure of the property, on the property level, 
meaning
we have a new satisfaction relation. Let $\tight$ be the tight satisfaction
relation, $\models$ the satisfaction relation and $\non$ the
non-vacuous  relation. An attempt of a property $P$ on a suffix $w$
pass non vacuously iff $w,{}\models P$ and $w,{}\non P$.

The definition of $\non$ is per attempt on a suffix $w$ of a computation.

Base: For every sequence $R$, property $P=R$, and assignment $L$, we 
have that          
$w,L\non P$.

Induction:

 * For $P =  (P_1)$ and assignment $L$, we have that $w,L\non P$  iff
     $w,L \non P_1$.

 * For $P = R |-> P_1$ and assignment $L$, we have that $w,L\non P$  iff
     there exists $i \geq 0$, and an assignment $L_1$ such that
     $w^{0..i}, {}, L_1 \tight R$ and $w^{i..}, L_1\non P_1$.

 * For $P = P_1 and P_2$ and assignment $L$, we have that $w,L\non P$  iff
     $w,L \non P_1$ or $w,L\non P_2$.

 * For $P = P_1 or P_2$ and assignment $L$, we have that $w,L\non P$  iff
     $w,L \non P_1$ or $w,L\non P_2$.

 * For $P = not P_1$ and assignment $L$, we have that $w,L\non P$  iff
     $w,L \non P_1$.

 * For $P = disable iff (b) P_1$ and assignment $L$, we have that 
$w,L\non P$  iff
     $w,L \non P_1$.