Selected Objects
| def | sm_state | M.state == {M.ds} |
| def | sm_action | M.action == ( M.da) |
| def | sm | sm{i:l}() == da:Decl ds:Decl({ds}  Prop)({ds}(da){ds}Prop) |
| def | sm_da | t.da == 1of(t) |
| def | sm_ds | t.ds == 1of(2of(t)) |
| def | sm_init | t.init == 1of(2of(2of(t))) |
| def | sm_trans | t.trans == 2of(2of(2of(t))) |
| def | mk_sm | mk_sm(da, ds, init, trans) == < da,ds,init,trans > |
| def | sm_all |  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)) |
| THM | small_state | M:(Ism{i:l}()), j:I, x:i:IM(i).state. x M(j).state |
| THM | small_action | M:(Ism{i:l}()), j:I, x:i:IM(i).action. x M(j).action |
| def | sm_a_rename | (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)) |
| THM | sm_a_rename_state | M:sm{i:l}(), f:(LabelLabel), s:(f o M).state. s M.state |
| def | trace_reachable | (rec) 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') |
| THM | trace_reachable_one | M:sm{i:l}(), a:M.action, s,s':M.state. trace_reachable(M;s;[a];s')   M.trans(s,a,s') |
| def | initially | (M |= initially x,tr.P(x;tr)) == x:M.state. M.init(x)  P(x;nil) |
| THM | trace_reachable_append | 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')) |
| def | reachable_via | (M -tr- > s) == s0:M.state. M.init(s0) & trace_reachable(M;s0;tr;s) |
| def | trace_inv | (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) |
| THM | trace_inv_induction | 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)) |
| def | tla | (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]) |
| def | while | (M |= x,tr.P(x;tr) while Q(x;tr)) == (M |= x,x',tr,tr'.P(x;tr) Q(x;tr) Q(x';tr') P(x';tr')) |
| THM | trace_inv_as_while | 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)) |