(3steps) PrintForm Definitions mb state machine Sections GenAutomata Doc

At: trace reachable one 2
1. M: sm{i:l}()
2. a: M.action
3. s: M.state
4. s': M.state
5. M.trans(s,a,s')

x:M.state. M.trans(s,a,x) & x = s'
By: InstConcl [s']
Generated subgoals:

None

About:
applyequalandexists

(3steps) PrintForm Definitions mb state machine Sections GenAutomata Doc