At: trace inv as while 3 2
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')
P(x',l @ [act])
By: InstHyp [x;x';l;act] 3
Generated subgoal:| 1 | (M -l- > x) |
About:
