Thm* M:sm{i:l}(), I:(M.state![](FONT/dash.png) (M.action List)![](FONT/dash.png) Prop).
( x:M.state. M.init(x) ![](FONT/eq.png) I(x,nil)) ![](FONT/eq.png)
( s0,x:M.state, act:M.action, x':M.state, l:M.action List.
M.init(s0) ![](FONT/eq.png) trace_reachable(M;s0;l;x) ![](FONT/eq.png) I(x,l) ![](FONT/eq.png) M.trans(x,act,x') ![](FONT/eq.png) I(x',l @ [act]))
![](FONT/eq.png)
(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')
![](FONT/if_big.png)
( x:M.state. trace_reachable(M;s;l1;x) & trace_reachable(M;x;l2;s')) | [trace_reachable_append] |
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) ![](FONT/eq.png) M.trans(x,a,x') ![](FONT/eq.png) R(x;x';tr;tr @ [a]) | [tla] |