WhoCites
Definitions
mb
hybrid
Sections
GenAutomata
Doc
Who Cites event
is
snd?
event_is_snd
Def is-send(E) == 1of(2of(2of(2of(2of(E)))))
Thm*
E:EventStruct. is-send(E)
|E|
pi2
Def
2of(t) == t.2
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 2of(p)
B(1of(p))
pi1
Def
1of(t) == t.1
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 1of(p)
A
Syntax:
is-send(E)
has structure:
event_is_snd(E)
About:
WhoCites
Definitions
mb
hybrid
Sections
GenAutomata
Doc