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]
Thm* M:sm{i:l}(), l:M.action List, s,s':M.state. trace_reachable(M;s;l;s') Prop	[trace_reachable_wf]
Thm* M:sm{i:l}(). M.trans M.stateM.actionM.stateProp	[sm_trans_wf]
Thm* M:sm{i:l}(). M.init M.stateProp	[sm_init_wf]
Def sm{i:l}() == da:Declds:Decl({ds}Prop)({ds}(da){ds}Prop)	[sm]

In prior sections: core well fnd int 1 bool 1 fun 1 int 2 list 1 rel 1 mb basic mb nat mb list 1

Try larger context: GenAutomata