At: trace inv as while 3 2 1
1. M: sm{i:l}()
2. P: M.state
(M.action List)Prop
3. 
s,x':M.state, t:M.action List, a:M.action.
(M -t- > s) 
M.trans(s,a,x') P(s,t) True True P(x',t @ [a])
4. (M |= initially s,t.P(s,t))
5. s0: M.state
6. x: M.state
7. act: M.action
8. x': M.state
9. l: M.action List
10. M.init(s0)
11. trace_reachable(M;s0;l;x)
12. P(x,l)
13. M.trans(x,act,x')
(M -l- > x)
By:
Unfold `reachable_via` 0
THEN
InstConcl [s0]
Generated subgoals:None
About:
