(9steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: switchable induced tagged 1 1 1 1
1. E: EventStruct
2. P: (|E| List)Prop
3. A: Type
4. f: A|E|
5. t: ALabel
6. switchable(E)(P)

< A,MS(E),msg(E) o f,loc(E) o f,is-send(E) o f,t, > = < A,MS(E),msg(E) o f,loc(E) o f,is-send(E) o f, > E:TypeM:MessageStruct(E|M|)(ELabel)(E)Top
By: Repeat Analyze
Generated subgoal:

1 < t, > = Top

About:
pairproductproductlistboolitapplyfunctionuniverseequaltopprop

(9steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc