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

At: trace inv as while 3 1
1. M: sm{i:l}()
2. P: M.state(M.action List)Prop
3. s,x':M.state, t:M.action List, a:M.action. (M -t- > s) M.trans(s,a,x') P(s,t) True True P(x',t @ [a])
4. (M |= initially s,t.P(s,t))
5. x: M.state
6. M.init(x)

P(x,nil)
By: EasyHypThen Auto
Generated subgoals:

None

About:
listconsnilapplyfunctionpropimpliestrueall

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