mb
structures
Sections
GenAutomata
Doc
Def
l[i] == hd(nth_tl(i;l))
is mentioned by
Thm*
E:TaggedEventStruct, tr:|E| List, i:
||tr||. (tr[i]
< tr > _tag(E)(tr[i]))
[tag_sublist_member_trivial]
Def
No-dup-send(E)(tr) ==
i,j:
||tr||.
(is-send(E)(tr[i]))
(is-send(E)(tr[j]))
(tr[i] =msg=(E) tr[j])
i = j
[no_duplicate_send]
In prior sections:
list
1
mb
list
1
mb
list
2
Try larger context:
GenAutomata
mb
structures
Sections
GenAutomata
Doc