At: trace reachable append 2
1. M: sm{i:l}()
2. l1: M.action List
3. l2: M.action List
4. s: M.state
5. s': M.state
6. x: M.state
7. trace_reachable(M;s;nil;x)
8. trace_reachable(M;x;l2;s')
trace_reachable(M;s;nil @ l2;s')
By:
Reduce 0
THEN
RecUnfold `trace_reachable` -2
THEN
Reduce -2
THEN
HypSubst -2 0
Generated subgoals:None
About:
