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))x:M.state. M.init(x) 
P(x;nil)
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] |
Try larger context: GenAutomata