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}(), l1,l2:M.action List, s,s':M.state. trace_reachable(M;s;l1 @ l2;s') (x:M.state. trace_reachable(M;s;l1;x) & trace_reachable(M;x;l2;s'))	[trace_reachable_append]
Thm* M:sm{i:l}(), a:M.action, s,s':M.state. trace_reachable(M;s;[a];s') M.trans(s,a,s')	[trace_reachable_one]
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}(), f:(LabelLabel), s:(f o M).state. s M.state	[sm_a_rename_state]
Thm* M:(Ism{i:l}()), j:I, x:i:IM(i).action. x M(j).action	[small_action]
Thm* M:(Ism{i:l}()), j:I, x:i:IM(i).state. x M(j).state	[small_state]
Thm* M:sm{i:l}(). M.trans M.stateM.actionM.stateProp	[sm_trans_wf]
Thm* M:sm{i:l}(), a:M.action. kind(a) Label & kind(a) Pattern	[kind_wf2]
Thm* M:sm{i:l}(). M.init M.stateProp	[sm_init_wf]
Thm* t:sm{i:l}(). t.ds Decl	[sm_ds_wf]
Thm* t:sm{i:l}(). t.da Decl	[sm_da_wf]
Def (M |= x,x',tr,tr'.R(x;x';tr;tr')) == x,x':M.state, tr:M.action List, a:M.action. (M -tr- > x) M.trans(x,a,x') R(x;x';tr;tr @ [a])	[tla]
Def (M |= always s,t.P(s;t)) == t:M.action List, s0,s:M.state. M.init(s0) trace_reachable(M;s0;t;s) P(s;t)	[trace_inv]
Def (M |= initially x,tr.P(x;tr)) == x:M.state. M.init(x) P(x;nil)	[initially]
Def i:I M(i) == mk_sm(M(i).da for i I, M(i).ds for i I, s.i:I. M(i).init(s), s1,a,s2. i:I. M(i).trans(s1,a,s2))	[sm_all]

In prior sections: core well fnd int 1 bool 1 sqequal 1 fun 1 int 2 list 1 prog 1 rel 1 mb basic mb nat union num thy 1 mb list 1 mb label mb declaration mb record

Try larger context: GenAutomata