At: trace inv as while 2 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. M.init(s)
trace_reachable(M;s;nil;s)
By:
RecUnfold `trace_reachable` 0
THEN
Reduce 0
Generated subgoals:None
About:
