M:sm{i:l}(), l1,l2:M.action List, s,s':M.state. trace_reachable(M;s;l1 @ l2;s') (x:M.state. trace_reachable(M;s;l1;x) & trace_reachable(M;x;l2;s'))

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')
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')
3	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. trace_reachable(M;s;[u / v] @ l2;s') x:M.state. trace_reachable(M;s;[u / v];x) & trace_reachable(M;x;l2;s')
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')

About: