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