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] |
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 -tr- > s) == s0:M.state. M.init(s0) & trace_reachable(M;s0;tr;s) | [reachable_via] |
Def (M |= initially x,tr.P(x;tr)) == x:M.state. M.init(x)  P(x;nil) | [initially] |
Def (f o M)
== mk_sm(M.da o f, M.ds, M.init, s1,a,s2. l:Label. kind(a) = f(l) & M.trans(s1, < l,value(a) > ,s2)) | [sm_a_rename] |
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] |