Compact event notation

When following Toaq's semantics algorithm, a certain pattern shows up often: an existential quantification of an event, combined with its aspect and verb participant information. For example, Luı heaqdo jí súq máq … becomes

$\exists e.\tau (e)<\mathrm {t} \wedge {\text{heaqdo}}_{w}({\text{suq}},{\text{maq}})(e)\wedge {\text{AGENT}}(e)(w)={\text{jı}}\color {teal}\wedge P(e)$

There is an event e, whose runtime precedes the implicit tense t, and which is an event of heaqdo-ing súq máq in world w, and whose agent is jí, (and which satisfies P(e).)

Kuna supports generating a compact notation for this:

$\exists \mathop {\text{heaqdo}} \limits _{<\mathrm {t} }{}_{w}^{e}\left({\text{jı}};{\text{suq}},{\text{maq}}\right)\color {teal}.P(e)$

It works as follows:

1. When an existential quantifier $\exists$ is followed by a Toaq verb, it asserts the existence of an event of that verb.
2. The event variable $e$ being bound is given by the following superscript.
3. The world variable $w$ the event is in is given by the following subscript.
4. The aspect information is given underneath the verb. If it starts with a relational operator $<t$ it abbreviates $\tau (e)<t$.
5. The participants are listed in parentheses. If there is an agent, it's separated from the non-agent participants by a semicolon.
6. Optionally, a final dot announces the rest of the formula $P(e)$ in which $e$ is bound.

Example

The full denotation of Pu tao jí hóq da (i.e. Ruaq jí ꝡä pu tao jí hóq ka) is:

$\exists e.\ \tau (e)\subseteq {}{\text{t}}_{0}\land {}{\text{AGENT}}(e)({\text{w}})={\text{jı}}\land {}{\text{ruaq}}_{\text{w}}(\lambda w.\ \exists e'.\ \tau (e')\subseteq {}{\text{t}}\land {}{\text{AGENT}}(e')(w)={\text{jı}}\land {}{\text{tao}}_{w}({\text{a}})(e'))(e)\ |\ {\text{t}}<{\text{t}}_{0}\ |\ {\text{abstract}}({\text{a}})$

Using compact notation, it becomes a bit less daunting:

$\exists \mathop {\text{ruaq}} \limits _{\subseteq {}{\text{t}}_{0}}{}_{\text{w}}^{e}\left({\text{jı}};\lambda w.\ \exists \mathop {\text{tao}} \limits _{\subseteq {}{\text{t}}}{}_{w}^{e'}\left({\text{jı}};{\text{a}}\right)\right)\ |\ {\text{t}}<{\text{t}}_{0}\ |\ {\text{abstract}}({\text{a}})$