At: trace inv induction 1 2 1 1
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])
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. x1: M.state
12. trace_reachable(M;s0;ys;x1)
13. x@0: M.state
14. M.trans(x1,x,x@0)
15. x@0 = s
I(x@0,ys @ [x])
By:
AllHyps (InstHyp [s0;x1;x;x@0;ys])
THEN
Easy
Generated subgoals:None
About:
