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

t:M.action List, s0,s:M.state. M.init(s0) trace_reachable(M;s0;t;s) I(s,t)

BackThru Thm* Q:((T List)Prop). Q(nil) (ys:T List, x:T. Q(ys) Q(ys @ [x])) (zs:T List. Q(zs))

1	s0,s:M.state. M.init(s0) trace_reachable(M;s0;nil;s) I(s,nil)
2	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]))

About: