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))
Q(x;tr) Q(x';tr') P(x';tr'))
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