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]
Thm* M:sm{i:l}(), I:(M.state(M.action List)Prop). (x:M.state. M.init(x) I(x,nil)) (s0,x:M.state, act:M.action, x':M.state, l:M.action List. M.init(s0) trace_reachable(M;s0;l;x) I(x,l) M.trans(x,act,x') I(x',l @ [act])) (M |= always s,t.I(s,t))	[trace_inv_induction]

Try larger context: GenAutomata