(9steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
switchable
induced
tagged
1
1
2
1.
E:
EventStruct
2.
P:
(|E| List)
Prop
3.
A:
Type
4.
f:
A
|E|
5.
t:
A
Label
6.
switchable(E)(P)
| < A,f,t > (E)| = A
By:
Reduce 0
Generated subgoals:
None
About:
(9steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc