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:(Label Label), s:(f o M).state. s M.state | [sm_a_rename_state] |
Thm* M:(I sm{i:l}()), j:I, x: i:IM(i).state. x M(j).state | [small_state] |
Thm* M:sm{i:l}(). M.trans M.state M.action M.state Prop | [sm_trans_wf] |
Thm* M:sm{i:l}(). M.init M.state Prop | [sm_init_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 -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 trace_reachable(M;s;l;s')
== Case of l
nil s = s' M.state
a.l' x:M.state. M.trans(s,a,x) & trace_reachable(M;x;l';s')
(recursive) | [trace_reachable] |