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

At: trace inv induction

M:sm{i:l}(), I:(M.state(M.action List)Prop). (x:M.state. M.init(x) I(x,nil)) (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])) (M |= always s,t.I(s,t))
By:
Auto
THEN
Unfold `trace_inv` 0
Generated subgoal:

11. 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])
t:M.action List, s0,s:M.state. M.init(s0) trace_reachable(M;s0;t;s) I(s,t)

About:
listconsnilapplyfunctionpropimpliesall

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