is mentioned by

Thm* M:sm{i:l}(), P:(M.state(M.action List)Prop). (M |= always s,t.P(s,t)) (M |= s,t.P(s,t) while True) & (M |= initially s,t.P(s,t))

[trace_inv_as_while]

In prior sections: core mb list 1 bool 1

Try larger context: GenAutomata