| Rank | Theorem | Name |
| 3 |
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] |
| cites |
| 0 |
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] |
| 2 |
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] |