Nuprl - Pf trace_inv_induction 1 2

(6steps) PrintForm Definitions Lemmas mb state machine Sections GenAutomata Doc

1. M: sm{i:l}()
2. I: M.state(M.action List)Prop
3. x:M.state. M.init(x) I(x,nil)
4. s0,x:M.state, act:M.action, x':M.state, l:M.action List. M.init(s0) trace_reachable(M;s0;l;x) I(x,l) M.trans(x,act,x') I(x',l @ [act])

ys:M.action List, x:M.action. (s0,s:M.state. M.init(s0) trace_reachable(M;s0;ys;s) I(s,ys)) (s0,s:M.state. M.init(s0) trace_reachable(M;s0;ys @ [x];s) I(s,ys @ [x]))

By: Auto

Generated subgoal:

1 5. ys: M.action List
6. x: M.action
7. s0,s:M.state. M.init(s0) trace_reachable(M;s0;ys;s) I(s,ys)
8. s0: M.state
9. s: M.state
10. M.init(s0)
11. trace_reachable(M;s0;ys @ [x];s)
I(s,ys @ [x])

About:

(6steps) PrintForm Definitions Lemmas mb state machine Sections GenAutomata Doc