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

At: trace inv as while 1
1. M: sm{i:l}()
2. P: M.state(M.action List)Prop
3. (M |= always s,t.P(s,t))

(M |= s,t.P(s,t) while True)
By:
All (Unfolds [`trace_inv`;`while`])
THEN
Unfold `tla` 0
Generated subgoal:

13. 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. (M -t- > s)
9. M.trans(s,a,x')
10. P(s,t)
11. True
12. True
P(x',t @ [a])

About:
listconsnilfunctionproptrue

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