Nuprl - Pf trace_inv_induction 1 1

(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])

s0,s:M.state. M.init(s0) trace_reachable(M;s0;nil;s) I(s,nil)

By: RecUnfold `trace_reachable` 0 THEN Reduce 0 THEN RevHypSubst -1 0 THEN Easy

Generated subgoals:

None

About:

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