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

At: trace reachable one

M:sm{i:l}(), a:M.action, s,s':M.state. trace_reachable(M;s;[a];s') M.trans(s,a,s')
By:
RepeatFor 2 ((RecUnfold `trace_reachable` 0) THEN (Reduce 0))
THEN
ExRepD
Generated subgoals:

11. 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')
21. 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'

About:
consnilapplyequalandallexists

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