x:Label. pred_mentions(p;x) 
covers_var(A;x)
fr:frame().
fr 
< fr A.frame | 
fr.var =
x >
& (a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > ))
is mentioned by
|
Def covers_pred(A;p) == x:Label. pred_mentions(p;x) covers_var(A;x) | [covers_pred] |
In prior sections: mb automata 2
Try larger context: GenAutomata