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

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

M.trans(s,a,s')
By: RevHypSubst -1 0
Generated subgoals:

None

About:
applyequal

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