Nuprl - Pf trace_reachable

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

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')

By: Reduce -1 THEN RecUnfold `trace_reachable` -1 THEN Reduce -1 THEN ExRepD THEN AllHyps (InstHyp [l2;x;s']) THEN SimpHyp -1 THEN ExRepD THEN InstConcl [x@0] THEN RecUnfold `trace_reachable` 0 THEN Reduce 0 THEN AutoInstConcl []

Generated subgoals:

None

About:

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