(5steps) PrintForm Definitions mb state machine Sections GenAutomata Doc

At: trace reachable append 4
1. M: sm{i:l}()
2. l1: M.action List
3. u: M.action
4. v: M.action List
5. l2:M.action List, s,s':M.state. trace_reachable(M;s;v @ l2;s') (x:M.state. trace_reachable(M;s;v;x) & trace_reachable(M;x;l2;s'))
6. l2: M.action List
7. s: M.state
8. s': M.state
9. x: M.state
10. trace_reachable(M;s;[u / v];x)
11. trace_reachable(M;x;l2;s')

trace_reachable(M;s;[u / v] @ l2;s')
By:
Reduce 0
THEN
RecUnfold `trace_reachable` 0
THEN
Reduce 0
THEN
RecUnfold `trace_reachable` -2
THEN
Reduce -2
THEN
ExRepD
THEN
AutoInstConcl []
THEN
AllHyps (InstHyp [l2;x1;s'])
THEN
Easy
Generated subgoals:

None

About:
listconsandallexists

(5steps) PrintForm Definitions mb state machine Sections GenAutomata Doc