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

At: trace inv as while 1 1 1 1
1. M: sm{i:l}()
2. P: M.state(M.action List)Prop
3. t:M.action List, s0,s:M.state. M.init(s0) trace_reachable(M;s0;t;s) P(s,t)
4. s: M.state
5. x': M.state
6. t: M.action List
7. a: M.action
8. s0: M.state
9. M.init(s0)
10. trace_reachable(M;s0;t;s)
11. M.trans(s,a,x')
12. P(s,t)
13. True
14. True

trace_reachable(M;s0;t @ [a];x')
By:
RWO "trace_reachable_append" 0
THEN
InstConcl [s]
Generated subgoal:

1 trace_reachable(M;s;[a];x')

About:
listconsnilapplyfunctionpropimpliestrueall

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