At: trace inv as while 1 1 1 1 1
1. M: sm{i:l}()
2. P: M.state
(M.action List)Prop
3. 
t:M.action List, s0,s:M.state. M.init(s0) 
trace_reachable(M;s0;t;s) P(s,t)
4. s: M.state
5. x': M.state
6. t: M.action List
7. a: M.action
8. s0: M.state
9. M.init(s0)
10. trace_reachable(M;s0;t;s)
11. M.trans(s,a,x')
12. P(s,t)
13. True
14. True
trace_reachable(M;s;[a];x')
By: BackThru
Thm* M:sm{i:l}(), a:M.action, s,s':M.state.
trace_reachable(M;s;[a];s') 
M.trans(s,a,s')
Generated subgoals:None
About:
