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_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 > )) | [covers_var] |
In prior sections: mb automata 1
Try larger context:
GenAutomata